Completeness (in logic)

A property close to the concept of a maximal element in a partially ordered set. The term completeness in mathematical logic is used in contexts such as the following: complete calculus, complete theory (or complete set of axioms), $\omega$-complete theory, axiom system complete in the sense of Post, complete embedding of one model in another, complete formula of a complete theory, etc.

One of the most important concepts — in a gnosiological context — is that of completeness of a calculus with respect to a given semantics. A calculus is called complete if any formula true in the semantic sense in that calculus is derivable in it. Here the concept of derivability should be effective, i.e. there are a set of rules and a set of instructions for using them that enable one to construct derivations, and there is an algorithm that distinguishes derivations from non-derivations. The concept of a semantically correct formula on the other hand is commonly formulated by the use of ineffective concepts employing universal quantifiers with respect to infinite and even uncountable sets. In completeness theorems in classical and intuitionistic predicate calculus, completeness is understood in that sense. In the case of a classical calculus, one takes as semantically correct those formulas in the language of pure (narrow) predicate calculus that are true in all models for that language. In the intuitionistic case, one takes as semantically correct all formulas that are true in all Kripke models. The concept of a formula being true in a given model also uses quantifiers over infinite domains (if the model is infinite) both in the classical and in the intuitionistic cases. Sometimes one considers calculi that do not satisfy the requirement of effectiveness.

The concept of completeness in a calculus is closely related to that of a complete theory. A theory (more precisely, an elementary theory) is any set $T$ of closed formulas in the language of pure predicate calculus. A consistent theory $T$ is called complete if the set of all consequences from $T$ in the classical predicate calculus is a maximal consistent set, i.e. the addition to $T$ of any closed formula not derivable from $T$ enables one to derive any formula. In this definition it is not assumed that the set $T$ is given effectively, so the concept of a derivation becomes also ineffective. Completeness of a theory $T$ is equivalent to the following condition: For any closed formula $\phi$, precisely one of the two assertions applies: either $\phi$ is derivable from $T$ or $\neg\phi$ is derivable from $T$.

If one is given some model $M$ of the language of pure predicate calculus, one gets the semantic concept of a formula being true in the model $M$. A theory $T$ is called complete with respect to the model $M$ if the classical predicate calculus supplemented with the formulas from $T$ allows one to derive precisely all the formulas true in $M$. There is the following relationship between the concepts of completeness of a theory and completeness with respect to $M$. A theory $T$ is complete if and only if there exists a model $M$ with respect to which it is complete. A model $M$ is called a model for the theory $T$ if all the formulas from $T$ are true in $M$. A sufficient criterion for completeness of a theory is: If, for a certain infinite cardinality, all models of a theory $T$ are pairwise isomorphic and if $T$ has no finite models, then $T$ is complete. The converse is not always true.

The concept of completeness of a theory is used in questions of solvability theory because of the following property of complete theories: If a theory $T$ is complete and the set $T$ is finite or even recursively enumerable, then there exists an algorithm that will recognise for any formula $\phi$ whether it is derivable or not. If one does not require the effective specification of the set $T$, any theory can be completed, i.e. it can be extended by the addition of new axioms to a complete theory. The situation is not the same if effectiveness is required, as Gödel's theorem on the incompleteness of arithmetic shows. A theory $T'$ is called an extension of a theory $T$ if any formula derivable from $T$ is derivable from $T'$. Let $T$ be a recursively-enumerable consistent theory. The theory $T$ is called effectively incompletable if in any recursively-enumerable consistent extension $T'$ of $T$ one can effectively find a formula $\phi$ that is formally unsolvable in $T'$, i.e. such that neither $\phi$ nor $\neg\phi$ is derivable in $T'$. Gödel's incompleteness theorem asserts that a particular arithmetic theory $Q$ having a finite number of axioms is effectively incompletable. This theorem implies the incompleteness with respect to the standard model of the natural numbers of any arithmetic calculus that satisfies the requirement of effectiveness.

An arithmetic theory $T$ is called $\omega$-complete if, for every formula $\phi(x)$ in one free variable $x$, the fact that in $T$ one can derive all the formulas of the form

$$\phi(0),\phi(1),\dots,\label{*}\tag{*}$$

implies that the formula $\forall x\phi(x)$ is derivable in $T$. It follows from the proof of Gödel's incompleteness theorem that there exist theories that are not $\omega$-complete, and even ones in which both the infinite series of formulas \eqref{*} is derivable as well as the formula $\exists x\neg\phi(x)$, but in which nevertheless contradictions cannot be derived. Such a theory is called $\omega$-inconsistent.

A consistent axiom system is called complete in the sense of Post if the addition to it of any axiom scheme either does not extend the set of derivable formulas or transforms the system into an inconsistent one. For example, the axiomatics of classical propositional calculus are complete in the sense of Post, while intuitionistic propositional calculus is not complete.

References

[1]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)
[2]	H.J. Keisler, C.C. Chang, "Model theory" , North-Holland (1973)
[3]	J.R. Shoenfield, "Mathematical logic" , Addison-Wesley (1967)
[4]	H. Rogers jr., "Theory of recursive functions and effective computability" , McGraw-Hill (1967) pp. 164–165
[5]	S.A. Kripke, "Semantical analysis of intuitionistic logic" J.N. Crossley (ed.) M.A.E. Dummett (ed.) , Formal systems and recursive functions , North-Holland (1965) pp. 22–130