Changes

From Nordan Symposia
Jump to navigationJump to search
5,420 bytes added ,  19:07, 5 September 2010
Created page with 'File:lighterstill.jpgcenter|frame *[http://en.wikipedia.org/wiki/16th_century 1594] ==Definitions== *1a archaichttp://nordan.daynal.org/wiki/skins/c...'
[[File:lighterstill.jpg]][[File:Consistency.jpg|center|frame]]

*[http://en.wikipedia.org/wiki/16th_century 1594]
==Definitions==
*1a archaichttp://nordan.daynal.org/wiki/skins/common/images/button_link.png : condition of adhering [[together]] : firmness of [[material]] substance
:b : firmness of [[constitution]] or [[character]] : [[persistency]]
*2: [[degree]] of firmness, [[density]], viscosity, or resistance to movement or separation of constituent [[particles]] <boil the juice to the consistency of a thick syrup>
*3a : [[agreement]] or [[harmony]] of parts or features to one another or a whole : [[correspondence]]; specifically : [[ability]] to be asserted together without contradiction
:b : [[harmony]] of [[conduct]] or [[practice]] with [[profession]] <followed her own advice with consistency>
==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.

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.

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).

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.
==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.

[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.

[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.

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.

[[Category: Logic]]

Navigation menu