Does intuitionist logic deny diagonal argument?

Question

Let us for example give an example of diagonal proof of uncountability of the set of real numbers $\mathbb{R}$. Would intuitionists accept this, or deny this? If they deny this argument, why would they?

Answer 1

The general methods of the diagonal argument are fine intuitionistically.

Also, because $\lnot P$ is equivalent to $P \to \bot$, it is fine to prove $\lnot P$ by assuming $P$ and deriving a contradiction. So there is no problem with proving "the reals are not countable" by assuming "the reals are countable" and deriving a contradiction.

The main thing to worry about is whether any classical logic slipped into the intermediate steps of the proof. This is particularly relevant to real numbers because of the way real numbers are handled in intuitionistic logic.

Nevertheless, at least one version of proof that the real numbers are not countable (by a variation of the nested interval diagonal method due to Cantor) is intuitionistically valid.