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.
Modified realizability is one way to show that Markov's principle is not derivable in intuitionistic logic.
Understood as a generalization of Cohen’s forcing, it was used to provide new models of set theory.