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