Philosophy 270, Fall 2006

Examples for the derivation worksheet

procedure pdf worksheet pdf
A ∧ D, C ∧ ¬ (D ∧ E) ⇒ C ∧ ¬ E
off 0 1 2 3 4 5 6 7 8 9 all
│A ∧ D 1
│C ∧ ¬ (D ∧ E) 2
├─
1 Ext │A
1 Ext │D (8)
2 Ext │C (4)
2 Ext │¬ (D ∧ E) 6
│
││●
│├─
4 QED ││C 3
│
│││E (9)
││├─
│││││●
││││├─
8 QED │││││D 7
││││
│││││●
││││├─
9 QED │││││E 7
│││├─
7 Cnj ││││D ∧ E 6
││├─
6 CR │││⊥ 5
│├─
5 RAA ││¬ E 3
├─
3 Cnj │C ∧ ¬ E
 gap prox. arg. & applicable rules rule usedstg
‣only A ∧ D,Ext C ∧ ¬ (D ∧ E)Ext / C ∧ ¬ ECnj Ext (for A ∧ D) 1
‣only A, D, C ∧ ¬ (D ∧ E)Ext / C ∧ ¬ ECnj Ext 2
‣only A, D, C, ¬ (D ∧ E) / C ∧ ¬ ECnj Cnj 3
‣1st A, D, C, ¬ (D ∧ E) / CQED QED 4
‣only A, D, C, ¬ (D ∧ E) / ¬ ERAA RAA 5
‣only A, D, C, ¬ (D ∧ E),CR E / ⊥ CR 6
‣only A, D, C, E / D ∧ ECnj Cnj 7
‣1st A, D, C, E / DQED QED 8
‣only A, D, C, E / EQED QED 9
‣none      
¬ (A ∧ (B ∧ C)), A ∧ D ⇒ A ∧ C
off 0 1 2 3 4 5 6 7 8 9 10 all
│¬ (A ∧ (B ∧ C)) 6
│A ∧ D 3, 10
├─
│││¬ A (4)
││├─
3 Ext │││A (4)
3 Ext │││D
│││●
││├─
4 Nc │││⊥ 2
│├─
2 IP ││A 1
│
│││¬ C (9)
││├─
│││││
││││├─
│││││A 7
││││
││││││
│││││├─
││││││B 8
│││││
│││││││¬ C
││││││├─
10 Ext │││││││A
10 Ext │││││││D
│││││││○ ¬ C, A, D ⇏ ⊥
││││││├─
│││││││⊥ 9
│││││├─
9 IP ││││││C 8
││││├─
8 Cnj │││││B ∧ C 7
│││├─
7 Cnj ││││A ∧ (B ∧ C) 6
││├─
6 CR │││⊥ 5
│├─
5 IP ││C 1
├─
1 Cnj │A ∧ C
 gap prox. arg. & applicable rules rule usedstg
‣only ¬ (A ∧ (B ∧ C)), A ∧ DExt / A ∧ CCnj Cnj 1
‣1st ¬ (A ∧ (B ∧ C)), A ∧ DExt / AIP IP 2
‣1st ¬ (A ∧ (B ∧ C)),CR A ∧ D,Ext ¬ A / ⊥ Ext 3
‣1st ¬ (A ∧ (B ∧ C)), A, D, ¬ A / ⊥Nc Nc 4
‣only ¬ (A ∧ (B ∧ C)), A ∧ DExt / CIP IP 5
‣only ¬ (A ∧ (B ∧ C)),CR A ∧ D,Ext ¬ C / ⊥ CR 6
‣only A ∧ D,Ext ¬ C / A ∧ (B ∧ C)Cnj Cnj 7
‣2nd A ∧ D,Ext ¬ C / B ∧ CCnj Cnj 8
‣3rd A ∧ D,Ext ¬ C / CIP IP 9
‣3rd A ∧ D,Ext ¬ C / ⊥ Ext 10
‣3rd A, D, ¬ C / ⊥ dead end