The realizer, however, usually gives more information about the formula than a formal proof would directly provide.
Kleene's original version of realizability uses natural numbers as realizers for formulas in Heyting arithmetic.
A few pieces of notation are required: first, an ordered pair (n,m) is treated as a single number using a fixed primitive recursive pairing function; second, for each natural number n, φn is the computable function with index n. 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, known as Kleene's 1945-realizability relation:[2] With this definition, the following theorem is obtained:[3] On the other hand, there are classical theorems (even propositional formula schemas) that are realized but which are not provable in HA, a fact first established by Rose.
Kreisel introduced modified realizability, which uses typed lambda calculus as the language of realizers.
Understood as a generalization of Cohen’s forcing, it was used to provide new models of set theory.