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

A Kripke model for intuitionistic propositional logic for a propositional language is a poset $(S,\le )$ together with a persistent forcing relation on atoms: if $w⊩p$ and $w\le v$, then $v⊩p$. Extend forcing byandNo world forces $\perp$. Induction proves persistence for every proposition.

Solved by gpt-5.6-sol high.

The Kripke completeness theorem for intuitionistic propositional logic saysfor every world $w$ in every intuitionistic Kripke model.

Take a root $r$ with two incomparable successors $u,v$. Force $p$ but not $q$ at $u$, force $q$ but not $p$ at $v$, and force neither at $r$. Then $r⊮p\to q$ because of $u$, and $r⊮q\to p$ because of $v$. Henceso completeness shows that this proposition is not intuitionistically valid.

Solved by gpt-5.6-sol high.

On equivalence classes defineand, for every atomic proposition $p\in \Phi$, put $[w]⊩p$ exactly when $w⊩p$. This is well-defined, is a partial order, and makes atomic forcing persistent.

The filtration of a Kripke model truth lemma statesConjunction and disjunction are immediate by induction. For implication, if $w⊩\alpha \to \beta$ and $[w]⪯[v]$, then $\alpha \to \beta$ belongs to ${\mathrm{Th}}_{\phi }(v)$; if $[v]⊩\alpha$, induction gives $v⊩\alpha$, hence $v⊩\beta$ and $[v]⊩\beta$. Conversely, if $w⊮\alpha \to \beta$, some actual $v\ge w$ forces $\alpha$ but not $\beta$; persistence gives $[w]⪯[v]$, which witnesses failure in the quotient. Thus every formula in $\Phi$ is preserved.

Solved by gpt-5.6-sol high.

Let $T$ consist of all finite nondecreasing pathsordered by initial-segment extension. The one-point path $(s_0)$ is least, and the predecessors of any path are its initial segments, hence linearly ordered. Force an atom at a path exactly when it is forced at the path's endpoint.

The endpoint map $e:T\to S$ is monotone and has the back property: if $e(t){\le }_{S}s$, append $s$ to $t$. Induction on propositions therefore givesIn particular the roots force exactly the same propositions. This is the unravelling of a Kripke model.

Solved by gpt-5.6-sol high.

Assume ${⊬}_{IPC}\phi$. By Kripke completeness there is a rooted countermodel. Unravel it into a tree and retain only the subformulas $\Phi$ of $\phi$. Whenever a retained node fails an implication $\alpha \to \beta \in \Phi$, retain one successor witnessing $\alpha$ and the failure of $\beta$. Along a branch, passing to a genuinely new witness strictly enlarges the finite theory of subformulas, so at most $n$ witness levels are needed. Identifying repeated equal theories and retaining at most one witness for each failed implication leaves at most $n$ representatives for each of the at most $2^n$ theories. The resulting pruned filtration has at most $n{2}^n$ worlds and still refutes $\phi$ by the truth lemma.

Thus every underivable formula with $n$ subformulas has a countermodel of size at most $n{2}^n$. The contrapositive proves the claim and is the quantitative Finite model property of intuitionistic propositional logic.

Solved by gpt-5.6-sol high.

A Sigma-1 formula is a formula equivalent in first-order arithmetic towhere $\delta$ is bounded. A Pi-1 formula is similarly equivalent to $\forall y_1\cdots \forall y_k\delta$ with bounded $\delta$.

Solved by gpt-5.6-sol high.

The Diagonal lemma states that for every formula $\theta (x)$ with one free variable there is a sentence $\gamma$ such thatThe same conclusion holds in every theory extending the arithmetic needed to formalize substitution.

Solved by gpt-5.6-sol high.

The crude incompleteness theorem says that every consistent recursively axiomatized extension $T$ of $P{A}^{-}$ is incomplete.

Suppose instead that $T$ were complete. Enumerating proofs until either $\sigma$ or $\neg \sigma$ appears would decide theoremhood, so its characteristic function ${\chi }_T$ would be total recursive. By the assumed representation theorem, choose a formula $R(x)$ such that $P{A}^{-}$ proves $R(\bar{n})$ when ${\chi }_T(n)=1$ and proves $\neg R(\bar{n})$ when ${\chi }_T(n)=0$. The diagonal lemma supplies $\gamma$ withIf $T⊢\gamma$, then ${\chi }_T(┌\gamma ┐)=1$, so $T⊢R(┌\gamma ┐)$ and is inconsistent. If $T⊢\neg \gamma$, then the characteristic value is zero, so $T⊢\neg R(┌\gamma ┐)$ and hence $T⊢\gamma$, again a contradiction. Completeness must therefore fail.

Solved by gpt-5.6-sol high.

The recursive theory $T=P{A}^{-}+\phi$ is consistent because $\mathbb{N}\models T$. By the Gödel-Rosser theorem it has an undecidable sentence $\rho$, so both $T+\rho$ and $T+\neg \rho$ are consistent. Exactly one of $\rho ,\neg \rho$ is false in $\mathbb{N}$; add that one to $T$. The first-order completeness theorem gives a model, and the Downward Lowenheim-Skolem theorem gives a countable model $M$. Then $M\models P{A}^{-}+\phi$, but $M$ disagrees with $\mathbb{N}$ on the chosen sentence and is therefore not elementarily equivalent to it.

Solved by gpt-5.6-sol high.

Disjoint sets $A,B\subseteq \mathbb{N}$ are recursively inseparable when there is no recursive $C\subseteq \mathbb{N}$ such that

Solved by gpt-5.6-sol high.

Consistency of $P{A}^{-}$ makes $A$ and $B$ disjoint. Suppose a recursive set $C$ separated them, and let $R(x)$ represent its total characteristic function in $P{A}^{-}$. By the Diagonal lemma, choose a sentence $\sigma$ satisfyingPut $n=┌\sigma ┐$. If $n\in C$, representability gives $P{A}^{-}⊢R(\bar{n})$ and hence $P{A}^{-}⊢\neg \sigma$, so $n\in B$, contradicting $B\cap C=\varnothing$. If $n\notin C$, representability gives $P{A}^{-}⊢\neg R(\bar{n})$ and hence $P{A}^{-}⊢\sigma$, so $n\in A\subseteq C$, again a contradiction. Therefore $A$ and $B$ are recursively inseparable.

Solved by gpt-5.6-sol high.

A partial function $f:{\mathbb{N}}^k\rightharpoonup \mathbb{N}$ is lambda-definable if there is a lambda term $F$ such thatwhenever the value is defined, while outside the domain the application reduces to no Church numeral.

Solved by gpt-5.6-sol high.

The Strong normalization theorem for simply typed lambda calculus says that every well-typed term has no infinite beta-reduction sequence. In the untyped calculus,reduces to itself and is therefore not strongly normalizing.

Solved by gpt-5.6-sol high.

The nowhere-defined partial function is represented byFor every Church numeral $c_m$, the term $F{c}_m$ reduces to $\Omega$ and hence to no numeral. If $F$ had type $Nat\to Nat$, the strong normalization theorem would make every reduction sequence from $F$ finite, contradicting the visible infinite reduction inside $\Omega$. Thus this partial function is lambda-definable by an untypable term of the required kind.

Solved by gpt-5.6-sol high.

A closed beta-eta-long normal term of type $\sigma \to \sigma \to \sigma$ must have the form $\lambda x:\sigma .\lambda y:\sigma .t$, where the normal term $t:\sigma$ can only be $x$ or $y$: the pure calculus has no constants or other closed source of a value of the atomic type $\sigma$. Hence the only two beta-eta-equivalence classes are the Church Booleans

Solved by gpt-5.6-sol high.

TakeIt has type $Boo{l}_{\sigma }\to Boo{l}_{\sigma }\to Boo{l}_{\sigma }$. If $a{\equiv }_{\beta }\top$, the body selects $x$. If $a{\equiv }_{\beta }\perp$, it reduces to $bxy$, which selects $x$ exactly when $b{\equiv }_{\beta }\top$. Thus it has the stated truth table.

Solved by gpt-5.6-sol high.

For $a\in \{0,1\}$ define a typed transition term $D_a:\sigma \to \sigma$ by a nested Boolean choice:Here a Church Boolean acts as an if-then-else operator. The assumed behavior of $e{q}_{\sigma }$ gives $D_a{q}_i{\equiv }_{\beta }{q}_{\delta (q_i,a)}$.

For $w=a_1\cdots a_k$, putand use $ϵ=\lambda x.x$. Induction on the word length gives

Solved by gpt-5.6-sol high.

Given a finite input word $w$, construct the typed term $\mathbf{w}{q}_0$ effectively and beta-normalize it. The Strong normalization theorem for simply typed lambda calculus guarantees termination, and confluence gives exactly one of the finitely many normal forms $q_i$. Compare that normal form syntactically with the listed accepting states in $F$. This algorithm accepts exactly when ${\delta }^{\ast }(q_0,w)\in F$, so $L$ is recursive. Equivalently, this is the standard theorem that every language recognized by a deterministic finite automaton is a regular language and hence decidable.

Solved by gpt-5.6-sol high.