The really fascinating thing is that the distinction between ¬¬x and x actually parallels the distinction between proof by contradiction and normal proofs. Tha

The really fascinating thing is that the distinction between ¬¬x and x actually parallels the distinction between proof by contradiction and normal proofs. That is, if you have any classical proof of x, you have a constructive proof of ¬¬x. The way I like to think of it is that, in constructive logic, both x and ¬¬x represent evidence for x—it's just that ¬¬x is weaker. You can still derive all the results you want, you simply have to be more explicit about whether you have constructive evidence or not.