Validity undecidable in first order logic I am a little confused about the decidablity of validity of first order logic formulas. I have a textbook that seems to have 2 contradictory statements. 
1)Church's theorem: The validity of a first order logic statement is undecidable.
(Which I presume means one cannot prove whether a formula is valid or not)
2)If A is valid then the semantic tableau of not(A) closes. (A is a first order logic statement)
According to me 2 contradicts one since you would then be able to just apply the semantic tableau algorithm on A and prove its validity.
I am sure I am missing something, but what?
 A: First order logic isn't undecidable exactly, but rather often referred to as semidecidable.  A valid first order statement is always provably valid. This is a result of the completeness theorems. For all valid statements, there is a decidable, sound and complete proof calculus.
However, satisfiability is undecidable as a consequence of Church's theorem. If you can solve the Entscheidungsproblem for a first order statement and its negation you have an algorithm for first order satisfiability, but Church's theorem demonstrates that this isn't possible.
Now you can approach this with several sample statements: $\phi$, a valid statement, $\psi$, a statement whose negation is valid, and $\chi$, a statement where neither it nor its negation are valid. Statements $\phi$ and $\psi$ are decidable and provable, with tableau or resolution; we use our proof calculus on $\phi$, $\lnot$$\phi$, $\psi$, and $\lnot$$\psi$ to find out which statements are valid. For invalid statements this doesn't terminate, but we can abandon our search after we find the valid ones.
For statement $\chi$ however there is no algorithm to determine that it isn't valid that is guaranteed to terminate. This is because you can use your proof calculus (pick whatever complete one you want) to determine validity of a statement, or its negation. If neither $\chi$ nor $\lnot$$\chi$ are valid however, your proof calculus for determining validity won't give you any information about validity because it won't terminate.
A: What about if the sentence is not valid? Then the algorithm will not terminate. 
Alternately, for any of the usual proof systems, we can enumerate all sequences of sentences, and check mechanically for each sequence whether it is a proof of $\varphi$. Not very useful if $\varphi$ is not a theorem. 
Remark: We can get something useful out of the idea. Suppose that $T$ is a recursively axiomatized theory which is complete (for any $\varphi$, either $\varphi$ is a theorem of $T$, or $\lnot\varphi$ is a theorem of $T$). Then there is indeed an algorithm that, for any input $\varphi$, will determine whether or not $\varphi$ is a theorem of $T$. 
