Trakhtenbrot's theorem

In logic, finite model theory, and computability theory, Trakhtenbrot's theorem (due to Boris Trakhtenbrot) states that the problem of validity in first-order logic on the class of all finite models is undecidable. In fact, the class of valid sentences over finite models is not recursively enumerable (though it is co-recursively enumerable).

Trakhtenbrot's theorem implies that Gödel's completeness theorem (that is fundamental to first-order logic) does not hold in the finite case. Also it seems counter-intuitive that being valid over all structures is 'easier' than over just the finite ones.

The theorem was first published in 1950: "The Impossibility of an Algorithm for the Decidability Problem on Finite Classes".^[1]

The theorem is related to Church's result that the set of valid formulas in first-order logic is not decidable (however this set is semi-decidable).