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

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.

The overspill lemma says that if $\mathcal{M}$ is a Nonstandard model of Peano arithmetic and a definable property $\phi (x,\bar{a})$, possibly with parameters from $\mathcal{M}$, holds for every standard natural number, then it also holds for some nonstandard element of $\mathcal{M}$.

LetIf $A$ had no nonstandard member, its complement would be nonempty. The least-number principle in Peano arithmetic would give a least $c\notin A$. Because every standard number belongs to $A$, the element $c$ would be nonstandard and nonzero. Its predecessor $c-1$ would also be nonstandard, so the supposition gives $c-1\notin A$, whereas the minimality of $c$ gives $c-1\in A$. This contradiction proves that $A$ contains a nonstandard element.

Applying this argument to $\psi (y)\equiv \forall x\le y\phi (x,\bar{a})$ gives the useful stronger form: there is a nonstandard $b$ such that $\phi (x,\bar{a})$ holds for every $x\le b$.

No such formula exists. If $\varphi (x)$ defined precisely the standard cut of a nonstandard model of arithmetic, then $\mathcal{M}\models \varphi (n)$ for every standard natural number $n$. The overspill lemma would produce a nonstandard $b\in M$ satisfying $\varphi (b)$, contradicting the proposed definition. Thus the standard elements form an external, nondefinable subset of every nonstandard model of Peano arithmetic.

A term is in beta-normal form when it contains no beta-redex, meaning no subterm of the formEquivalently, no beta reduction can be performed anywhere in the term.

The Weak normalization theorem for simply typed lambda calculus states that every well-typed term of the simply typed lambda calculus admits at least one finite sequence of beta reductions ending in a beta-normal form.

No. The Omega combinator isIts only beta-redex contracts back to $\Omega$ itself. Every reduction sequence therefore repeats the same term, which is not in beta-normal form. Thus $\Omega$ has no beta-normal form.

Suppose a fixed-point combinator $F$ were typable in the simply typed lambda calculus. By the Weak normalization theorem for simply typed lambda calculus, it would have a beta-normal form. For a fresh variable $f$, the term $Ff$ would then also possess a beta-normal form, say $N$.

The fixed-point property givesReducing the occurrence of $Ff$ on the right to $N$ gives the normal form $fN$. The Church-Rosser theorem says that these beta-equivalent terms must have alpha-equivalent normal forms. This is impossible because $fN$ contains more symbols than $N$. Hence no typing context and simple type can type $F$.

A prime filter of a distributive lattice $P$ is a proper lattice filter: it contains the top element, is upward closed, and is closed under finite meets. Primality means

The Priestley dual space $\hat{L}$ of a distributive lattice $L$ has all prime filters of $L$ as its points. Its order is inclusion. For each $a\in L$, putThe topology is generated by the sets $a^{\ast }$ and their complements. Each $a^{\ast }$ is therefore a clopen up-set, and these sets separate points and order. With this topology and order, $\hat{L}$ is a compact totally order-disconnected ordered space.

The Stone prime filter theorem says that if a lattice filter $F$ and a lattice ideal $I$ of a distributive lattice are disjoint, then there is a prime filter of a distributive lattice $P$ such thatEquivalently, whenever $a\nleqq b$, there is a prime filter containing $a$ and omitting $b$.

For a prime filter $P\in \hat{H}$, first suppose $a\Rightarrow b\in P$. If $Q\supseteq P$ and $a\in Q$, then $a\Rightarrow b\in Q$ andso $b\in Q$. Thus no prime filter above $P$ belongs to $a^{\ast }\setminus b^{\ast }$, and

Conversely, suppose $a\Rightarrow b\notin P$. The lattice filter generated by $P\cup \{a\}$ is disjoint from the principal lattice ideal $\downarrow b$. Indeed, an intersection would give some $p\in P$ with $p\wedge a\le b$, whence $p\le a\Rightarrow b$ and then $a\Rightarrow b\in P$, a contradiction. The Stone prime filter theorem therefore extends this filter to a prime filter $Q\supseteq P$ that omits $b$. Then $Q\in a^{\ast }\setminus b^{\ast }$, so $P\in \uparrow (a^{\ast }\setminus b^{\ast })$.

We have proved, for every $P$,which is the required identity

Let $L$ be any distributive lattice. Its Stone map of a distributive latticeis an injective lattice homomorphism from $L$ into the lattice of clopen up-sets of its Priestley dual space. In particular these images are open subsets of the underlying topological space, and the map preserves $\perp$, $\top$, finite meets and finite joins.

Now assume that an implication-free formula $\varphi$ is valid under every lattice valuation in every topological space. Given any valuation of its variables in any distributive lattice $L$, compose it with the Stone map. Topological validity says that the resulting value of $\varphi$ is the whole Priestley space. Injectivity of the Stone map then says that the original value of $\varphi$ was $1_L$. Hence $\varphi$ is valid in every distributive lattice.

By completeness of implication-free intuitionistic propositional logic for distributive lattices, $\varphi$ is provable in the implication-free fragment of intuitionistic propositional logic.