Trakhtenbrot's theorem

In logic, finite model theory, and computability theory, Trakhtenbrot's theorem (due to Boris Trakhtenbrot) states that the problem of validity in first-order logic on the class of all finite models is undecidable. In fact, the class of valid sentences over finite models is not recursively enumerable (though it is co-recursively enumerable).

Trakhtenbrot's theorem implies that Gödel's completeness theorem (that is fundamental to first-order logic) does not hold in the finite case. Also it seems counter-intuitive that being valid over all structures is 'easier' than over just the finite ones.

The theorem was first published in 1950: "The Impossibility of an Algorithm for the Decidability Problem on Finite Classes".

We follow the formulations as in

Let σ be a relational vocabulary with one at least binary relation symbol.

Remarks

This proof taken from Chapter 10, section 4, 5 of Mathematical Logic by H.-D. Ebbinghaus.

As in the most common proof of Gödel's First Incompleteness Theorem through using the undecidability of the halting problem, for each Turing machine ${\displaystyle M}$ there is a corresponding arithmetical sentence ${\displaystyle \phi _{M}}$, effectively derivable from ${\displaystyle M}$, such that it is true if and only if ${\displaystyle M}$ halts on the empty tape. Intuitively, ${\displaystyle \phi _{M}}$ asserts "there exists a natural number that is the Gödel code for the computation record of ${\displaystyle M}$ on the empty tape that ends with halting".

...
Wikipedia