Comment by pron
> 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.