Mathematicians consider that there are "true" propositions of the form procedure P on input x does not halt but the propositions are not provable in ZFC.
Mathematicians consider them to be true because they are provably true, i.e., they hold in the unique up to isomorphism model of the theory Ordinals, which subsumes ZFC.
Ok, so Ordinals is the new foundation of mathematics so to speak? Doesn’t that mean that all of mathematics can be formalized within this Ordinals theory?
All of classical mathematics before 1930 can be formalized in the the theory Ordinals. However, formalizing digital computation requires the theory Actors, which is axiomatized here:
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.
The strongly-typed higher-order theory Ordinals is consistent because it has a unique up to isomorphism model by a unique isomorphism. Consequently, ZFC is consistent because it is a special case of the theory Ordinals.
This is nonsense. It's true; but nonsense nevertheless. Because it gives the misleading impression that you can only prove the consistency of a formal system using a "stronger" system. But that's quite wrong: it only needs to be a different formal system.
Mistake is often made that ZFC is the be-all and end-allultimate foundation of mathematics. Unfortunately, 1st-order ZFC (often referred to as just "ZFC") is a very weak theory.
For example, if O is the type of the ordinals, then
O
Boolean // type of all functions from ordinals into type Boolean
cannot be represented in ZFC because it does not exist in the cumulative hierarchy of sets.
No, I mean, why me, specifically? Did I accidentally say something to give the impression I find your odd rantings interesting? Because if I did, please let me know so I can correct the misunderstanding.
Can anybody give an example of mathematics that mathematicians consider “true”, but which is not provable in ZFC?
If no such mathematics exist, then mathematics is essentially just a game of symbol manipulation, right?