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

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.