Which is a "stronger" theory than ZFC; but you can also prove ZFC consistent in a system consisting of ZFC plus the axiom that "ZFC is consistent"; or indeed, in weaker theories than ZFC, augmented with the axiom that "ZFC is consistent".
Doesn’t your example of an axiom that “ZFC is consistent” show of how little use proofs within stronger systems are? I at least feel tempted to say that proofs of ZFCs consistency within stronger systems tell you nothing about ZFCs consistency.
They most certainly do, though! They do tell you something about the consistency of ZFC; they tell you that if the system you're working in is consistent, then so is ZFC. Is that not worth knowing?
It does sound a bit like you want something out of formal systems that they just can't give you, which is "absolute" truth.
edited to add: It's also worth noting that very, very few mathematicians care about actually formalising proofs in a formal system - it's a niche area. The vast majority of mathematicians go on about their business without giving much thought to ZFC and its axioms at all.
Many can't even name them all. (I know this, because they are quite surprised when you tell them what some of the axioms are. Especially the Axiom of Infinity.) Lol, I probably can't either,I suspect I would miss a few if I did it off the top of my head.
I don’t think I want more from formal systems than they can offer. I definitely don’t think of truth as “absolute”.
I think it’s actually the opposite: I’m skeptical of the “absolute” and almost mystical truth that some mathematicians seem to ascribe to mathematics. Do you believe in it? :)
So all of mathematics can never be formalized? And this is not just a question of effort and difficulty, it’s a fundamental philosophical limit of some sort?
If so, why should I believe that? What’s the evidence?
Of course, adding the axiom ZFC is consistent to the theory ZFC does _not_ produce a convincing proof of the consistency of ZFC!
The theory Ordinals has a convincing proof of consistency because the theory has a provably unique up to isomorphism model. Consequently, ZFC must also be consistent because it is a special case of the theory Ordinals.
