# Some different versions of completeness of a formal system, of a logic and of a theory

I have seen people talking about Gödel's complete theorems and Gödel's incomplete theorems on math.SE. I am curious what they are really about, so I try to understand the meaning of completeness first.

My questions are:

1. In the following different versions of completeness, are some of them actually the same concept?
2. When talking about completeness, some refers to completeness of a formal system, some uses completeness of a theory, and some uses completeness of a logic. Are these equivalent?

I know that every formal system has a theory as its component, but I am not sure if every formal system has a logic as its component?

Note that a formal system consists of a language, a set of axioms, a set of inference rules, and a set of theorems (which are derived from the axioms and inference rules), called a theory.

3. There are some specific questions about each version of completeness below.

Different versions of completeness:

1. From Wikipedia

A formal system S is syntactically complete or deductively complete or maximally complete or simply complete if and only if for each formula φ of the language of the system either φ or ¬φ is a theorem of S. This is also called negation completeness.

In another sense, a formal system is syntactically complete if and only if no unprovable axiom can be added to it as an axiom without introducing an inconsistency.

Does "either φ or ¬φ is a theorem of S" allows both φ and ¬φ to be theorems of S?

Does "for each formula φ of the language of the system ..." mean that there is no formula in the language of the formal system such that neither φ or ¬φ is a theorem of S?

2. From Wikipedia:

a theory is complete if it is a maximal consistent set of sentences, i.e., if it is consistent, and none of its proper extensions is consistent.

Is this a different completeness concept from the one in part 1? I think they are the same, because part 2 seems same as "no unprovable axiom can be added to it as an axiom without introducing an inconsistency" in part 1.

3. From Wikipedia

A formal system S is semantically complete or simply complete, if every tautology of S is a theorem of S.

From Wikipedia

a complete logic, which asserts that for every theory that can be formulated in the logic, all semantically valid statements are provable theorems (for an appropriate sense of "semantically valid"). Gödel's completeness theorem is about this kind of completeness.

I wonder if "semantically valid statements" and "tautologies" are the same concept?

Are the above two "completeness" the same concept?

4. From Wikipedia:

A formal system S is strongly complete or complete in the strong sense if and only if for every set of premises Γ, any formula which semantically follows from Γ is derivable from Γ.

A formal system has its own fixed set of axioms. So I wonder if "every set of premises Γ" means every subset of the set of axioms of the formal system?

Thanks and regards!

-
Just a comment, but the emphasis on simply complete is a misreading of the article: it should be "simply complete." –  goblin Jun 7 at 7:36

As the quotations reveal, there are indeed two different notions here.

1 & 2 belong together. A formal theory $T$ is negation-complete if for any sentence of $T$'s language, either $T$ proves $\varphi$ or $T$ proves $\neg\varphi$ (in symbols, either $T \vdash \varphi$, then $T \vdash \neg\varphi$).

3 & 4 belong together. A logical system (e.g. for quantificational logic) is complete if whenever the premisses $\Gamma$ semantically entail the conclusion $\varphi$, there is a formal deduction in the system of $\varphi$ from premisses in $\Gamma$. (In symbols, if whenever $\Gamma \vDash \varphi$, then $\Gamma \vdash \varphi$.)

So quite different ideas: one is to do with how a deductive logic relates to the relevant notion of semantic entailment; the other is a purely syntactic notion. You can have negation-incomplete theories with complete logics, and negation-complete theories with incomplete logics (as well as the other two combinations).

Famously Gödel proved that essentially the Hilbert/Ackermann axiomatic version of quantificational logic is complete -- every semantically valid quantificational consequence (assuming a classical semantics) can be formally derived in that axiomatic system. Hence Gödel's completeness theorem (about a system of logic).

Famously Gödel proved that essentially a cut-down version of Principia's formal theory is not negation-complete: there are sentences which can't be decided one way or the other by the axioms. And the proof generalizes to any consistent formal theory that can "do enough arithmetic" (and which satisfies another condition which doesn't matter here). Hence Gödel's incompleteness theorem (about theories containing enough arithmetic).

Two different Gödelian results about different notions (so, there's no tension between them!).

-
Thanks, Peter Smith! I wonder if you can try to address (other) specific questions in my post? My confusion in the questions and the funny way I was talking come from not understanding some basic concepts. I have never formally studied formal system and logic before. –  Tim Sep 17 '12 at 22:31
For example, is there difference between consistency of a theory and consistency of a formal system? Difference between completeness of a theory and completeness of a formal system or of a logic? –  Tim Sep 18 '12 at 0:06