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.