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.
The theorem was first published in 1950: "The Impossibility of an Algorithm for the Decidability Problem on Finite Classes".
Remarks This proof is 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
asserts "there exists a natural number that is the Gödel code for the computation record of
[3] Note in the above statement that the corollary also entails the theorem, and this is the direction we prove here.
Theorem Proof According to the previous lemma, we can in fact use finitely many binary relation symbols.
What we want to prove is that for every Turing machine M we construct a sentence φM of vocabulary τ such that φM is finitely satisfiable if and only if M halts on the empty input, which is equivalent to the halting problem and therefore undecidable.
Let M= ⟨Q, Σ, δ, q0, Qa, Qr⟩ be a deterministic Turing machine with a single infinite tape.
We define τ so that we can represent computations: Where: The sentence φM states that (i) <, min, Ti's and Hq's are interpreted as above and (ii) that the machine eventually halts.
The halting condition is equivalent to saying that Hq∗(s, t) holds for some s, t and q∗ ∈ Qa ∪ Qr and after that state, the configuration of the machine does not change.
The sentence φM is: φ ≡ α ∧ β ∧ γ ∧ η ∧ ζ ∧ θ.
We break it down by components: Where θ2 is: And: Where θ3 is: s-1 and t+1 are first-order definable abbreviations for the predecessor and successor according to the ordering <.
If it is, then all is handled by θ1: everything is the same, except the head does not move to the left but stays put.
It follows that M halts on the empty input iff φM has a finite model.
Since halting on the empty input is undecidable, so is the question of whether φM has a finite model
Corollary Proof From the previous lemma, the set of finitely satisfiable sentences is recursively enumerable.
Assume that the set of all finitely valid sentences is recursively enumerable.
It follows that the set of finitely satisfiable sentences is recursive, which contradicts Trakhtenbrot's theorem.