Past exam of the mathematics course of the University of Cambridge / 2024 / iii / Paper 120 / 3

Under the Implicational Curry-Howard correspondence, propositions are simple types and assumptions are typed variables. The natural-deduction rulescorrespond respectively to the typing rulesAn assumption $x:A$ corresponds to the variable rule. Induction on a proof converts each rule into the matching typing construction; induction on a typing derivation reverses the process. Thus derivability of an implicational formula from assumptions is equivalent to inhabitation of its corresponding type.

By part (a), such a term would provein intuitionistic propositional logic. Consider the two-world Kripke model for intuitionistic propositional logic $r<s$. Let $\sigma$ hold only at $s$ and let $\tau$ hold nowhere. At both worlds $\sigma \to \tau$ fails, so $(\sigma \to \tau )\to \sigma$ holds at $r$ vacuously, while $\sigma$ does not hold at $r$. The displayed formula therefore fails at $r$. By the Kripke completeness theorem for intuitionistic propositional logic, it is not derivable, so no simply typed lambda term inhabits that type.

No such first-order theory exists. Suppose $T$ axiomatized the Heyting algebras having only finitely many regular elements. Expand the language by constants $c_n$ and addEvery finite subset has a model: take a sufficiently large finite Boolean algebra, in which every element is regular. By the compactness theorem, the entire expanded theory has a model. Its reduct is a model of $T$ with infinitely many distinct regular elements, contradicting the proposed axiomatization.