Consistency proof
Encyclopedia : C : CO : CON : Consistency proof
In mathematical logic, a formal system is consistent if it does not contain a contradiction, or, more precisely, for no proposition φ are both φ and ¬φ 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.
Although consistency can be proved by means of model theory, it is often done in a purely syntactical way, without any need reference to some model of the logic. The cut-elimination (or equivalently the normalization of the underlying calculus if there is one) implies the consistency of the calculus: since there is obviously no cut-free proof of falsity, there is no contradiction in general.
Consistency and completeness
The fundamental results relating consistency and completeness were proven by Kurt Gödel:
- Gödel's completeness theorem shows that any consistent first-order theory is complete with respect to a maximal consistent set of formulae which are generated by means of a proof search algorithm.
- Gödel's incompleteness theorems show that theories capable of expressing their own provability relation and of carrying out a diagonal argument are capable of proving their own consistency only if they are inconsistent. Such theories, if consistent, are known as essentially incomplete theories.
- Inconsistent theories, which have no models;
- Theories which cannot talk about their own provability relation, such as Tarski's axiomatisation of point and line geometry, and Presburger arithmetic. Since these theories are satisfactorily described by the model we obtain from the completeness theorem, such systems are complete;
- 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;
- Essentially incomplete theories.
See also
- Continuum hypothesis
- Consistency proof
- Hilbert's third problem
- Hilbert's fourth problem
- Hilbert's fifth problem
- Hilbert's sixth problem
- Hilbert's seventh problem
- Riemann hypothesis
- Hilbert's ninth problem
- Matiyasevich's theorem
- Hilbert's eleventh problem
- Hilbert's twelfth problem
- Hilbert's thirteenth problem
- Hilbert's fourteenth problem
- Hilbert's fifteenth problem
- Hilbert's sixteenth problem
- Hilbert's seventeenth problem
- Hilbert's eighteenth problem
- Hilbert's nineteenth problem
- Hilbert's twentieth problem
- Hilbert's twenty-first problem
- Hilbert's twenty-second problem
- Hilbert's twenty-third problem
From Wikipedia, the Free Encyclopedia. Original article here. Support Wikipedia by contributing or donating.
All text is available under the terms of the GNU Free Documentation License See Wikipedia Copyrights for details.
All text is available under the terms of the GNU Free Documentation License See Wikipedia Copyrights for details.
