> which is that mathematicians compute /all sorts/ of uncomputable systems, with no apparent restriction

You are flattering us, but that's not actually true. We already have lots of trouble with proving (which is the same as computing, essentially) many computable things as it is. It is only occasionally that we can make progress on some uncomputable problem, and it's always because of making use of some properties very specific to said problem. The point of Rice theorem is that there's no universal method to solve any problem without any concern for the guts of that problem, and that's true: when mathematicians or computer scientists are proving that some computer program halts, they don't apply the same general machine, but instead they try to figure out some "tricks" based on the particular situation at hand, which will not generalize to every conceivable problem.

> all mathematics greater than or equal to number theory is uncomputable

That's not what Godel's Incompleteness Theorem says though. Nor would I agree that "mathematicians compute /all sorts/ of uncomputable systems, with no apparent restriction."

It is hard to describe the behavior of real-world mathematicians since that is the realm of psychology rather than logic or mathematics, but if we stick to the realm of idealized proofs, it's clear that we are only ever computing over computable descriptions of uncomputable systems (which is totally fine and something we do all the time!).

For example, the first-order theory of the real numbers (real closed fields) is a classic example of a complete and decidable theory. Every first-order statement in that theory can be proved or disproved in an automated fashion.

Yet how can this situation persist for the real numbers, entities which we clearly know are non-computable? Well the theory of real closed fields is capable of only describing a subset of the properties of the real numbers. It is worth emphasizing that this is a subset! Those properties in the theory of real closed fields apply perfectly fine to the real numbers. They just don't capture all its properties.

So what about the other properties of the real numbers that, for example, make up the field of analysis? Well we can prove those in a larger theory, e.g. ZFC. And again the proofs in ZFC are computable objects, although ZFC itself is no longer decidable. So again the description of the real numbers is a computable thing, even if now we don't know how to computably enumerate all of its consequences (but again we know how to enumerate subsets of them!).

Now does ZFC completely describe the reals? This depends on whether you're a mathematical Platonist or not. Do you believe in the notion of the one, true set of real numbers that exist on a Platonic plane independently of our axioms about them? That is there are no "independent" theorems, only theorems for which we haven't found the best way of grasping their Platonic truth? Then no ZFC does not completely describe the reals either as a result of Godel's incompleteness theorem.

Alternatively do you believe that the real numbers are an artificial mathematical construction which can have different properties depending on which axioms you are willing to admit? Then there will be properties of the real numbers which are independent of ZFC as a result of Godel's incompleteness theorems.

> Alternatively do you believe that the real numbers are an artificial mathematical construction which can have different properties depending on which axioms you are willing to admit? Then there will be properties of the real numbers which are independent of ZFC as a result of Godel's incompleteness theorems.

This is actually not correct. The propositions that are undecidable are NOT AT ALL connected to the propositions that are independent. Things like the CH or Axiom of Determinacy have to do with providing a definition to things that have no defined truth value. But the undecidable propositions are already true or false they just can't be listed or computed in any meaningful fashion.

> The propositions that are undecidable are NOT AT ALL connected to the propositions that are independent.

I'm not quite sure what you mean by undecidable propositions, but I assume it to mean something like the following?

Propositions which must be true or must be false (i.e. are satisfied/not satisfied respectively by all models which satisfy the overall theory), but for which there is no finite proof that they hold.

In contexts where Godel's Completeness theorem (not incompleteness theorem) holds undecidable propositions are exactly independent propositions. The two are one and the same. This is in fact an equivalent restatement of the Completeness theorem (which holds for contexts involving most common mathematical theories such as ZFC and Peano Arithmetic). In fact in such contexts, statements such as Con(PA) which is informally "the axioms of Peano Arithmetic are consistent" are in fact independent propositions and there are models of Peano Arithmetic that satisfy both Con(PA) and Not(Con(PA)).

What about contexts where the Completeness theorem fails (e.g. the second-order equivalents of those theories)? For example, what about CH in second-order ZFC (which is categorical under full semantics, i.e. has no independent statements and only undecidable ones?). In those contexts independence gets weird, especially in the way I think you're using it here. Usually we say that if a sentence s is independent of theory T then both s and Not(s) are consistent with T. However, consistency is phrased in terms of proofs. That is s is consistent with T if there is no finite proof in T of Not(s).

So if there are statements that are undecidable, but not independent (on the other hand all independent statements must be undecidable, although their independence may itself be decidable), we are effectively saying there exist consistent theories which have no mathematical model that satisfies them.

But this is a very weird way of doing mathematics (which is why most logicians are wary of using systems where the Completeness theorem fails to hold as foundations for mathematics). In particular it means that simply showing that a list of axioms is consistent is insufficient to allow its use. You must appeal to some other force to show that your mathematical theory is "valid" and allowed to be used.

But that's not a bar that modern mathematics tries to clear. Modern mathematicians do not try to justify the "validity" of mathematical theories beyond showing (or assuming) consistency.

For example, mathematicians generally don't hem and haw over whether the complex numbers "exist" in some real sense. They just show that they are a consistent extension of the real numbers and move on and use them.

To take a step back, the assertion that there are fundamentally undecidable mathematical propositions in the real sense you're laying out (as opposed to more formal treatments of truth in model theory) is a statement of the Platonist school of mathematical philosophy. Which is totally fine, but it is a statement of philosophy at the end of the day, rather than one of logic.

> To take a step back, the assertion that there are fundamentally undecidable mathematical propositions in the real sense you're laying out (as opposed to more formal treatments of truth in model theory) is a statement of the Platonist school of mathematical philosophy.

To go one step forward, these undecidable/uncomputable statements are computed by humans all the time, which makes the Platonist school of mathematics much more than an intellectual curio.

> these undecidable/uncomputable statements are computed by humans all the time

This is a far stronger statement than I think even Platonists would accept. What examples of non-computable statements that are computed by humans do you have in mind?

Even putting on my Platonist hat (which I'll wear for the rest of this reply), I would still argue, in line with xyzzyz's comment, that at most humans deal with computable descriptions of non-computable things. For example, the description of the real numbers is computable even if the real numbers themselves are not. Likewise even if the real numbers are not computable, we can only ever work with computably-definable (indeed only finitely definable) real numbers rather than arbitrary real numbers.

To use the map-territory analogy, while the territory is the thing we care about, the only things we can work with, manipulate, and compute are computable maps.

For example Chaitin's Constant is a non-computable real number. However, we never work with Chaitin's Constant directly, but rather with our finite description of it, from which we deduce all sorts of other facts.

There are therefore many things about Chaitin's Constant we will never know. But that is the Platonist's lot in life.

As an aside, there's in fact a formalization of this that states that a mathematical universe consisting solely of finitely definable entities and nothing else is perfectly reconcilable with ZFC. See https://mathoverflow.net/questions/44102/is-the-analysis-as-...). Now as I continue to wear my Platonist hat I don't believe for a second that this is in fact how the mathematical universe actually operates, but it is a good explanation for why it is beyond the mathematical abilities of humans to distinguish between this definable universe and the real universe we live in.