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

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$.