 Finite validity problem for first-order logic

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.