Prev: FORBIDDEN LOGIC IN EINSTEINIANA
Next: How can FOL logic be at the same time complete and only semi-decidable?
From: luca.rivelli on 7 Aug 2010 08:09
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

Luca Rivelli
From: Ken Pledger on 8 Aug 2010 19:09
In article
<6412ba2a-de7d-41d6-bcf3-a98d6764de90(a)t20g2000yqa.googlegroups.com>,
"luca.rivelli(a)gmail.com" <luca.rivelli(a)gmail.com> wrote:

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


No. It's not too hard to think of a formula A such that neither A
nor not-A is a theorem. Semantically, some assignments to the variables
will make A come out true, and some won't. Perhaps you're not quite
clear about the word "valid".

Ken Pledger.
 | 
Pages: 1
Prev: FORBIDDEN LOGIC IN EINSTEINIANA
Next: How can FOL logic be at the same time complete and only semi-decidable?