Is Entscheidungsproblem in Co-RE? And Proof if it is. As I study through, I learned that Entscheidungsproblem has a negative answer. Then I came to wonder whether the problem is in Co-RE. If it is, can anyone show me the proof? 
Thanks.
 A: From wikipedia

The Entscheidungsproblem has often been identified in particular with the decision problem for first-order logic (that is, the problem of algorithmically determining whether a first-order statement is universally valid).

The set of universally valid first-order statements is known to be r.e. and not recursive. If it was co-r.e. (by which I mean its complement is r.e.), then it would be recursive. (A set that is both r.e. and co-r.e. is recursive). Hence it is not co-r.e.
A: Suppose $X$ is the set of all first-order statements true in $\mathbb{N}$. You already know that $X$ is uncomputable. Now suppose that $X$ was r.e. or co-r.e., and consider $\{\lnot \varphi : \varphi \in X \}$. What can you deduce?
Edit: It seems that the correct interpretation of "universally valid" implies that we can use Gödel's completeness theorem to recursively enumerate all universally true statements by going through all valid proofs. The incompleteness theorem shows that for some theories there will be statements $\varphi$ such that neither $\varphi$ nor $\lnot \varphi$ show up in this enumeration.
