Finite validity problem for first-order logic
= 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.