Past exam of the mathematics course of the University of Cambridge / 2022 / iii / Paper 120 / 1

Under the Curry-Howard correspondence, Intuitionistic propositional logic propositions are types and proofs are typed terms. Assumptions correspond to typed variables. The logical implication $A\to B$ corresponds to the function type, logical conjunction $A\wedge B$ to the product type, logical disjunction $A\vee B$ to the sum type, logical truth to the unit type, and logical falsity to the empty type.

The rules of natural deduction become term constructors. Implication introduction sends a derivation of $B$ from a variable $x:A$ to the abstraction $\lambda x.M:A\to B$, while implication elimination becomes application $MN$. Pairing and projection implement conjunction, and injections with case analysis implement disjunction. Under this correspondence, normalization of proofs is computation by beta reduction in the simply typed lambda calculus.

A Heyting algebra is a bounded lattice $H$ equipped with an operation $a\Rightarrow b$ satisfyingThus, for fixed $a$, the map $x\mapsto x\wedge a$ is left adjoint to $y\mapsto a\Rightarrow y$. A left adjoint preserves joins, soThis is one distributive law for lattices; the other follows from it and the absorption laws. Hence every Heyting algebra is a distributive lattice. This argument is the distributivity of a Heyting algebra.

Take a three-world Kripke model for intuitionistic propositional logic with a root $r$ and two incomparable terminal successors $u$ and $v$. Force $p$ only at $u$, force $q$ only at $v$, and force neither atom at $r$.

At $u$, the atom $p$ holds, so $u⊩\neg \neg p$, while $u⊮q$. ThereforeLikewise $v⊩\neg \neg q$ and $v⊮p$, soThe Kripke forcing relation for a disjunction requires one disjunct to be forced at the current world. Consequentlywhich is the required Kripke countermodel.

Soundness follows by induction on derivations: assumptions are forced by hypothesis, implication introduction uses the definition of Kripke forcing relation, and implication elimination uses it at the current world.

For completeness, form the canonical Kripke model for implicational intuitionistic logic. Its worlds are deductively closed implicational theories $\Delta$ extending $\mathrm{Cn}(\Gamma )$, ordered by inclusion, andfor each atom $p$. We prove the truth lemmaby induction on implicational formulas. The atomic case is the definition. For $\alpha \to \beta$, membership implies forcing by closure under implication elimination. Conversely, if $\alpha \to \beta \notin \Delta$, the implication-introduction rule shows that $\mathrm{Cn}(\Delta \cup \{\alpha \})$ does not contain $\beta$; this extension forces $\alpha$ but not $\beta$, so $\Delta$ does not force $\alpha \to \beta$.

If $\Gamma {⊬}_{\mathrm{IPC}(\to )}\phi$, the root $\mathrm{Cn}(\Gamma )$ of this canonical model forces every member of $\Gamma$ but does not force $\phi$. Together with soundness, this proves Kripke completeness of implicational intuitionistic logic.

Finally suppose the implicational formulas $\Gamma$ and $\phi$ satisfy $\Gamma {⊢}_{\mathrm{IPC}}\phi$. The soundness theorem for propositional logic for intuitionistic Kripke semantics gives $\Gamma {\models }_{\mathrm{Kripke}}\phi$, and the completeness just proved gives $\Gamma {⊢}_{\mathrm{IPC}(\to )}\phi$. This is the conservativity of intuitionistic propositional logic over its implicational fragment.