Realizability

In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them.[1] Formulas from a formal theory are "realized" by objects, known as "realizers", in a way that knowledge of the realizer gives knowledge about the truth of the formula. There are many variations of realizability; exactly which class of formulas is studied and which objects are realizers differ from one variation to another.

Realizability can be seen as a formalization of the BHK interpretation of intuitionistic logic; in realizability the notion of "proof" (which is left undefined in the BHK interpretation) is replaced with a formal notion of "realizer". Most variants of realizability begin with a theorem that any statement that is provable in the formal system being studied is realizable. The realizer, however, usually gives more information about the formula than a formal proof would directly provide.

Beyond giving insight into intuitionistic provability, realizability can be applied to prove the disjunction and existence properties for intuitionistic theories and to extract programs from proofs, as in proof mining. It is also related to topos theory via the realizability topos.

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.

With this definition, the following theorem is obtained:[2]

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.[3]

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

Later developments

Kreisel introduced modified realizability, which uses typed lambda calculus as the language of realizers. Modified realizability is one way to show that Markov's principle is not derivable in intuitionistic logic. On the contrary, it allows to constructively justify the principle of independence of premiss:

(A \rightarrow \exists x\;P(x)) \rightarrow \exists x\;(A \rightarrow P(x)).

Relative realizability[5] is an intuitionist analysis of recursive or recursively enumerable elements of data structures that are not necessarily computable, such as computable operations on all real numbers when reals can be only approximated on digital computer systems.

Applications

Realizability is one of the methods used in proof mining to extract concrete "programs" from seemingly nonconstructive mathematical proof. Program extraction using realizability is implemented in some proof assistants such as Coq.

See also

Notes

  1. van Oosten 2000
  2. van Oosten 2000, p. 7
  3. Rose 1953
  4. van Oosten 2000, p. 6
  5. Birkedal 2000

References

External links