Comment by btilly
I believe that you are misrepresenting Hilbert here.
If ZFC led to a result that doesn't agree with physical reality, Hilbert would not reject that result. Instead, at worst, he would simply move it from the category of being a real formula, to being an ideal formula. For example, Euclid's geometry doesn't agree with physical reality. Therefore it is an ideal formula, not a real formula. And yet we do not reject this geometry from mathematics.
But the distinction between real and ideal is a question for physics. It is not a question that mathematicians need worry about. The questions that mathematicians need worry about are entirely those which are internal to the formal game.
> Instead, at worst, he would simply move it from the category of being a real formula, to being an ideal formula.
No. No result, either ideal or real, may contradict reality (it's just that since infinitary statements do not describe reality, they obviously cannot contradict it). You can think about it like this: According to Hilbert, a valid mathematical foundation is any logical theory that is a conservative extension of reality. ZFC, constructive foundations, and ultrafinitist foundations all satisfy that, so they would all be valid foundations according to that principle.
> For example, Euclid's geometry doesn't agree with physical reality.
It may not describe physical reality, but it doesn't contradict it.
> But the distinction between real and ideal is a question for physics. It is not a question that mathematicians need worry about. The questions that mathematicians need worry about are entirely those which are internal to the formal game.
Not only does that disagree with Hilbert's formalism, it also disagrees with constructivism. The question of the philosophy of mathematics is precisely what, if anything, does mathematics describe beyond symbols.