Mathematicians have been dealing with this problem in concrete ways for longer than implied. For instance, the necessity of the parallel postulate for Euclidian geometry and the existence of non-Euclidean geometries where it doesn't hold were demonstrated in the 19th century. The question of how many and which axioms are required as the basis of a field of mathematics has long been known to be a valid, meaningful question.
What Gödel proved is that in the formal systems we use to model mathematical propositions and proofs, there is no finite number of axioms that enable you to prove or disprove all of the propositions that can be formulated. For someone who grew up in the post-Gödel world, this isn't shocking at all and looks like a natural progression from previous results. You need a certain number of postulates. To get Euclidean geometry, for example, you need the parallel postulate. It's natural to ask how many postulates you need to decide all interesting mathematical questions, and there's no reason to assume the answer to that question is finite. Apparently, that attitude reflects a lot of hindsight bias, but there is no way for us to experience the shock of Gödel's work the way it was experienced by mathematicians at the time, since the books we learn from now are written by mathematicians who have already digested Gödel's discoveries.
As he posted on the FOM mailing list earlier this month, the 'final' version of Friedman's book on boolean relation theory is now up on his website. [1] It clocks in at around 900 pages. Not for the faint of heart.
For those interested, the crux of Friedman's argument for pursuing examples of "Concrete" Incompleteness is:
> The second rationale for pursuing Concrete Mathematical
Incompleteness preserves ZFC as the ambitious target. The
idea is that normal mathematical activity up to now
represents only an infinitesimal portion of eventual
mathematical activity. Even if current mathematical
activity does not give rise to Concrete Mathematical
Incompleteness from ZFC, this is a very poor indication of
whether this will continue to be the case, particularly far
out into the future.
tldr; Gödel proved the incompleteness of finite axiomatizations of arithmetic. Further more there is no maximum set of unprovable sentences in arithmetic. Therefore, there must be interesting and unprovable sentences in arithmetic.
The article discusses a couple such sentences but unfortunately does not actually state the sentences, which is the interesting part.
Edit: unsurprisingly: "The extent to which we have concrete incompleteness and what the wider implications are, will not be clear for hundreds of years, if not longer." -- Friedman
I'm curious: If you add a new axiom in order to make a undecidable proposition decidable, will this new axiom add more than one undecidable proposition, or is the number of new undecidable propositions unknown? Or are there infinitely undecidable propositions for every set of rules?
If the former is true, couldn't we theoretically just apply axioms in order to solve undecidable propositions which have a practical application if solved? Or will it practically be hard to find these axioms?
It's been a long time since I had my Theory of Computation class, but as I recall, the proof that there are computationally undecidable questions uses the same diagonalization technique[1] used to demonstrate that the real numbers are not countably infinite.
The same technique can be used to show there are still computationally undecidable questions if you have a Turing Machine with an Oracle.
This proof technique suggests not only are there undecidable questions, there are uncountably many of them. Even if you have an Oracle.
It's more like this. You can prove more theorems by adding axioms, but if you add too many, then you might get an inconsistent proof system (containing undiscovered contradictions). Because of this, mathematicians are extreme conservatives when it comes to adding axioms, and if they ever got to that point they would stop believing they were doing mathematics.
What Gödel proved is that in the formal systems we use to model mathematical propositions and proofs, there is no finite number of axioms that enable you to prove or disprove all of the propositions that can be formulated. For someone who grew up in the post-Gödel world, this isn't shocking at all and looks like a natural progression from previous results. You need a certain number of postulates. To get Euclidean geometry, for example, you need the parallel postulate. It's natural to ask how many postulates you need to decide all interesting mathematical questions, and there's no reason to assume the answer to that question is finite. Apparently, that attitude reflects a lot of hindsight bias, but there is no way for us to experience the shock of Gödel's work the way it was experienced by mathematicians at the time, since the books we learn from now are written by mathematicians who have already digested Gödel's discoveries.