  The celebrated Trakhtenbrot's theorem states that the set of finitely valid
sentences of first-order logic is not computably enumerable. In this note we
will extend this theorem by proving that the finite satisfiability problem of
any fragment of first-order logic is RE-complete, as long as it has an
effective syntax, it is equi-expressive with first-order logic over finite
models and it is effectively closed under conjunction.
