################################################################ 1 AvB ~A c B ################################################################ 2 A&(B&D) c B Derive B&D B&D Apply &ELIM/Right to A&(B&D) Apply &ELIM/Left to B&D ################################################################ 3 ~F&G K c G&K Derive G G Apply &ELIM/Right to ~F&G Apply &INTRO to obtain G&K ################################################################ 4 (F&B)&(G&S) H I (H&I)->K (F&G)->M c M&K ################################################################ 5 A&~C D&(EvF) c ~C&(EvF) Derive ~C ~C Apply &EL to A&~C Derive EvF EvF Apply &EL to D&(EvF) Apply &IN to obtain ~C&(EvF) ################################################################ 6 ~A&B c ~(A&B) *Assume A&B A&B *Derive A A *Apply &ELIM to A&B *Derive ~A ~A *Apply &ELIM *Apply ~IN RETURN ################################################################ 7 ~((C->D)&~B) C->D c B *Assume ~B ~B *Derive ~((C-> D)&~B) ~((C-> D)&~B) *Derive ((C-> D)&~B) ((C-> D)&~B) *Apply &IN to obtain ((C-> D)&~B) Apply ~EL to obtain B ################################################################ 8 D c ~(A&~D) *Assume A&~D A&~D *Derive D D *Send D *Derive ~D ~D *Apply &EL to obtain ~D Apply ~IN to obtain ~(A&~D) ################################################################ 9 Av~B c ~(~(Av~B)&C) No hints! ################################################################ 10 ~(A&~B) ~(B&~C) ~C c ~A *Assume A A *Derive 2 contradic. sentences *Derive (A&~B) A&~B *Derive ~B ~B **Assume B B **Derive 2 contradic. sentences **Derive ~(B&~C) B&~C **Derive ~(B&~C) ~(B&~C) **Apply ~IN to obtain ~B *Return ~B *Apply &IN to obtain (A&~B) *Derive ~(A&~B) ~(A&~B) *Apply ~IN to obtain ~A Return ~A ################################################################ 11 B&~A A&~B c C->D Apply ~EL strategy ################################################################ 12 C c ~(A&~(BvC)) Apply ~IN strategy *Assume (A&~(B&~C)) (A&~(B&~C)) *Derive 2 contradic.sentences *No more hints! C *Apply ~IN ~(A&~(B&~C)) ################################################################ 13 ~(~A&~(C&~C)) c A Apply ~EL strategy *Assume ~A ~A *Derive 2 contradic.sentences ~C *Derive ~(C&~C) ~(C&~C) **Assume (C&~C) (C&~C) **Derive 2 contradic.sentences **Apply ~IN to obtain ~(C&~C) *Return ~(C&~C) *Apply ~EL to obtain A ################################################################ 14 ~(A&~B) ~(A&~C) c ~(A&~(B&C)) Apply the ~IN strategy No more hints! ################################################################ 15 A->~~C BvD c ~(E&~E) No hints! ################################################################ 16 ~(A&~B)&~(~A&B) ~A c ~B No hints! ################################################################ 17 A&(~B&C) ~(C&E) ~(~E&H) c ~H No hints! ################################################################ 18 A->(B&C) A B->D c C&D Derive C C Derive (B&C) (B&C) Apply -> EL to (A-> (B&C)) Apply &EL to (B&C) Derive D D Derive B from (B&C) B Apply -> EL to obtain (B-> D) (C&D) Apply &IN to obtain (C&D) ################################################################ 19 A->B B->C c ~C->~A *Assume ~C ~C *Derive ~A ~A **Assume A A **Derive 2 contradic.sentences **Derive C **Derive ~C ~C **Apply ~IN to obtain ~A *Return ~A *Apply -> IN to obtain (~C-> ~A) Return (~C-> ~A) ################################################################ 20 A->(B&~B) ~B->A c B ~ELIM strategy *Assume ~B ~B *Derive 2 contradic. sentences *Derive B B *Apply ~ELIM to obtain B Return B ################################################################ 21 C->(Dv~E) C&~D c ~E Derive (Dv~E) (Dv~E) Derive C C Apply -> EL to (C-> (Dv~E)) Derive ~D ~D Apply &EL to (C&~D) Apply vEL to obtain ~E ################################################################ 22 (Ev~F)->(C&R) ~F&(C->B) c B&R Derive B B Derive R R Apply &IN to obtain (B&R) ################################################################ 23 ~(A->(B->C)) c ~CvB *Assume ~(~CvB) *Derive 2 contradic. sentences ~(~CvB) Apply RR Apply ~ELIM ################################################################ 24 ~Av(B->~C) A&C c ~B&C Derive ~B ~B Derive C C Apply &IN to obtain (~B&C) ################################################################ 25 D->~E ~A->C c (~AvD)->(~EvC) ################################################################ 26 A<->(Cv~D) C-> B ~B&A c ~D Derive (Cv~D) (Cv~D) Apply <-> EL to obtain (A-> (Cv~D)) Derive A A Apply -> EL to obtain (Cv~D) Derive ~C ~C Apply MT Apply vEL to obtain ~D ################################################################ 27 A->(B->C) ~D->(C->A) B&~D c C<->A ################################################################ 28 ~(Av~(~B&~C)) A->~B c D->~C *Assume D D *Derive ~C ~C *Apply RR De Morgan and &EL (Bv~C) * to obtain (Bv~C) Apply -> IN to obtain (D-> ~C) ################################################################ 29 ~D<->(A&~B) c ~(~D&~A) ################################################################ 30 A&(~C->~A) B&(~BvD) c C<->D ################################################################ 31 A<->B B<->~C c A<->~C ################################################################ 32 A<->B ~B&C c ~A ##################### Try only & and ~ Rules 33 ~(~A&~B) ~(A&~C) ~(B&~D) c ~(~C&~D) ##################### Try only & and ~ Rules 34 ~(A&~B) A c B ##################### Try only & and ~ Rules 35 ~(~A&~B) ~A c B ##################### Try only & and ~ Rules 36 B c ~(A&~B) ##################### Try only & and ~ Rules 37 A c ~(~A&~B) ##################### Theorem: Idempotence/& 38 c A<->(A&A) ##################### Theorem: Idempotence/v 39 c A<->(AvA) ##################### Theorem:Comutativity/& 40 c (A&B)<->(B&A) ##################### Theorem:Comutativity/v 41 c (AvB)<->(BvA) ##################### Theorem: DM 1 42 c (AvB)<->~(~A&~B) ##################### Theorem: DM 2 43 c (A&B)<->~(~Av~B)