Asserts existence without necessarily providing a witness.
Example: Irrational a,b such that ab is rational
Classic non-constructive proof using excluded middle:
Let x=22.
If x∈Q, we are done.
If x∈/Q, let a=x and b=2. 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: [[Propositional Logic#intuitionistic-fragment|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)$ | $(x:A) \to P(x)$ | Dependent Function |
| $\exists x \in A, P(x)$ | $(x:A) \times 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]]