《逻辑学导论》第九章集中讨论符号逻辑的证明，有大量有趣的证明练习，做完忍不住有一丝成就感，特将部分解题过程发布于此。
D
### 1
1. ~A
∴ A⊃B
2. ~A⋁B 1, Add.
3. A⊃B 2, Impl. Q.E.D.
### 2
1. C
∴ D⊃C
2. C⋁~D 1, Add.
3. ~D⋁C 2, Com.
4. D⊃C 3, Impl. Q.E.D.
### 3
1. E⊃(F⊃G)
∴ F⊃(E⊃G)
2. (E∙F)⊃G 1, Exp.
3. (F∙E)⊃G 2, Com.
4. F⊃(E⊃G) 3, Exp. Q.E.D.
### 4
1. H⊃(I∙J)
∴ H⊃I
2. ~H⋁(I∙J) 1, Impl.
3. (~H⋁I)∙(~H⋁J) 2, Dist.
4. ~H⋁I 3, Simp.
5. H⊃I 4, Impl. Q.E.D.
### 5
1. K⊃L
∴ K⊃(L⋁M)
2. ~K⋁L 1, Impl.
3. (~K⋁L)⋁M 2, Add.
4. ~K⋁(L⋁M) 3, Assoc.
5. K⊃(L⋁M) 4, Impl. Q.E.D.
### 6
1. N⊃O
∴ (N∙P)⊃O
2. ~N⋁O 1, Impl.
3. (~N⋁O)⋁~P 2, Add.
4. (~N⋁~P)⋁O 3, Assoc. Com.
5. ~(N∙P)⋁O 4, De M.
6. (N∙P)⊃O 5, Impl. Q.E.D.
### 7
1. (Q⋁R)⊃S
∴ Q⊃S
2. ~(Q⋁R)⋁S 1, Impl.
3. (~Q∙~R)⋁S 2, De M.
4. (~Q⋁S)∙(~R⋁S) 3, Dist.
5. ~Q⋁S 4, Simp.
6. Q⊃S 5, Impl. Q.E.D.
### 8
1. T⊃U
2. T⊃V
∴ T⊃(U∙V)
3. ~T⋁U 1, Impl.
4. ~T⋁V 2, Impl.
5. (~T⋁U)∙(~T⋁V) 3,4, Conj.
6. ~T⋁(U∙V) 5, Dist.
7. T⊃(U∙V) 6, Impl. Q.E.D.
### 9
1. W⊃X
2. Y⊃X
∴ (W⋁Y)⊃X
3. ~W⋁X 1, Impl.
4. ~Y⋁X 2, Impl.
5. (~W⋁X)∙(~Y⋁X) 3,4, Conj.
6. (~W∙~Y)⋁X 5, Dist.
7. ~(W⋁Y)⋁X 6, De M.
8. (W⋁Y)⊃X 7, Impl. Q.E.D.
### 10
1. Z⊃A
2. Z⋁A
∴ A
3. ~A⊃~Z 1, Trans.
4. ~Z⊃A 2, Impl.
5. ~A⊃A 3,4, H.S.
6. A⋁A 5, Impl.
7. A 6, Taut. Q.E.D.
E
### 1
1. A⊃~B
2. ~(C∙~A)
∴ C⊃~B
3. ~C⋁A 2, De M.
4. C⊃A 3, Impl.
5. C⊃~B 4,1, H.S. Q.E.D.
### 2
1. (D∙~E)⊃F
2. ~(E⋁F)
∴ ~D
3. ~E∙~F 2, De M.
4. ~E 3, Simp.
5. ~F∙~E 3, Com.
6. ~F 5, Simp.
7. ~(D∙~E) 1,6, M.T.
8. ~D⋁E 7, De M.
9. ~D 8,4, D.S. Q.E.D.
### 3
1. (G⊃~H)⊃I
2. ~(G∙H)
∴ I⋁~H
3. (~G⋁~H)⊃I 1, Impl.
4. ~(G∙H)⊃I 3, De M.
5. I 4,2, M.P.
6. I⋁~H 5. Add. Q.E.D.
### 4
1. (J⋁K)⊃~L
2. L
∴ ~J
3. L⊃~(J⋁K) 1, Trans.
4. ~(J⋁K) 3,2, M.P.
5. ~J∙~K 4, De M.
6. ~J 5, Simp. Q.E.D.
### 5
1. [(M∙N)∙O]⊃P
2. Q⊃[(O∙M)∙N]
∴ ~Q⋁P
3. [O∙(M∙N)]⊃P 1, Com.
4. [(O∙M)∙N]⊃P 3, Assoc.
5. Q⊃P 2,4, H.S.
6. ~Q⋁P 5, Impl.
### 6
1. R⋁(S∙~T)
2. (R⋁S)⊃(U⋁~T)
∴ T⊃U
3. (R⋁S)∙(R⋁~T) 1, Dist.
4. R⋁S 3, Simp.
5. U⋁~T 2,4, M.P.
6. ~T⋁U 5, Com.
7. T⊃U 6, Impl. Q.E.D.
### 7
1. (~V⊃W)∙(X⊃W)
2. ~(~X∙V)
∴ W
3. (V⋁W)∙(~X⋁W) 1, Impl.
4. (V∙~X)⋁W 3, Dist.
5. (~X∙V)⋁W 4, Com.
6. W 5, D.S. Q.E.D.
### 8
1. [(Y∙Z)⊃A]∙[(Y∙B)⊃C]
2. (B⋁Z)∙Y
∴ A⋁C
3. Y∙(B⋁Z) 2, Com.
4. (Y∙B)⋁(Y∙Z) 3, Dist.
5. A⋁C 1,4, C.D. Q.E.D.
### 9
1. ~D⊃(~E⊃~F)
2. ~(F∙~D)⊃~G
∴ G⊃E
3. G⊃(F∙~D) 2, Trans.
4. (~D∙~E)⊃~F 1, Exp.
5. (~E∙~D)⊃~F 4, Com.
6. ~E⊃(~D⊃~F) 5, Exp.
7. ~(~D⊃~F)⊃E 6, Trans.
8. ~(D⋁~F)⊃E 7, Impl.
9. (~D∙F)⊃E 8, De M.
10. (F∙~D)⊃E 9, Com.
11. G⊃E 3,10, H.S. Q.E.D.
### 10
1. [H⋁(I⋁J)]⊃(K⊃J)
2. L⊃[I⋁(J⋁H)]
∴ (L∙K)⊃J
3. [(I⋁J)⋁H]⊃(K⊃J) 1, Com.
4. [I⋁(J⋁H)]⊃(K⊃J) 3, Assoc.
5. L⊃(K⊃J) 2,4, H.S.
6. (L∙K)⊃J 5. Exp.
### 11
1. M⊃N
2. M⊃(N⊃O)
∴ M⊃O
3. M⊃(M∙N) 1, Abs.
4. (M∙N)⊃O 2, Exp.
5. M⊃O 3,4, H.S. Q.E.D.
### 12
1. (P⊃Q)∙(P⋁R)
2. (R⊃S)∙(R⋁P)
∴ Q⋁S
3. P⊃Q 1, Simp.
4. R⊃S 2, Simp.
5. P⋁R 1, Simp.
6. (P⊃Q)∙(R⊃S) 3,4 Conj.
7. Q⋁S 6,5, C.D. Q.E.D.
### 13
1. T⊃(U∙V)
2. (U⋁V)⊃W
∴ T⊃W
3. ~T⋁(U∙V) 1, Impl.
4. (~T⋁U)∙(~T⋁V) 3, Dist.
5. ~T⋁U 4, Simp.
6. T⊃U 5, Impl.
7. ~(U⋁V)⋁W 2, Impl.
8. (~U∙~V)⋁W 7, De M.
9. (~U⋁W)∙(~V⋁W) 8, Dist.
10. ~U⋁W 9, Simp.
11. U⊃W 10, Impl.
12. T⊃W 6,11, H.S. Q.E.D.
### 14
1. (X⋁Y)⊃(X∙Y)
2. ~(X⋁Y)
∴ ~(X∙Y)
3. ~X∙~Y 2, De M.
4. ~X 3, Simp.
5. ~X⋁~Y 4, Add.
6. ~(X∙Y) 5, De M. Q.E.D.
### 15
1. (Z⊃Z)⊃(A⊃A)
2. (A⊃A)⊃(Z⊃Z)
∴ A⊃A
3. (A⊃A)⊃(A⊃A) 2,1, H.S.
4. (~A⋁A)⊃(~A⋁A) 3, Impl.
5. ~(~A⋁A)⋁(~A⋁A) 4, Impl.
6. (A∙~A)⋁(~A⋁A) 5, De M.
7. [A⋁(~A⋁A)]∙[~A⋁(~A⋁A)] 6, Dist.
8. ~A⋁(~A⋁A) 7, Simp.
9. (~A⋁~A)⋁A 8, Assoc.
10. ~A⋁A 9, Taut.
11. A⊃A 10, Impl. Q.E.D.
### 16
1. ~B⋁[(C⊃D)∙(E⊃D)]
2. B∙(C⋁E)
∴ D
3. [~B⋁(C⊃D)]∙[~B⋁(E⊃D)] 1, Dist.
4. [B⊃(C⊃D)]∙[B⊃(E⊃D)] 3, Impl.
5. [(B∙C)⊃D)]∙[(B∙E)⊃D)] 4, Exp.
6. (B∙C)⋁(B∙E) 2, Dist.
7. D⋁D 5,6, C.D.
8. D 7, Taut. Q.E.D.
### 17
1. ~F⋁~[~(G∙H)∙(G⋁V)]
2. (G⊃H)⊃[(H⊃G)⊃I]
∴ F⊃(F∙I)
3. F⊃~[~(G∙H)∙(G⋁V)] 1, Impl.
4. F⊃[(G∙H)⋁~(G⋁V)] 3, De M.
5. F⊃[(G∙H)⋁(~G∙~V)] 4, De M.
6. F⊃[(G⊃H)∙(H⊃G)] 5, Equiv.
7. [(G⊃H)∙(H⊃G)]⊃I 2, Exp.
8. F⊃I 6,7, H.S.
9. F⊃(F∙I) 8, Abs. Q.E.D.
### 18
1. J⋁(~J∙K)
2. J⊃L
∴ (L∙J)≡J
3. J⊃(J∙L) 2, Abs.
4. J⊃(L∙J) 3, Com
5. (J⋁~J)∙(J⋁K) 1, Dist.
6. J⋁~J 5, Simp.
7. (J⋁~J)⋁~L 6, Add.
8. (~L⋁~J)⋁J 7, Assoc. Com.
9. ~(L∙J)⋁J 8, De M.
10. (L∙J)⊃J 9, Impl.
11. (L∙J)≡J 4,10, Equiv. Q.E.D.
### 19
1. (M⊃N)∙(O⊃P)
2. ~N⋁~P
3. ~(M∙O)⊃Q
∴ Q
4. (~N⊃~M)∙(~P⊃~O) 1, Trans.
5. ~M⋁~O 4,2, C.D.
6. ~(M∙O) 5, De M.
7. Q 6, M.P. Q.E.D.
### 20
1. (R⋁S)⊃(T∙U)
2. ~R⊃(V⊃~V)
3. ~T
∴ ~V
4. ~T⋁~U 3, Add.
5. ~(T∙U) 4, De M.
6. ~(R⋁S) 1,5, M.T.
7. ~R∙~S 6, Dist.
8. ~R 7, Simp.
9, V⊃~V 2,8, M.P.
10, ~V⋁~V 9, Impl.
11, ~V 10, Taut. Q.E.D.
G
### 1
1. H⊃P
2. S⊃W
∴ (H⋁S)⊃(P⋁W)
3. ~H⋁P 1, Impl.
4. ~H⋁P⋁W 3, Add.
5. ~H⋁(P⋁W) 4, Assoc.
6. ~S⋁W 2, Impl.
7. ~S⋁W⋁P 6, Add.
8. ~S⋁(W⋁P) 7, Assoc.
9. ~S⋁(P⋁W) 8, Com.
10. [~H⋁(P⋁W)]∙[~S⋁(P⋁W)] 5,9, Conj.
11. (~H∙~S)⋁(P⋁W) 10, Dist.
12. ~(H⋁S)⋁(P⋁W) 11, De M.
13. (H⋁S)⊃(P⋁W) 12, Impl. Q.E.D.
### 2
1. H⊃P
2. S⊃W
∴ (H∙S)⊃(P∙W)
3. ~H⋁P 1, Impl.
4. ~H⋁P⋁~S 3, Add.
5. ~H⋁~S⋁P 4, Com.
6. ~(H∙S)⋁P 5. De M.
7. ~S⋁W 2, Impl.
8. ~S⋁W⋁~H 7, Add.
9. ~H⋁~S⋁W 8, Com.
10. ~(H∙S)⋁W 9, De M.
11. [~(H∙S)⋁P]∙[~(H∙S)⋁W] 6,10, Conj.
12. ~(H∙S)⋁(P∙W) 11, Dist.
13. (H∙S)⊃(P∙W) 12, Impl. Q.E.D.
### 3
1. F⊃A
2. F⊃(A⊃P)
3. A⊃(P⊃C)
∴ F⊃C
4. F⊃(F∙A) 1, Abs.
5. (F∙A)⊃P 2, Exp.
6. F⊃P 4,5, H.S.
7. F⊃(F∙P) 6, Abs.
8. F⊃(P⊃C) 1,3, H.S.
9. (F∙P)⊃C 8, Exp.
10. F⊃C 7,9, H.S. Q.E.D.
### 4
1. G
∴ H⋁~H
2. G⋁~H 1, Add.
3. ~H⋁G 2, Com.
4. H⊃G 3, Impl.
5. H⊃(H∙G) 4, Abs.
6. ~H⋁(H∙G) 5, Impl.
7. (~H⋁H)∙(~H⋁G) 6, Dist.
8. ~H⋁H 7, Simp. Q.E.D.
### 5
1. (H⋁~H)⊃G
∴ G
2. ~(H⋁~H)⋁G 1, Impl.
3. (~H∙H)⋁G 2, De M.
4. (~H⋁G)∙(H⋁G) 3, Dist.
5. ~H⋁G 4, Simp.
6. H⊃G 5, Impl.
7. H⋁G 4, Simp.
8. G⋁H 7, Com.
9. ~G⊃H 8, Impl.
10. ~G⊃G 9,6, H.S.
11. G⋁G 10, Impl.
12. G 11, Taut. Q.E.D.
9.10 C
### 1
1. B⊃S
2. D⊃C
3. (S⋁C)⊃I
4. ~I
∴ ~(B⋁D)
5. ~(S⋁C) 3,4, M.T.
6. ~S∙~C 5, De M.
7. ~S 6, Simp.
8. ~B 1,7, M.T.
9. ~C 6, Simp.
10. ~D 2,9, M.T.
11. (~B)∙(~D) 8,10, Conj.
12. ~(B⋁D) 11, De M.