# Is it a bad idea to require a correctness proof as part of a computable real number?

At 30:42 of Norman Wildberger's Difficulties with real numbers as infinite decimals (II) lecture, he raises the question whether "certificates of boundedness" (of the runtime of the algorithm to compute a certain number of digits) should be part of a computable real number.

I thought the answer to that question would be clearly no. However, a similar idea occurs in section "2.2 Numbers as programs" on page 5 of Exact Real Com­puter Arithmetic with Con­tin­ued Frac­tions by Jean Vuillem­in, 1987. That paper appears to be quite good and very reasonable otherwise, so now I wonder whether I might be wrong here. Here is the reasoning:

Theorem 1 (Cantor) Let $$\mathcal R$$ denote the subset of $$\mathcal L$$-expressions which represent numbers, that is the computable reals expressed as programs in $$\mathcal L$$.

1. The set $$\mathcal R$$ is denumerable.
2. No algorithm can effectively enumerate all the elements of $$\mathcal R$$.

As equivalent to (2), we see that no algorithm can decide, in finite time, if an arbitrary $$\mathcal L$$-expression $$e$$ denotes a number, i.e., $$e \in \mathcal R$$. Therefore, since we cannot expect the computer to do it for us, we must provide a correctness proof with every real number definition, i.e., program.

My problem is that a correctness proof only makes sense after an axiom system has been specified. And I believe that for any reasonable axiom system, the ("extensional") set of computable real numbers which can be proven correct in that axiom system will be a proper subset of the ("extensional") set of all computable real numbers.

On the other hand, I might be wrong. For example, the ("extensional") set of languages defined by the provably polynomial time algorithms is identical to the ("extensional") set of languages defined by all polynomial time algorithms.

• In fact, if an axiom system for the correctness proof is given, then an algorithm can effectively enumerate the set of computable real numbers which can be proven correct in that axiom system by just searching for the correctness proof itself. Still, requiring a correctness proof seems to be done by some authors, so I must be missing something. – Thomas Klimpel Mar 17 at 15:05
• This is an interesting topic, but I'm a bit confused: what is the actual question here? (OK, the title does give a question, but it's fairly broad - what criteria are we using, exactly? - and I'm wondering if you have something more specific in mind.) – Noah Schweber Mar 18 at 4:56
• @NoahSchweber My question is: "Do I miss something here? If yes, what am I missing?" Things I could miss: Maybe I am not allowed to talk about the naive set of (computable) reals, but only about the corresponding set living in some given axiomatic theory like ZFC. Maybe some of my naive computable reals are uncomputable reals in ZFC, or even not reals at all in some model of ZFC. Or maybe I am actually right, and it is indeed a bad idea to require a correctness proof as part of a computable real number. – Thomas Klimpel Mar 18 at 8:07
• @NoahSchweber I guess I understand now what I am missing: Jean Vuillem­in wants his operations (addition, subtraction, multiplication, division) on his computable real numbers to produce numbers which can be proved to be valid, if one has access to proofs that the input numbers are valid. May sound trivial, but he also wants (and achieves) this for the case of 1/0 and 0/0. So he doesn't really care about some absolute proof of validity for a real number, despite the fact that his words say exactly this. – Thomas Klimpel Mar 21 at 7:44