3 ms·
Ah, thanks! My blocker was that I thought contraposition wasn't valid at all in intuitionistic logic, but actually the one direction still holds, i.e "(P -> Q)
by bubblyworld 2y ago
Ah, thanks! My blocker was that I thought contraposition wasn't valid at all in intuitionistic logic, but actually the one direction still holds, i.e "(P -> Q) -> (not Q -> not P)" is a tautology. In the other direction you get "(not Q -> not P) -> (P -> not not Q)" instead which is basically what you said in the first place =)
- schoen 2y agoYes, 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.)