# Consistency proof

In mathematical logic, a formal system is consistent if it does not contain a contradiction, or, more precisely, for no proposition [itex]\phi\,[itex] are both [itex]\phi\,[itex] and [itex]\neg\phi\,[itex] provable.

A consistency proof is a formal proof that a formal system is consistent. The early development of mathematical proof theory was driven by the desire to provide finitary consistency proofs for all of mathematics as part of Hilbert's program. Hilbert's program fell to Gödel's insight that sufficiently strong proof theories cannot prove their own consistency.

## Consistency and completeness

The fundamental results relating consistency and completeness were proven by Kurt Gödel:

By applying these ideas, we see that we can find first-order theories of the following four kinds:

1. Inconsistent theories, which have no models;
2. Theories which cannot talk about their own provability relation, such as Tarski's axiomatisation of point and line geometry, and Presburger arithmetic. These theories are satisfactorily described by the model we obtain from the completeness theorem; we can say such systems are complete;
3. Theories which can talk about their own consistency, and which include the negation of the sentence asserting their own consistency. Such theories are complete with respect to the model one obtains from the completeness theorem, but contain as a theorem the derivability of a contradiction, in contradiction to the fact that they are consistent;
4. Essentially incomplete theories.

In addition, it has recently been discovered that there is a fifth class of theory, the self-verifying theories, which are strong enough to talk about their own provability relation, but are too weak to carry out Gödelian diagonalisation, and so which can consistently prove their own consistency.

• Art and Cultures
• Countries of the World (http://www.academickids.com/encyclopedia/index.php/Countries)
• Space and Astronomy