Predictability – Is it a bad idea to request a proof of correctness as part of a predictable real number?

At 30:42 of Norman Wildberger's difficulty with real numbers as an infinite decimal (II), he teaches the question of whether "certificates of limitation" (of the algorithm's running time for calculating a certain number of digits) should be part of a calculable number real number ,

I thought the answer to that question would definitely be no. However, a similar idea occurs in Section "2.2 Numbers as Programs" on page 5 of Exact Real Computer Arithmetic with Continued Fractions by Jean Vuillemin, 1987. This article seems to be pretty good and very reasonable otherwise, so I'm wondering if I could do this wrong here's the reasoning here:

Sentence 1 (Cantor) To let $ mathcal R $ denote the subset of $ mathcal L $Expressions that represent numbers, ie the calculable real ones, expressed as programs in $ mathcal L $,

  1. The sentence $ mathcal R $ is payable.
  2. No algorithm can effectively list all elements of $ mathcal R $,

As an equivalent to (2) we see that no algorithm can decide in finite time whether it is arbitrary $ mathcal L $-Expression $ e $ denotes a number, i. $ e in mathcal R $, Since we can not expect the computer to do this for us, we need to look at each definition of the real number; H. To the program, provide a proof of correctness.

My problem is that a proof of correctness only makes sense if an axiom system has been specified. And I believe that for any rational axiom system, the ("extensional") set of calculable real numbers that may prove correct in this axiom system is an appropriate subset of the ("extensional") set of all calculable real numbers ,

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