Hacker News new | ask | show | jobs
by ihm 3980 days ago
The reals one defines thee reals constructively in essentially the same way as one does classically. When the parent commenter says the reals in constructive mathematics are uncountable, he means that inside of a constructive system one can prove the statement

    There does not exist a bijection between the natural numbers and the real numbers.
which is true. You are free to interpret constructive logic in various ways. If you interpret it as the logic of computable things, in which case this statement becomes interpreted as something like

    There is no computable bijection between the natural numbers and the computable reals.
If you interpret it into classical logic, it becomes (now in the classical sense)

    There is no bijection between the natural numbers and the reals.