Trakhtenbrot theorem
= Trakhtenbrot theorem
{c}
{wiki=Trakhtenbrot's_theorem}
The finite satisfiability problem is undecidable, and the set of first-order sentences valid in every finite structure is not computably enumerable. A halting computation can be encoded as a finite ordered tableau satisfying finitely many local first-order constraints; the resulting sentence has a finite model exactly when the computation halts.