LOGIC - NOTATION AND RULES

PROPOSITIONAL RULES
RULE	PREMISES	CONCLUSION
MP	ϕ, ϕ→ψ	ψ
MT	¬ψ, ϕ→ψ	¬ϕ
DNE	¬¬ϕ	ϕ
DNI	ϕ	¬¬ϕ
SIMP	ϕ∧ψ	ϕ ψ
ADJ	ϕ, ψ	ϕ∧ψ
MTP	ϕ∨ψ, ¬ϕ	ψ
MTP	ϕ∨ψ, ¬ψ	ϕ
ADD	ϕ	ϕ∨ψ
ADD	ψ	ϕ∨ψ
BC	ϕ↔ψ	ϕ→ψ ψ→ϕ
CB	ϕ→ψ, ψ→ϕ	ψ↔ϕ
HS	ϕ→ψ, ψ→χ	ϕ→χ
CND	ϕ	ψ→ϕ
CND	¬ϕ	ϕ→ψ
NCND	¬(ϕ→ψ)	ϕ∧¬ψ
NCND	ϕ, ¬ψ	¬(ϕ→ψ)
CONP	ϕ→ψ	¬ψ→¬ϕ
CONP	¬ψ→¬ϕ	ϕ→ψ
DIL	ϕ→ψ, ¬ϕ→ψ	ψ
CM	¬ϕ→ϕ	ϕ
EFQ	¬ϕ, ϕ	ψ
DM	¬ϕ∧¬ψ	¬(ϕ∨ψ)
DM	¬(ϕ∨ψ)	¬ϕ∧¬ψ
DM	¬ϕ∨¬ψ	¬(ϕ∧ψ)
DM	¬(ϕ∧ψ)	¬ϕ∨¬ψ
CASES	ψ∨χ, ψ→ϕ, χ→ϕ	ϕ

SYMBOL	DESCRIPTION
χ	CHI
ϕ	PHI
ψ	PSI
→	IMPLIES
↔	IF AND ONLY IF
¬	NOT
𝔻	DOMAIN
∧	AND
∨	OR
⊻	XOR
⊤	TAUTOLOGY
⊥	CONTRADICTION
∀	FOR EACH
∃	EXISTS
∃!	NOT EXISTS
≡	DEFINITION
⊢	PROVES
⊨	MODELS

DERIVED RULE PROOFS

CASES
1.  SHOW: P
2.    Q v R               :PR
3.    Q->P                :PR
4.    R->P                :PR
5.    SHOW: ~~P
6.      ~P                :AS
7.      ~Q                :MT 3 6
8.      ~R                :MT 4 6
9.      ~Q/\~R            :ADJ 7 8
10      SHOW: ~(Q v R)
11.       Q v R           :AS
12.       ~R              :S 9
13.       Q               :MTP 11 12
14.       ~Q              :S 9
15.     :ID 13 14
16.   :ID 2 10
17.   P                   :DNE 5
18. :DD 17

CM
1.  SHOW: P
2.    ~P->P               :PR
3.    SHOW: ~~P
4.      ~P                :AS
5.      P                 :MP 2 4
6.    :ID 4 5
7.    P :DNE 3
8.  :DD 7

CND_1
1.  SHOW: Q->P
2.    Q                   :AS
3.    P                   :PR
4.  :CD 3

CND_2
1.  SHOW: P->Q
2.    P                   :AS
3.    ~P                  :PR
4.    SHOW: ~~Q
5.      ~Q                :AS
6.    :ID 2 3
7.    Q                   :DNE 4
8.  :CD 7

CONP_1
1.  SHOW: ~Q->~P
2.    ~Q                  :AS
3.    P->Q                :PR
4.    ~P                  :MT 2 3
5.  :CD 4

CONP_2
1.  SHOW: P->Q
2.    P                   :AS
3.    ~Q->~P              :PR
4.    ~~P                 :DNI 2
5.    ~~Q                 :MT 3 4
6.    Q                   :DNE 5
7.  :CD 6

DIL
1.  SHOW: Q
2.    P->Q                :PR
3.    ~P->Q               :PR
4.    SHOW: ~~Q
5.      ~Q                :AS
6.      ~~P               :MT 3 5
7.      ~P                :MT 2 5
8.    :ID 6 7
9.    Q                   :DNE 4
10  :DD 9

EFQ
1.  SHOW: Q
2.    P                   :PR
3.    ~P                  :PR
4.    SHOW: P->Q
5.      SHOW: ~~Q
6.        ~Q              :AS
7.      :ID 2 3
8.      Q                 :DNE 5
9.    :CD 8
10    Q                   :MP 2 4
11. :DD 10

DM_1
1.  SHOW: ~(P v Q)
2.    P v Q               :AS
3.    ~P/\~Q              :PR
4.    ~P                  :S 3
5.    Q                   :MTP 2 4
6.    ~Q                  :S 3
7.  :ID 5 6

DM_2
1.  SHOW: ~P/\~Q
2.    ~(P v Q)            :PR
3.    SHOW: ~P
4.      P                 :AS
5.      P v Q             :ADD 4
6.    :ID 2 5
7.    SHOW: ~Q
8.      Q                 :AS
9.      P v Q             :ADD 8
10    :ID 2 9
11.   ~P/\~Q              :ADJ 3 7
12. :DD 11

DM_3
1.  SHOW: ~(P/\Q)
2.    P/\Q                :AS
3.    ~P v ~Q             :PR
4.    P                   :S 2
5.    ~~P                 :DNI 4
6.    ~Q                  :MTP 3 5
7.    Q                   :S 2
8.  :ID 6 7

DM_4
1.  SHOW: ~P v ~Q
2.    SHOW: ~~(~P v ~Q)
3.      ~(~P v ~Q)        :AS
4.      ~(P/\Q)           :PR
5.      SHOW: ~~P/\~~Q
6.        SHOW: ~~P
7.          ~P            :AS
8.          ~P v ~Q       :ADD 7
9.        :ID 3 8
10        SHOW: ~~Q
11.         ~Q            :AS
12.         ~P v ~Q       :ADD 11
13.       :ID 3 12
14.       ~~P/\~~Q        :ADJ 6 10
15.     :DD 14
16.     ~~P               :S 5
17.     ~~Q               :S 5
18.     P                 :DNE 16
19.     Q                 :DNE 17
20.     P/\Q              :ADJ 18 19
21.   :ID 4 20
22.   ~P v ~Q             :DNE 2
23. :DD 22

HS
1.  SHOW: Q->R
2.    Q                   :AS
3.    Q->P                :PR
4.    P->R                :PR
5.    P                   :MP 2 3
6.    R                   :MP 4 5
7.  :CD 6

NCND_1
1.  SHOW: P/\~Q
2.    ~(P->Q)             :PR
3.    SHOW: ~~P
4.      ~P                :AS
5.      SHOW: P->Q
6.        P               :AS
7.        SHOW: ~~Q
8.          ~Q            :AS
9.        :ID 4 6
10        Q               :DNE 7
11.     :CD 10
12.   :ID 2 5
13.   P                   :DNE 3
14.   SHOW: ~Q
15.     Q                 :AS
16.     SHOW: P->Q
17.       P               :AS
18.     :CD 15
19.   :ID 2 16
20.   P/\~Q               :ADJ 13 14
21. :DD 20

NCND_2
1.  SHOW: ~(P->Q)
2.    P->Q                :AS
3.    P                   :PR
4.    ~Q                  :PR
5.    Q                   :MP 2 3
6.  :ID 4 5

QN_1
1.  SHOW: Ax~F(x)
2.    ~ExF(x)             :PR
3.    SHOW: ~F(x)
4.      F(x)              :AS
5.      ExF(x)            :EG 4
6.    :ID 2 5
7.  :UD 3

QN_2
1.  SHOW: Ex~F(x)
2.    ~AxF(x)             :PR
3.    SHOW: ~~Ex~F(x)
4.      ~Ex~F(x)          :AS
5.      SHOW: Ax~~F(x)
6.        SHOW: ~~F(x)
7.          ~F(x)         :AS
8.          Ex~F(x)       :EG 7
9.        :ID 4 8
10      :UD 6
11.     SHOW: AxF(x)
12.       ~~F(c)          :UI 5
13.       F(c)            :DNE 12
14.     :UD 13
15.   :ID 2 11
16.   Ex~F(x)             :DNE 3
17. :DD 16