> ~ ~ ~ P -> ~ P is a theorem also in constructive mathematics.
Could you provide a citation for this? I can vaguely see how that might work, being ~~Q->Q for the special case where Q can be decomposed into Q = ~P, but it's obviously rather difficult to search for.
It is very easy to prove. Note first that ~P is an abbreviation for P -> False. So we can rewrite this as
(~ ~ P -> False) -> P -> False.
This is tautologically true by modes ponens if P -> ~ ~ P. But that is a well known fact.
Could you provide a citation for this? I can vaguely see how that might work, being ~~Q->Q for the special case where Q can be decomposed into Q = ~P, but it's obviously rather difficult to search for.