........................................................................................
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.
