\Sigma_n-realizability and its predicate logic
by
Valery Plisko
Faculty of Mechanics and Mathematics, Moscow State University, Moscow, 119899, Russia

A function f:N --> N is \Sigma_n-computable (n>0) if its graph is a \Sigma_n-set in the Kleene - Mostowski arithmetic hierarchy. \Sigma_n-computable functions are exactly the functions computable in \emptyset^(n-1). An enumeration of the \Sigma_n-computable functions is induced by the enumeration of the Turing mashines with an oracle or by the enumeration of \Sigma_n-formulas. \Sigma_n-realizability for arithmetic sentences is defined by analogy with Kleene's recursive realizability, \Sigma_n-computable functions and their numbers being used instead of the partial recursive functions. The notion of \Sigma_n-realizability admits a formalization in the intuitionistic arithmetic HA. Some results on recursive realizability can be extended to \Sigma_n-realizability.

Theorem 1. For any n, every arithmetic sentence deducible in HA is \Sigma_n-realizable.

Thus the set of \Sigma_n-realizable arithmetic sentences is an intuitionistic theory. It is easy to prove that this theory is complete and has the existential property. The set of \Sigma_n-realizable arithmetic sentences is recursively isomorphic to the set \emptyset^(\omega).

A closed predicate formula is called \Sigma_n-realizable if the universal closure of every its arithmetic instance is \Sigma_n-realizable. A schema is a first-order formula in the language obtained by adding predicate variables to the language of formal arithmetic. The notion of \Sigma_n-realizable schema is defined in a natural way.

Theorem 2 (the theorem on schemas). For any closed schema A, one can effectively construct a closed predicate formula A' such that A' is \Sigma_n-realizable if and only if A is \Sigma_n-realizable.

The following rather general metamathematical result was recently proved by the author.

Theorem 3. If T is a complete intuitionistic arithmetic theory having the existential property and the theorem on schemas holds for the notion of T-valid predicate formula, then the corresponding predicate logic is \Pi₁^T-complete.

The results stated above imply the following theorem:

Theorem 4. For any n, the set of \Sigma_n-realizable predicate formulas is recursively isomorphic to the complement of the set \emptyset^\omega+1.

Therefore the predicate logics based on the notion of \Sigma_n-realizability for different n are mutually recursively isomorphic and are recursively isomorphic to the logic of recursive realizability (n=1). Note that in the "limit" case of realizability using \Sigma_n-computable functions for any n (i.e. all arithmetic functions) we obtain exactly the classical predicate logic.

Date received: February 26, 1999