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 (FO) 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).

It is considered a very important result, since it implies that the completeness theorem (that is fundamental to FO) 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".^[1]

Mathematical Formulation

We follow the formulations as in ^[2]

Theorem

Finite Satisfiability is not decidable in First-order logic (FO).

Remarks

1. That is, the set { φ | φ is a sentence of FO satisfiable in the finite } is not decidable.

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

1. That is, the set { φ | φ is a sentence of FO[σ] valid in all finite structures } is not recursively enumerable.
2. This implies that Gödel's completeness theorem fails in the finite. (since completeness implies recursive enumerability)
3. 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.

Alternative Proof

In this section we exhibit an alternative proof from Libkin.^[3] 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, Σ, δ, q₀, Q_a, Q_r⟩ 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,
• q₀ is the initial state,
• Q_a and Q_r 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, T₀ (⋅,⋅), T₁ (⋅,⋅), (H_q(⋅,⋅))_{(q ∈ Q)}}

Where:

• < is a linear order and min is a constant symbol for the minimal element with respect to < (our finite domain will be associated with an initial segment of the natural numbers).
• T₀ and T₁ are tape predicates. T_i(s,t) indicates that position s at time t contains i, where i ∈ {0,1}.
• H_q's are head predicates. H_q(s,t) indicates that at time t the machine is in state q, and its head is in position s.

The sentence φ_M states that (i) <, min, T_i's and H_q's are interpreted as above and (ii) that the machine eventually halts. The halting condition is equivalent to saying that H_q∗(s, t) holds for some s, t and q∗ ∈ Q_a ∪ Q_r and after that state, the configuration of the machine does not change. Configurations of a halting machine (the nonhalting is not finite) can be represented as a τ (finite) sentence (more precisely, a finite τ-structure which satisfies the sentence). The sentence φ_M is: φ ≡ α ∧ β ∧ γ ∧ η ∧ ζ ∧ θ.

We break it down by components:

• α states that < is a linear order and that min is its minimal element
• γ defines the initial configuration of M: it is in state q₀, the head is in the first position and the tape contains only zeros: γ ≡ H_q0(min,min) ∧ ∀s T₀ (s, min)
• η states that in every configuration of M, each tape cell contains exactly one element of Δ: ∀s∀t(T₀(s, t) → ¬ T₁(s, t))
• β imposes a basic consistency condition on the predicates H_q's: at any time the machine is in exactly one state:

$\forall t \exists ! s (\bigvee_{q\in Q} H_q (s,t))\land \neg\exists s \exists t (\bigvee_{q,q'\in Q, q\neq q} H_q(s,t)\land H_{q'} (s,t))$

• ζ states that at some point M is in a halting state:

$\exists s \exists t \bigvee_{q\in Q_a\cup Q_r} H_q (s,t)$

• θ consists of a conjunction of sentences stating that T_i's and H_q's are well behaved with respect to the transitions of M. As an example, let δ(q,0)=(q',1, left) meanining that if M is in state q reading 0, then it writes 1, moves the head one position to the left and goes into the state q'. We represent this condition by the disjunction of θ₀ and θ₁:

$\theta_0 \equiv \forall s \forall t (s\neq \underline{min} \land T_0(s,t) \land H_q (s, t)) \to \theta_2$

Where θ₂ is:

$T_1 (s, t+1)\land H_{q'} (s-1, t+1)\land \forall s' (s\neq s' \to (\bigwedge_{i=0,1} T_i (s', t+1)\leftrightarrow T_i(s',t)))$

And:

$\theta_1 \equiv \forall s \forall t (s = \underline{min} \land T_0(s,t) \land H_q (s, t)) \to \theta_3$

Where θ₃ is:

$T_1 (s, t+1)\land H_{q'} (s, t+1)\land \forall s' (s\neq s' \to (\bigwedge_{i=0,1} T_i (s', t+1)\leftrightarrow T_i(s',t)))$

s-1 and t+1 are first order definable abbreviations for the predecessor and successor according to the ordering <. The sentence θ₀ assures that the tape content in position s changes from 0 to 1, the state changes from q to q', the rest of the tape remains the same and that the head moves to s-1 (i. e. one position to the left), assuming s is not the first position in the tape. If it is, then all is handled by θ₁: everything is the same, except the head does not move to the left but stays put.

If φ_M has a finite model, then such a model that represents a computation of M (that starts with the empty tape (i.e. tape containing all zeros) and ends in a halting state). If M halts on the empty input, then the set of all configurations of the halting computations of M (coded with <, T_i's and H_q's) is a model of φ_M, which is finite, since the set of all configurations of halting computations is finite. 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 $\mathcal{A}$ (equivalently, whether φ_M is finitely satisfiable) is also undecidable (recursively enumerable, but not recursive). This concludes the proof.

Corollary

The set of finitely satisfiable sentences is recursively enumerable.

Proof

Enumerate all pairs $(\mathcal{A}, \phi)$ where $\mathcal{A}$ is finite and $\mathcal{A}\models \phi$.

Corollary

For any vocabulary containing at least one binary relation symbol, the set of all finitely valid sentences is not recursively enumerable.

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. Since ¬φ is finitely valid iff φ is not finitely satisfiable, we conclude that the set of sentences which are not finitely satisfiable is recursively enumerable. If both a set A and its complement are recursively enumerable, then A is recursive. It follows that the set of finitely satisfiable sentences is recursive, which contradicts Trakhtenbrot's theorem.

References

1. Trakhtenbrot, Boris (1950). "The Impossibility of an Algorithm for the Decidability Problem on Finite Classes". Proceedings of the USSR Academy of Sciences (in Russian) 70 (4): 569–572.
2. Ebbinghaus, Heinz-Dieter; Flum, Jörg (1995). Finite Model Theory. Springer. ISBN 978-3-540-60149-4.
3. Libkin, Leonid (2010). Elements of Finite Model Theory. Springer. ISBN 978-3-642-05948-3.

• Boolos, Burgess, Jeffrey. Computability and Logic, Cambridge University Press, 2002.
• Simpson, S. "Theorems of Church and Trakhtenbrot". 2001.