## Can any formal system prove its own consistency? [closed]

My curiosity was piqued by this discussion:

http://mathoverflow.net/questions/9864/presburger-arithmetic

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?

-
Short answer: I don't know. Longer answer. I don't think anyone else knows either. Given the amount of time that has elapsed and the number of researchers interested in consistency results, I think we would have heard of such a theory by now. So I vote no. Gerhard "Ask Me About System Design" Paseman, 2011.05.21 – Gerhard Paseman May 21 2011 at 7:02
An inconsistent formal system can! – Qiaochu Yuan May 21 2011 at 7:34
@Qiaochu: your comment makes me realise that stating my question formally is going to be harder than I initially imagined ... – Tom Ellis May 21 2011 at 7:42
Poking around, it seems that Dan Willard has worked on this question, and as far as I can make out with my amateur understanding the answer is "yes": cs.albany.edu/FacultyStaff/profiles/willard.htm – Tom Ellis May 21 2011 at 7:47
@Tom: doesn't Neel Krishnaswamis answer in the discussion you cite provide an answer? – Michael May 21 2011 at 8:20