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

How to Cite This Entry:
Recursive realizability. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Recursive_realizability&oldid=48460
This article was adapted from an original article by V.E. Plisko (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article