[MaxRegret]

Also, proving ¬P by assuming P and deriving a contradiction is not "proof by contradiction"! That is just how you prove negations — ¬P is often taken to be syntax sugar for P ⇒ False.

It's only proof by contradiction if you prove P by assuming ¬P and deriving a contradiction. Technically, what you've actually done is proven ¬(¬P). Now if you're a classical logician, you would say that ¬(¬P) is equivalent to P; if you're a constructivist, you wouldn't.

So proof by contradiction isn't in the constructivist's toolbox, with the proviso that many people think they're doing a proof by contradiction when they're not actually.

[markovblanket]

woah truee