Propositional Logic - Equivalences

Here we list some equivalences within propositional logic.

Contraposition

This rule is quite useful, often a shortcut. We have that \( p \rightarrow q \equiv \neg q \rightarrow \neg p \). We can prove the right direction as thus

p => q assumption; [l1] p \/ ~ p by lem ; [l2] ( p assumption; [l3] q by imp_e l3 l1 ; [l4] ( ~ q assumption; [l5] bot by neg_e l4 l5 ; [l6] ~ p by bot_e l6 ) ; [imp1] ~ q => ~ p by imp_i imp1 ) ; [dis1] ( ~ p assumption; [l3] ( ~ q assumption; [l4] ~ p by copy l3 ) ; [imp2] ~ q => ~ p by imp_i imp2 ) ; [dis2] ~ q => ~ p by dis_e l2 dis1 dis2 .

And the left direction (almost same proof) as thus

~ q => ~ p assumption; [l1] q \/ ~ q by lem ; [l2] ( ~ q assumption; [l3] ( p assumption; [l4] ~ p by imp_e l3 l1 ; [l5] bot by neg_e l4 l5 ; [l6] q by bot_e l6 ) ; [imp1] p => q by imp_i imp1 ) ; [dis1] ( q assumption; [l3] ( p assumption; [l4] q by copy l3 ) ; [imp1] p => q by imp_i imp1 ) ; [dis2] p => q by dis_e l2 dis2 dis1 .

E1

We have that \( \neg p \lor q \equiv p \rightarrow q \). This we have already shown in the previous chapter.

E2

We have that \( p \land \neg q \equiv \neg (p \rightarrow q) \). We can show the left direction here:

~ (p => q) assumption; [l1] ( ~ p assumption; [l2] ( p assumption; [l3] bot by neg_e l3 l2 ; [l4] q by bot_e l4 ) ; [imp1] p => q by imp_i imp1 ; [l5] bot by neg_e l5 l1 ) ; [neg1] p by pbc neg1 ; [l6] ( q assumption; [l7] ( p assumption; [l8] q by copy l7 ) ; [imp2] p => q by imp_i imp2 ; [l9] bot by neg_e l9 l1 ) ; [neg2] ~ q by neg_i neg2 ; [l10] p /\ ~ q by con_i l6 l10 .

De Morgans #1

We have that \( \neg(p \land q) \equiv \neg p \lor \neg q \). We can prove the right direction:

~ (p /\ q) assumption; [l1] p \/ ~ p by lem ; [l2] ( p assumption; [l3] ( q assumption; [l4] p /\ q by con_i l3 l4 ; [l5] bot by neg_e l5 l1 ) ; [neg1] ~ q by neg_i neg1 ; [l6] ~ p \/ ~ q by dis_i2 l6 ) ; [dis1] ( ~ p assumption; [l7] ~ p \/ ~ q by dis_i1 l7 ) ; [dis2] ~ p \/ ~ q by dis_e l2 dis1 dis2 .

De Morgans #2

We have that \( \neg p \land \neg q \equiv \neg (p \lor q) \). We can show the left direction:

~ p /\ ~ q assumption; [l1] ( p \/ q assumption; [l2] ( p assumption; [l3] ~ p by con_e1 l1 ; [l4] bot by neg_e l3 l4 ) ; [dis1] ( q assumption; [l3] ~ q by con_e2 l1 ; [l4] bot by neg_e l3 l4 ) ; [dis2] bot by dis_e l2 dis1 dis2 ) ; [neg1] ~ (p \/ q) by neg_i neg1 .

Modus Tollens (Theorem)

This we can only prove one way, hence theorem. We have that \( p \rightarrow q, \neg q \vdash \neg p \). We prove:

p => q assumption; [l1] ~ q assumption; [l2] ( p assumption; [l3] q by imp_e l3 l1 ; [l4] bot by neg_e l4 l2 ) ; [neg1] ~ p by neg_i neg1 .

Modus Tollendo Ponens (Theorem)

We have that \( p \lor q, \neg q \vdash p \).

Modus Ponendo Tollens

We have that \( \neg(p \land q), q \vdash \neg q \).