Recursive realizability

A more precise definition of the intuitionistic semantics of arithmetical formulas, based on the concept of a partial recursive function as proposed by S.C. Kleene (see [1], [2]). For every closed arithmetical formula $ F $, a relation "the natural number e realizes the formula F" is defined; it is denoted by $ erF $. The relation $ erF $ is defined inductively according to the structure of the formula $ F $.

1) If $ F $ is an atomic formula without free variables, i.e. $ F $ is of the form $ s= t $ where $ s $ and $ t $ are constant terms, then $ erF $ if and only if $ e= 0 $ and the values of the terms $ s $ and $ t $ coincide.

Let $ A $ and $ B $ be formulas without free variables.

2) $ er( A \& B) $ if and only if $ e = 2 ^ {a} \cdot 3 ^ {b} $, where $ arA $, $ brB $.

3) $ er( A \lor B) $ if and only if $ e = 2 ^ {0} \cdot 3 ^ {a} $ and $ arA $, or $ e = 2 ^ {1} \cdot 3 ^ {b} $ and $ brB $.

4) $ er( A \supset B) $ if and only if $ e $ is the Gödel number of a unary partial recursive function $ \phi $ such that for any natural number $ a $, $ arA $ implies that $ \phi $ is defined at $ a $ and $ \phi ( a) rB $.

5) $ er( \neg A) $ if and only if $ er( A \supset 1= 0) $.

Let $ A( x) $ be a formula without free variables other than $ x $; if $ n $ is a natural number, then $ \overline{n}\; $ is a term which denotes the number $ n $ in formal arithmetic.

6) $ er( \exists xA( x)) $ if and only if $ e = 2 ^ {n} \cdot 3 ^ {a} $ and $ arA( \overline{n}\; ) $.

7) $ er( \forall xA( x)) $ if and only if $ e $ is the Gödel number of a recursive function $ f $ such that for any natural number $ n $ the number $ f( n) $ realizes $ A( \overline{n}\; ) $.

A closed formula $ F $ is called realizable if there is a number $ e $ which realizes $ F $. A formula $ A( y _ {1} \dots y _ {m} ) $ containing the free variables $ y _ {1} \dots y _ {m} $ can be regarded as a predicate in $ y _ {1} \dots y _ {m} $( "the formula Ay1…ym is realizable" ). If a formula $ F $ is derivable from realizable formulas in intuitionistic arithmetic, then $ F $ is realizable (see [3]). In particular, every formula which can be proved in intuitionistic arithmetic is realizable. A formula $ A( x) $ can be given for which the formula $ \forall x ( A( x) \lor \neg A( x)) $ is not realizable. Accordingly, in this case the formula $ \neg \forall x( A( x) \lor \neg A( x)) $ is realizable although it is classically false.

Every predicate formula $ \mathfrak U $ which is provable in intuitionistic predicate calculus has the property that each arithmetical formula obtained from $ \mathfrak U $ by substitution is realizable. Predicate formulas possessing this property are called realizable. It has been shown [4] that the propositional formula:

$$ (( \neg \neg D \supset D) \supset ( \neg \neg D \lor \neg D)) \supset ( \neg \neg D \lor \neg D), $$

where $ D $ denotes the formula $ \neg p \lor \neg q $, is realizable but cannot be derived in intuitionistic propositional calculus.

References

[1]	S.C. Kleene, "On the interpretation of intuitionistic number theory" J. Symbolic Logic , 10 (1945) pp. 109–124
[2]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[3]	D. Nelson, "Recursive functions and intuitionistic number theory" Trans. Amer. Math. Soc. , 61 (1947) pp. 307–368
[4]	G.F. Rose, "Propositional calculus and realizability" Trans. Amer. Math. Soc. , 75 (1953) pp. 1–19
[5]	P.S. Novikov, "Constructive mathematical logic from a classical point of view" , Moscow (1977) (In Russian)

References

[a1]	M.J. Beeson, "Foundations of constructive mathematics" , Springer (1985)
[a2]	D. Mumford, "Abelian varieties" , Oxford Univ. Press (1974)