Take the 2-minute tour ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

My curiosity was piqued by this discussion:

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?

share|improve this question

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

This question is unlikely to help any future visitors; it is only relevant to a small geographic area, a specific moment in time, or an extraordinarily narrow situation that is not generally applicable to the worldwide audience of the internet. For help making this question more broadly applicable, visit the help center.If this question can be reworded to fit the rules in the help center, please edit the question.

    
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 '11 at 7:02
7  
An inconsistent formal system can! –  Qiaochu Yuan May 21 '11 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 '11 at 7:42
1  
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 '11 at 7:47
3  
@Tom: doesn't Neel Krishnaswamis answer in the discussion you cite provide an answer? –  Michael Bächtold May 21 '11 at 8:20

Browse other questions tagged or ask your own question.