Realizability - Example: Realizability By Numbers

Example: Realizability By Numbers

Kleene's original version of realizability uses natural numbers as realizers for formulas in Heyting arithmetic. The following clauses are used to define a relation "n realizes A" between natural numbers n and formulas A in the language of Heyting arithmetic. A few pieces of notation are required: first, an ordered pair (n,m) is treated as a single number using a fixed effective pairing function; second, for each natural number n, φ_n is the computable function with index n.

• A number n realizes an atomic formula s=t if and only if s=t is true. Thus every number realizes a true equation, and no number realizes a false equation.
• A pair (n,m) realizes a formula A∧B if and only if n realizes A and m realizes B. Thus a realizer for a conjunction is a pair of realizers for the conjuncts.
• A pair (n,m) realizes a formula A∨B if and only if the following hold: n is 0 or 1; and if n is 0 then m realizes A; and if n is 1 then m realizes B. Thus a realizer for a disjunction explicitly picks one of the disjuncts (with n) and provides a realizer for it (with m).
• A number n realizes a formula A→B if and only if, for every m that realizes A, φ_n(m) realizes B. Thus a realizer for an implication is a computable function that takes a realizer for the hypothesis and produces a realizer for the conclusion.
• A pair (n,m) realizes a formula (∃ x)A(x) if and only if m is a realizer for A(n). Thus a realizer for an existential formula produces an explicit witness for the quantifier along with a realizer for the formula instantiated with that witness.
• A number n realizes a formula (∀ x)A(x) if and only if, for all m, φ_n(m) is defined and realizes A(m). Thus a realizer for a universal statement is a computable function that produces, for each m, a witness for the formula instantiated with m.

With this definition, the following theorem is obtained:

Let A be a sentence of Heyting arithmetic (HA). If HA proves A then there is an n such that n realizes A.

On the other hand, there are formulas that are realized but which are not provable in HA, a fact first established by Rose.

Further analysis of the method can be used to prove that HA has the "disjunction and existence properties":

• If HA proves a sentence (∃ x)A(x) then there is an n such that HA proves A(n)
• If HA proves a sentence A∨B then HA proves A or HA proves B.