Abstract
The Curry-Howard correspondence establishes a fundamental connection between the semantics of logic and the semantics of intuitionistic type theory.
Historical Context
Foundational Crisis
Russell’s Paradox demonstrated inconsistency in Frege’s set theory.
Intuitionism
The BHK Interpretation, initiated by Brouwer and Heyting.
- Semantics-based: mathematics consists of mental constructions.
- Rejection of the Law of the Excluded Middle ().
Formalism
Initiated by Hilbert.
- Syntax-based: mathematics is a manipulation of symbols according to formal rules.
- Desired properties for a formal system:
- Completeness
- Consistency
- Finitary consistent: Consistency demonstrable using only Finitary methods.
Computational Interpretations
Unifies intuitionism and formalism.
- Logical proofs correspond to programs.
- Kreisel’s Unwinding Program: extracting computational content from non-constructive proofs.
- Recursion up to explicit ordinals; recursion at higher types.
Constructive vs Non-Constructive Mathematics
Constructive Mathematics
Requires a witness for existence.
Classical Logic
Asserts existence without necessarily providing a witness.
Example: Irrational such that is rational
Classic non-constructive proof using excluded middle: Let . If , we are done. If , let and . Then:
a^b &= (\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} \\ &= \sqrt{2}^2 \\ &= 2 \in \mathbb{Q} \end{aligned}$$ ## Definition The *BHK Interpretation* (Brouwer-Heyting-Kolmogorov) provides a logic of constructions forming the foundation for [[Type Theory]]. * $\bot$ has no proof. * A proof of $X \wedge Y$ is a pair $(p_X, p_Y)$. * A proof of $X \vee Y$ is a tagged value (e.g., pair $\langle 0, p_X \rangle$ or $\langle 1, p_Y \rangle$). * $\forall$ and $\to$ are functions/constructions transforming proofs. ## Combinatory Logic Developed via [[Shonfinkel's combinatory logic]] (1924) and [[Curry]] (1934). A system based on application and two combinators $S$ and $K$. $$\begin{aligned} K x y &= x \\ S x y z &= x z (y z) \end{aligned}$$ Typed as Hilbert-style axioms: $$\begin{aligned} K &: A \to B \to A \\ S &: (A \to B \to C) \to (A \to B) \to A \to C \end{aligned}$$ ## The Correspondence Correspondence between systems of formal logic and computational calculi. | Logic | Computation | | :--- | :--- | | Formula | Type | | Proof System | Programming Language | | Proof | Program / Term | | Normalisation | Execution | | Normal form | Value | | Provability | Inhabitation | ### Curry-Howard-Lambek Extends the correspondence to category theory. * Logic: [[Intuitionistic Propositional Logic]]. * Computation: Simply Typed [[Lambda Calculus]]. * [[Category Theory]]: [[Cartesian Closed Categories]] (CCC). ## Formalization ### Martin-Löf Type Theory Per Martin-Löf formalized the BHK interpretation via the propositions-as-types correspondence. #### Judgements vs Propositions We distinguish between the judgement (meta-level) and the proposition (object level). 1. $A \text{ type}$ 2. $A = B$ 3. $a : A$ 4. $a = b : A$ #### Canonical Forms | Logic | Type Theory | Construction | | --- | --- | --- | | $\forall x \in A, P(x)$ | $\Pi_{(x:A)} P(x)$ | Dependent Function | | $\exists x \in A, P(x)$ | $\Sigma_{(x:A)} P(x)$ | Dependent Pair | | $A \land B$ | $A \times B$ | Product | | $A \lor B$ | $A \uplus B$ | Coproduct | | $a =_A b$ | $\text{Id}_A(a, b)$ | Identity Type | ### Homotopy Type Theory Extends [[Martin-Löf Type Theory]] with the univalence axiom, treating isomorphic structures as equal. * Constructive View: [[Cubical Type Theory]] provides computational content for univalence via dimension variables and glue types, restoring canonicity. ## References * [[Proof Theory]] * [[Model Theory]] * [[Second-Order Logic]]