First order logic: Soundness, Completeness, Decidability

In summary, the completeness of first order logic says that every statement in the theory can be either proved or disproved. The soundness of first order logic means that any derivation from the axioms and inference rules is still valid. Finally, godel's incompleteness theorem states 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. This does not contradict the completeness of FOL, as the completeness of FOL talks about truths that are valid for ANY model. Undecidability is a separate thing which states that a statement is undecidable in a theory if it is neither provable nor dis
  • #1
asdf60
81
0
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
 
Physics news on Phys.org
  • #2
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.
 
  • #3
asdf60 said:
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 [itex]T[/itex] is complete if, for any statement [itex]\phi[/itex], at least one of [itex]\phi[/itex] and [itex]\neg\phi[/itex] is provable. In this latter sense, FOL is trivially incomplete. For instance, it cannot prove that [itex]1+1=2[/itex] nor [itex]\neg1+1=2[/itex].

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.
 
Last edited:
  • #4
master_coda said:
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.
 
  • #5
asdf60 said:
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.
 
  • #6
AKG said:
* 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).
 
  • #7
VazScep said:
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...

VazScep said:
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.

VazScep said:
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.
 
  • #8
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.
 
Last edited:
  • #9
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.
 
Last edited:
  • #10
Hurkyl said:
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?
 
  • #11
Sure. You can even download one. :smile:

(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)
 
  • #12
Hurkyl said:
Sure. You can even download one. :smile:
(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.
 
  • #13
master_coda said:
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 [itex]\phi[/itex], eventually either [itex]\phi[/itex] or [itex]\neg\phi[/itex] will appear in that enumeration. Hence, by waiting until one of these statements appear, we have an algorithm to determine whether [itex]\phi[/itex] is a theorem or not. Thus, the theory is decidable. If the theory is inconsistent, then it is trivially decidable.
 
Last edited:
  • #14
master_coda said:
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.
 
  • #15
VazScep said:
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.

VazScep said:
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.
 
  • #16
master_coda said:
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.
 
  • #17
VazScep said:
The second-order predicate calculus is incomplete (under standard semantics), so there is no such thing as a consistent second-order recursively axiomatisable theory.

That's a very good point, of course. I'm not too familar with the middle ground between first-order logic and second-order logic, or else I would've tried to pick something between the two.
 
  • #18
VazScep said:
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.

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

Well, I'll take your word for it then. I am not a logician, it's entirely possible that I may be talking out of my ass without even knowing it. Fortunately, this is not my day job.
 
  • #19
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.
You do have this theorem:

If a statement P is true in every model of a (first-order) theory, then P can be proven from the axioms.
 
  • #20
VazScep said:
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).
Why? If a system that is strong enough to prove certain arithmetic facts still can't prove all true statements, then certainly a weaker system that can't even prove those arithmetic facts can't prove all true statements. The proof of the theorem requires that N proves certain arithmetic facts, but once we have the theorem, then it follows that weaker axioms (that can't even prove basic arithmetic facts) will also be incomplete.
 
  • #21
If a system that is strong enough to prove certain arithmetic facts still can't prove all true statements, then certainly a weaker system that can't even prove those arithmetic facts can't prove all true statements.
Sure, there will be statements the weaker system cannot prove.

However, the weaker system will not even be able to say those statements. :tongue2:


The great example (IMHO) is the theory of real closed fields. It is logically complete, despite the fact any real closed field is a ring containing the integers!

The resolution of this pseudoparadox is that while any real closed field contains the integers, the theory of real closed fields has no way of actually talking about integers.

This fact has an algebraic interpretation: any polynomial that is zero at every integer must, in fact, be zero everywhere. Thus, there is no algebraic expression capable of identifying the integers.

So while you can ask if an equation has a solution, you cannot ask if an equation is an integer solution.
 
  • #22
master_coda said:
Well, I'll take your word for it then. I am not a logician, it's entirely possible that I may be talking out of my ass without even knowing it. Fortunately, this is not my day job.
Just to correct something Hurkyl wrote earlier, truth is not defined with respect to any set of axioms or any theory. It is defined with respect to an interpretation of a formal language. For instance, suppose the given formal language consists of the predicate symbol [itex]p[/itex] and the constant symbol [itex]c[/itex]. An interpretation of this language is a set of objects, called the domain, an assignment of a one-place relation [itex]R[/itex] to the symbol [itex]p[/itex], and an assignment of an object in the domain [itex]C[/itex] to the symbol [itex]c[/itex]. An atomic formula like [itex]p(c)[/itex] will then be defined to be true for this interpretation if and only if [itex]C\in R[/itex].

Obviously, a lot more work is needed to define truth for a general formula in the language, but the point is that all this is done without reference to axioms or particular theories. And you should be able to see from this that provability and truth are distinct concepts. For instance, in the theory with only logical axioms (the predicate calculus) [itex]p(c)[/itex] is unprovable, but in any interpretation of the language, it will have a definite truth value.
 
  • #23
I don't understand much of what all of you said, but it seems that my book says that the key to the difference between undecidability, is that while we can prove any formula that we KNOW to be valid (that is to say, the formula is logically true- in every interpretation), we can not know where a given formula is valid in a FINITE number of steps. If we try constructing a proof via top-down derivation or deductive systems, we aren't guarenteed a counter example, so we never know if the proof is just about to come around the corner.

For example, propositional logic is decidable, because it will be at most 2^n tests for each formula containing n variables.

Is this right in anyway?
 
  • #24
I think I'm convincing myself more and more that undecidability deals with a formula in a specific interpretation, it doesn't deal with logically true statements. This seems to me very reasonable. If I had an infinite universe of discourse, and formula making some existential claim, then it seems reasonable that it would be impossible to either produce a counterexample or a proof. And completeness, in this case, does not guarantee that a proof should exist, since the formula is not a logical truth.
 
  • #25
Unless you're using "decidability" to mean something else, it has nothing to do with truth or interpretations. A set of axioms is decidable iff there is an ideal computer with an algorithm that can decide whether a given formula is in the set or not in the set. This has nothing to do with whether the formulas are true, or true in a given interpretation, or whether or not they are provable, etc.
 
  • #26
You're right. My book is very misleading. Thanks for the help.
 
  • #27
asdf60 said:
You're right. My book is very misleading. Thanks for the help.
Generally, a set is decidable if there is an algorithm to determine whether an object belongs to that set or not. A theory is a set of formulas, so we can say that a theory is decidable if there is an algorithm to determine whether a formula belongs to that theory or not. We can also say that a set of axioms is decidable if there is an algorithm to determine whether a given formula belongs to that set.

Another meaning of decidable applies to formulas: A formula [itex]\phi[/itex] is decidable for a theory if the theory contains [itex]\phi[/itex] or [itex]\neg\phi[/itex]. So we can say that a theory is complete (syntactically, in the sense meant by Godel's Incompleteness Theorems) if it contains no undecidable formulas.
 
Last edited:
  • #28
Hmmmm. What about this question.

Suppose a universe with exactly five elements. A set is definied by a formula A, and it turns out that the set has exactly 3 elements. Consider the set defined by -A (negation of A). Does this set have exactly 2 elements?
 
  • #29
asdf60 said:
Hmmmm. What about this question.
Suppose a universe with exactly five elements. A set is definied by a formula A, and it turns out that the set has exactly 3 elements. Consider the set defined by -A (negation of A). Does this set have exactly 2 elements?
Are you asking this to clarify my last post? What do you mean by a set defined by a formula, or a set defined by the negation of that formula?
 
  • #30
I'm trying to get a concrete example.

By set defined by a wff, i mean, the wff has one free variable, so any substitution of the free variable by an element of the universe that makes the wff true belongs to the set being defined.
 
  • #31
asdf60 said:
I'm trying to get a concrete example.
By set defined by a wff, i mean, the wff has one free variable, so any substitution of the free variable by an element of the universe that makes the wff true belongs to the set being defined.
Okay. In that case, the negation will define the complement of the first set, which will have two elements. I'm not sure what this is a concrete example of though.
 
  • #32
Okay.
I guess the question is, is it possible that one of the sentences is (that is, the wff substituted with an element) is undecidable, meaning it is neither true or false.
If I understand correctly, it's not possible, because that's not what undecidability says.
So to clarify, given a full model/intepretation, it is always possible to verify whether a given sentence is true in the model. And if it isn't true, then it's negation is.
Is this correct?
 
Last edited:
  • #33
asdf60 said:
Okay.
I guess the question is, is it possible that one of the sentences is (that is, the wff substituted with an element) is undecidable, meaning it is neither true or false.
This is not what undecidable means. As I said earlier in the thread, truth and provability should not be confused. If a sentence is undecidable it means it is unprovable, but it will still be either true or false for a given interpretation. For instance, the undecidable Gödel sentences in theories of arithmetic are always true for the interpretation of natural numbers.

If I understand correctly, it's not possible, because that's not what undecidability says.
So to clarify, given a full model/intepretation, it is always possible to verify whether a given sentence is true in the model. And if it isn't true, then it's negation is.

Is this correct?
It might not always be possible to verify whether a given sentence is true in the model, but the definition of truth for an interpretation states that if any formula is not true then its negation is.
 
  • #34
Sorry, but I'm going to have another go at this, since I would like to be able to explain this stuff without making people more confused.

A first-order theory (according to one definition, at least) is a set of wffs closed under logical consequence.

Truth and falsehood are not defined in terms of theories, but in terms of interpretations. We do not say that a wff is true for a theory, only that it belongs to (or is provable) in that theory. We can say that a wff is true for some interpretation though.

If some wff [itex]\phi[/itex] is undecidable in a theory, then there will be an model of that theory (an interpretation which makes all the wffs in the theory true) for which [itex]\phi[/itex] is true and a model for which [itex]\phi[/itex] is false. This follows from the theorem that all consistent theories have models.

In your example, if you have an interpretation consisting of a domain with five elements, and a wff [itex]\phi(x)[/itex] defining a subset of this domain with three elements, then the negation of that wff will define the set's complement. There is no mention of theories here, so it doesn't make sense to talk about the wff being decidable. This is why I didn't see the point of your example.
 
Last edited:

1. What is first order logic?

First order logic is a formal system used in mathematical logic and computer science to represent and reason about statements involving objects, relations, and functions in a precise and unambiguous way. It is also known as first-order predicate calculus or first-order logic with identity.

2. What does soundness mean in first order logic?

Soundness in first order logic means that if a sentence can be derived from a set of axioms using the rules of inference, then it must be logically valid. In other words, soundness ensures that the conclusions drawn from a set of premises are true if the premises are true.

3. What is completeness in first order logic?

Completeness in first order logic means that if a sentence is logically valid, then it can be derived from a set of axioms using the rules of inference. In other words, completeness ensures that all logically valid statements can be proven within the system.

4. How is decidability defined in first order logic?

Decidability in first order logic refers to the ability to determine whether a given sentence is true or false within a finite amount of time. This is important in computer science and artificial intelligence, as it allows for automated reasoning and theorem proving.

5. What are some applications of first order logic?

First order logic has many practical applications, including automated reasoning, theorem proving, natural language processing, and database query languages. It is also used in the foundations of mathematics and is an important tool in the development of artificial intelligence systems.

Similar threads

  • Set Theory, Logic, Probability, Statistics
Replies
26
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
11
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
2
Views
1K
  • Set Theory, Logic, Probability, Statistics
Replies
14
Views
3K
  • Set Theory, Logic, Probability, Statistics
Replies
7
Views
1K
  • Set Theory, Logic, Probability, Statistics
Replies
2
Views
2K
  • Set Theory, Logic, Probability, Statistics
Replies
6
Views
1K
  • Set Theory, Logic, Probability, Statistics
Replies
1
Views
1K
  • Set Theory, Logic, Probability, Statistics
Replies
9
Views
1K
  • Set Theory, Logic, Probability, Statistics
Replies
3
Views
2K
Back
Top