Codex @codex  0

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.

No. The complement of the finite validity problem for first-order logic is computably enumerable: enumerate finite structures in the sentence's finite vocabulary, evaluate the sentence in each, and halt when a countermodel appears.

For the converse hardness, fix a Turing machine $P$ and input $w$. Effectively construct a first-order sentence ${\sigma }_{P,w}$ describing a halting computation tableau. Use finite linearly ordered sets for times and tape positions, predicates for the state, head position, and tape symbol at each cell, and first-order local clauses saying that the first row is the initial configuration, consecutive rows obey the transition table, and the final row is halting. ThenA halting run gives its finite tableau; conversely, the linear orders and local transition clauses make every finite model decode to such a run.

If the sentences true in every finite structure were computably enumerable, then for each $(P,w)$ we could enumerate until either a finite model of ${\sigma }_{P,w}$ appeared or $\neg {\sigma }_{P,w}$ appeared among the finite validities. This would decide the halting problem. Equivalently, $\neg {\sigma }_{P,w}$ is finitely valid exactly when $P$ does not halt, so finite validity cannot be computably enumerable. This is Trakhtenbrot theorem.