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

A Heyting algebra is a bounded distributive lattice $L$ in which, for every $a,b\in L$, there is an element $a\Rightarrow b$ satisfyingThus $a\Rightarrow b$ is the greatest element whose meet with $a$ lies below $b$.

Solved by gpt-5.6-sol high.

For a finite distributive lattice, defineDistributivity and finiteness giveEvery $x$ with $x\wedge a\le b$ occurs in the join, so $x\le a\Rightarrow b$. This proves the defining adjunction and makes $L$ a Heyting algebra.

Solved by gpt-5.6-sol high.

Under the Curry-Howard correspondence, the term takes a proof $p$ of $\varphi \wedge \psi$, extracts proofs of $\varphi$ and $\psi$, and applies $f:\varphi \to (\psi \to \perp )$ to obtain a contradiction. It is therefore a proof ofequivalently $(\varphi \wedge \psi )\to \neg (\varphi \to \neg \psi )$.

Solved by gpt-5.6-sol high.

No. Although $\neg (\varphi \to \neg \psi )$ is classically equivalent to $\varphi \wedge \psi$, the reverse implication $\neg (\varphi \to \neg \psi )\to \varphi \wedge \psi$ is not intuitionistically valid, as part e shows. More generally, the standard normal-form separation theorem for the implicational fragment with falsity says that no formula built uniformly from $\varphi ,\psi ,\to ,\perp$ has both the pairing introduction rule and the two projection elimination rules of conjunction. Hence conjunction is not definable from implication and falsity in Intuitionistic propositional logic.

Solved by gpt-5.6-sol high.

Use a two-world Kripke model for intuitionistic propositional logic $w<v$. Force neither $\varphi$ nor $\psi$ at $w$, and force both at $v$. Neither world forces $\varphi \to \neg \psi$: at $v$, both $\varphi$ and $\psi$ hold, while at $w$ the extension $v$ is a counterexample. Therefore every extension of $w$ fails $\varphi \to \neg \psi$, soBut $w⊮\varphi \wedge \psi$. The implication is therefore not intuitionistically valid by Kripke completeness theorem for intuitionistic propositional logic.

Solved by gpt-5.6-sol high.

If $w$ determines an atom $p$, then either $w⊩p$, in which case persistence gives $u⊩p$ for every $u\ge w$, or $w⊩\neg p$, in which case no such $u$ forces $p$. Thus every relevant atom has a constant truth value throughout the cone above $w$. Structural induction on $\varphi$ now shows that every subformula has the same forcing value at all worlds above $w$: conjunction and disjunction are immediate, and an implication is forced exactly when the corresponding implication between these fixed truth values holds. Hence $w⊩\varphi$ exactly when $w^{\prime }⊩\varphi$.

Solved by gpt-5.6-sol high.

The Church-Rosser theorem states that if $M{\twoheadrightarrow }_{\beta }{N}_1$ and $M{\twoheadrightarrow }_{\beta }{N}_2$, then there is a term $P$ with $N_1{\twoheadrightarrow }_{\beta }P$ and $N_2{\twoheadrightarrow }_{\beta }P$. Equivalently, beta reduction is confluent.

Solved by gpt-5.6-sol high.

The Weak normalization theorem for simply typed lambda calculus says that every term typable in the implicational simply typed lambda calculus has a beta-normal form. Define reducibility by induction on types: a term of atomic type is reducible when it is weakly normalizing, and $M:A\to B$ is reducible when $MN$ is reducible at $B$ for every reducible $N:A$. Induction on types shows that every reducible term is weakly normalizing and that variables are reducible.

The fundamental substitution lemma is proved by induction on a typing derivation: if $\Gamma ⊢M:A$ and each variable in $\Gamma$ is replaced by a reducible term of its declared type, then the resulting term is reducible at $A$. The application case is the definition at arrow type; in the abstraction case, applying the abstraction to any reducible argument makes one beta step to the substituted body, which is reducible by induction. Substituting each free variable by itself makes every well-typed term reducible, hence weakly normalizing.

Solved by gpt-5.6-sol high.

A lambda term $F$ lambda-defines $f:{\mathbb{N}}^k\to \mathbb{N}$ when, for all $n_1,\dots ,n_k$,where $c_n$ is the Church numeral for $n$.

Solved by gpt-5.6-sol high.

No. Let $c_0=\lambda f.\lambda x.x$ and setBoth terms send every Church numeral to $c_0$, so both define the constant-zero function. They are distinct beta-normal forms, however, and the Church-Rosser theorem implies that distinct beta-normal forms cannot be beta-equivalent.

Solved by gpt-5.6-sol high.

TakeIf $L$ is a fixed-point combinator, then $Lf{\equiv }_{\beta }f(Lf)$, so eta-conversion givesConversely, if $L{\equiv }_{\beta \eta }\delta L$, application to an arbitrary $f$ gives $Lf{\equiv }_{\beta \eta }f(Lf)$, which is precisely the fixed-point-combinator property.

Solved by gpt-5.6-sol high.

A Sigma-1 formula is a formula equivalent in arithmetic to $\exists y_1\cdots \exists y_r\delta$, where $\delta$ is bounded. A Pi-1 formula is similarly equivalent to $\forall y_1\cdots \forall y_r\delta$ with $\delta$ bounded.

Solved by gpt-5.6-sol high.

The total function $f:{\mathbb{N}}^k\to \mathbb{N}$ is Sigma-1 represented in $T$ when there is a Sigma-1 formula $F(\mathbf{x},y)$ such that, for every standard tuple $\mathbf{n}$ and $m=f(\mathbf{n})$,Thus $T$ proves the correct unique output on every standard input.

Solved by gpt-5.6-sol high.

The Diagonal lemma says that for every one-variable formula $\theta (x)$ there is a sentence $\gamma$ such thatLet $d(n)$ be the computable function taking the code of a one-variable formula $\alpha (x)$ to the code of $\alpha (\bar{n})$. By the assumed representation theorem, choose a Sigma-1 formula $D(x,y)$ representing $d$. Given $\theta$, putand let $b=┌\beta ┐$. Taking $\gamma =\beta (\bar{b})$, representability proves in $T$ that the unique relevant $y$ is $d(b)=┌\gamma ┐$, yielding the required equivalence.

Solved by gpt-5.6-sol high.

Suppose such a formula $\theta (x)$ existed. Apply the Diagonal lemma to $\neg \theta (x)$ to obtain a sentence $\sigma$ for whichBecause $M\models {\mathrm{PA}}^{-}$, the equivalence holds in $M$. But the defining property of $\theta$ says $M\models \theta (┌\sigma ┐)$ exactly when $M\models \sigma$, producing $M\models \sigma$ exactly when $M/\models \sigma$, a contradiction.

Solved by gpt-5.6-sol high.

The Tennenbaum theorem states that no countable nonstandard model of Peano arithmetic has a presentation on $\mathbb{N}$ in which both its addition and multiplication operations are recursive.

Solved by gpt-5.6-sol high.

Assume multiplication in $M$ were recursive. The multiplication half of Tennenbaum's coding argument says that, for a fixed nonstandard code $c$, bothare computably enumerable from the multiplication table. The proof uses the canonical prime-power coding in PA; bounded inequalities are replaced by existential sum-of-four-squares conditions using the Lagrange four-square theorem, and the resulting witnesses can be searched for effectively from multiplication. Dovetailing the two searches decides the coded set. Applied to $c$, this would make $X$ recursive, contradicting the hypothesis. Therefore multiplication in $M$ cannot be recursive.

Solved by gpt-5.6-sol high.