most recent 30 from http://mathoverflow.net 2013-06-19T23:55:12Z http://mathoverflow.net/feeds/question/65626 http://www.creativecommons.org/licenses/by-nc/2.5/rdf http://mathoverflow.net/questions/65626/can-any-formal-system-prove-its-own-consistency Tom Ellis 2011-05-21T06:50:52Z 2011-05-21T06:50:52Z

<p>My curiosity was piqued by this discussion:</p> <p><a href="http://mathoverflow.net/questions/9864/presburger-arithmetic" rel="nofollow">http://mathoverflow.net/questions/9864/presburger-arithmetic</a></p> <p>I'll state this question loosely (rather than formally in terms of first-order logic or another formal framework) but I think it's clear what I'm asking.</p> <p>Is there any formal system that can prove its own consistency?</p> <p>PA is essentially too <em>strong</em> to prove its own consistency. The choice of axioms makes the theory "too complicated" a structure for it to be able to deal with itself in this way.</p> <p>(From my limited understanding) Presburger arithmetic is too <em>weak</em> to prove its own consistency. Indeed the question of its consistency is not representable within it.</p> <p>Is there something in the middle? A system powerful enough to represent a formula (or some other formal construct) stating that it itself is consistent, yet not <em>too</em> powerful to allow the second incompleteness theorem to take over?</p>