> In article > <email@example.com>, > WM <firstname.lastname@example.org> wrote: > >> On 1 Mai, 11:15, Dan <dan.ms.ch...@gmail.com> wrote: >> > > It is necessary for Cantor's proof. Unless every digit exists on the >> > > diagonal, the diagonal number is undefined in an undefined list. But >> > > that is Cantor's claim: forall n : a_nn =/= d_n. >> > >> > It exists "as formula" , whether or not you know the formula . >> >> There are only countably many formulas. If all diagonals exist as >> formulas, then all belong to a countable set. > > But if there were only countably many reals, one only needs countably > many formulas to find the nth digit of the nth real.
In fact WM tells us that there is a single finite description P(n,m) of the paths through the binary tree such that for every pair of naturals n,m, P(n,m) characterises the nth digit of the mth path.