A Predicate Logic Based on the Gödel Interpretation and the System of Hereditary Effective Operations

Valeri Plisko

Let T be an intuitionistic arithmetic theory, i. e. an arbitrary set of arithmetic sentences closed under derivability in the intuitionistic arithmetic HA. A closed predicate formula will be called T -valid if each its closed arithmetic instance is in T. The set of all T -valid predicate formulas will be denoted by L(T). An arithmetic theory T is called an IS-theory if there are arithmetic Σ_{1}-formulas A(x) and B(x) such that the formula

∀x¬(A(x) & B(x)) & ¬∀x∃y((A(x) ⊃ y = 0) & (B(x) ⊃ y ≠ 0))

is in T. An arithmetic formula is said to be negative if it does not contain ∨ and ∃. The negative fragment of a theory T is denoted by T^{−}.

Theorem 1 If T is an intuitionistic IS-theory, then T^{−} ≤_{1} L(T) .

The theory T consists of arithmetic sentences A such that its Dialectica interpretation A^{D} in the language of arithmetic in all finite types is true if variables in A^{D} are interpreted as hereditary effective operations. One can to prove that T is an intuitionistic IS-theory and T^{−} is not recursively enumerable. The following theorem is a consequence of this fact and Theorem 1:

Theorem 2 The logic L(T) is not recursively enumerable.

An analogous result for the predicate logic based on the Gödel interpretation and the system of hereditary recursive operations was proved in [1].

The author is partially supported by RFBR grant 98-01-00249.

[1] V. Plisko. Two semantics and logics based on the Gödel interpretation. In: Computational Logic and Proof Theory. Proc. 5th Kurt Gödel Colloquium, KGC’97, Vienna, Austria, August 1997 (Lecture Notes in Computer Science 1289), pp. 233-240

Address: Department of Mathematical Logic and Theory of Algorithms, Faculty of Mechanics and Mathematics, Moscow State University, Moscow, 119899, Russia

E-mail: plisko@ttk.ru, plisko@lpcs.math.msu.ru