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

I think we can formalize constructible structures as any mathematical structure which can be uniquely defined by at least one finite sequence of symbols.

As far as not wanting to pedantically refer to "constructible reals", I agree that doesn't sound fun.

The better solution would be having a clear common pithy term for "unconstructible reals", for:

1. Teaching math related to numbers, until unconstructible reals or other structures had any relevance. I.e. most people never, ever.

2. For talking about algorithms, physics and other constructible structures, where the term reals is pervasivably used to mean constructible reals.

3. Most students get introduced to the fact that the cardinality of reals is greater than the cardinality of integers. But would be surprised, and get more use, out of knowing that the cardinality of instantiatable numbers (the ones they could define, calculate, measure or apply in virtually every situation but highly abstract math games), is EXACTLY the same as the integers.

Un-constructible structures are an interesting but exotic concept that shouldn't be riding around sereptitiously in common vocabulary.

A fair number of responses here involved confusion about what "reals" covers. And this is HN.