4

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?

Murdock
  • 223

2 Answers2

3

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.

martinkunev
  • 269
dezakin
  • 2,206
2

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

André Nicolas
  • 507,029
  • Well I am no expert but for invalid formulas we can just use the contrapositve of 2. Which states if not(A) does not close then A is invalid. – Murdock Dec 19 '13 at 07:28
  • It still does not look like you are answering my question. How can both 1 and 2 be true? – Murdock Dec 19 '13 at 07:29
  • 1
    How can we determine whether not$(A)$ does not close? The reason 1 and 2 can both be true is that 2 does not give an algorithm. – André Nicolas Dec 19 '13 at 07:30
  • Well by applying the algorithm for a semantic tableau. As I understand it this is indeed a proof since one can apply it systematically on the formula. And if A is then valid, by definition not(A) WILL close. – Murdock Dec 19 '13 at 07:33
  • 1
    And if it is not valid, then not$(A)$ will not close. An algorithm for validity is a mechanical procedure that (ultimately) halts and says Yes if the input sentence is valid, and halts and says No if the input sentence is not valid. Note that $\varphi$ being not valid is very different from $\lnot\varphi$ being valid. – André Nicolas Dec 19 '13 at 07:37
  • Ah... So let me get this.So obviously a semantic tableau can be invalid and because a invalid statement,A, could potentially have an infinite proof for not(A) we cant just say A is not valid since it might halt after a trillion iterations? – Murdock Dec 19 '13 at 07:40
  • There is no such thing as an infinite proof in first-order logic. And yes, however long we compute, there is no stage at which we can assert that $A$ is not valid. – André Nicolas Dec 19 '13 at 07:45
  • Maybe include this in your answer. Thanx for the help – Murdock Dec 19 '13 at 07:47