Past exam of the mathematics course of the University of Cambridge / 2017 / iii / Paper 135 (Logic)

Work in ZF with the law of excluded middle, without the axiom of choice. The paper's terminology is an infinite Dedekind-finite set. The useful common principle is countable union of explicitly ordered finite lists without choice: given an actual sequence of finite lists, enumerate their entries by list number and position using a Cantor pairing function. If the union of entries is infinite, repeatedly take the entry with the least code not already selected. This produces an injection from $\mathbb{N}$ without choosing any enumerations of unordered sets.

Consequently, if a family of objects has an explicitly ordered finite list of labels for each object, and only finitely many objects can be made from any given finite pool of labels, then a countably infinite list of distinct objects forces a countably infinite subset of the label set. For a Dedekind-finite label set this is impossible. If the label set embeds into the object family as well, infinitude is preserved. ThusThe distinction between ordered lists supplied by the data and arbitrary finite subsets is essential: a blanket countable-union theorem for unordered finite sets would introduce a choice principle.

Let $\mathrm{Inj}(<\omega ,X)$ denote the finite repetition-free sequences, including the empty sequence. The map $x\mapsto (x)$ is injective, so this set is infinite when $X$ is infinite. Suppose, for a contradiction, that it contains a countably infinite subset. Fix its given injective enumeration $s_0,s_1,\dots$; this is part of the supposition, not a choice from a family of sets.

Enumerate all pairs $(n,j)$ with $j<\mathrm{length}(s_n)$ by their natural-number pairing codes, recording the corresponding entries $s_n(j)$. If the union of entries were infinite, recursively selecting the first new entry would give an injection $\mathbb{N}\to X$, contradicting Dedekind-finiteness. Therefore the union is a finite set $F$, say of size $m$. A repetition-free sequence over $F$ has length at most $m$, and there are exactlysuch sequences, with the empty product equal to one. All $s_n$ would belong to this finite set, contradicting their distinctness. Finite counting and the least-code construction use no axiom of choice. This proves finite repetition-free sequences preserve Dedekind-finiteness and the required infinitude:

Write $\mathcal{T}(D)$ for the recursively repetition-free labelled trees. Each rooted tree is finite because the inductive definition forms it from an already constructed finite list of finite child rooted trees. Its label list is obtained by visiting the root first, then each child subtree in its prescribed order, using a depth-first traversal of a tree. This list can have repetitions. In particular, different branches may use the same label; the children are required to be distinct rooted trees, not to have distinct root labels.

For any finite label pool $F$, prove by mathematical induction on $|F|$ that $\mathcal{T}(F)$ is finite. For $F=\varnothing$ it is empty. For each root $d\in F$, the children form a finite repetition-free sequence from $\mathcal{T}(F\setminus \{d\})$, which is finite by mathematical induction. There are therefore finitely many child lists for that root, and the finite union over $d\in F$ is finite. More explicitly, if $t_m$ is the number of rooted trees on a pool of $m$ labels, thenThere is no countable choice in this finite mathematical induction.

Now suppose $T_0,T_1,\dots$ were an injective enumeration of a countably infinite subset of $\mathcal{T}(D)$. Their canonical traversal lists give an explicit enumeration of all labels used. If infinitely many different labels occur, the least-first-occurrence procedure gives a countably infinite subset of $D$, a contradiction. Otherwise all labels belong to one finite set $F$. Every $T_n$ then belongs to $\mathcal{T}(F)$: recursively its root lies in $F$ and its child rooted trees use only $F$ with that root removed. But $\mathcal{T}(F)$ is finite by the preceding mathematical induction, again a contradiction. Finally $d\mapsto$ the single-vertex rooted tree labelled $d$ is injective, so $\mathcal{T}(D)$ is infinite. Hence recursively repetition-free labelled trees preserve Dedekind-finiteness:

For subsets $A,B\subseteq \mathbb{N}$, a many-one reduction $A{\le }_{m}B$ is a total computable function $h$ with $n\in A⟺h(n)\in B$. A Turing reduction $A{\le }_{T}B$ is an oracle machine with oracle $B$ computing the total indicator function ${\chi }_A$. It may make several adaptive oracle queries. A many-one reduction gives a Turing reduction using one query; the definitions impose no enumerability assumption on $A,B$.

The Friedberg–Muchnik theorem asserts that there exist computably enumerable sets $A,B$ withWe give the finite-injury priority construction. Fix an effective list ${\Phi }_e$ of Turing functionals and imposein priority order $R_0,S_0,R_1,S_1,\dots$. Each strategy has an unassigned, waiting or protected state; a private witness $x$ when assigned; and a restraint on the oracle set when protected. All witnesses, even abandoned ones, are permanently recorded and never reused. A strategy for $R_e$ is the only strategy ever allowed to enumerate its witness into $A$; the analogous statement holds for $S_e$ and $B$.

Start with finite sets $A_0=B_0=\varnothing$. At stage $s$, inspect the first $s+1$ strategies. An unassigned strategy needs attention. A waiting $R_e$ strategy needs attention if the computation ${\Phi }_e^{B_s}(x)$ converges within $s$ steps; waiting $S_e$ is symmetric. Act on the highest-priority strategy needing attention, if any. On assignment choose a fresh witness greater than $s$, every earlier witness and every higher-priority restraint, and enter the waiting state. On a convergence with output $v$ and oracle use $u$, act as follows: if $v=0$, enumerate the witness into its own target set; if $v\ne 0$, leave the witness out. Enter the protected state and restrain the oracle below $u$. The current characteristic value at the witness is now different from $v$, including outputs other than zero or one. Whenever a strategy acts, initialize every lower-priority strategy, discarding its current witness and restraint but retaining the permanent record of used witnesses. If none needs attention, change nothing.

Every enumeration respects higher-priority restraints: its witness was chosen beyond them after its last initialization, and a later higher-priority action would have initialized it. Each stage is effective, finite and monotone in $A_s,B_s$, so $A={\bigcup }_s{A}_s$ and $B={\bigcup }_s{B}_s$ are computably enumerable. Lower-priority restraints may be violated by a higher-priority action, exactly the allowed injuries.

Induct on priority to verify finite injury and satisfaction. Once all higher-priority strategies have made their last actions, the current strategy receives its final assignment and can act at most once more, on a convergence. If convergence is observed it is then protected permanently; otherwise it waits without further action. In either case every strategy acts only finitely often. After the final initialization of $R_e$, if it acts on a convergence, no higher strategy subsequently changes its assumptions and every lower strategy respects its restraint. The observed oracle computation therefore remains valid for the final $B$, while the permanently private witness retains the opposite characteristic value in $A$.

If it waits forever, then ${\Phi }_e^B(x)$ cannot converge. A convergent final computation uses only finitely many oracle bits; those bits in the increasing enumeration $B_s$ eventually equal their final values. For a sufficiently large stage the same finite computation would have been observed, and after the higher strategies have stopped it would receive attention, contradicting perpetual waiting. Thus $R_e$ is satisfied either by disagreement or by divergence. The same proof satisfies every $S_e$. This is private-witness diagonalization for incomparable enumerable sets, with the finite-injury verification supplying the required permanent disagreements.

A computable set reduces to every oracle, so incomparability makes both sets noncomputable. Every computably enumerable set reduces to the halting problem; if either of these sets had the halting degree, the other would reduce to it. Thus their c.e. degrees are also incomplete, giving the intermediate degrees sought by the Post problem.

The countable form of the omitting types theorem is as follows. Let $L$ be a countable first-order language and $T$ a consistent first-order theory in $L$. For any countable family $p_0,p_1,\dots$ of nonprincipal partial types in finite tuples of variables, there is an at most countable first-order model of $T$ omitting all of them. Nonprincipality means that no $T$-consistent first-order formula $\theta (\mathbf{x})$ entails every member of the type modulo $T$. A complete first-order theory with nonisolated complete types is the usual special case; neither an uncountable language nor an arbitrary uncountable family is covered by this statement.

Use the Godel completeness theorem to pass between consistency and the existence of a first-order model. Adjoin a countable stock $C$ of new constants. Construct finite conditions ${\Gamma }_s$ with $T\cup {\Gamma }_s$ consistent, interleaving three countable lists of requirements: decide each $L(C)$-sentence; provide a fresh constant witness for each existential sentence; and, for each $p_i$ and each tuple $\mathbf{t}$ of closed terms of its arity, add $\neg \psi (\mathbf{t})$ for some $\psi \in p_i$. Sentence decisions preserve consistency by choosing a consistent sign. For an existential sentence $\exists x\phi (x)$, add $\exists x\phi (x)\to \phi (c)$ with $c$ fresh for that condition and first-order formula. This is consistent: any first-order model of the old condition can interpret $c$ as a witness if one exists, and otherwise arbitrarily in the nonempty domain.

The omission step is the key Henkin omission extension lemma. Let $\sigma (\mathbf{c})$ be the logical conjunction of the current finite condition, listing every new constant occurring either there or in $\mathbf{t}$. If adding $\neg \psi (\mathbf{t})$ were inconsistent for every $\psi \in p_i$, then $T$ would entail $\sigma (\mathbf{c})\to \psi (\mathbf{t}(\mathbf{c}))$ for each such $\psi$. Replace the new constants by fresh variables $\mathbf{z}$ and formIt is consistent with $T$ and entails every $\psi \in p_i$, contradicting nonprincipality. Hence some omission extension is consistent. The construction need not be computable; countability merely permits all these requirements to be scheduled.

Let $T^{\ast }$ be the deductive closure of $T\cup {\bigcup }_s{\Gamma }_s$. It is consistent by the finite character of formal proofs, complete by sentence decisions, and has the Henkin witness property. Its term model consists of closed terms modulo provable logical equality and has at most countably many elements. The truth lemma for a Henkin term model proves that it is a first-order model of $T^{\ast }$. Every tuple in it is represented by closed terms, whose scheduled omission requirement supplies a negated member of each corresponding type. Thus

A universal sentence has the form $\forall \mathbf{x}\psi (\mathbf{x})$ with quantifier-free $\psi$, including an empty quantifier block. Embeddings preserve and reflect quantifier-free truth, so universal sentences pass to substructures of a first-order structure. For the converse Łoś-Tarski preservation theorem, let $T_{\forall }$ be all universal consequences of an arbitrary first-order theory $T$, and take $A\models T_{\forall }$. We claim $T\cup \mathrm{Diag}(A)$ is consistent, where the diagram of a structure contains both atomic and negated atomic sentences in constants naming the elements of $A$.

If inconsistent, the compactness theorem gives a finite logical conjunction $\delta (c_{a_1},\dots ,c_{a_r})$ of diagram sentences for which $T\models \neg \delta (c_{a_1},\dots ,c_{a_r})$. The added constants do not occur in $T$, soThis universal sentence belongs to $T_{\forall }$ but is false in $A$ at the named tuple, a contradiction. The compactness theorem therefore produces $B\models T$ containing an isomorphic embedded copy of $A$. The signed diagram ensures a genuine substructure of a first-order structure: functions are preserved, constants are included and relations are preserved and reflected. If the first-order model class of $T$ is closed under substructures of a first-order structure, this copy, and hence $A$, is a first-order model of $T$. We have provedNo countability assumption is needed for this second argument. An inconsistent first-order theory is covered as well, with a universally false axiom and an empty first-order model class.

One form of the Ehrenfeucht-Mostowski theorem says that, for every infinite first-order structure $M$ and every total order $I$, an elementary extension contains distinct elements $(a_i{)}_{i\in I}$ forming an order-indiscernible sequence. After a suitable Skolem expansion, their Skolem hull is a first-order model of $\mathrm{Th}(M)$, and every order automorphism of $I$ extends to a structure automorphism of that hull. If $M$ has a definable infinite linearly ordered subset $P$, the generators may lie in $P$ and their order may agree with that definable order. Uniqueness of the extended structure automorphism is asserted in the chosen Skolem expansion, rather than for every structure automorphism of its reduct.

Here is an ultraproduct proof of the Ehrenfeucht-Mostowski theorem. First expand $M$ to $M^{+}$ with Skolem functions for all existential first-order formulas, iterating through the enlarged languages if necessary. This is done in the ordinary classical metatheory; the choice restriction in question 1 is not a restriction on this question. Fix a nonprincipal ultrafilter $\mathcal{U}$ on $\mathbb{N}$.

We can obtain an infinite sequence of distinct elements $b_0,b_1,\dots$ in an elementary extension $M_0$ of $M^{+}$ by one preliminary ultrapower. For each $n\ge 1$ choose a finite list of $n$ distinct elements of $M^{+}$. Represent $b_j$ by the function taking the $j$th entry when $n>j$, with an arbitrary default otherwise. Distinctness holds on a cofinite set, so follows from Łoś theorem. In the definably ordered variant, first name any parameters defining $P$, and choose each finite list increasingly inside $P$ instead; then $M_0\models P(b_j)$ and $b_j<b_k$ for $j<k$. Infinitude of an ordered set supplies every finite increasing chain. This preparatory step uses no Ramsey theorem.

For a finite subset $F=\{i_1<\cdots <i_r\}$ of $I$, define the ultrafilter ${\mathcal{U}}_F$ on ${\mathbb{N}}^F$ by nested membership, in this order:where $(\mathcal{U}n)Q(n)$ means $\{n:Q(n)\}\in \mathcal{U}$. This is the ordered Fubini product of ultrafilters. Closure under intersections and the decision between a set and its complement hold at each nested level, proving it is an ultrafilter. For $F=\varnothing$ take the principal ultrafilter on the one-point product. PutIf $F\subseteq G$, pull a function back along the projection ${\mathbb{N}}^G\to {\mathbb{N}}^F$. A test independent of an omitted coordinate is unchanged by its ultrafilter quantifier, so projection pushes ${\mathcal{U}}_G$ to ${\mathcal{U}}_F$. The induced map $N_F\to N_G$ is therefore an elementary embedding by Łoś theorem. These maps are coherent, giving a directed system indexed by finite subsets of $I$.

Take its directed limit of elementary embeddings $N$. One can verify elementarity directly: representatives of a finite tuple occur at a common stage; functions and atomic relations are interpreted there. In the existential step, a witness in the limit occurs with the parameters at some later common stage, and elementarity pulls the existence statement back. Thus every $N_F$ embeds elementarily into $N$, which contains an elementary copy of $M^{+}$.

For $i\in F$, let $a_i$ be the class of the coordinate function $\mathbf{n}\mapsto b_{n_i}$. Projection coherence makes this independent of $F$. If $i<j$, then for each fixed $n_i$ the set $\{n_j:n_j\ne n_i\}$ is cofinite. The nested test therefore gives $a_i\ne a_j$. In the ordered variant, the same argument with $n_j>n_i$ gives $P(a_i)$ and $a_i<a_j$.

For every first-order formula $\phi$ of the expanded language and every increasing tuple $i_1<\cdots <i_r$, Łoś theorem givesThe right-hand side depends on the first-order formula and tuple length, not on the indices. This proves order indiscernibility in the expanded language. Let $H$ be the Skolem hull of the generators in $N$. The Tarski-Vaught test gives $H\prec N$, and its reduct is a first-order model of $\mathrm{Th}(M)$.

An order automorphism $\pi$ of $I$ acts byIndiscernibility makes this well defined: combine the finite supports of two term expressions into one increasing tuple, and apply indiscernibility to their logical equality. Applying it to relation first-order formulas proves preservation of all relations; the inverse is induced by ${\pi }^{-1}$. Every element of the hull is such a term, so the extension is unique among structure automorphisms preserving the Skolem expansion. MoreoverThis proves the theorem, including its ordered version and structure automorphism conclusion, using ultrapowers and a directed limit throughout.

Use the Gödel-Gentzen negative translation, writing $A^N$ for the translated first-order formula. On atomic formulas $P$, including logical equality, put $P^N=\neg \neg P$, and put ${\perp }^N=\perp$. Extend recursively byLogical negation abbreviates logical implication to logical falsity, so $(\neg A{)}^N=\neg A^N$. The displayed logical disjunction and existential clauses are intuitionistically equivalent to the usual negative clauses $\neg (\neg A^N\wedge \neg B^N)$ and $\neg \forall x\neg A^N$, respectively. Thus these clauses specify the same negative interpretation. Translation commutes with capture-avoiding substitution of terms for free variables.

First prove by structural induction the stability of a formula under double negation:Every double logical negation is stable, since intuitionistic first-order logic proves $\neg \neg \neg \neg C\to \neg \neg C$; logical falsity is stable as well. Stability passes to logical conjunction by obtaining double logical negation of each component. For a logical implication $C\to D$ with stable $D$, assume $\neg \neg (C\to D)$ and $C$. An assumption $\neg D$ would give $\neg (C\to D)$, a contradiction, so $\neg \neg D$ and then $D$. For a universal first-order formula, $\neg \neg \forall xC(x)$ implies $\neg \neg C(y)$ for arbitrary fresh $y$; use stability pointwise and generalize. Logical disjunction and existential translations are already double negations. This proves all cases.

Now regard classical first-order natural deduction as intuitionistic natural deduction plus unrestricted double-negation elimination, and induct on a classical derivation. The rules for logical conjunction, logical implication, universal quantification and logical falsity translate directly. Logical disjunction introduction gives $A^N\vee B^N$ and then its double logical negation. For logical disjunction elimination, the translated premise is $\neg \neg (A^N\vee B^N)$ and the two translated branches yield the stable conclusion $C^N$. Assuming $\neg C^N$ makes each branch contradictory, giving $\neg A^N$ and $\neg B^N$, hence $\neg (A^N\vee B^N)$, which contradicts the premise. We have $\neg \neg C^N$ and remove it by stability.

Existential introduction likewise adds a double logical negation to the ordinary witness introduction. In existential elimination, the witness branch $A^N(y)⊢C^N$ has the original fresh-variable condition. Assuming $\neg C^N$ makes that branch give $\neg A^N(y)$; generalization gives $\forall y\neg A^N(y)$ and therefore $\neg \exists y{A}^N(y)$, contradicting the translated premise. Again stability supplies $C^N$. The universal-rule side conditions are preserved because the translation introduces no new free variables.

For logical equality, reflexivity gives $t=t$ and then its double logical negation. For substitution, from $\neg \neg (s=t)$ and $A^N(s)$, temporarily assume $\neg A^N(t)$. An assumption $s=t$ would transport $A^N(s)$ to $A^N(t)$ by intuitionistic logical equality substitution, so it gives a contradiction and hence $\neg (s=t)$. The first premise contradicts this. Thus $\neg \neg A^N(t)$ holds and stability gives $A^N(t)$. Finally a classical double-negation elimination step translates precisely to $\neg \neg A^N\to A^N$, already proved. Every rule is therefore covered, giving negative translation of a classical proof:In particular a classical thesis has an intuitionistic, constructive translated proof. If nonlogical assumptions are present, they must be translated too.

In classical logic, double-negation elimination gives $P^N\leftrightarrow P$ on atoms. Structural induction propagates equivalence through logical conjunction, logical implication and both quantifiers, and removes the added double negations on logical disjunction and existence. Therefore

Use untyped lambda calculus and normal-order beta reduction. Write $c_n=\lambda fx.f^{n}x$ for the Church numeral of $n$. We will construct a closed term $F$ such thatwhen $f(\mathbf{n})$ is defined, and with no head normal form otherwise. The latter condition implies that the result is not in beta equivalence with any Church numeral, so both definedness and the output are represented.

First represent all total primitive recursive functions. The zero function is $\lambda \mathbf{x}.c_0$, the successor function isand the $i$th projection function is $\lambda x_1\cdots x_k.x_i$. Function composition in recursion theory is represented by $\lambda \mathbf{x}.G(H_1\mathbf{x})\cdots (H_r\mathbf{x})$. This composition claim is used here for total functions, whose inner terms all reduce to numerals.

For primitive recursion use Church pairs and iteration. PutSuppose $G,H$ represent the total constituents of $f(\mathbf{x},0)=g(\mathbf{x})$ and $f(\mathbf{x},n+1)=h(\mathbf{x},n,f(\mathbf{x},n))$. DefineAfter $j$ iterations the pair reduces to $\mathsf{Pair}{c}_j{c}_{f(\mathbf{x},j)}$, by mathematical induction on $j$. Its second projection is the required result. This lambda definition of primitive recursion by pair iteration and structural induction on the primitive recursive construction give terms for all primitive recursive functions.

For an arbitrary partial computable function use the Kleene normal form theorem with its program index fixed. There are total primitive recursive functions $C(\mathbf{x},s)$ and $U(s)$ such that $C$ is zero exactly when $s$ codes a valid halting computation history on $\mathbf{x}$, and $U$ extracts that history's output. Checking finite coded configurations and each transition is primitive recursive. Determinism ensures that every accepted history on an input has the same output. HenceIf the input computation never halts, no history is accepted. Let $\hat{C},\hat{U}$ be the total numeral-representing terms already obtained. The Church numeral zero test is $\mathsf{Zero}=\lambda n.n(\lambda z.\mathsf{F})\mathsf{T}$, returning $\mathsf{T}$ exactly on zero. A Church Boolean applied to two arguments selects the appropriate branch without evaluating the other.

Take the fixed-point combinator $Y=\lambda h.(\lambda z.h(zz))(\lambda z.h(zz))$. For the input tuple defineExpanding the displayed abbreviations gives a genuine finite combinator. At a numeral code $c_j$, the total predicate computation terminates. If it returns a positive numeral, the false Church Boolean selects the next search code. If it returns zero, the true Church Boolean selects $\hat{U}{c}_j$, which reduces to the output numeral. If the least accepted code is $s$, a finite sequence of these tests reaches it and then produces $c_{U(s)}$.

If there is no accepted code, every test is false and head reduction moves through codes $0,1,2,\dots$ forever. At no finite point can a head variable or an outer numeral abstraction be produced: the applied search term must first unfold the fixed point and evaluate the next total test, and the decoder branch is always discarded. Thus it has no head normal form. The standard head-normalization property, or the Church-Rosser theorem together with normalization of normal-order reduction, rules out beta equivalence to a numeral. In particular, we have avoided a lazy-composition pitfall: an outer function that discards an argument need not force a divergent inner computation. The decoder is reached only after the guarded search succeeds. This proves lambda representation of partial computable functions: