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.

Modified realizability: Adds truth: n ⊩ᵐ φ means n realizes φ and φ is true. Avoids some counterexamples of pure realizability.

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.

Symbol	Unicode	Name	Meaning
⊩	U+22A9	Realizes	Computational witness
{n}(m)	—	Application	TM n on m
(n)ᵢ	—	Projection	i-th component
↓	U+2193	Defined	Computation terminates
∀	U+2200	Universal	For all
∃	U+2203	Existential	Exists (witnessed)

Metatheory. Realizability validates intuitionistic logic. Does not validate excluded middle (no uniform realizer). Church's thesis is realizable: all functions are computable. Markov's principle is realizable. Independence results: shows certain principles independent. 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.