> The idea is we can't actually prove a non-computable real number exists without purposefully having axioms that allow for deriving non-computable things.

Sorry, what do you mean?

The real numbers are uncountable. (If you're talking about constructivism, I guess it's more complicated. There's some discussion at https://mathoverflow.net/questions/30643/are-real-numbers-co... . But that is very niche.)

The set of things we can compute is, for any reasonable definition of computability, countable.

▲

egorelik 3 hours ago | parent [-]

I am talking about constructivism, but that's not entirely the same as saying the reals are not uncountable. One of the harder things to grasp one's head around in logic is that there is a difference between, so to speak, what a theory thinks is true vs. what is actually true in a model of that theory. It is entirely possible to have a countable model of a theory that thinks it is uncountable. (In fact, there is a theorem that countable models of first order theories always exist, though it requires the Axiom of Choice).

▲

creata 3 hours ago | parent [-]

I think that what matters here (and what I think is the natural interpretation of "not every real number is computable") is what the theory thinks is true. That is, we're working with internal notions of everything.

	▲	egorelik 2 hours ago \| parent [-]
		I'd agree with that for practical purposes, but sometimes the external perspective can be enlightening philosophically. In this case, to actually prove the statement internally that "not every real number is computable", you'd need some non-constructive principle (usually added to the logical system rather than the theory itself). But, the absence of that proof doesn't make its negation provable either ("every real number is computable"). While some schools of constructivism want the negation, others prefer to live in the ambiguity.