# 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)