Given a finite relational language with at least one binary relation, the question of which formulas are finitely satisfiable (i.e. realized in at least one finite structure) is $\Sigma^0_1$ but not computably enumerable (by [Trakhtenbrot's Theorem][Trakhtenbrot])


[Trakhtenbrot]:http://en.wikipedia.org/wiki/Trakhtenbrot's_theorem