How can first-order logic be at the same time complete and only semi-decidable?
Hi, I'm new to this forum. I have a doubt about completeness and decidability in First-order logic that I cannot solve: how is it possible for first-order logic to be at the same time complete and only semi-decidable? Let me explain.
In 1930 Kurt Goedel demonstrated the completeness of first-order logic (I mean FOL: logic with predicates and quantifiers):
1) if a sentence A of FOL is valid, i.e. it is a logical consequence of the axioms, (that is it cannot be false while the axioms are true, and this is a semantical concept), then A is a theorem, i.e. it is (syntactically, mechanically) derivable in the language of FOL from the axioms.
The converse, that
2) every theorem is valid
comes from the already demonstrated soundness of FOL.
so, 1) and 2) together allow us to say that, at least in FOL, the concept of validity (so that of truth) and that of being derivable have the same extensionality: in other words, every true statement of FOL is a theorem of it and vice-versa (this does not hold for arithmetic, where for Goedel incopleteness theorem, 1931, if arithmetic is sound, there ARE true statements that are NOT theorems).
BUT, it is also demonstrated that FOL is not decidable, that it is only semi-decidable:
3) DEF.: A theory T is semi-decidable if, given a statement P in the language of the theory, it does exist a general mechanical procedure (let's call it Theorem Checker, with argument A TC(P)) for determining if P is a theorem, that outputs a positive answer in a finite time if P is actually a theorem, but does not halt at all if P is not a theorem.
Let's give the definition of decidability for a theory also:
4) DEF.: A theory T is decidable iff given a statement P in the language of the theory, it does exist a general mechanical procedure that always ends in a finite time for checking if P is or is not a theorem of T.
From the known semi-decidability (3) of FOL, given a statement A expressed in the language of FOL, it follows that if A is a theorem of FOL, then a mechanical theorem checker TC(A) will certainly halt after a finite amount of time. But that if A is not a theorem, TC(A) will NEVER halt.
Now, if A is NOT a theorem, then from the completeness of FOL (1), it follows that A is not valid, i.e. it is false. So, not-A is true, i.e. it is valid. But then again, from the completeness of FOL it follows that not-A is a theorem. So, we know that a procedure TC(not-a ) for checking if not-A is a theorem WILL halt, eventually, saying it is a theorem.
SO, given a generic A, of which we don't know it is a theorem or not, we could build a mechanical procedure TC2(A) ALTERNATING at each step TC(A) and TC(not-A), knowing that, being either A or (not-A) a theorem, TC2(A) WILL stop in a finite time (TC2 a is built with the condition that, as soon as one of its subroutines TC(a) or TC(not-a) halts, so does the entire TC2 procedure).
So, given the definition of decidability (4) and the always-ending procedure TC2 described above, (which relies on the completeness of FOL (1)) we can now say FOL IS decidable!
SO, it seems that if FOL is complete, then it IS DECIDABLE. How come than that there is a well known demonstration (involving the halting problem for a Turing machine) that it is NOT?!?! (i.e. that it is only semi-decidable)?
Sorry for the long and complex post, but I had to explain the question carefully. I hope some of you can shed some light on this (for me) paradox.
Thanks a lot