>>11710302You appear to think that the claim is that the transcendental number thus defined can't be part of any enumeration.
But the prove only shows that the reals (or the powerset of N) is countable. In other words, there's no bijection between N and R (or N and PN). That's what it says.
If you want to speak about constructive or not, then it's saver and suffices to speak of the counter-example number in the argument being defined (you don't need the number to be "constructed", in a constructive sense, for the proof of non-existence to go through).
Btw. there's nice abstracted formulations of the idea underlying the proof
https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theoremhttps://youtu.be/rHsuesTdFLMTo throw more fire into the ring, note that "defined" can't be defined within the theory (similarly to Tarskis truth predicate), and thus arguments such as
>The definable numbers are countable, the reals aren't countable, thus there exists reals that can't be definedis very hard to make precise or formalize within one level of analysis.
Moreover, there's models of constructive ZF set theory where the reals are not more than N.
