[egorelik]

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. (We can't prove they don't exist either, without making some strong assumptions).

[creata]

> 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]

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]

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]

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.

[aeneasmackenzie]

I hold that the discovery of computation was as significant as the set theory paradoxes and should have produced a similar shift in practice. No one does naive set theory anymore. The same should have happened with classical mathematics but no one wanted to give up excluded middle, leading to the current situation. Computable reals are the ones that actually exist. Non-computable reals (or any other non-computable mathematical object) exist in the same way Russel’s paradoxical set exists, as a string of formal symbols.

Formal reasoning is so powerful you can pretend these things actually exist, but they don’t!

I see you are already familiar with subcountability so you know the rest.

[foxes]

What do you really mean exists - maybe you mean has something to do with a calculation in physics, or like we can possibly map it into some physical experience?

Doesn't that formal string of symbols exist?

Seems like allowing formal string of symbols that don't necessarily "exist" (or well useful for physics) can still lead you to something computable at the end of the day?

Like a meta version of what happens in programming - people often start with "infinite" objects eg `cycle [0,1] = [0,1,0,1...]` but then extract something finite out of it.

[aeneasmackenzie]

They don’t exist as concepts. A rational number whose square is 2 is (convenient prose for) a formal symbol describing some object. It happens that it does not describe any object. I am claiming that many objects described after the explosion of mathematics while putting calculus on a firmer foundation to resolve infinitesimals do not exist.

List functions like that need to be handled carefully to ensure termination. Summations of infinite series deal are a better example, consider adding up a geometric series. You need to add “all” the terms to get the correct result.

Of course you don’t actually add all the terms, you use algebra to determine a value.

[lg5689]

You can go farther and say that you can't even construct real numbers without strong enough axioms. Theories of first order arithmetic, like Peano arithmetic, can talk about computable reals but not reals in general.