Originally Posted by

**lukee** 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).