Interpretations of Kleene's metamathematical predicate Γ ∣ a in intuitionistic arithmetic
T. Thacher Robinson · Journal of Symbolic Logic · 1965
Let Pp, Pd, and N be the intuitionistic systems of prepositional calculus, predicate calculus, and elementary arithmetic, respectively, described in [3]. Kleene [4] introduces a metamathematical predicate Γ ∣ A for each of the systems Pp, Pd, and N, where Γ ranges over finite sequences of wffs, and A ranges over wffs, of that system. In the case of N, if Γ is consistent, then ‘ Γ ∣ A’ is essentially the result of deleting all references to recursive functions from the metamathematical predicate ‘A is realizable-(Γ ⊦)’ described in [3], pp. 502–503. Through use of this predicate, Kleene [4] obtains elegant constructive proofs of the following results for N: Metatheorem 0.1. If B ∨ C is a closed theorem of N, then ⊦ B or ⊦ C. Metatheorem 0.2. If (∃a)D(a) is a closed theorem of N, then there is a numeral n such that ⊦D(n). Metatheorem 0.3. If A is a closed wff of N, then A ∣ A is a necessary and sufficient condition that, for all closed B, C, (∃a)D(a) inN: (0.3.1) ⊦ A ⊃ B ∨ C implies ⊦ A ⊃ B or ⊦A ⊃ C and (0.3.2) ⊦A ⊃ (∃)D(a) implies there is a numeral n such that ⊦ A ⊃ D(n).