Realizability connects proofs to programs, showing how logical formulas translate to computational tasks. It's a bridge between abstract math and concrete algorithms, revealing the hidden computational power in logical reasoning.

This idea fits into proof theory by demonstrating how formal proofs aren't just abstract symbols, but contain real-world instructions. It shows that logic and computation are deeply intertwined, not separate realms.

Realizability and Constructive Proofs

Kleene Realizability and Computational Interpretation

• Kleene realizability provides a computational interpretation of intuitionistic arithmetic and logic
• Associates each formula $A$ with a set $|A|$ of "realizers" which can be seen as programs that validate the computational content of $A$
• A realizer $e \in |A|$ can be thought of as a program that computes the evidence or proof of the formula $A$
• Kleene realizability establishes a connection between intuitionistic proofs and computable functions

Constructive Proofs in Intuitionistic Arithmetic

• In intuitionistic arithmetic, proofs are constructive and computationally meaningful
• Constructive proofs provide explicit algorithms or methods for constructing mathematical objects
• Intuitionistic logic rejects the law of excluded middle ($A \vee \neg A$) and double negation elimination ($\neg\neg A \rightarrow A$)
• Constructive proofs avoid non-constructive principles like the axiom of choice and proof by contradiction
• Intuitionistic arithmetic is weaker than classical arithmetic but is well-suited for extracting computational content from proofs

Program and Witness Extraction

Extracting Programs from Proofs

• Program extraction is the process of deriving a program from a constructive proof
• Given a constructive proof of a formula $\exists x. P(x)$, program extraction produces a program that computes a witness $a$ such that $P(a)$ holds
• The extracted program is correct by construction since it is derived directly from the proof
• Program extraction enables the synthesis of certified programs from proofs ($\lambda$-terms)

Witness Extraction and Proof-Carrying Code

• Witness extraction is a technique for extracting computational content from classical proofs
• It extends program extraction to handle classical logic and axioms like the law of excluded middle
• Witness extraction produces a program along with a proof of its correctness (proof-carrying code)
• The extracted program computes a witness that satisfies the specification given by the proof
• Proof-carrying code enables the verification of program properties and ensures trust in the extracted code

Variants of Realizability

Modified Realizability and Other Variants

• Modified realizability is a variant of Kleene realizability that allows for the extraction of programs from classical proofs
• It extends realizability to handle the law of excluded middle and other non-constructive principles
• Modified realizability provides a way to extract computational content from proofs in classical logic
• Other variants of realizability include:
  • Dialectica interpretation: Associates formulas with games and strategies
  • Functional interpretations: Maps formulas to higher-order functionals
  • Friedman's translation: Embeds classical arithmetic into intuitionistic arithmetic
• These variants provide different perspectives on the computational content of proofs and enable program extraction in various settings