The way I think of it, is that constructivist logic allows “proof of negation” via contradiction which is often conflated with “proof by contradiction”. So if you want to prove ¬P, it’s enough to assume P and then derive a contradiction. And if you want to prove ¬¬P, it’s enough to assume ¬P and then derive a contradiction. But if you want to prove P, it’s not enough to assume ¬P and then derive a contradiction. This makes sense I think—if you assume ¬P and then derive a contradiction, you get ¬¬P, but in constructivist logic there’s no way to go directly from ¬¬P to P.
Proof of negation (allowed): Prove ¬P by assuming P and deriving a contradiction
Proof by contradiction (not allowed): Prove P by assuming ¬P and deriving a contradiction
The way I think of it, is that constructivist logic allows “proof of negation” via contradiction which is often conflated with “proof by contradiction”. So if you want to prove ¬P, it’s enough to assume P and then derive a contradiction. And if you want to prove ¬¬P, it’s enough to assume ¬P and then derive a contradiction. But if you want to prove P, it’s not enough to assume ¬P and then derive a contradiction. This makes sense I think—if you assume ¬P and then derive a contradiction, you get ¬¬P, but in constructivist logic there’s no way to go directly from ¬¬P to P.
Proof of negation (allowed): Prove ¬P by assuming P and deriving a contradiction
Proof by contradiction (not allowed): Prove P by assuming ¬P and deriving a contradiction