Consistency

The property of a formal system requiring that not every formula of the system is provable in it. Formal systems having this property are called consistent or formally consistent. In the opposite case the formal system is called contradictory or inconsistent. For the broad class of formal systems whose language contains the negation symbol $\neg$, consistency is equivalent to the property that "there is no formula $\phi$ such that both $\phi$ and $\neg\phi$ are provable". A class of formulas of a given formal system is called consistent if not every formula of the system is deducible from the given class. A formal system is called satisfiable if there is a model in which all theorems of the system are true. If a formal system is satisfiable, then it is consistent. For formal systems based on classical predicate calculus the converse is also true: by the Gödel completeness theorem for classical predicate calculus, every such consistent system has a model. Thus, one of the methods of proving the consistency of a formal system consists in constructing a model. Another (meta-mathematical) method, put forward at the beginning of the 20th century by D. Hilbert, consists in the fact that the assertion of the consistency of a certain formal system can be regarded as a statement on the proofs that are possible in this system. A theory whose objects are arbitrary mathematical proofs is called a proof theory or a meta-mathematics. An example of the application of a meta-mathematical method is the proof due to G. Gentzen of the consistency of the formal system of arithmetic (see Gentzen formal system).

Any consistency proof uses tools of one mathematical theory or other and so only reduces the question of the consistency of one theory to that of another. One also says that the first theory is consistent relative to the second. Of great significance is Gödel's second theorem, which asserts that the consistency of a formal theory containing arithmetic cannot be proved by the tools of the relevant theory itself (provided that the theory is in fact consistent).

References

[1]	D. Hilbert, P. Bernays, "Grundlagen der Mathematik" , 1–2 , Springer (1968–1970)
[2]	P.S. Novikov, "Elements of mathematical logic" , Oliver & Boyd and Acad. Press (1964) (Translated from Russian)
[3]	A.A. Fraenkel, Y. Bar-Hillel, "Foundations of set theory" , North-Holland (1958)
[4]	G. Gentzen, M.E. Szebo (ed.) , Collected papers , North-Holland (1969)
[5]	G.E. Mints, "Theory of proofs (arithmetic and analysis)" Soviet Math. , 7 : 4 (1977) pp. 501–531 Itogi Nauk. i Tekhn. Algebra Topol. Geom. , 13 (1975) pp. 5–49
[6]	K. Gödel, "Die Vollstandigkeit der Axiomen des logischen Funktionalkalküls" Monatsh. Math. Physik , 37 (1930) pp. 349–360

Comments

The fact that a satisfiable system is consistent is also called the "soundness of the system". Gödel's second theorem is also called the Gödel incompleteness theorem.