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?
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$.