Ah! I get the point.

Because the discontinuity occurs at an un-constructible r, the constructible limit "process" of x approaching r, never includes r. So f(x->r) encounters a limit of 0. And 1 from the other side.

That does leaves the validity of defining continuity of constructible functions over constructible reals intact.

It is only a problem if un-constructible numbers are "brought" in.

Previously you stated:

> Basically all of calculus needs all the reals because if you don't you get some really pathological results.

This is then what I don't understand.

Why would un-constructible reals be needed?

I would agree that all constructible reals are needed (after all, constructible functions as a class are by definition, sensitive to constructible reals as a class).

But why would un-constructible reals be necessary for anything?

At best I can see them as a kind of contrivance that shortens some proofs, that could be made without them with more careful reasoning.

But ... ?

--

> However, (because of Cantor's diagonal argument) we know there infinitely more real numbers than constructible real numbers.

Cantor uses sleight of hand out of the gate. From out of nowhere, he postulates that there can be infinite digit numbers, without finite description.

That is really interesting thing to suggest.

Because until then, numbers were built up in steps, from the concepts of increment, repetition, and orthogonal units (to post-formalize the actual progression of informal to formal).

Constructibility (in practice and theory) was inherent in what it meant to "have" a number.

A number is a relationship. A relationship isn't a relationship because I can pick a name "r" and say it is a relationship.

But suddenly Cantor talks about infinite digit numbers with no expression. No defined relation. And then an (attempted) list of all of them.

So constructibility of numbers is abandoned as a precondition for his arguments. Before any point of diagonal incompleteness is made.

It gets worse. Even if we had access to magic oracles that will generate any number of un-constructible reals we desire, with any number of digits supplied, so we can add, subtract and compare them: The process would remain indistinguishable from the same process in which we are actually being given constructible numbers.

My conviction (very open to being shot down of course!) is that un-constructible reals are an interesting concept, and interesting to reason about as mathematical puzzles, perhaps good exercises for inspiring new proof tactics, but in direct relation to anything we do with "actual" real numbers, they are unnecessary.

Also, any actual reasoning about infinite information structures and higher order infinities is going to itself be isomorphic to a finite (or countably infinite) system with 1-to-1 behaviors not interpreted as about un-constructible things. Because anything we do, even reasoning about the un-constructible, remains a constructible domain.

If I am wrong, I would be very interested to understand why.

> That does leaves the validity of defining continuity of constructible functions over constructible reals intact.

What I think you're getting at is that even though my function f breaks what we think of as continuity of functions over the constructible reals, f is clearly un-constructible. So if we only do analysis using constructible functions, all is well.

I was thinking about how this works and trying to think of an example proof that doesn't work with only constructible reals, but actually the same proof basically works, so I'll just share that instead:

Intermediate value theorem: if f is continuous, f(a) is negative and f(b) is positive, then there is some c such that f(c)=0.

Proof for real functions: Define S = { x ∈ [a,b] : f(x) ≤ 0 }.

S is nonempty because a ∈ S (f(a) < 0).

S is bounded above by b, so S has a least upper bound c = sup S with c ∈ [a,b].

We claim f(c) = 0.

Suppose first that f(c) > 0. By continuity at c there is δ > 0 such that for all x with |x−c| < δ we have |f(x)−f(c)| < f(c). In particular for such x we get f(x) > 0 (since f(c) − |f(x)−f(c)| > 0). But then every x in (c−δ, c+δ)∩[a,b] is not in S, so there is no point of S greater than or equal to c−δ/2. That contradicts c being the least upper bound of S because then c−δ/2 would be an upper bound smaller than c. Hence f(c) ≤ 0.

Now suppose f(c) < 0. By continuity at c there is ε > 0 such that for all x with |x−c| < ε we have |f(x)−f(c)| < −f(c) (note −f(c) > 0). Then for such x we get f(x) < 0, so every x in (c, c+ε)∩[a,b] also satisfies f(x) ≤ 0 and hence belongs to S. But that gives points of S strictly greater than c, contradicting that c is an upper bound of S. Thus f(c) < 0 is impossible.

If we instead talk about constructible functions, note that f is constructible, so S is constructible, so c = sup S is constructible. We know that c is in the domain of f, and using the proof above we can show f(c)=0.

So maybe if we limit ourselves to constructible functions analysis works out. There are still two reasons why you might not want to do this. Adding a line at the end of every proof explaining why all the numbers you're talking about are constructible feels unnecessary when you can just talk about the reals. Secondly, (as far as I understand) its impossible to actually formalize our idea of constructible.