> And if it failed to do that, I am confident that the problem is a mistake in the logic theory proof.

You can axiomatically add oracles without introducing logical inconsistencies. It is commonly done in complexity theory. The "mistake" is in interpreting such results as directly corresponding to the real world (same as interpreting 2 + 1 = 0 in modular arithmetic as if it were saying something about natural numbers). That is Hilbert's point: we need to be clear about how we map certain mathematical statements to the real world, and "to make it a universal requirement that each individual formula then be interpretable by itself is by no means reasonable", i.e. even when we're clear about such a mapping, it is not a requirement that every forumla had such a mapping. Or, perhaps more clear, Hilbert's point is that if in a logical theory not every formula can be assigned a "real meaning", that does not invalidate assigning real meaning to some formulas.

> Basically he's just saying, "Math is a formal game. People got interested in this game because part of the game corresponds to things we experience in reality." But that doesn't mean that the game itself depends in any way upon physical reality - it exists in its own terms.

He is very explicit that he is not saying that about the "real" propositions. He calls them "contentual", as in carrying content beyond the symbols. From the same talk:

If we now begin to construct mathematics, we shall first set our sights upon elementary number theory; we recognize that we can obtain and prove its truths through contentual intuitive considerations. The formulas that we encounter when we take this approach are used only to impart information.

He is very clear that the justification for the use of formulas that are "just a symbols game" is that they are consistent with formulas that are contentual and are not just a symbols game. That is the debate between Hilbert and Brouwer, or formalism and intuitionism: whether or not all formulas must have an intuitive meaning ("content"). In formalism, not all of them must.

It is precisely because Hilbert's justification was based on consistency, as without it, "real" propositions could be wrong, that the incompleteness results made that justification unprovable.

> I have absolutely no idea how physical reality can contradict a statement about a formal symbol game.

Of course it can! For example, if some logic theory contains the theorem that a particular realisable polynomial-time algorithm that can solve an EXPTIME-hard problem, that would contradict physical reality.

I should clarify that when I talk about "physical reality" that's shorthand for things that are, at least in principle, verifiable using physical means.

> I am also convinced that what you are saying is not what Hilbert actually meant. But he died before I was born, so I can't ask him. Besides, I don't speak German.

Ok, but if you're not sure what a certain philosophical position is, surely you cannot find fault with it. But I was able to locate my Heijenoort, so we can try, assuming you trust Heijenoort's translation.

So here's just a tidbit from Hilbert's 1925 "On The Infinite" (Heijenoort p.367):

And the net result is, certainly, that we do not find anywhere in reality a homogeneous continuum that permits of continued division and hence would realize the infinite in the small. The infinite divisibility of a continuum is an operation that is present only in ourthoughts; it is merely an idea, which is refuted by our observations of nature and by the experience gained in physics and chemistry.

And here are parts of Hilbert, 1927, "The foundations of mathematics" (Heijenoort p.464):

All the propositions that constitute mathematics are converted into formulas, so that mathematics proper becomes an inventory of formulas.

...even elementary mathematics contains, first, formulas to which correspond contentual communications of finitary propositions (mainly numerical equations or inequalities, or more complex communications composed of these) and which we may call the real propositions of the theory, and, second, formulas that -just like the numerals of contentual number theory - in themselves mean nothing but are merely things that are governed by our rules and must be regarded as the ideal objects of the theory.

These considerations show that, to arrive at the conception of formulas as ideal propositions, we need only pursue in a natural and consistent way the line of development that mathematical practice has already followed till now.

... Now the fundamental difficulty that we face here can be avoided by the use of ideal propositions. For, if to the real propositions we adjoin the ideal ones, we obtain a system of propositions in which all the simple rules of Aristotelian logic hold and all the usual methods of mathematical inference are valid.

... To be sure, one condition, a single but indispensable one, is always attached to the use of the method of ideal elements, and that is the proof of consistency; for, extension by the addition of ideal elements is legitimate only if no contradiction is thereby brought about in the old, narrower domain, that is, if the relations that result for the old objects whenever the ideal objects are eliminated are valid in the old domain.

... To make it a universal requirement that each individual formula then be interpretable by itself is by no means reasonable; on the contrary, a theory by its very nature is such that we do not need to fall back upon intuition or meaning in the midst of some argument. What the physicist demands precisely of a theory is that particular propositions be derived from laws of nature or hypotheses solely by inferences, hence on the basis of a pure formula game, without extraneous considerations being adduced. Only certain combinations and consequences of the physical laws can be checked by experiment just as in my proof theory only the real propositions are directly capable of verification.

The value of pure existence proofs consists precisely in that the individual construction is eliminated by them and that many different constructions are subsumed under one fundamental idea, so that only what is essential to the proof stands out clearly; brevity and economy of thought are the raison d'être of existence proofs.

In other words, "ideal" propositions may mean nothing in and of themselves but they are valid as long as they are a conservative extension of the "real" propositions (the narrower domain), which are necessarily meaningful as they are "directly capable of verification".

> 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.

> Some of the humans who have thought about it do reject them.

I think they reject them only if they misrepresent Hilbert's formalism, because formalism does not assign them any meaning of truth beyond the symbolic. It makes no statement that could be rejected: a mathematical theorem that proves a set "exists" does not necessarily make any claim about its "actual" existence (unlike, say, Platonism). You asked in what sense does such a set exist, and Hilbert would say, great question, which is why I don't claim there necessarily is any such sense.

What those who reject Hilbert's formalism reject is the validity of a system of mathematics where only some but not all propositions are "externally" meaningful, but such a rejection, I think, can only be on aesthetic grounds, because, again, for Hilbert, all "valid" foundations must agree with physical reality when it comes to statements that could be assigned physical meaning. If ZFC led to any result that doesn't agree with physical reality, Hilbert would reject it, too. But it hasn't yet.

I can't locate my Heijenoort right now, but here's a description from the Stanford Encyclopedia of Philosophy [1] (which points to Heijenoort):

The analogy with physics is striking... In the second half of the 1920s, Hilbert replaced the consistency program with a conservativity program: Formalized mathematics was to be considered by analogy with theoretical physics. The ultimate justification for the theoretical part lies in its conservativity over “real” mathematics: whenever theoretical, “ideal” mathematics proves a “real” proposition, that proposition is also intuitively true. This justifies the use of transfinite mathematics: it is not only internally consistent, but it proves only true intuitive propositions (and indeed all, since a formalization of intuitive mathematics is part of the formalization of all mathematics).

In 1926, Hilbert introduced a distinction between real and ideal formulas. This distinction was not present in 1922b and only hinted at in 1923. In the latter, Hilbert presents first a formal system of quantifier-free number theory about which he says that “The provable formulae we acquire in this way all have the character of the finite”

In other words, Hilbert does not require assigning any sense of truth beyond the symbolic one to those mathematical statements that do not correspond to physical reality, but those statements that can correspond to physical reality (i.e. the "real formulas") must do so, and those "real formulas" are meaningfully true beyond the symbols.

The earlier formalism (mathematics is just symbols) could no longer be justified after Gödel, as consistency was its main justification.

If anything, I think it's constructivism that suffers from a philosophical issue in requiring meaning that isn't physically realisable -- unlike ultrafinitism, for example. Personally, I find both Hilbert's formalism and ultrafinitism more philosophically satisfying than constructivism, as they're both rooted in physical reality, whereas constructivism is based on "computation in principle" (but not in practice!).

> As for what most people think about the philosophical implications, nobody should be expected to have any meaningful philosophical opinions about topics that they have not yet tried to think about

I mean people who have thought about it.

[1]: https://plato.stanford.edu/entries/hilbert-program/