there is an inconsistent formal system with fewer than 100 axioms in which all theorems with proofs of length smaller than BB(100) are consistent with each other. Why couldn’t PA be such a system?
I suspect that for most “naive” ways of constructing such a system X, the very long proof of inconsistency for X should reduce to a very short proof of inconsistency for X+Con(X), because the latter system should be enough to capture most “informal” reasoning that you used to construct X in the first place. The existence of such a proof wouldn’t imply the inconsistency of X directly (there are consistent systems X such that X+Con(X) is inconsistent, e.g. X=Y+not(Con(Y)) where Y is consistent), but if PA+Con(PA) were ever shown to be inconsistent, that would be highly suggestive and would cause me to abandon my intuitions expressed above.
But as far as we know now, PA+Con(PA) looks just as consistent as PA itself. Moreover, I think you can add a countable-ordinal pile of iterated Con’s on top and still get a system that’s weaker than ZFC. (I’m not 100% confident of that, would be nice if someone corrected me!)
So I’m pretty confident that PA is consistent, conditional on the statement “PA is consistent” being meaningful. Note that you need a notion of “standard integers” to make sense of the latter statement too, because integers encode proofs.
I suspect that for most “naive” ways of constructing such a system X, the very long proof of inconsistency for X should reduce to a very short proof of inconsistency for X+Con(X), because the latter system should be enough to capture most “informal” reasoning that you used to construct X in the first place. The existence of such a proof wouldn’t imply the inconsistency of X directly (there are consistent systems X such that X+Con(X) is inconsistent, e.g. X=Y+not(Con(Y)) where Y is consistent), but if PA+Con(PA) were ever shown to be inconsistent, that would be highly suggestive and would cause me to abandon my intuitions expressed above.
But as far as we know now, PA+Con(PA) looks just as consistent as PA itself. Moreover, I think you can add a countable-ordinal pile of iterated Con’s on top and still get a system that’s weaker than ZFC. (I’m not 100% confident of that, would be nice if someone corrected me!)
So I’m pretty confident that PA is consistent, conditional on the statement “PA is consistent” being meaningful. Note that you need a notion of “standard integers” to make sense of the latter statement too, because integers encode proofs.