Skip to content
Coordinates of ThoughtHome of Philosophy
Join
Question · Explain

Soundness and completeness of a logical system: what exactly is being proved?

Pieter van Dijkhuizen Fellow
· 4 replies
Logic & argumentAnalyticKurt GödelW. V. O. Quine#completeness#metalogic#soundness#syntax-and-semantics
Follow

Its coordinates: 4.1 Formal Logic · 4.1.1 Propositional Logic · 4.1.2 Predicate Logic +4 more

I'm stuck on vocabulary, having no formal training in logic.

I've read that a logical system can be sound and complete: everything provable is true, and everything true is provable. Fine. But then I read that Gödel proved a completeness theorem in his dissertation around 1929 and then, in 1931, proved an incompleteness theorem. That looks like a contradiction, or at least like he changed his mind.

And separately, I already know that a "sound argument" is a valid argument with true premises. Is a sound system something different?

Could someone untangle these for me? I suspect the word "true" is doing different jobs in each case.

LikeAnswer
Follow4 answers

Join the conversation: members reply here, and joining is free. Reading is always free.

Join free to reply Sign in

4 answers

Accepted answer

  1. Tomasz Szewczak

    ✓ Accepted answer Fellow

    You've guessed the key. Let me separate three uses.

    Syntax and semantics. A system has rules for deriving formulas (syntax: what is provable), and a notion of interpretation, where a formula is valid if it comes out true under every interpretation (semantics). "True" in "everything true is provable" means valid in that sense: true in every model, not true about the actual world.

    Soundness and completeness of a logic. Soundness: everything provable is valid. Completeness: everything valid is provable. Gödel's 1929 result is that first-order logic has both. Its proof rules capture exactly the valid formulas, no more and no less.

    Completeness of a theory. A theory, such as a set of axioms for arithmetic, is called complete if for every sentence in its language it proves either the sentence or its negation. Gödel's 1931 result is that no consistent, effectively axiomatised theory containing enough arithmetic is complete in this sense. Some sentence true in the intended model of the natural numbers is not provable from the axioms.

    So there's no contradiction. The first theorem is about the logic: it is as strong as it should be. The second is about theories of arithmetic: no axiom set captures all arithmetical truth.

    And a sound argument, valid with true premises, is a third thing, though it's the same spirit as a sound system: nothing false comes out.

Other answers

  1. Derek Hollis

    Fellow

    An engineering version that helps people at work: a type checker is sound if every program it accepts really is free of the errors it checks for, and complete if it accepts every program that really is free of them. Most practical checkers are deliberately sound and incomplete. They reject some fine programs to guarantee they never accept a bad one. Same two words, same logic.

    Helpful · 1
  2. Pieter van Dijkhuizen

    Fellow

    That's very clear, thank you, Tomasz, and Derek's analogy makes it stick. Follow-up: is every logic complete in the first sense? I've seen second-order logic mentioned as more powerful. Does it have a complete proof system too?

    Helpful · 2
  3. Oskar Nyberg

    Fellow

    No, and that's one of the main reasons first-order logic became the standard. With its standard semantics, second-order logic has no proof system that is sound, complete and effective at once. You gain expressive power and lose the match between provability and validity. Quine was famously unimpressed, calling second-order logic "set theory in sheep's clothing", because so much of its power comes from what its semantics quietly assumes about sets.

    Helpful · 3