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

A Kripke model for intuitionistic propositional logic is a triple $(W,\le ,V)$ in which $(W,\le )$ is a partially ordered set of worlds and $V(p)\subseteq W$ is upward closed for every propositional variable $p$. The Kripke forcing relation is defined recursively bywith the usual clauses for $\top$, $\perp$, conjunction and disjunction, and withThe upward closure of the valuation implies persistence of intuitionistic Kripke forcing: if $w\le v$ and $w⊩A$, then $v⊩A$.

The Kripke completeness theorem for intuitionistic propositional logic states that, for every set of formulae $\Gamma$ and formula $A$,The forward implication is soundness, and the reverse implication is completeness.

Take two worlds $r<s$ and let $p$ be forced only at $s$. Neither world forces $\neg p$: at $s$ this follows from $s⊩p$, while at $r$ the extension $s$ forces $p$. Consequently every extension of $r$ that forces $\neg p$ also forces $p$ vacuously, soBut $r⊮p$. The implication clause therefore giveswhich is a finite Kripke countermodel and proves that the formula is not intuitionistically valid.

Both sequents follow directly from the introduction and elimination rules of the implication-free fragment of intuitionistic propositional logic. From a proof of $\varphi \wedge (\psi \vee \chi )$, eliminate the conjunction to obtain $\varphi$ and $\psi \vee \chi$. Eliminate the disjunction: in the $\psi$ branch introduce $\varphi \wedge \psi$ and then the left disjunct; in the $\chi$ branch introduce $\varphi \wedge \chi$ and then the right disjunct. This yieldsConversely, eliminate the outer disjunction. From $\varphi \wedge \psi$, obtain $\varphi$ and introduce the left side of $\psi \vee \chi$; from $\varphi \wedge \chi$, obtain $\varphi$ and introduce its right side. In either branch, conjunction introduction produces $\varphi \wedge (\psi \vee \chi )$. HenceThis is the proof-theoretic form of the distributive law for lattices.

Suppose neither $\varphi$ nor $\psi$ is provable. By the Kripke completeness theorem for intuitionistic propositional logic, there are rooted Kripke countermodels with roots $r_{\varphi }⊮\varphi$ and $r_{\psi }⊮\psi$. Take their disjoint union and place a fresh world $r$ below every world in both components, forcing no propositional variables at $r$ beyond those required by persistence.

If $r⊩\varphi$, persistence would imply $r_{\varphi }⊩\varphi$, a contradiction; similarly $r⊮\psi$. Thus $r⊮\varphi \vee \psi$. By soundness, $\varphi \vee \psi$ is not provable. Taking the contrapositive proves the disjunction property of intuitionistic propositional logic:

Assume that $A$ is not intuitionistically valid. Completeness gives a Kripke countermodel for $A$. Apply filtration of a Kripke model through the finite set of subformulae of $A$: two worlds are identified when they force the same subformulae, and the quotient order is induced by inclusion of those finite theories. The filtration lemma preserves the forcing of every subformula of $A$, so the image of the original counterexample world still fails to force $A$. There are at most $2^n$ quotient worlds when $A$ has $n$ distinct subformulae. Hence the quotient is a finite countermodel.

This proves the Finite model property of intuitionistic propositional logic. Its contrapositive says that a proposition forced by every finite intuitionistic Kripke model is intuitionistically valid.