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?