Thread: 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

Interesting post! I'm not so sure, though, that if a statement is not a theorem, that it is therefore false, and that its negation is true, and therefore a theorem. What about contingent statements? Simplest case: A implies B. That's not "true" or "false" based on the axioms. Its truth depends on the assignment of truth values to A and B, right? I guess it comes down to this: if a statement has all FALSE's in its truth table, then its negation is TRUE, and therefore a theorem. Or, if a statement has all TRUE's in its truth table, then it's a theorem. But a statement that has some FALSE's and some TRUE's is going to be contingent, and not fit either category.

I think I would argue that it is precisely these contingent wff's that your theorem-checker would hang on, unless it has the capability of deciding that neither one of these statements nor its negation is a theorem.

Those are my thoughts.

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

This is not a valid decision procedure for first-order validity of a sentence, because it is just not true that either a first-order sentence is a "theorem" or its negation is a theorem. There is also the rather large class of first-order sentences that are not theorems and the negations of which aren't theorems either.
If you feed your decision procedure TC2 such a first-order sentence , it will never halt (because neither nor is a theorem) and you will never be in a position to tell whether it is going to halt at some future time or not.

Originally Posted by Ackbeet

I think I would argue that it is precisely these contingent wff's that your theorem-checker would hang on, unless it has the capability of deciding that neither one of these statements nor its negation is a theorem.

I'm sorry to have basically just duplicated your post: I didn't know you were already in the process of supplying an answer.
To make good for this I would like to point out that R.M.Smullyan, in his book "First-Order Logic", page 63, tells us a little more precisely that:

The real 'mystery class' consists of those formulas which are neither unsatisfiable nor satisfiabe in any finite domain.

I think one might call such formulas (possible) "axioms of infinity".
Smullyan comes to this conclusion by intepreting the system of "natural deduction" (tableau system) for first-order logic. Proving a first-order formula valid in a tableau system amounts to proving that any attempt at constructing a model of the negation of that formula fails.
So Smullyan's "mystery class" consists of all those formulas the negation of which has only an infinite model. The tablau method could be said to deliver such a model, if one exists (thus proving the formula invalid), but, sadly, it takes an infinite number of steps to construct an infinite model...

Of course I missed the distinction between contingent and necessary truth! Thanks a lot, now it's clear which passage in my meta "demonstration" is wrong: it is the following:

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

the error obviously (but on ly now it's obvious to me, thanks to your hints!) lies in the passage from not-valid to LOGICALLY FALSE.

Intuitively, I think the problem is, when you talk about logic you don't talk about a formal system wich is intepreted in a fixed model, so you forget that in FOL not every sentence is simply true or false, but that can be true in a possible world and false in another. While when talking about let's say, arithmetic, you talk about an intepreted system for which every statement is either true or false, and being not true means being false. In logic, when you say it's a validity you don't simply say it's true, but that it's true in every possible interpretation. Anyway, such questions always confuse me a bit. For example: decidability
Is the definition I cited correct? It was this one:

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.

BUT in many textbooks I found a definition that states " for checking if P is or is not a
VALID formula of T". So, it seems the first one is SYNTACTICAL, the second a SEMANTIC requirement. Accfording to yuo, which is the standard meaning of "decidable theory"? Which it seems to this is the same as asking "what do we mean with 'theory', the set of all derivations from the aìxioms (syntax) or the set of all logical consequences (semantics)?" What is your opinion?

Moreover, can anybody of you please clarify the distinction between syntactic an semantic completeness? I found many definitions of them, not always clear. Is this distinction related in a way to the distinction between the two definition of decidability I mentioned above?

Thanks a lot

Luca Rivelli, graduating student in Philosophy, Universita' di Padova, Italy

According to Hunter's Metalogic, page 116, there are several ways you might define syntactic completeness. One is this:

A formal system is [syntactically] complete iff for each formula (of the language of the system) either or is a theorem of .

FOL is not complete in this sense. Another way you might define syntactic completeness is as follows:

A formal system is syntactically complete (in one sense) iff no unprovable schema can be added to it as an axiom-schema without inconsistency.

In this sense, Hunter's 'PS' system is syntactically complete. I think you could also prove that FOL is complete in this way.

As for semantic completeness, Hunter defines it this way:

A formal system with language is complete with respect to the class of all truth-functional tautologies iff (1) is adequate for the expression of any truth function and (2) every tautology of is a theorem of .

Semantics has more to do with the interpretation of a formal system, and syntactics more to do with the formal structure of the language itself without regard to its interpretation.

I haven't studied decidability very much at all, so I'm afraid I can't be more help than this.

Originally Posted by lukee

Of course I missed the distinction between contingent and necessary truth! Thanks a lot, now it's clear which passage in my meta "demonstration" is wrong: it is the following:

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

the error obviously (but on ly now it's obvious to me, thanks to your hints!) lies in the passage from not-valid to LOGICALLY FALSE.

So, in a way, you have mixed up syntactic completeness (that either A or not A is valid/derivable) and semantic completeness for first-order logic. First-order logic cannot be syntactically complete: but that's not a shortcoming of it at all.
But if you have a first-order theory that aims at formally describing a single model with the utmost precision, you'd expect it to be syntactically complete. However, Gödel also showed that any first-order theory that contains a formalization of number theory cannot be syntactically complete - dven though we would expect a statement about natural numbers to be either true of false.

Is the definition I cited correct? It was this one:

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.

Seems about ok to me. (Although, if I wanted to be really pedantic I could complain that the quantifier "exist" for the mechanical procedure needs to be moved one level up: you must have the mechanical procedure before you have chosen the statement P, of course.)

BUT in many textbooks I found a definition that states " for checking if P is or is not a
VALID formula of T".

Since the theorems of T can be enumerated it suffices to require that the non-theorems of T can also be enumerated: in that case you can run a decision procedure that is roughly analogous to your TC2: you run both enumeration procedures alternatingly. The theorem to be checked will necessarily occur in one of the two enumations after a finite number of steps.

So, it seems the first one is SYNTACTICAL, the second a SEMANTIC requirement.

Um, I have to think some more about that.

Accfording to you, which is the standard meaning of "decidable theory"?

As I wrote: there is no deep difference between these two definitions, they are equivalent.

Which it seems to this is the same as asking "what do we mean with 'theory', the set of all derivations from the aìxioms (syntax) or the set of all logical consequences (semantics)?" What is your opinion?

We are talking about first-order theories, right? This means your theory consists of axioms + the rules of first-order logic. Without the rules of first-order logic, you would not even get off the ground. You could not derive anything. The rules of derivation are essentially the rules of first-order logic.
Hence, in the first-order case there is no difference between formal derivability of a formula and it's being implied (in the first-order sense) logically by the "axioms". This is because of the (semantic) completeness of first-order logic.

Moreover, can anybody of you please clarify the distinction between syntactic an semantic completeness? I found many definitions of them, not always clear. Is this distinction related in a way to the distinction between the two definition of decidability I mentioned above?

See Akbeet's post and perhaps also Wikipedia: Completeness - Wikipedia, the free encyclopedia

Failure, you said:

>Hence, in the first-order case there is no difference between formal derivability of a >formula and it's being implied (in the first-order sense) logically by the "axioms". This >is because of the (semantic) completeness of first-order logic.

Yes, this true, but only in the case of FOL, NOT in other more "powerful" but still first-order systems, like arithmetics, where Goedel incompleteness theorem holds. In such a system, if we assume the system consistent, we must agree that the goedelian statement G is not derivable in the system, otherwise the system would be inconsistent (for it would permit the derivation of a false statement, G of course) . So, having decided G is not derivable, it shows itself as true, for it "says" exactly that. And, for that reason G IS a (semantic) logic consequence of the system's axioms (for it could never be the case that G is false when the axioms are all true, given it is not dependent from the axioms). In this case there IS a difference between formal derivability of a formula and its being implied logically by the axioms. STILL we are in a first-order theory (given that the axiom of induction is stated as a schema for infinite substitutions of its meta-variables with predicates). I think we could say that Goedel with the incompleteness theorem showed that arithmetic is SEMANTICALLY incomplete, while FOL alone is only SYNTACTICALLY incomplete (If I've correctly understood Hunter's Metalogic definitions cited above by Ackbeet).

What do you think?
Cheers

Luca Rivelli, graduating student in Philosophy, Universita' di Padova, Italy

Thanks a lot I have that book from my faculty library but I still have to read it. It seems to be very good, though, so are your citations and comments, Ackbeet.

Originally Posted by lukee

Failure, you said:

>Hence, in the first-order case there is no difference between formal derivability of a >formula and it's being implied (in the first-order sense) logically by the "axioms". This >is because of the (semantic) completeness of first-order logic.

Yes, this true, but only in the case of FOL, NOT in other more "powerful" but still first-order systems, like arithmetics, where Goedel incompleteness theorem holds.

I think it is a serious mistake to think of a first-order theory of arithmetic as having a first-order interpretation (aka. semantics). This is because the axiom of induction is really a second-order statement: for all A {[if A(0) and for all n: A(n) implies A(n+1)] implies [for all n A(n)]}.

Here, the quantifier for all A is really second-order. Goedel's completeness theorem for first-order logic still means that all first-order consequences of the axioms can be derived. But those are not all consequences of the axioms plus the second-order axiom of induction.

In such a system, if we assume the system consistent, we must agree that the goedelian statement G is not derivable in the system, otherwise the system would be inconsistent (for it would permit the derivation of a false statement, G of course) . So, having decided G is not derivable, it shows itself as true, for it "says" exactly that. And, for that reason G IS a (semantic) logic consequence of the system's axioms (for it could never be the case that G is false when the axioms are all true, given it is not dependent from the axioms).

I think G is not a first-order consequence of the axioms: it is the second-order nature of the induction axiom that makes simply drawing all first-order consequences insufficient.

I think we could say that Goedel with the incompleteness theorem showed that arithmetic is SEMANTICALLY incomplete, while FOL alone is only SYNTACTICALLY incomplete.

No, I think that's quite mistaken: a first-order axiomatization of arithmetic is syntactically incomplete, because, as Goedel showed, there exist statements G of that first-order arithmetic that are neither provable (G) nor disprovable (not G) in it. That's, by definition, a case of a theory being syntactically incomplete, as I wrote earlier.

Since arithmetic is thought of as a particular object (model), one would expect a theory of it, in the ideal case, to be syntactically complete, because we (or, to be more exact, classical mathematics) assume that any statement of arithmetic must be either true or false.

Originally Posted by Failure

I think it is a serious mistake to think of a first-order theory of arithmetic as having a first-order interpretation (aka. semantics). This is because the axiom of induction is really a second-order statement: for all A {[if A(0) and for all n: A(n) implies A(n+1)] implies [for all n A(n)]}.

Yes, if you state the axiom as something quantified over predicates, then it is second-order. But in the post above I posed the condition that the axiom of induction is stated as a schema for infinite substitutions of its meta-variables with predicates: i mean some axiom SCHEME of the form:

1) for all A {[if alpha[x/0] and for all x: alpha[x] implies alpha[x+1]] implies [for all x alpha[x]]}.

where alpha stands for any wff with a free variable, so in other words stands for a predicate, which we can substitute (this is a metalanguage operation) in 1) to obtain a single new FIRST-ORDER axiom for each substitution. The trick works by avoiding to operate this susbstitution as the "content" of a second-order variable like the A you used in your post, to obtain a similar result by "meta-substituting" the string "alpha" with any wff, i.e., ideally re-writing the scheme 1) as a (countable) list of axioms, for example:

a) for all A {[if Even(2*0) and for all x: Even(2*x) implies Even(2*(x+1))] implies [for all x Even(2*x)]}.

or

b) for all A {[if (2*(0+2)<=(0+2)*(0+2)( and for all x: (2*(x+2)<=(x+2)*(x+2)) implies (2*(x+2+1)<=(x+2+1)*(x+2+1))] implies [for all x (2*(x+2)<=(x+2)*(x+2))}

and so on...

where a) and b) are first-order axioms obtained by substituting alpha in 1) with a wff of arithmetic with a free variable. The same solution is explained in the Wikipedia entry on "Peano arithmetic", at the section "First-order theory of arithmetic"

In this way, which is a workaround found also in many textbooks, we can AVOID going to second order while defining arithmetic. So it seems Goedel incompleteness theorem holds for first-order systems too (to be honest, many Goedel theorem explainations I found state that we operate at first order when demonstrating it).

Originally Posted by Failure

No, I think that's quite mistaken: a first-order axiomatization of arithmetic is syntactically incomplete, because, as Goedel showed, there exist statements G of that first-order arithmetic that are neither provable (G) nor disprovable (not G) in it. That's, by definition, a case of a theory being syntactically incomplete, as I wrote earlier.

Yes, of course, I think I simply wrote a dubious statement when I wrote "I think we could say that Goedel with the incompleteness theorem showed that arithmetic is SEMANTICALLY incomplete, while FOL alone is only SYNTACTICALLY incomplete".

What I really meant is: FOL is consistent, SYNTACTICALLY incomplete (which, as you stated, means that there exist statements of that language that are neither provable nor disprovable in the deductive system of FOL, such as the contingently true statements), it is semidecidable and has no other limitation. In fact, it is SEMANTICALLY complete, for it is demonstrated that every logical validity is a theorem of FOL.
On the other hand, arithmetic, seen as a first-order theory (which is feasible with the axiom scheme workaround I cited above), inherits all limitation of FOL (syntactic incompleteness and semi-decidability) but it is ALSO (if it is consistent) SEMANTICALLY incomplete, and this come from Goedel incompleteness theorem. In fact, the sentence G shows exactly the two kinds of incompleteness: on the syntactic front, it shows up as being neither provable nor disprovable; on the semantic front, if we decide the system must be consistent, G it shows up a logical consequence of the axioms (being independent of them, it is obviously a logical consequence of them, for every true statement is entailed by anything). So we have a logical validity that is not provable in the system, hence the semantic incompleteness (by definition).

Originally Posted by Failure

Since arithmetic is thought of as a particular object (model), one would expect a theory of it, in the ideal case, to be syntactically complete, because we (or, to be more exact, classical mathematics) assume that any statement of arithmetic must be either true or false.

Well, of course this is exactly where Goedel beats classical mathematics expectations, by showing there are statements of arithmetic that can't be proved nor disproved in it. But this is different from being true or false, for the not-povable G shows up being true anyway.

Originally Posted by lukee

Yes, if you state the axiom as something quantified over predicates, then it is second-order. But in the post above I posed the condition that the axiom of induction is stated as a schema for infinite substitutions of its meta-variables with predicates: i mean some axiom SCHEME of the form:

1) for all A {[if alpha[x/0] and for all x: alpha[x] implies alpha[x+1]] implies [for all x alpha[x]]}.

where alpha stands for any wff with a free variable, so in other words stands for a predicate, which we can substitute (this is a metalanguage operation) in 1) to obtain a single new FIRST-ORDER axiom for each substitution. The trick works by avoiding to operate this susbstitution as the "content" of a second-order variable like the A you used in your post, to obtain a similar result by "meta-substituting" the string "alpha" with any wff, i.e., ideally re-writing the scheme 1) as a (countable) list of axioms

Yes, of course: and that just creates the problem I was hinting at. It is this difference between what an axiom schema like this can capture and what a full second order interpretation of the axiom of induction "means" that creates an opening through which Goedel can slip through his incompleteness argument.

I wanted to say that a "semantic" interpetation of the axiom of induction is second order, but, of course, I agree that a true first-order axiomatization of it is not - cannot be.

And why don't we just use a second-order formalization of number theory? - Well, because second-order logic is just the thing we, collectively, cannot wrap our heads around.

Well, of course this is exactly where Goedel beats classical mathematics expectations, by showing there are statements of arithmetic that can't be proved nor disproved in it. But this is different from being true or false, for the not-povable G shows up being true anyway.

Now comes the really bad thing about Goedel's incompleteness result: suppose you know (for whatever reason) that a given first-order axiomatization A of number theory is consistent. Then, via Goedelization of A, we can find a first-order statement G, which neither itself nor its negation is provable in A.
Which of the two statements, G or not G, is now "true" and which is "false" for the "One And Only True Number Theory" you have in mind? - You don't want to claim that both, G and not G, are true, do you. And you don't want to claim that neither of them is true, agreed?

Note that both extensions of the original first-order axiomatization that you get by adding G or not G as a new axiom are consistent. Note too, that the "truth" of G is only a truth of it when interpreted via Goedelization of the original axiomatization. It is not, just because of this, true as a first-order statement about numbers in your "One And Only True Number Theory".