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

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.