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".
Mathematical formulation
We follow the formulations as in Ebbinghaus and Flum
Theorem
Satisfiability for finite structures is not decidable in first-order logic. That is, the set { φ | φ is a sentence of first-order logic that is satisfiable among finite structures} is undecidable.
Corollary
Let σ be a relational vocabulary with one at least binary relation symbol. The set of σ-sentences valid in all finite structures is not recursively enumerable.
Remarks
This implies that Gödel's completeness theorem fails in the finite since completeness implies recursive enumerability. It follows that there is no recursive function f such that: if φ has a finite model, then it has a model of size at most f(φ). In other words, there is no effective analogue to the Löwenheim–Skolem theorem in the finite.
Intuitive proof
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 there is a corresponding arithmetical sentence , effectively derivable from , such that it is true if and only if halts on the empty tape. Intuitively, asserts "there exists a natural number that is the Gödel code for the computation record of on the empty tape that ends with halting".
If the machine does halt in finite steps, then the complete computation record is also finite, then there is a finite initial segment of the natural numbers such that the arithmetical sentence is also true on this initial segment. Intuitively, this is because in this case, proving requires the arithmetic properties of only finitely many numbers.
If the machine does not halt in finite steps, then is false in any finite model, since there's no finite computation record of that ends with halting.
Thus, if halts, is true in some finite models. If does not halt, is false in all finite models. So, does not halt if and only if is true over all finite models.
The set of machines that does not halt is not recursively enumerable, so the set of valid sentences over finite models is not recursively enumerable.
Alternative proof
In this section we exhibit a more rigorous proof from Libkin. Note in the above statement that the corollary also entails the theorem, and this is the direction we prove here.
Theorem
For every relational vocabulary τ with at least one binary relation symbol, it is undecidable whether a sentence φ of vocabulary τ is finitely satisfiable.
Proof
According to the previous lemma, we can in fact use finitely many binary relation symbols. The idea of the proof is similar to the proof of Fagin's theorem, and we encode Turing machines in first-order logic. 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.
Q is the set of states, Σ is the input alphabet, Δ is the tape alphabet, δ is the transition function, q0 is the initial state, Qa and Qr are the sets of accepting and rejecting states.
Since we are dealing with the problem of halting on an empty input we may assume w.l.o.g. that Δ={ 0,1} and that 0 represents a blank, while 1 represents some tape symbol. We define τ so that we can represent computations:
τ := { <, min, T0 (⋅,⋅), T1 (⋅,⋅), (Hq(⋅,⋅))(q ∈ Q)}
Where: