Realizability

Origin. Kleene introduced realizability (1945) to interpret intuitionistic logic via computable functions. A formula is true if "realized" by a computation. Connects constructive logic to computability theory. Extended by Kreisel, Troelstra, and others. Foundation for program extraction from proofs.

Models. Truth as computability. Classical: φ is true if satisfied in models. Realizability: φ is true if a computable function "realizes" it. Realizers are evidence — computation that witnesses truth. Existential: realizer provides the witness. Implication: realizer transforms realizers.

Formalism.

Kleene realizability (number realizability): n ⊩ φ — "n realizes φ"

• n ⊩ ⊥ — never
• n ⊩ (φ ∧ ψ) iff (n)₀ ⊩ φ and (n)₁ ⊩ ψ
• n ⊩ (φ ∨ ψ) iff ((n)₀ = 0 and (n)₁ ⊩ φ) or ((n)₀ ≠ 0 and (n)₁ ⊩ ψ)
• n ⊩ (φ → ψ) iff for all m: m ⊩ φ implies {n}(m)↓ and {n}(m) ⊩ ψ
• n ⊩ ∀x.φ(x) iff for all m: {n}(m)↓ and {n}(m) ⊩ φ(m)
• n ⊩ ∃x.φ(x) iff (n)₁ ⊩ φ((n)₀)

where {n}(m) is Turing machine n on input m.

q-realizability (realizability with truth): Kleene's variant, and the one that "adds truth". The clauses are those above with a copy of the formula conjoined at implication and universal quantification: n q (φ → ψ) iff ∀m (m q φ → {n}(m)↓ ∧ {n}(m) q ψ) and (φ → ψ). The trailing conjunct yields n q φ ⟹ φ, which is exactly what number realizability lacks. That property makes q-realizability the tool for deriving rules — Church's rule, Markov's rule — rather than for validating axioms, since a closure result needs the realizer to certify the formula itself.

Modified realizability (Kreisel 1959): A different interpretation, not a truth-augmented one, and the two must not be conflated. Realizers are typed functionals of HAω, not numbers, and the interpretation is over finite types rather than Kleene's indices. Kreisel introduced it for a specific purpose: to show Markov's principle is not derivable in HAω. Characterized by HAω + AC (choice in all finite types) + IP (independence of premise): those are precisely the sentences modified-realized. It refutes rather than validates MP — mr gives a model of ¬MP, so HAω + AC + IP + ¬MP is consistent.

The two interpretations sit on opposite sides of both principles. Kleene number realizability is characterized by ECT₀ (extended Church's thesis) and validates MP; ECT₀ is incompatible with IP. Modified realizability validates IP and refutes MP. So "realizability" without qualification settles neither principle.

Function realizability: Uses partial recursive functions instead of numbers. n ⊩ (φ → ψ) requires uniform transformation.

Dialectica interpretation: Gödel's variant: extracts bounds and witnesses. Used in proof mining.

Symbols.

Metatheory. Realizability validates intuitionistic logic. Does not validate excluded middle (no uniform realizer). Church's thesis is realizable: all functions are computable — indeed Kleene number realizability is exactly characterized by ECT₀, in the sense that HA ⊢ (φ ↔ ∃n. n ⊩ φ) holds for every φ precisely under HA + ECT₀. Markov's principle is realizable on that interpretation; the qualification is essential, since modified realizability refutes it. Independence results: shows certain principles independent — this is the main use, and it works in both directions, ECT₀ and MP from number realizability, AC and IP from modified. Soundness: if ⊢ φ in HA, then some n ⊩ φ.

Applies to. Program extraction from proofs. Constructive mathematics foundations. Type theory semantics (realizability toposes). Independence proofs in arithmetic. Proof mining (extracting computational content). Verified software (Coq, Agda extraction).

Limitations. Only validates constructive logic. Realizers can be complex — not always efficient programs. Classical logic not realizable in standard sense. Extensionality requires care (intensional). Higher-order realizability is more complex. Not all intuitionistic principles are realized uniformly.

© 2026 Lingenic LLC