Trakhtenbrot's theorem
= Trakhtenbrot's theorem
{c}
{wiki}
= Trakhtenbrot theorem
{c}
{synonym}
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.