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), -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 of closed formulas in the language of pure predicate calculus. A consistent theory is called complete if the set of all consequences from in the classical predicate calculus is a maximal consistent set, i.e. the addition to of any closed formula not derivable from enables one to derive any formula. In this definition it is not assumed that the set is given effectively, so the concept of a derivation becomes also ineffective. Completeness of a theory is equivalent to the following condition: For any closed formula , precisely one of the two assertions applies: either is derivable from or is derivable from .

If one is given some model of the language of pure predicate calculus, one gets the semantic concept of a formula being true in the model . A theory is called complete with respect to the model if the classical predicate calculus supplemented with the formulas from allows one to derive precisely all the formulas true in . There is the following relationship between the concepts of completeness of a theory and completeness with respect to . A theory is complete if and only if there exists a model with respect to which it is complete. A model is called a model for the theory if all the formulas from are true in . A sufficient criterion for completeness of a theory is: If, for a certain infinite cardinality, all models of a theory are pairwise isomorphic and if has no finite models, then 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 is complete and the set is finite or even recursively enumerable, then there exists an algorithm that will recognise for any formula whether it is derivable or not. If one does not require the effective specification of the set , 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 is called an extension of a theory if any formula derivable from is derivable from . Let be a recursively-enumerable consistent theory. The theory is called effectively incompletable if in any recursively-enumerable consistent extension of one can effectively find a formula that is formally unsolvable in , i.e. such that neither nor is derivable in . Gödel's incompleteness theorem asserts that a particular arithmetic theory 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 is called -complete if, for every formula in one free variable , the fact that in one can derive all the formulas of the form

(*)

implies that the formula is derivable in . It follows from the proof of Gödel's incompleteness theorem that there exist theories that are not -complete, and even ones in which both the infinite series of formulas (*) is derivable as well as the formula , but in which nevertheless contradictions cannot be derived. Such a theory is called -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