PLS Lab

Completeness

The word 'completeness' is a tortured word that can mean many things in logic. It is probably one of the most overloaded and misused words in the field.

There are at least four different (or slightly different) uses of completeness:

  1. in comparing provability with entailment
  2. in the algebraic semantics of logic
  3. in the semantics of proofs
  4. in the notion of incompleteness

Provability vs. Entailment

The usual undergraduate presentation of logic uses what we call truth-theoretic or Tarski semantics: things mean what we think they do, in that \land means 'and,' \lor means 'or,' and so on.

This leads to a fairly strict definition of truth:

In the first case, no external information is necessary (other than an assignment of true or false to each propositional variable). In the second case, a universe of elements is needed: all the basic propositions of first-order logic (which are usually equalities t = u of terms or relations R(t_1, \dots, t_n)) will be decided based on the interpretation of these primitives in that structure.

We then have two relations: logical consequence and semantic entailment.

Completeness for First-order Logic

That first-order logic is complete is the domain of Gödel's completeness theorem, which is harder.

Please expand.

Completeness for Second-order Logic

Please expand.

Completeness for Higher-order Logic

Please expand.

Completeness in algebraic logic

The algebraic approach to logic takes us a step further from truth (but not exactly into proofs yet).

An algebraic semantics assigns to every formula \phi of a logical system some sort of mathematical object \llbracket \phi \rrbracket. The collection of these objects is called a model, and usually organises into some structure, for example a Boolean or Heyting algebra.

One then has the usual notions of soundness and completeness:

Notice the appearance of the word every in the definition of completeness above. This stands in sharp contrast with, say, the Tarski semantics of propositional logic, which is essentially just one model.

In fact, this universal quantification makes completeness proofs trivial. For example, no matter the presentation (Hilbert system, natural deduction, ...), classical propositional logic is complete for Boolean algebras. The proof of this is fact is deceptively simple, and is known by the posh name of the Lindenbaum-Tarski construction. Here are the main steps:

  1. Define a relation \sim between formulas of propositional logic, where \phi \sim \psi whenever \vdash \phi \leftrightarrow \psi. That is, two formulas are equivalent exactly when the proof system proves them equivalent.
  2. Take the equivalence classes of this relation, and prove it is a Boolean algebra - the Lindenbaum-Tarski algebra. This should be relatively straightforward if your axiomatization is actually complete. Show that [\phi]_\sim = \top implies \vdash \phi.
  3. Show that when propositional logic is interpreted in this model, we have \llbracket \phi \rrbracket = [\phi]_{\sim}, i.e. each formula is mapped to its equivalence class.
  4. If \llbracket \phi \rrbracket = \top in all models, then it is also so in the Lindenbaum-Tarski algebra. Hence \vdash \phi.

Completeness in the Proof-theoretic Semantics

Proof-theoretically, there is a distinction between the aforementioned shallow notion of 'for every model' completeness, and full completeness.

The first one holds whenever an equality of proofs that holds in all models is also provable in the equational theory of proofs; it usually holds ''for free.''

Full completeness, on the other hand, is a term used to mean that every element of the model is the denotation of a certain proof.

Completeness vs. Incompleteness

A common source of confusion: incompleteness is not the negation of logical completeness!

Constructive proofs of completeness?

There is a subtle point here relating to the object language/metalanguage dichotomy. When proving a completeness theorem, how strong does our metalanguage need to be?

For example, the usual proof of completeness of the usual truth-theoretic semantics of classical first-order logic uses classical reasoning in the metalanguage in a very strong way. Can we avoid this? That is, can we prove the completeness of the usual FOL semantics in an intuitionistic language? This might be of serious interest in the quest for the formalisation of mathematics, which often uses constructive languages, such as type theory.

Interestingly, it seems like the answer to this question is negative: we cannot constructively prove the completeness of classical FOL unless we change the notion of model of FOL. See the following preprint: