First order logic: Soundness, Completeness, Decidability

**asdf60** · Dec13-05, 12:16 PM

So I'm a bit confused about these metatheorems about first order logic, partly because I haven't read any of the real proofs, but I just want to know the results for right now. Here is what I understand:

Soundness means that any derivation from the axioms and inference rules is still valid. As I understand, first order logic is sound.

Completeness means that any formula that is valid can be proven from the axioms. Once again, FOL is complete.

Now comes the confusing part. Godel's Incompleteness and Undecidability.
So godel's incompleteness theorem says that in a first order language with a model/interpretation defined sufficient to talk about mathematics, there exists truths that are not provable through the axioms. How does this not contradict the Completeness of FOL discussed above? Is it because the the completeness of FOL talks about truths that are valid for ANY model, while Godel's Incompleteness talks about truths that are valid in a more specific class of models?

Also, undecidability. What exactly does this mean? And how does it not contradict the completeness of FOL. If a formula can not be proven, then completeness assures us that the formula must be false. So what is the undecidability.

Thanks,

ASDF

**master_coda** · Dec13-05, 12:51 PM

Completeness of FOL basically says that if something is provable in every model of a first-order theory, then it is provable from the axioms of the theory.

Meanwhile, completeness of a FO theory says that every statement in the theory can be either proved or disproved.

So you can see that we're really looking at two different kinds of completeness. If something is true in some models of a theory but false in others, then the completeness of FOL tells us nothing (although soundness tells us that if something is true in some models and false in others, then it can't be proven true or false in the theory).

As for decidability, it's really a separate thing. Decidability talks about if there exists an algorithmic way to decide if statements in a theory are true or false; obviously, if a theory is decidable then it is complete. On the other hand, just because a theory is complete, there's no reason to assume that there's a mechanical way to determine if statements in the theory are true.

Also, completeness does not tell us that if we cannot prove something then it must be false; the whole point of incompleteness is that we can't prove something is true OR false.

**VazScep** · Dec13-05, 02:01 PM

Originally Posted by asdf60

So I'm a bit confused about these metatheorems about first order logic, partly because I haven't read any of the real proofs, but I just want to know the results for right now. Here is what I understand:
Soundness means that any derivation from the axioms and inference rules is still valid. As I understand, first order logic is sound.
Completeness means that any formula that is valid can be proven from the axioms. Once again, FOL is complete.
Now comes the confusing part. Godel's Incompleteness and Undecidability.
So godel's incompleteness theorem says that in a first order language with a model/interpretation defined sufficient to talk about mathematics, there exists truths that are not provable through the axioms.

Godel's Incompleteness Theorem is better stated without any reference to models or truth -- it's a purely syntactic result. For any consistent theory with a recursive set of axioms that can prove a sufficient amount of arithmetic, there is a statement which cannot be proved nor disproved in that theory.

How does this not contradict the Completeness of FOL discussed above? Is it because the the completeness of FOL talks about truths that are valid for ANY model, while Godel's Incompleteness talks about truths that are valid in a more specific class of models?

As master_coda points out, there are two kinds of "completeness" being discussed here. The sort of "completeness" we are thinking of with regards to FOL is a semantic property: Every statement true in all interpretations is provable in FOL. The sort of "completeness" we are thinking of with regards to the Incompleteness Theorems is syntactic completeness: A theory

is complete if, for any statement $LaTeX Code: \\phi$ , at least one of $LaTeX Code: \\phi$ and $LaTeX Code: \\neg\\phi$ is provable. In this latter sense, FOL is trivially incomplete. For instance, it cannot prove that

nor $LaTeX Code: \\neg1+1=2$ .

Also, undecidability. What exactly does this mean? And how does it not contradict the completeness of FOL. If a formula can not be proven, then completeness assures us that the formula must be false. So what is the undecidability.
Thanks,
ASDF

"Undecidability" also has two meanings. A statement is undecidable in a theory if it is neither provable nor disprovable in that theory. A theory is (effectively) decidable if there is an algorithm to determine whether a given statement belongs to that theory.

**VazScep** · Dec13-05, 02:52 PM

Originally Posted by master_coda

As for decidability, it's really a separate thing. Decidability talks about if there exists an algorithmic way to decide if statements in a theory are true or false;

More accurately, whether they are provable or not. Truth and provability should not be confused.

obviously, if a theory is decidable then it is complete.

Why do you think this?

On the other hand, just because a theory is complete, there's no reason to assume that there's a mechanical way to determine if statements in the theory are true.

But if it is complete and has a recursive set of axioms, then it will always be decidable.

**AKG** · Dec13-05, 03:15 PM

Originally Posted by asdf60

So I'm a bit confused about these metatheorems about first order logic, partly because I haven't read any of the real proofs, but I just want to know the results for right now. Here is what I understand:
Soundness means that any derivation from the axioms and inference rules is still valid. As I understand, first order logic is sound.

Completeness means that any formula that is valid can be proven from the axioms. Once again, FOL is complete.

Now comes the confusing part. Godel's Incompleteness and Undecidability.
So godel's incompleteness theorem says that in a first order language with a model/interpretation defined sufficient to talk about mathematics, there exists truths that are not provable through the axioms. How does this not contradict the Completeness of FOL discussed above? Is it because the the completeness of FOL talks about truths that are valid for ANY model, while Godel's Incompleteness talks about truths that are valid in a more specific class of models?

Yes. The version of Godel's First Incompleteness Theorem I know says that there are sentences which are true in the standard model of number theory, but not provable from just the logical axioms*. The completeness theorem states that sentences which are true in every model of your FOL are provable from just those logical axioms. There's no contradiction here, all it means is that those sentences which are true in the standard model of number theory but aren't provable from just the logical axioms* are not true in every model of number theory. By "model of number theory" I mean an L-structure, where L is the first order language of number theory (it is your basic FOL, together with a constant symbol 0, three function symbols +, x, ^, and a relation symbol <).

* Of course, the Incompleteness Theorem says more than that there is some true sentence (in the standard model) unprovable from just the logical axioms, it says that even if you add N to the logical axioms, where N is a consistent, recursive (I believe 'recursive' and 'decidable' are synonymous in this context) set of axioms, there are still true sentences (in the s.m.) that are unprovable from the logical axioms + N.

Also, undecidability. What exactly does this mean? And how does it not contradict the completeness of FOL. If a formula can not be proven, then completeness assures us that the formula must be false. So what is the undecidability.

Suppose, for your set of axioms N, you chose all true sentences of the standard model. Then certainly, every true sentence would be provable from N, but the set N is no longer decidable, i.e. there is no algorithm that can determine whether an arbitrary sentence is in N or not. Basically, once you add enough axioms to N such that N is now powerful enough to prove every fact of number theory, N becomes undecidable, meaning that there's no algorithm that can tell whether a given sentence is in N or not.

**VazScep** · Dec13-05, 03:31 PM

Originally Posted by AKG

* Of course, the Incompleteness Theorem says more than that there is some true sentence (in the standard model) unprovable from just the logical axioms, it says that even if you add N to the logical axioms, where N is a consistent, recursive (I believe 'recursive' and 'decidable' are synonymous in this context)

They are equivalent assuming the Church-Turing Thesis. Decidable sets are those for which there is an algorithm which determines whether an object belongs to that set or not. Recursive sets are a mathematical formalisation of this idea.

set of axioms, there are still true sentences (in the s.m.) that are unprovable from the logical axioms + N.

For the Incompleteness Theorem to apply, N also has to prove a sufficient amount of arithmetic (it must prove enough statements true in the standard model).

**master_coda** · Dec13-05, 07:30 PM

Originally Posted by VazScep

More accurately, whether they are provable or not. Truth and provability should not be confused.

I can't think of any useful mathematical meaning of the word "truth" other than "provable from the axioms". That said, I would be more than happy to never again have to use the word "truth" in mathematics. If only everybody else would stop using it...

Originally Posted by VazScep

Why do you think this?

If I can algorithmically determine whether or not every sentance in the theory is true or false, that's a pretty clear indication that the theory is complete. In fact, I think that's a standard way to prove that a theory is complete - by provding an algorithm for determining if a statement is true or false.

Originally Posted by VazScep

But if it is complete and has a recursive set of axioms, then it will always be decidable.

Really? I'm not sure. It's not that I don't agree with you, it's just that it doesn't seem obvious to me.

**Hurkyl** · Dec13-05, 07:49 PM

I can't think of any useful mathematical meaning of the word "truth" other than "provable from the axioms".

(disclaimer: I often use a similar but wrong word in logical contexts! I really need to make myself a dictionary for this, but anyways...)

A truth valuation v is a function from the set of propositions to a set of truth values that satisfies a certain collection of properties, such as:

If P is an axiom of the theory under consideration, then v(P) is true.
If v(P) = true and v(Q) = false, then v(P or Q) = true.

And so on.

**Hurkyl** · Dec13-05, 07:53 PM

Really? I'm not sure. It's not that I don't agree with you, it's just that it doesn't seem obvious to me.

It's a dumb algorithm, but it works. Suppose you want to decide a proposition P...

There are countably many symbols in your alphabet. Therefore, you can enumerate all strings of symbols.

For each string of symbols:
::: If this string of symbols is a proof of P, accept P.
::: If this string of symbols is a proof of ~P, reject P

There exists either a proof of P or a proof of ~P, so this algorithm terminates, and thus decides the theory.

**master_coda** · Dec13-05, 08:21 PM

Originally Posted by Hurkyl

It's a dumb algorithm, but it works. Suppose you want to decide a proposition P...
There are countably many symbols in your alphabet. Therefore, you can enumerate all strings of symbols.
For each string of symbols:
::: If this string of symbols is a proof of P, accept P.
::: If this string of symbols is a proof of ~P, reject P
There exists either a proof of P or a proof of ~P, so this algorithm terminates, and thus decides the theory.

Hmm, I should have been able to think of that. Still, this does assume that you can algorithmically determine if a string of symbols is a proof of P; is it true that you can always do that?

**Hurkyl** · Dec13-05, 08:28 PM

Sure. You can even download one.

(It's important for this algorithm you're able to decide whether a statement P is one of the axioms. I think I can tweak it to work in the case where you are merely able to recognize if P is an axiom)

**master_coda** · Dec13-05, 08:38 PM

Originally Posted by Hurkyl

Sure. You can even download one.
(It's important for this algorithm you're able to decide whether a statement P is one of the axioms. I think I can tweak it to work in the case where you are merely able to recognize if P is an axiom)

But does that only work for first-order logic? I'm would expect that you can do that sort of thing for FOL given how "nice" it is. I'm not so sure about what happens when you move to something like second-order logic.

**VazScep** · Dec13-05, 08:46 PM

Originally Posted by master_coda

I can't think of any useful mathematical meaning of the word "truth" other than "provable from the axioms". That said, I would be more than happy to never again have to use the word "truth" in mathematics. If only everybody else would stop using it...

In mathematical logic, provability and truth have precise definitions, as Hurkyl indicates above. The two should not be confused. For instance, truth is only defined with respect to some interpretation of a first-order language. There is no general sense of a statement in an arbitrary theory being true or false.

If I can algorithmically determine whether or not every sentance in the theory is true or false, that's a pretty clear indication that the theory is complete. In fact, I think that's a standard way to prove that a theory is complete - by provding an algorithm for determining if a statement is true or false.

Completeness and decidability are syntactic properties of a theory, and not about truth. A theory is complete if, for any statement, it proves that statement or its negation. A theory is decidable if there is an algorithm which determines whether an arbitrary statement belongs to the theory.

Really? I'm not sure. It's not that I don't agree with you, it's just that it doesn't seem obvious to me.

Given a consistent theory with a recursive vocabularly and set of axioms, it is possible to numerically code every possible proof, and then enumerate them. If the theory is complete, then for any sentence $LaTeX Code: \\phi$ , eventually either $LaTeX Code: \\phi$ or $LaTeX Code: \\neg\\phi$ will appear in that enumeration. Hence, by waiting until one of these statements appear, we have an algorithm to determine whether $LaTeX Code: \\phi$ is a theorem or not. Thus, the theory is decidable. If the theory is inconsistent, then it is trivially decidable.

**VazScep** · Dec13-05, 08:54 PM

Originally Posted by master_coda

But does that only work for first-order logic? I'm would expect that you can do that sort of thing for FOL given how "nice" it is. I'm not so sure about what happens when you move to something like second-order logic.

The second-order predicate calculus is incomplete (under standard semantics), so there is no such thing as a consistent second-order recursively axiomatisable theory.

**master_coda** · Dec13-05, 09:00 PM

Originally Posted by VazScep

In mathematical logic, provability and truth have precise definitions, as Hurkyl indicates above. The two should not be confused. For instance, truth is only defined with respect to some interpretation of a first-order language. There is no general sense of a statement in an arbitrary theory being true or false.

Hurkyl's definition of a truth valuation looked an awful lot like "assign P a value of true if P is derivable from the axioms of the theory". In that case, I don't see how "P is true in this theory" and "P is provable from the axioms in this theory" are any different.

Originally Posted by VazScep

Completeness and decidability are syntactic properties of a theory, and not about truth. A theory is complete if, for any statement, it proves that statement or its negation. A theory is decidable if there is an algorithm which determines whether an arbitrary statement belongs to the theory.

How does this contradict my statement that "decidable => complete"? If a theory is not complete, it sure isn't decidable; thus, if a theory is decidable, it must be complete.

**VazScep** · Dec13-05, 09:06 PM

Originally Posted by master_coda

Hurkyl's definition of a truth valuation looked an awful lot like "assign P a value of true if P is derivable from the axioms of the theory". In that case, I don't see how "P is true in this theory" and "P is provable from the axioms in this theory" are any different.

I only said "indicates". If you want to find out the way that truth is defined for interpretations, I can recommend some logic textbooks -- the definitions are quite long-winded.

How does this contradict my statement that "decidable => complete"? If a theory is not complete, it sure isn't decidable; thus, if a theory is decidable, it must be complete.

The monadic predicate calculus (the predicate calculus in a language with only one-place predicates) is decidable but incomplete.