• Martin Raza
    4
    Gӧdel proved that FOL is complete. The arithmetical theory Q is closed under first-order logical consequence, and yet Gӧdel's theorems establish that Q is incomplete. What are the relationships between the relevant concepts involved, and why these facts are mutually compatible?
  • fdrake
    5.9k
    A list of statements is closed under first order logical consequence = everything that can be derived from that list's elements using first order logical consequence is in the list.

    Incompleteness says that there are tautologies which can't be derived (as theorems). Closure says everything that can be derived is thrown in, incompleteness says there are semantic truths that can't be derived (using the relevant entailment).
  • fishfry
    2.6k
    Incompleteness says that there are tautologies which can't be derived (as theorems).fdrake

    I'm no expert on this stuff but every tautology has a proof. Incompleteness involves propositions that aren't tautologies, whose truth value varies with the model. For example the axioms for a group say nothing about whether the group is Abelian. The statement "xy = yx for all x, y" is true in some models and not in others. So the group axioms are not complete.

    A proposition is a tautology (true in every model), if and only if it has a proof. That's Gödel's completeness theorem.

    https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem
  • fdrake
    5.9k
    I'm no expert on this stuff but every tautology has a proof. Incompleteness involves propositions that aren't tautologies, whose truth value varies with the model. For example the axioms for a group say nothing about whether the group is Abelian. The statement "xy = yx for all x, y" is true in some models and not in others. So the group axioms are not complete.fishfry

    Seems I was confused and wrong then.

    To set the record straight, do you agree with this:

    Edit: (0) Call a well formed formula of a system's language which can be true or false "a statement".
    (1) That a tautology of a system is a statement in it that evaluates as true in every model of that system.
    (2) That a system is semantically complete if there is a derivation for every tautology (every tautology is a theorem). FOL is semantically complete.
    (3) That a system is syntactically complete if for every statement in it, either it or its negation is provable.
    (4) A system is consistent if it proves no contradictions
    *
    (if the theory proves P and also proves not-P then it proves a contradiction)
    .
    (5) The first incompleteness theorem says that every (sufficiently strong) system which is consistent cannot be syntactically complete.
    (6) That a list of statements is closed under derivations if that list of statements contains every statement which is derivable from it.

    In the context of the OP:

    (7) Q is closed under first order logical derivations; which means every (first order) statement which can be derived from Q is in Q.
    (8) Q contains additional structure to raw FOL - it proves more. So the completeness theorem applies to the underlying logic but not to Q. There are Q theorems which are not raw FOL theorems.
    (9) Q is incomplete (if it is consistent) since Godel's incompleteness theorem applies to it. This shows that there are statements which can be made using the language of Q for which the statement and its negation cannot be proved (syntactically derived) (if it is consistent).

    (9) and (7) may appear to contradict each other, but they don't, as "everything which can be proved from Q is already in Q" and "nevertheless there are things which Q can't prove" don't contradict each other. Analogy, you wouldn't expect the principles underlying Gordon Ramsey's Perfect Scrambled Eggs recipe to allow you to also cook Gordon Ramsey's Perfect Beef Tenderloin.

    Edit2: and in further connection to your post, I think you were very right to hammer on my incorrect use of the word "tautology", because if Q failed to prove x and failed to prove not-x, Q could be augmented with x or not-x as an axiom, and this new system Qx would still be a model of Q's axioms, just like an Abelian group is a model of the group axioms, as is a non-Abelian group. A statement being a tautology blocks that ability to assume a model where it is false.
  • fishfry
    2.6k
    (4) A system is consistent if it proves no contradictions (statements false in every model).fdrake

    I got in trouble here. A system is inconsistent if it proves both P and not-P for some statement P.

    But if a system is inconsistent, it has no model at all; so the claim that a contradiction is false in every model doesn't make sense to me.

    "The semantic definition states that a theory is consistent if it has a model ..."

    https://en.wikipedia.org/wiki/Consistency

    I looked up Q, which turns out to be Robinson arithmetic. I've heard of it but I'm not familiar with it so it's best if I don't try to add anything to the discussion beyond the minor correction I noted earlier.
  • fdrake
    5.9k
    But if a system is inconsistent, it has no model at all; so the claim that a contradiction is false in every model doesn't make sense to me.fishfry

    That makes sense. I'm using terms way too loosely and wrong.

    A model of a theory is an object which satisfies all that theory's true statements. Like the real numbers are a model of the field axioms. Contradictions can never be true; so a contradiction is a statement for which no model exists (by definition a model of a contradiction would make that contradiction true). If a theory proves a contradiction, then whatever would model it would also have to model that contradiction. But there are no models of contradictions. So that theory would not have a model.

    I was getting confused with the idea of a countermodel - for a contradiction, every model is a countermodel.

    Sorry for all the confusion. I edited the post you quoted to explain a contradiction as "(statements which are always false)"
  • fishfry
    2.6k
    Sorry for all the confusion. I edited the post you quoted to explain a contradiction as "(statements which are always false)"fdrake

    Darn. I am afraid I have to be picky again. A contradiction is not false. A contradiction is a pair of syntactic derivations, one of some statement P and the other of not-P. There is no truth or falsity in syntax.

    2 + 2 = 5 is false in every model of the Peano axioms, but it's not a contradiction.

    Gordon Ramsey's Perfect Scrambled Eggs recipe to allow you to also cook Gordon Ramsey's Perfect Beef Tenderloin.fdrake

    His cooking videos are very good. But when he's doing those restaurant rescues and verbally berates some underage female waitperson, he's a bit of a bully. He has daughters himself and should know better.
  • fdrake
    5.9k
    Darn. I am afraid I have to be picky again. A contradiction is not false. A contradiction is a pair of syntactic derivations, one of some statement P and the other of not-P. There is no truth or falsity in syntax.fishfry

    Fair! I think that's equivalent to a theory deriving (P and not-P) though, which is always false. IE, a theory managing to prove something that no object could make true/satisfy.

    Spelling out that connection: that immediately means you've got no models. Since if a hypothetical model satisfies P then it cannot satisfy not-P. The converse also holds. Therefore there are no models of such a theory. Then it's a contradiction in the "no models" sense. So having a model immediately blocks that situation.

    I edited the post again to: "if a theory proves P and it also proves not-P then it proves a contradiction".
  • GrandMinnow
    169


    The completeness theorem, as applied to Q in particular, is that for first order logic, if a formula F is entailed by a set of formulas Gamma, then there is a proof of F from Gamma. In other words, if Gamma symantically entails F, then Gamma syntactically proves F.

    The incompleteness theorem, as applied to Q in particular, is that there are formulas in the language of Q such that neither the formula nor its negation is a theorem of Q. That is purely syntactical. It does not require mentioning any semantic notion, though, of course, we can go on to observe many corollaries about semantics, such as that there are formulas that are true in the standard model for Q that are not theorems of Q.

    In any case, there is no need for explanation of why the Completeness theorem applied to Q does not conflict with the Incompleteness theorem applied to Q. It's just that the word 'completeness' is used in two different senses in the nicknames of the theorems.
  • GrandMinnow
    169
    "FOL is syntactically complete."

    That is incorrect. It is not the case that for every formula, either FOL proves the formula or FOL proves the negation of the formula.

    "a list of statements is closed under derivations if that list of statements contains every statement which is derivable from it"

    I would put it this way: A set of formulas is closed under deduction if and only if every formula derivable from the set is a member of the set. A theory is a set of sentences closed under deduction.

    /

    "the claim that a contradiction is false in every model doesn't make sense to me"

    A contradiction is false in every model. In any given model (for a given language), every sentence (of the language) is exactly one: true or false. So a contradiction (of the language) is always false in any model (of the language).

    "A contradiction is not false. A contradiction is a pair of syntactic derivations, one of some statement P and the other of not-P."

    No, a contradiction is any formula of the form P & ~P (or, more broadly any formula that is equivalent in pure FOL to P & ~P).
  • fdrake
    5.9k
    That is incorrect. It is not the case that for every formula, either FOL proves the formula or FOL proves the negation of the formula. That result is known as Church's theorem.GrandMinnow

    :up:

    Again, I was wrong.

    Example: for all x P(x) => Q(x) is a statement of FOL, but neither it or its negation are provable.
  • GrandMinnow
    169
    Yes, and even more simply, no atomic formula or its negation is provable in pure FOL.
bold
italic
underline
strike
code
quote
ulist
image
url
mention
reveal
youtube
tweet
Add a Comment