I'm a mathematician. I can't understand your post at all. > The double-negation holds in propositional logic Double-negation isn't a proposition, so don't kn

I'm a mathematician. I can't understand your post at all. > The double-negation holds in propositional logic Double-negation isn't a proposition, so don't know what this means. Double-negation elimination, that is, the proposition: for all A, ~ (~ A) -> A does not hold in constructive logic. However, double-negation introduction, that is, the proposition: for all A, A -> ~(~ A) does definitely hold in constructive logic. Here is a proof in Coq: Theorem A_implies_not_not_A : forall A : Prop, A -> ~ (~ A). unfold not. intros. apply (H0 H). Qed.