6

2

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?

flag
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
6 
 An inconsistent formal system can! – Qiaochu Yuan May 21 2011 at 7:34
1 
 @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
3 
 @Tom: doesn't Neel Krishnaswamis answer in the discussion you cite provide an answer? – Michael May 21 2011 at 8:20
show 3 more comments

closed as no longer relevant by Tom Ellis, Andrej Bauer, Dan Petersen, Qiaochu Yuan, Felipe Voloch May 21 2011 at 11:08

Browse other questions tagged or ask your own question.