Changes

[[File:lighterstill.jpg]][[File:Consistency.jpg|center|frame]]

[[File:lighterstill.jpg]][[File:Consistency.jpg|center|frame]]

*[http://en.wikipedia.org/wiki/16th_century 1594]

*[https://en.wikipedia.org/wiki/16th_century 1594]

==Definitions==

==Definitions==

*1a archaic : condition of [[adhering]] [[together]] : firmness of [[material]] substance  

*1a archaic : condition of [[adhering]] [[together]] : firmness of [[material]] substance  

==Description==

==Description==

In [[logic]], a '''consistent''' [[theory]] is one that 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 [http://en.wikipedia.org/wiki/Term_logic 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.

In [[logic]], a '''consistent''' [[theory]] is one that 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 [https://en.wikipedia.org/wiki/Term_logic 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 [http://en.wikipedia.org/wiki/Sentential_calculus sentential calculus] was proved by [http://en.wikipedia.org/wiki/Paul_Bernays Paul Bernays] in 1918  and [http://en.wikipedia.org/wiki/Emil_Post Emil Post] in 1921, while the completeness of [http://en.wikipedia.org/wiki/Predicate_calculus predicate calculus] was proved by [http://en.wikipedia.org/wiki/Kurt_G%C3%B6del Kurt Gödel] in 1930, and consistency [[proofs]] for arithmetics restricted with respect to the [http://en.wikipedia.org/wiki/Induction induction axiom schema] were proved by Ackermann (1924), von Neumann (1927) and Herbrand (1931. Stronger logics, such as [http://en.wikipedia.org/wiki/Second-order_logic second-order logic], are not complete.

If these [[semantic]] and [[syntactic]] definitions are [[equivalent]] for a particular [[logic]], the logic is complete. The completeness of [https://en.wikipedia.org/wiki/Sentential_calculus sentential calculus] was proved by [https://en.wikipedia.org/wiki/Paul_Bernays Paul Bernays] in 1918  and [https://en.wikipedia.org/wiki/Emil_Post Emil Post] in 1921, while the completeness of [https://en.wikipedia.org/wiki/Predicate_calculus predicate calculus] was proved by [https://en.wikipedia.org/wiki/Kurt_G%C3%B6del Kurt Gödel] in 1930, and consistency [[proofs]] for arithmetics restricted with respect to the [https://en.wikipedia.org/wiki/Induction induction axiom schema] were proved by Ackermann (1924), von Neumann (1927) and Herbrand (1931. Stronger logics, such as [https://en.wikipedia.org/wiki/Second-order_logic second-order logic], are not complete.

A consistency [[proof]] is a [[mathematical]] proof that a particular [[theory]] is consistent. The early [[development]] of mathematical [http://en.wikipedia.org/wiki/Proof_theory proof theory] was driven by the [[desire]] to provide finitary consistency proofs for all of mathematics as part of [http://en.wikipedia.org/wiki/Hilbert%27s_program Hilbert's program]. Hilbert's program was strongly impacted by [http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems incompleteness theorems], which showed that sufficiently strong [[proof]] theories cannot prove their own consistency (provided that they are in fact consistent).

A consistency [[proof]] is a [[mathematical]] proof that a particular [[theory]] is consistent. The early [[development]] of mathematical [https://en.wikipedia.org/wiki/Proof_theory proof theory] was driven by the [[desire]] to provide finitary consistency proofs for all of mathematics as part of [https://en.wikipedia.org/wiki/Hilbert%27s_program Hilbert's program]. Hilbert's program was strongly impacted by [https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems incompleteness theorems], which showed that sufficiently strong [[proof]] theories cannot prove their own consistency (provided that they are in fact consistent).

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 [http://en.wikipedia.org/wiki/Cut-elimination cut-elimination] (or equivalently the [http://en.wikipedia.org/wiki/Normalization_property normalization] of the [http://en.wikipedia.org/wiki/Curry-Howard 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.

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 [https://en.wikipedia.org/wiki/Cut-elimination cut-elimination] (or equivalently the [https://en.wikipedia.org/wiki/Normalization_property normalization] of the [https://en.wikipedia.org/wiki/Curry-Howard 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 in arithmetic==

==Consistency and completeness in arithmetic==

In theories of arithmetic, such as [http://en.wikipedia.org/wiki/Peano_arithmetic Peano arithmetic], there is an intricate [[relationship]] between the consistency of the [[theory]] and its completeness. A theory is complete if, for every formula φ in its language, at least one of φ or ¬ φ is a logical consequence of the theory.

In theories of arithmetic, such as [https://en.wikipedia.org/wiki/Peano_arithmetic Peano arithmetic], there is an intricate [[relationship]] between the consistency of the [[theory]] and its completeness. A theory is complete if, for every formula φ in its language, at least one of φ or ¬ φ is a logical consequence of the theory.

[http://en.wikipedia.org/wiki/Presburger_arithmetic Presburger arithmetic] is an [[axiom]] [[system]] for the natural numbers under addition. It is both consistent and complete.

[https://en.wikipedia.org/wiki/Presburger_arithmetic Presburger arithmetic] is an [[axiom]] [[system]] for the natural numbers under addition. It is both consistent and complete.

[http://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems Gödel's incompleteness theorems] show that any sufficiently strong effective theory of arithmetic cannot be both complete and consistent. Gödel's theorem applies to the theories of Peano arithmetic (PA) and [http://en.wikipedia.org/wiki/Primitive_recursive_arithmetic Primitive recursive arithmetic] (PRA), but not to Presburger arithmetic.

[https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems Gödel's incompleteness theorems] show that any sufficiently strong effective theory of arithmetic cannot be both complete and consistent. Gödel's theorem applies to the theories of Peano arithmetic (PA) and [https://en.wikipedia.org/wiki/Primitive_recursive_arithmetic Primitive recursive arithmetic] (PRA), but not to Presburger arithmetic.

Moreover, Gödel's second incompleteness theorem shows that the consistency of sufficiently strong effective theories of arithmetic can be tested in a particular way. Such a theory is consistent if and only if it does not prove a particular sentence, called the Gödel sentence of the theory, which is a formalized statement of the claim that the theory is indeed consistent. Thus the consistency of a sufficiently strong, effective, consistent theory of arithmetic can never be proven in that system itself. The same result is true for effective theories that can describe a strong enough fragment of arithmetic – including set theories such as [http://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory Zermelo–Fraenkel set theory]. These set theories cannot prove their own Gödel sentences – provided that they are consistent, which is generally believed.

Moreover, Gödel's second incompleteness theorem shows that the consistency of sufficiently strong effective theories of arithmetic can be tested in a particular way. Such a theory is consistent if and only if it does not prove a particular sentence, called the Gödel sentence of the theory, which is a formalized statement of the claim that the theory is indeed consistent. Thus the consistency of a sufficiently strong, effective, consistent theory of arithmetic can never be proven in that system itself. The same result is true for effective theories that can describe a strong enough fragment of arithmetic – including set theories such as [https://en.wikipedia.org/wiki/Zermelo%E2%80%93Fraenkel_set_theory Zermelo–Fraenkel set theory]. These set theories cannot prove their own Gödel sentences – provided that they are consistent, which is generally believed.

[[Category: Logic]]

[[Category: Logic]]