[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.