Ækvivalenser

[22.11.2023] [Nørderier/Teori]

Vi har været gennem de basale regler samt tre afledte, nemlig PBC samt LEM og MT. Vi har også kikket på logisk ækvivalens. Der er en hel serie af formler vi kan vise er ækvivalente. Flere af dem kan bruges som en genvej til at lave beviser. Så de kan være handy at have adgang til. Lad os gennemgå nogle og bevise nogle af dem vi gennemgår.

Kontraposition

Denne er tit ret nyttig. Vi har at \( p \rightarrow q \equiv \neg q \rightarrow \neg p \). Vi viser den ene vej:

p => q assumption; [l1] p \/ ~ p by lem ; [l2] ( ~ q assumption; [s1] ( p assumption; [s11] q by imp_e s11 l1 ; [s12] bot by neg_e s12 s1 ; [s13] ~ p by bot_e s13 ) ; [case1] ( ~ p assumption; [s12] ~ p by copy s12 ) ; [case2] ~ p by dis_e l2 case1 case2 ) ; [imp1] ~ q => ~ p by imp_i imp1 .

A

Vi har at \( \neg p \lor q \equiv p \rightarrow q \). Vi har vist den ene vej på forrige side. Vi kan her vise den anden (her ved brug af LEM):

p => q assumption; [l1] p \/ ~ p by lem ; [l2] ( p assumption; [s1] q by imp_e s1 l1 ; [s2] ~ p \/ q by dis_i2 s2 ) ; [dis1] ( ~ p assumption; [s11] ~ p \/ q by dis_i1 s11 ) ; [dis2] ~ p \/ q by dis_e l2 dis1 dis2 .

B

Vi har at \( p \land \neg q \equiv \neg (p \rightarrow q) \). Vi kan vise den ene af vejene:

p /\ ~ q assumption; [l1] ( p => q assumption; [s1] p by con_e1 l1 ; [s2] q by imp_e s2 s1 ; [s3] ~ q by con_e2 l1 ; [s4] bot by neg_e s3 s4 ) ; [case1] ~ (p => q) by neg_i case1 .

C - De Morgans

Vi har at \( \neg p \lor \neg q \equiv \neg (p \land q) \). Vi kan vise den ene af vejene (den er lidt omfattende, den her):

~ (p /\ q) assumption; [l1] p \/ ~ p by lem ; [l2] ( p assumption; [s1] q \/ ~ q by lem ; [s2] ( q assumption; [s11] p /\ q by con_i s1 s11 ; [s12] bot by neg_e s12 l1 ; [s13] ~ p \/ ~ q by bot_e s13 ) ; [case11] ( ~ q assumption; [s11] ~ p \/ ~ q by dis_i2 s11 ) ; [case12] ~ p \/ ~ q by dis_e s2 case11 case12 ) ; [case1] ( ~ p assumption; [s1] ~ p \/ ~ q by dis_i1 s1 ) ; [case2] ~ p \/ ~ q by dis_e l2 case1 case2 .

D - De Morgans

Vi har at \( \neg p \land \neg q \equiv \neg (p \lor q) \). Både denne og C er ret intuitive - måske værd at tænke over. Vi viser den ene vej:

~ p /\ ~ q assumption; [l1] ( p \/ q assumption; [s1] ( p assumption; [s11] ~ p by con_e1 l1 ; [s12] bot by neg_e s11 s12 ) ; [case11] ( q assumption; [s21] ~ q by con_e2 l1 ; [s22] bot by neg_e s21 s22 ) ; [case12] bot by dis_e s1 case11 case12 ) ; [case1] ~ (p \/ q) by neg_i case1

Teoremer

Teoremer er ikke ækvivalente da de kun kan vises den ene vej. E, F, G kaldes syllogismer - et udsagn der består af 2 præmisser og en konklusion.

E - Modus Tollens

Vi har at \( p \rightarrow q, \neg q \vdash \neg p \). Og det viser vi sgu da bare:

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

F - Modus Tollendo Ponens

Vi har at \( p \lor q, \neg q \vdash p \). Dette kan også udtrykkes som \( (p \lor q) \land \neg q \rightarrow p \). Bevis udeladt.

G - Modus Ponendo Tollens

Vi har at \( \neg (p \land q), p \vdash \neg q \). Og det kan vi da godt vise:

~ (p /\ q) assumption; [l1] p assumption; [l2] ( q assumption; [s1] p /\ q by con_i l2 s1 ; [s2] bot by neg_e s2 l1 ) ; [neg1] ~ q by neg_i neg1 .

Index

Del