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.
New to topics? Read the docs here!