Past exam of the mathematics course of the University of Cambridge / 2021 / iii / Paper 120 / 6

Let $M$ be a nonstandard model of the Theory of true arithmetic whose carrier is $\mathbb{N}$, and suppose for contradiction that the graphs of ${+}^M$ and ${\times }^M$ are decidable. Because these operations are total, searching their decidable graphs computes their output on any pair of carrier elements.

Choose disjoint recursively inseparable sets $A,B$ that are computably enumerable, with primitive recursive stage predicates $E_A(n,s)$ and $E_B(n,s)$. Let $c\in M$ be nonstandard. True arithmetic proves finite sequence coding, so inside $M$ there is an element $a$ such that, for every $i<c$,where $p_i$ is the $i$th prime. This can be obtained by taking the product of the selected primes internally; it is the same finite coding mechanism as Gödel beta-function sequence coding.

Define the external setThis set is decidable from the assumed operations. For fixed standard $n$, compute the model element $p_n^M$. The division algorithm in $M$ gives unique $q$ and a remainder among the finitely many standard residuessuch that $a=q{\times }^M{p}_n^M+r$. Dovetail the search over $q$ and these finitely many residues, using the computable model operations. It eventually finds the unique remainder, and $n\in C$ exactly when that remainder is zero.

If $n\in A$, it enters $A$ at a standard stage below the nonstandard $c$, so $n\in C$. If $n\in B$, the true arithmetical sentence asserting that the two enumerations are disjoint holds in $M$, so $n$ cannot enter the coded $A$-set below $c$; hence $n\notin C$. Thuscontradicting recursive inseparability. The two operation graphs therefore cannot both be decidable. This is the recursively inseparable-set proof of Tennenbaum theorem.

No. The complement of the finite validity problem for first-order logic is computably enumerable: enumerate finite structures in the sentence's finite vocabulary, evaluate the sentence in each, and halt when a countermodel appears.

For the converse hardness, fix a Turing machine $P$ and input $w$. Effectively construct a first-order sentence ${\sigma }_{P,w}$ describing a halting computation tableau. Use finite linearly ordered sets for times and tape positions, predicates for the state, head position, and tape symbol at each cell, and first-order local clauses saying that the first row is the initial configuration, consecutive rows obey the transition table, and the final row is halting. ThenA halting run gives its finite tableau; conversely, the linear orders and local transition clauses make every finite model decode to such a run.

If the sentences true in every finite structure were computably enumerable, then for each $(P,w)$ we could enumerate until either a finite model of ${\sigma }_{P,w}$ appeared or $\neg {\sigma }_{P,w}$ appeared among the finite validities. This would decide the halting problem. Equivalently, $\neg {\sigma }_{P,w}$ is finitely valid exactly when $P$ does not halt, so finite validity cannot be computably enumerable. This is Trakhtenbrot theorem.