A Generalized Realizability for Constructive Arithmetics

Saeed Salehi

We introduce a generalized notion of realizability, appropriate for constructive arithmetics, in particular Basic Arithmetic, BA. This arithmetic is equivalent of HA on intuitionistic logic and of PA on classical logic, based on Basic Logic, the propositional counterpart of which, was invented by Visser, and is developed for the quantifier case by Ardeshir and Ruitenburg [1].

The crucial different cases from the Kleene’s one, are → and ∀. We restrict the recursive functions, associated for these cases, to a definable subclass, for example total recursives or primitive recursives. So the primitive recursive (PR-)realizability for A → B is:

n r^{P R}A → B ≡ P R(n) ∧ ∀x(x r^{P R}A ⟶ ∃z{T(n, x, z) ∧ Uz r^{P R}B})

The (primitive recursive) formula P R(x), intuitively says that in the “program” of the recursive function with code x, there is no use of (unbounded) minimalization. So if ℕ ⊧ P R(n) then φ_{n} is primitive recursive (but not necessary vice versa.)

One can prove the soundness of PR-realizability for BA, in the usual way. In the “usual” proof for HA, one can not restrict the partial recursives to a proper subclass, so it seems that Kleene’s definition, for HA, can not be optimized in this way.

A generalized form of Church’s Thesis, GCT^{PR}:

∀x(∃z(z r^{P R}A(x)) → ∃yϕ(x, y)) ⇒ ∃u[P R(u) ∧ ∀x(∃z(z r^{P R}A(x)) → ∃w{T(u, x, w) ∧ ϕ(x, Uw)})]

is realizable in BA, and the completeness theorem of Troelstra [2], holds for BA + GCT^{P R} and r^{P R}:

BA ⊢ ∃x(x r^{P R}ψ) ⟺ BA + GCT^{PR} ⊢ ψ

As applications, we deduce that BA enjoys the traditional constructive properties: Disjunction Property and Explicit Definability by Numbers, also each provably total function of BA is primitive recursive.

Keywords: Realizability, Basic Logic, Basic Arithmetic.

1991 Mathematics Subject Classification: Primary 03F50; Secondary 03F30, 03B20, 03F55, 03D20.

[1] Ruitenburg, Wim; Basic Predicate Calculus, Notre Dame J. of Formal Logic, Vol.39, N.1, (1998) pp. 18-46

[2] Troelstra, A.S.(ed.); Metamathematical Investigations of Intuitionistic Arithmetic and Analysis, Springer-Verlag, Berlin 1974.

Address: Institute of Mathematics, Polish Academy of Sciences, Śniadeckich 8, P.O. BOX 137, 00-950 Warsaw, poland

E-mail: salehi@impan.gov.pl