Tra(k)htenbrot's Theorem

This theorem is rarely presented in undergraduate or even beginning graduate courses on this kind of topic, because if you use some theory of arithmetic as your basic undecidable set instead of the halting problem the theorem becomes really hard to prove. The first examples of undecidable sets, due to Gö were of that sort, and so it is traditional to use them as basic, not the halting problem, outside of CS departments. CS people don't have much interest in Trahtenbrot's theorem, and so they don't bother to prove it either.

One of the main reasons I'm using this book is that they do things in mathematically the most efficient way instead of the way things happened to develop historically, and so they can prove Trahtenbrot's theorem easily.

Definition. A sentence %$\phi$% (of first-order logic) is satisfiable if it is true in some structure.

Definition. A sentence %$\phi$% (of first-order logic) is finitely satisfiable (fin-satisfiable) if there is a finite structure in which it is satisfied.

Definition. A sentence %$\phi$% (of first-order logic) is finitely valid (fin-valid) if it is true in every (appropriate) finite structure. ("Appropriate" just means with the right language.)

Example: We can map the natural numbers properly into themselves, by taking 0 to 1, 1 to 2, and so forth. You can't do that for a finite domain: on a finite domain a function that is injective from the domain to itself must also be surjective. Therefore, the sentence "if f is injective it is surjective" is fin-valid, but not valid. The negation is satisfiable, but not fin-satisfiable.

Lemma. The set of finitely satisfiable sentences is r.e. (R-enumerable).

Proof: You can list all sentences, you can, almost, list all finite structures, you can tell when a sentence is true in a structure, so use a busy beaver construction.

Of course, we can't really list all finite structures, we can't even list all structures with one-element domains: there are such structures for any object whatsoever, in particular, for any ordinal number whatsoever, and so there is a proper class of them. However, every structure with a one-element domain is isomorphic to a structure with domain {0}. Similarly, every finite structure is isomorphic to one with a domain of the form %$\{0,\dots ,n\}$%. If a sentence is satisfiable in a structure, it is satisfied in every structure isomorphic to the initial one, and so the finitely satisfiable sentences are the sentences satisfiable in a structure with domain of the form %$\{0,\dots ,n\}$%. Those structures are recursively enumerable.

Theorem. The set of finitely satisfiable sentences is not decidab le.

Proof. We need to reduce the halting problem to finite satisfiability. That is, we need, for each register machine %$P$% a sentence %$\psi_P$% that is finitely satisfiable if and only if the machine halts. The sentence %$\psi_P$% we used in the previous section of the book to reduce the halting problem to valid sentences works because when a machine halts, the corresponding model is finite, and it is infinite when the machine doesn't halt.%$\square$%

Corollary. (Trahtenbrot's theorem.) The set of finitely valid sentences is not r.e.

Proof. A sentence is either finitely satisfiable or the negation of a finitely valid sentence. If the finitely valid sentences were r.e. then (obviously) the set of their negations would also be r.e. That is, the set of finitely satisfiable sentences is r.e. and the set of not finitely satisfiable sentences would also be r.e. But that would make the finitely satisfiable sentences decidable, contradicting the theorem: just list the finitely satisfiable sentences and list the not finitely satisfiable sentences. Every sentence eventually appears on one or the other list, and yield a decision, which is the required contradiction.%$\square$%

It follows that the set of logical truths of second-order logic is not even r.e.: We show that by reducing finite validity to second-order validity. Since finite validity is not r.e., it will follow that second-order validity is not r.e.

We need for every first-order sentence %$\phi$% a second-order sentence that is valid if and only if %$\phi$% is finitely valid.

The sentence will say: "if the domain is finite then %$\phi$%." So, we just need to see how to say "the world is finite" in second-order logic. This will do: "Every injective function is surjective."

In detail, let %$\phi_\mbox{fin}$% be %\[\forall f(f{\text{ is injective}}\rightarrow f{\text{ is surjective}}),\]% that is, %\[\forall f(\forall x\forall y(fx\equiv fy\rightarrow x\equiv y)\rightarrow\forall x\exists yx\equiv fy).\]%

-- ProfessorShaughanLavine - 23 Mar 2005