= Solution
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. Then
$$
\sigma_{P,w}\text{ has a finite model}
\quad\Longleftrightarrow\quad
P\text{ halts on }w.
$$
A 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>.
Back to article page
