Let me be more explicit about the meaning of "meaningful". Consider the two well known theoremsWhat theorem are you talking about in (2) here? The usual proof of the consistency of PA does *not* assume con(ZF). This was pointed out by me in an earlier article in this thread (which you may have missed since I haven't seen a followup to it by you).(1) con(ZF) implies con(ZFC)
(2) con(ZF) implies con(PA)
If you can't even get your facts straight, your philosophical arguments lose what force they might otherwise have had.
You've alluded to the "usual" proof of con(PA) but have not specified the formal system within which this "usual" proof resides. Since there are infinitely many possibilities, I'm not able to guess which specific one you have in mind.
In general terms, if there exists a proof of con(PA) within a formal system X, then we have the meta-theorem { con(X) implies con(PA) }, so you can replace X with whatever formal system you consider to be the "usual" one for proofs of PA. The meaningfulness of such a theorem depends on our perception of the relative soundness of the systems X and PA. I assert that no system X within which con(PA) can be proved is evidently more consistent that con(PA) itself.
Here's a related quote from "Mathematical Logic", 2nd Ed, by H. D. Ebbinghaus, J. Flum, and W. Thomas, Springer-Verlag, 1994:
"The above argument [Goedel's 2nd Thm] can be transferred to other systems where there is a substitute for the natural numbers and where R-decidable relations and R-computable functions are representable. In particular, it applies to systems of axioms for set theory such as ZFC... Since contemporary mathematics can be based on the ZFC axioms, and since...the consistency of ZFC cannot be proved using only means available within ZFC, we can formulate [this theorem] as follows: If mathematics is consistent, we cannot prove its consistency by mathematical means."I wanted to include this quote because every time I say there is no meaningful formal proof of the consistency of arithmetic (PA), someone always says "oh yes there is, just work in ZFC, or ZF, or PA+transfinite_induction, or PA+primitive_recursive_functionals, or PA+con(PA), or just use the "usual" proof, or (as Ben Tilly advises) just stop and think about it!" But none of these proposed "proofs" really adds anything to the indubitability of con(PA). Of course, it's perfectly acceptable to say "I'm simply not interested in the foundational issues of mathematics or in the meaning of consistency for formal systems". However, disinterest should not be presented as a substitute for proof.
... are we really justified in asserting that EVERY one of the infinitely many paths from every premise to its evaluation gives the same result?If you allow associativity of modus ponens, then there is essentially only one proof of any classical formula.
The unmeasured application of the modus ponens (rule of detachment) is precisely what misleads people into thinking that a formal system must be either absolutely consistent or total gibberish. Then, when they consider systems such as naive set theory, PA, or ZFC, which are clearly not total gibberish, they conclude that they must be absolutely consistent.