Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

First order logic: Soundness, Completeness, Decidability

  1. Dec 13, 2005 #1
    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.


  2. jcsd
  3. Dec 13, 2005 #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.
  4. Dec 13, 2005 #3
    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.

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

    "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: Dec 13, 2005
  5. Dec 13, 2005 #4
    More accurately, whether they are provable or not. Truth and provability should not be confused.

    Why do you think this?

    But if it is complete and has a recursive set of axioms, then it will always be decidable.
  6. Dec 13, 2005 #5


    User Avatar
    Science Advisor
    Homework Helper

    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.
    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.
  7. Dec 13, 2005 #6
    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.
    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).
  8. Dec 13, 2005 #7
    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...

    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.

    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.
  9. Dec 13, 2005 #8


    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    (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: Dec 13, 2005
  10. Dec 13, 2005 #9


    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    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: Dec 13, 2005
  11. Dec 13, 2005 #10
    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?
  12. Dec 13, 2005 #11


    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    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)
  13. Dec 13, 2005 #12
    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.
  14. Dec 13, 2005 #13
    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.

    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.

    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: Dec 13, 2005
  15. Dec 13, 2005 #14
    The second-order predicate calculus is incomplete (under standard semantics), so there is no such thing as a consistent second-order recursively axiomatisable theory.
  16. Dec 13, 2005 #15
    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.

    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.
  17. Dec 13, 2005 #16
    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.
  18. Dec 13, 2005 #17
    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.
  19. Dec 13, 2005 #18
    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.
  20. Dec 13, 2005 #19


    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    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.
  21. Dec 13, 2005 #20


    User Avatar
    Science Advisor
    Homework Helper

    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.
  22. Dec 13, 2005 #21


    User Avatar
    Staff Emeritus
    Science Advisor
    Gold Member

    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.
  23. Dec 14, 2005 #22
    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.
  24. Dec 14, 2005 #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?
  25. Dec 14, 2005 #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.
  26. Dec 14, 2005 #25


    User Avatar
    Science Advisor
    Homework Helper

    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.
Share this great discussion with others via Reddit, Google+, Twitter, or Facebook