In logic, a theory is consistent if it does not contain a contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic definition states that a theory is consistent if it has a model; this is the sense used in traditional Aristotelian logic, although in contemporary mathematical logic the term satisfiable is used instead. The syntactic definition states that a theory is consistent if there is no formula P such that both P and its negation are provable from the axioms of the theory under its associated deductive system.
If these semantic and syntactic definitions are equivalent for a particular logic, the logic is complete. The completeness of sentential calculus was proved by Paul Bernays in 1918 and Emil Post in 1921, while the completeness of predicate calculus was proved by Kurt Gödel in 1930. Stronger logics, such as second-order logic, are not complete.
A consistency proof is a mathematical proof that a particular theory 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 was strongly impacted by incompleteness theorems, which showed 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 to reference 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.
By applying these ideas, we see that we can find first-order theories of the following four kinds:
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. However as with any theory, a theory proving its own consistency provides us with no interesting information, since inconsistent theories also prove their own consistency.
is said to be absolutely consistent or Post consistent iff at least one formula of is not a theorem of .
is said to be maximally consistent if and only if for every formula , if Con then .
is said to contain witnesses if and only if for every formula of the form there exists a term such that . See First-order logic.
(b) For all
2. Every satisfiable set of formulas is consistent, where a set of formulas is satisfiable if and only if there exists a model such that .
3. For all and :
(a) if not , then Con;
(b) if Con and , then Con;
(c) if Con , then Con or Con.
4. Let be a maximally consistent set of formulas and contain witnesses. For all and :
(a) if , then ,
(b) either or ,
(c) if and only if or ,
(d) if and , then ,
(e) if and only if there is a term such that .
Let be a maximally consistent set of formulas containing witnesses.
Define a binary relation on the set of S-terms if and only if ; and let denote the equivalence class of terms containing ; and let where is the set of terms based on the symbol set .
Define the S-structure over the term-structure corresponding to by:
(1) For -ary , if and only if ,
(2) For -ary , ,
(3) For , .
Let be the term interpretation associated with , where .