My curiosity was piqued by this discussion:

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.

Is there any formal system that can prove its own consistency?

PA is essentially too *strong* 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.

(From my limited understanding) Presburger arithmetic is too *weak* to prove its own consistency. Indeed the question of its consistency is not representable within it.

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 *too* powerful to allow the second incompleteness theorem to take over?

inconsistentformal system can! – Qiaochu Yuan May 21 '11 at 7:34