Finite satisfiability problem for first-order logic

The finite satisfiability problem asks whether a first-order sentence has a finite model. It is computably enumerable because finite structures and their truth relations can be searched effectively.

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.

The finite validity problem asks whether a sentence holds in every finite structure. Its complement is computably enumerable by searching for a finite countermodel, but Trakhtenbrot theorem says that finite validity itself is not computably enumerable.