1) (By Goedel's) One can not prove, in PA, a formula that can be interpreted to express the consistency of PA. (Hopefully I said it right. Specialists correct me, please). 2) There are proofs (although for the purpose of this question I should putt it in quotations marks) of the consistency of PA.

The **questions** are:
A) Is it the consistency of PA still a mathematical question that can be considered open?
B) Is it a mathematical question? (To this I dare to say that it is a mathematical question. Goedel himself translated it into a specific formula, but then I have question C)
C) Is it accepting the proofs of the consistency of PA as conclusive a mathematically justified act or an act of taking a philosophical stance?

**Motivation:** There is a discussion in the mailing list FOM (Foundations Of Mathematics) about this topic, in part motivated by this talk link text . I thought a discussion about this fundamental matter concerns most mathematicians and wanted to bring it to a wider audience.

**Edit:** It is simple. Either:
1) Consistency of PA is proved and has a proof (as claimed by some in FOM) as valid as any other theorem in math, or
2) On top of the existing proofs a philosophic choice is needed (which explains the length of the discussions in FOM, justifies closing this question but contradicts what is being claimed emphatically by some in FOM)

But you see. If 1) is the case then there is no need for the lengthy discussions and this is a concrete math question as any other, terminating with a proof.

........................................................................................

**Edit 2:** Thank you all. Although I had seen some of these arguments at FOM now I think I have my ideas more organized and I can make my question more concrete. I would like to try to put aside what involves 'believes'. In, I think, all the answers shown there has been this action entering the argument quite soon, e.g. In Chow's: (approx.) If you believe in the existence of the naturals then con(PA) follows. In Friedman's (approx.) If you believe in (About a dozen Basic axioms) + (1/n subsequences) then con(PA) follows.

I want to put aside that initial action because (1): It is a philosophical question and that is not what I want to discuss, (2): Because of: If I believe (propositional logic) + (p/-p) then I believe ... for example (everything you can say) and maybe (3): Because I, personally, don't do math to believe what I prove. When I show P->Q, in a sequence of self imposed constrained steps I don't do it with the purpose of showing that, and at the end I don't have a complete conviction that, Q is a property of whatever could be a real world. But that is just philosophy and philosophy allows for any sort of choices. That is why I want to put it aside, at least until the moment in which it is inevitably needed.

**My question is:** Is any of the systems that prove con(PA) a system that has itself been proven consistent?

Why to ask this question? Regardless of how your feelings are about the ontological nature of what you prove. We can say that, since an inconsistent system proves everything, a consistent system is a bit more interesting for not doing so. At least if it is because there is not always a proof in which you use modus ponens twice (after you have found p/-p) for everything that you want to prove.

I guess that also, to answer the question above, it should be clarified what to accept for a consistency proof. Let's leave it kind of open and just try to delay the need for a philosophic stance as much as possible.

11more comments