Are propositional logic/first-order logic complete?

2.3k Views Asked by At

I don't mean "complete" in the sense of the completeness theorem (semantic provability => syntactic provability). I mean "complete" in the sense of the incompleteness theorem (prove all and only true sentences expressible in its language).

In the second sense of "complete", are propositional logic and/or first-order logic complete?

Thanks!

2

There are 2 best solutions below

5
On

I don't think there is any meaningful interpretation of "the second sense of complete" in this context that differs from the first. "Every true statement" could only mean "all statements true in every model." Reading the claim that way, completeness is exactly completeness in the first sense.

The reason for the distinction in the incompleteness theorem is that we have some particular model in mind (arithmetic), and we want to know if we can prove everything true in that model from our proof system together with our axioms. The completeness theorem says that our proof system is fine for such purposes. The incompleteness theorem says our axioms cannot be. Again, the distinction doesn't make sense if we're just talking about a proof system for some language.

6
On

I think that the adjcetives "syntactical" and "semantic" for the notion of completenss are not well chosen. Unfortunately, the role played by Gödel as author both of the Completeness Theorem (for first-order logic) and the Incompleteness Theorem (for formal arithmetic) does not help ...

The two notions are distinct but strictly linked, and both are forms of completeness of a formal theory with respect to the truth.

The notion of completeness dates back to Hilbert who, in his lecture course on the principles of mathematics he taught in the winter semester 1917/18 (that form the basis of Hilbert and Ackermann's textbook (1928)), states the first formulation of the completeness problem as a precise mathematical question to be answered for a system of axioms :

We want to call the system of axioms under consideration complete if we always obtain an inconsistent system of axioms by adding a formula which is so far not derivable to the system of basic formulas.

This general notion can be applied to a logic calculus, [and is what Wiki calls semantic] aimed to capture all the logical truths formulable in a given language or type of language.

For propositional logic, the completeness was proved independently by Bernays (1918) and Post (1921).

To Bernays is also due the first clear definition of universally valid [allgemeingultige] formula.

See David Hilbert & Wilhelm Ackermann, Principles of Mathematical Logic (engl transl of the 2nd german ed, 1938), page 14 :

It is now the first task of logic to find those combinations of sentences which are logically true, i.e. true independently of the truth values of the elementary sentences.

And see page 68 :

A formula of the predicate calculus is called logically true or, as we also say, universally valid only if, independently of the choice of the domain of individuals, the formula always becomes a true sentence for any substitution of definite sentences, of names of individuals belonging to the domain of individuals, and of predicates defined over the domain of individuals, for the sentential variables, the free individual variables, and the predicate variables respectively. The universally valid formulas of the predicate calculus will also, for convenience, sometimes be called simply valid [page 68].

The completenss of first-order logic was proved by Gödel in 1930 :

the question [...] arises whether the initially postulated system of axioms and principles of inference is complete, that is, whether it actually suffices for the derivation of every true logico-mathematical proposition, or whether, perhaps, it is conceivable that there are true propositions (which may even be provable by means of other principles) that cannot be derived in the system under consideration. For the formulas of the propositional calculus the question has been settled affirmatively; that is, it has been shown [footnote: Bernays 1926] that every true formula of the propositional calculus does indeed follow from the axioms given in Principia mathematica. The same will be done here for a wider realm of formulas, namely, those of the "restricted functional calculus"; that is, we shall prove

THEOREM I. Every valid [footnote: To be more precise, we should say "valid in every domain of individuals", which, according to well-known theorems, means the same as "valid in the denumerable domain of individuals".] formula of the restricted functional calculus is provable.

The same notion can be applied to other cases [and this is what Wiki calls syntactical and some authors call Gödel completeness], like theories purporting to formalize arithmetic; in this case, completeness means to prove every truth pertaining to some more restricted subject matter: the "intended" domain of discorse of the theory.

There is one important difference between the two: while completeness with respect to logical truths cannot be expected to satisfy a general law of excluded middle according to which for every sentence in a given language, either that sentence or its denial will be true, completeness with respect to e.g. the truth for arithmetic can reasonably be expected to satisfy such a principle.

And here we have Gödel again, in 1930 :

The system $S$ [i.e. the system obtained adding Peano axioms to the logic of Principia mathematica] is not complete [entscheidungsdefinit]; that is, it contains propositions $A$ (and we can in fact exhibit such propositions) for which neither $A$ nor $\overline A$ is provable and, in particular, it contains (even for decidable properties $F$ of natural numbers) undecidable problems of the simple structure $(\exists x)F(x)$, where $x$ ranges over the natural numbers.