Curry-Howard Correspondence

Constructive vs Non-Constructive Mathematics

Constructive Mathematics

Requires witness for existence.

Classical Logic

Asserts existence without necessarily providing a witness. Example: Every ring has a maximal ideal.

Example: Irrational $a,b$ such that $a^b$ is rational

Classic non-constructive proof using excluded middle: Let $x={\sqrt{2}}^{\sqrt{2}}$. If $x\in \mathbb{Q}$, we are done. If $x\notin \mathbb{Q}$, let $a=x$ and $b=\sqrt{2}$. Then:

$$a^b=({\sqrt{2}}^{\sqrt{2}}{)}^{\sqrt{2}}={\sqrt{2}}^2=2\in \mathbb{Q}$$

Historical Context

Foundational Crisis

• Russell’s Paradox demonstrated inconsistency in Frege’s set theory.

Intuitionism

Brouwer, Heyting.

• Semantics-based: mathematics consists of mental constructions.
• Rejection of Law of the Excluded Middle ($P\vee \neg P$).

BHK Interpretation

Logic of constructions.

• $\perp$ has no proof.
• Proof of $X\wedge Y$ is a pair $(p_X,p_Y)$.
• Proof of $X\vee Y$ is a tagged value (e.g., pair $⟨0,p_X⟩$ or $⟨1,p_Y⟩$).
• $\forall$ and $\to$ are functions/constructions transforming proofs.
• Foundation for Type Theory.

Formalism

Hilbert.

• Syntax-based: mathematics is a manipulation of symbols according to formal rules.
• Desired properties for a formal system:
  1. Completeness
  2. Consistency
  3. 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.

Combinatory Logic

Shonfinkel’s combinatory logic (1924), Curry (1934). System based on application and two combinators $S$ and $K$.

$$\begin{array}{rl}\mathbf{K}xy& =x\\ \mathbf{S}xyz& =xz(yz)\end{array}$$

Typed as Hilbert-style axioms:

$$\begin{array}{rl}K& :A\to B\to A\\ S& :(A\to B\to C)\to (A\to B)\to A\to C\end{array}$$

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).

See also

• Proof Theory
• Model Theory
• Second-Order Logic