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₀ and MP together are inconsistent with IP. Modified realizability validates IP and refutes MP. So "realizability" without qualification settles neither principle.

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

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

Symbols.

Metatheory. Soundness holds and is itself formalizable: if HA ⊢ φ then some numeral realizes φ, and the realizer is extracted primitive-recursively from the derivation; Nelson (1947) verified the soundness argument inside HA. Troelstra's characterization theorem fixes what number realizability is: HA + ECT₀ ⊢ φ ↔ ∃n (n ⊩ φ), and HA + ECT₀ ⊢ φ iff HA ⊢ ∃n (n ⊩ φ), so the realizable sentences are exactly the theorems of HA + ECT₀. Realizability is therefore not complete for HA — ECT₀ is realizable and unprovable in HA. Excluded middle has no realizer, since a uniform realizer of ∀x(A(x) ∨ ¬A(x)) for Σ⁰₁ A would decide the halting problem, and ECT₀ is outright inconsistent with classical logic. q-realizability yields closure rules rather than axioms: Church's rule, and with Friedman's A-translation (1978) Markov's rule. The neighbouring interpretations certify different principles — modified realizability by AC + IP over HAω, Gödel's Dialectica by AC + IP + Markov's principle. Hyland's effective topos (1982) is the categorical form of the same interpretation.

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. Realizability interprets intuitionistic arithmetic and nothing classical: excluded middle is unrealizable, and ECT₀, which realizability validates, is inconsistent with classical logic, so there is no extension of the interpretation to PA that preserves its content. It also refutes principles the Brouwerian constructivist wants — Kleene's singular tree is an infinite decidable binary tree with no computable path, so number realizability falsifies the fan theorem and the uniform continuity principle that follows from it; realizability constructivism and intuitionism are incompatible extensions of HA, not variants. Realizers are machine indices, not efficient programs: extraction carries no complexity bound. The interpretation is intensional — realizers are Gödel numbers, so extensionally equal functions carry different realizers and extensional principles must be imposed separately. And "realizability" names a family whose members disagree, number realizability validating Markov's principle and modified realizability refuting it, so unqualified claims about what is realizable are ill-formed.

© 2026 Lingenic LLC