Past exam of the mathematics course of the University of Cambridge / 2022 / iii / Paper 120 (Logic and Computability)

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.

For a first-order theory $T$ in a first-order language $L$, a complete $n$-type is a maximal $T$-consistent set $p(x_1,\dots ,x_n)$ of formulas whose free variables lie among $x_1,\dots ,x_n$. Equivalently, it chooses exactly one of $\phi$ and $\neg \phi$ for every such formula while remaining consistent with $T$.

An isolated type $p$ is isolated by a formula $\theta (\bar{x})$ when $T\cup \{\exists \bar{x}\theta (\bar{x})\}$ is consistent andfor every $\phi \in p$. The type is an omitted type in an $L$-structure $M$ when no tuple $\bar{a}\in M^n$ satisfies every formula in $p$.

The omitting types theorem states that if $T$ is a consistent theory in a countable language and $(p_i{)}_{i\in \mathbb{N}}$ is a countable family of nonisolated finite-arity types, then $T$ has a countable model omitting every $p_i$.

Let $\mathcal{U}$ be a nonprincipal ultrafilter on an infinite set $I$. It contains no finite set, so a finite $X\subseteq I$ does not belong to $\mathcal{U}$. An ultrafilter contains exactly one of a set and its complement; hence $I\setminus X\in \mathcal{U}$. Equivalently, every nonprincipal ultrafilter contains the cofinite filter.

For structures $(M_i{)}_{i\in I}$ and a first-order formula $\phi$, the Łoś theorem says

Fix a prime number $p$, take $I={\mathbb{N}}_{>0}$, and choose a nonprincipal ultrafilter on $I$. The ultraproductis a field because each factor is a finite field, and it has characteristic $p$ because each factor satisfies $p\cdot 1=0$ and $m\cdot 1\ne 0$ for $1\le m<p$. For every natural number $r$, all sufficiently large factors contain at least $r$ distinct elements. The first-order sentence asserting the existence of $r$ distinct elements therefore holds in $K$. Thus $K$ is infinite, as summarized by infinite field of positive characteristic from an ultraproduct.

The Ehrenfeucht-Mostowski theorem says that if a first-order theory $T$ has an infinite model, then for every total order $I$ there is a model $M\models T$ generated as the Skolem hull of distinct order indiscernibles $(a_i{)}_{i\in I}$, and every order automorphism of $I$ extends to an automorphism of $M$.

Given an infinite cardinal $\kappa$, let $I=\kappa \times \mathbb{Q}$ with the lexicographic order, viewed as $\kappa$ consecutive copies of the rational order. In each copy independently choose either the identity or a fixed nonidentity order automorphism of $\mathbb{Q}$. These choices give $2^{\kappa }$ distinct order automorphisms of $I$.

Apply the theorem to this order. Distinct order automorphisms act differently on the distinct generators $a_i$, so their extensions give an injection into the automorphism group of a first-order structure $\mathrm{Aut}(M)$. Therefore $|\mathrm{Aut}(M)|\ge 2^{\kappa }$, proving that $T$ has models with arbitrarily large automorphism groups.

The Church numeral corresponding to the natural number $n$ isA function $g:{\mathbb{N}}^k\to \mathbb{N}$ is a lambda-definable function if some closed lambda term $G$ satisfiesfor all natural numbers $n_1,\dots ,n_k$.

DefineThen beta reduction givesTherefore the successor function is lambda-definable; this is the lambda definition of the successor function.

A combinator is a lambda term without free variables. It is a fixed-point combinator whenfor every lambda term $F$.

The fixed-point theorem for the untyped lambda calculus states that every untyped lambda term $F$ has a fixed point up to beta equivalence. PutOne beta reduction giveswhich proves the theorem. Equivalently,is a fixed-point combinator.

Apply the theorem to the lambda term $\mathrm{Succ}$. Its fixed point $Y\mathrm{Succ}$ is a nonnormalizing lambda term satisfying $Y\mathrm{Succ}{\equiv }_{\beta }\mathrm{Succ}(Y\mathrm{Succ})$; it is not a Church numeral. The definition of a lambda-definable function describes the representing term only on Church-numeral inputs, so it does not turn this syntactic fixed point into a natural number $n$ satisfying $n+1=n$.

By assumption the set of combinators is recursively enumerable. Finite beta reduction sequences, and hence finite certificates of beta equivalence, are also recursively enumerable.

For a closed term $Y$, choose a fresh variable $f$. The term $Y$ is a fixed-point combinator exactly whenIndeed, substitution then gives the required equivalence for every $F$, and the forward direction follows by taking $F=f$. Dovetail the enumeration of closed terms with all finite beta-equivalence certificates. Whenever a certificate of the displayed equivalence is found, output $Y$. This enumerates exactly the fixed-point combinators, proving recursively enumerable fixed-point combinators.