# Why is completeness (as in Gödel completeness theorem) a desirable feature?

When justifying the dominance of first-order theory, an argument that is often made is that it is complete (as shown by Gödel).

This means that a theory formulated in first-order logic has a model if and only if it is consistent.

Equivalently, it means that a proposition (of such a theory) is a theorem if and only if it is true in every model of the theory.

I understand that, still I fail to see what completeness brings concretely.

Are there real advantages of completeness when dealing with a theory, either from the mathematical, computational or philosophical point of view?

• A complete proof system vaptures our natural understanding of deduction, that meas that the logical engine tracks faithfully the concept of logical consequence, that in turn formalizes our natural understanding of consequence. Commented Jun 27 at 17:20
• The "equivalence" of two very different views of "formality" the syntactical manipulation of symbols, and the truth preservation under every possible interpretation of the non-logical terms means that we have captured a deep and stable concept. Commented Jun 27 at 17:28
• @MichaelCarey What you are describing is en.wikipedia.org/wiki/Soundness. Completeness is essentially about the "P is true in every model of the theory" => "P is a theorem" way. Commented Jun 27 at 20:03
• @MichaelCarey: IMHO it's more that soundness is considered table stakes (an unsound deductive system is completely worthless unless it is paraconsistent, and that has its own issues, so almost any system that anyone wants to use for serious purposes will be sound). Commented Jun 28 at 3:32
• @Weier it's not extraneous. His name was Gödel and the usual convention for German names (and words more generally) is that where the umlaut is unavailable (as in the tags) it should be replaced with a following e i.e. Goedel. Commented Jun 28 at 11:00

If you have a set A of axioms, which you assume to be true, you would of course be interested in all the sentences that are necessarily true given A. On the surface, this is difficult to know because it involves all possible models of A, which may include (very) uncountably many models. But look! The semantic-completeness theorems for a deductive system for FOL implies that you can in fact (within that system) prove any such sentence. So if A is computably enumerable (which is always the case for practical formal systems), then the set of all sentences that are true in every model of A is also computably enumerable! We can write a computer program that would eventually generate all these sentences and no others!

• "you would of course be interested in all the sentences that are necessarily true given A." why "of course"? From a practical perspective I need all of the derived sentences to be true, but I don't see why it is a practical problem if I can't enumerate all true sentences, especially if the ones I can't enumerate are highly abstruse self-referential examples. I can see how "of course" applies to consistency, but not completeness. Commented Jun 28 at 17:09
• @DikranMarsupial The hard part arises when it is difficult to prove whether any given sentence is provable or not. As a practical matter, lots of philosophical topics run into self-referential patterns due to the concept behind the word "I." That being said, it's absolutely standard practice to try to come up with a sub model (a smaller model that is entailed by the larger one) with better properties (such as being complete because you removed all of the pesky statements). Commented Jun 28 at 20:08
• @DikranMarsupial: We must have that we can only deduce true statements from true assumptions. We hope that we can deduce all statements that are necessarily true given the assumptions. This has absolutely nothing to do with self-reference. Do not blindly assume that semantic-completeness is related to syntactic-completeness. Commented Jun 29 at 9:21
• @user21820 thank you for the clarification, but as far as I can see, that doesn't really answer my question (at least not in terms that I can appreciate). Commented Jun 29 at 14:02
• @DikranMarsupial: If it's not in terms that you can appreciate, then you need to do a proper study of FOL. Let me know your mathematical background and I can give you recommended references to work through that are suitable for your current level. Commented Jun 30 at 11:50

From Wikipedia:

Gödel's original formulation

The completeness theorem says that if a formula is logically valid then there is a finite deduction (a formal proof) of the formula.

Thus, the deductive system is "complete" in the sense that no additional inference rules are required to prove all the logically valid formulae. A converse to completeness is soundness, the fact that only logically valid formulae are provable in the deductive system. Together with soundness (whose verification is easy), this theorem implies that a formula is logically valid if and only if it is the conclusion of a formal deduction

Any statement in the language of first order predicate logic has a semantically equivalent statement formulatable in the propositional calculus. Rosser's system RS for the propositional calculus is complete, in the sense that all tautologies are theorems of RS. Since any logically valid formula is equivalent in meaning to a tautology, the proof that RS is complete simultaneously proves FOL is complete. Thus, you can bypass Godel's difficult proof of the completeness of a first order function calculus, by first proving FOL is reducible to the propositional calculus.

The reason completeness is desirable, is so you know your system, RS, or Hilbert Ackerman HA, or whatever, has enough axioms and underived rules of inference to prove all tautologies as theorems of the system.

• That's what I also think is the conclusion of Gödel's proof. However, if I may say so, and I'm sure someone like yourself, who's probably done tons of formal proofs using predicate logic, must've noticed - some proofs are, how shall I put it?, too long. Maybe if we added some more inference rules, we can shorten the distance, as it were, between premises and conclusion, oui? Commented Jun 28 at 2:56
• @Hudjefa, of course you can shorten the proofs, but my point is simply Godel's, and Leon Henkins for that matter, proof of completeness can be dispensed with. Once you prove the propositional calculus is complete you are done. And Henkin's proof is hard to follow. Commented Jun 28 at 3:01
• How would you answer the OP's query. What does completeness have to offer? As far as I'm concerned, I'm quite happy to have a system that ensures all valid formulae/arguments are derivable from a set of inference rules. Commented Jun 28 at 3:10