I have absolutely no idea how physical reality can contradict a statement about a formal symbol game.
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.
> 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".
> 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.
It would only contradict physical reality if a machine to calculate that algorithm failed to solve the EXPTIME-hard problem as promised. And if it failed to do that, I am confident that the problem is a mistake in the logic theory proof.
As for your long quote from Hilbert, I understand it very differently from you. He is saying that our interest in ideal mathematics starts with real mathematics. But ideal mathematics is something to engage with on its own terms, whether or not it corresponds with anything real.
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.
> 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 think what the poster above means is that any formal system in which, say, 1 + 1 = 75, even if internally consistent as a set of symbols, would not be considered a valid logical foundation for mathematics by Hilbert, because it directly contradicts physical reality. Of course, this is under the assumption that 1 and + and 75 are meant to have their usual meanings, not that we've redefined the + operator to mean "the 73rd successor", nor that we're operating in some exotic numerical base where 75 is just a different set of symbols to describe the number 2.