Yes, it's interesting how careful you have to be with what you can and can't do with negations. For example, some forms of De Morgan's Law work but some don't!

Yes, it's interesting how careful you have to be with what you can and can't do with negations. For example, some forms of De Morgan's Law work but some don't! These are valid intuitionistically: (P /\ Q) -> ~(~P \/ ~Q) (~P /\ ~Q) -> ~(P \/ Q) (P \/ Q) -> ~(~P /\ ~Q) ~(P \/ Q) -> (~P /\ ~Q) (~P \/ ~Q) -> ~(P /\ Q) These are not: ~(~P /\ ~Q) -> (P \/ Q) ~(P /\ Q) -> (~P \/ ~Q) ~(~P \/ ~Q) -> (P /\ Q) And with quantifiers, these are valid intuitionistically: (forall x, P x) -> (~exists x, ~P x) (exists x, P x) -> (~forall x, ~P x) ~(exists x, P x) -> (forall x, ~P x) But this isn't: ~(forall x, P x) -> (exists x, ~P x) (Assuming the existence of some x does not help here.)