2 2.1 自然演繹体系の証明例(述語編) 問題 (1) ¬∃xP (x) ⇐⇒ ∀x¬P (x) (2) ¬∀xP (x) ⇐⇒ ∃x¬P (x) ( =⇒ は古典) (3) ∀xP (x) ∧ ∀xQ(x) ⇐⇒ ∀x(P (x) ∧ Q(x)) (4) ∃xP (x) ∨ ∃xQ(x) ⇐⇒ ∃x(P (x) ∨ Q(x)) (5) ∀xP (x) ∨ ∀xQ(x) ⇐⇒ ∀x∀y(P (x) ∨ Q(y)) ( ⇐= は古典) (5’) ∀xP (x) ∨ ∀xQ(x) =⇒ ∀x(P (x) ∨ Q(x)) ( ⇐= は成り立たない) (6) ∃xP (x) ∧ ∃xQ(x) ⇐⇒ ∃x∃y(P (x) ∧ Q(y)) (6’) ∃xP (x) ∧ ∃xQ(x) ⇐= ∃x(P (x) ∧ Q(x)) ( =⇒ は成り立たない) (7) ∀xP (x) → ∀xQ(x) ⇐⇒ ∃x∀y(P (x) → Q(y)) ( =⇒ は古典) (8) ∃xP (x) → ∃xQ(x) ⇐⇒ ∃y∀x(P (x) → Q(y)) ( =⇒ は古典) (9) ∀xP (x) → ∃xQ(x) ⇐⇒ ∃x(P (x) → Q(x)) ( =⇒ は古典) (10) ∃xP (x) → ∀xQ(x) ⇐⇒ ∀x∀y(P (x) → Q(y)) (10’) ∃xP (x) → ∀xQ(x) =⇒ ∀x(P (x) → Q(x)) ( ⇐= は成り立たない) (11) ∀x∃y(P (x) → Q(y)) ⇐⇒ ∃y∀x(P (x) → Q(y)) ( =⇒ は古典) (11’) ∀x∃yP (x, y) ⇐= ∃y∀xP (x, y) ( =⇒ は成り立たない) 1 2.2 解答 (1) ¬∃xP (x) ⇐⇒ ∀x¬P (x) (1-1) ¬∃xP (x) =⇒ ∀x¬P (x) 仮定(∗1) P (a) 前提 ¬∃xP (x) ⊥ (∗1) ¬P (a) ∀x¬P (x) ∃xP (x) (1-2) ∀x¬P (x) =⇒ ¬∃xP (x) (∗2) 仮定(∗1) ∃xP (x) 仮定 P (a) ⊥ ¬∃xP (x) 前提 ∀x¬P (x) ¬P (a) ⊥ (∗2) (∗1) (2) ¬∀xP (x) ⇐⇒ ∃x¬P (x) ( =⇒ は古典) (2-1) ¬∀xP (x) =⇒ ∃x¬P (x) (古典) 仮定(∗1) ¬P (a) 仮定(∗2) ∃x¬P (x) ¬∃x¬P (x) ⊥ (∗1) ¬¬P (a) P (a) ∀xP (x) 前提 ¬∀xP (x) ⊥ ¬¬∃x¬P (x) ∃x¬P (x) (∗2) (2-2) ∃x¬P (x) =⇒ ¬∀xP (x) 仮定(∗2) ∀xP (x) 前提 ∃x¬P (x) P (a) ⊥ ¬∀xP (x) 仮定(∗1) ¬P (a) ⊥ (∗1) (∗2) 2 (3) ∀xP (x) ∧ ∀xQ(x) ⇐⇒ ∀x(P (x) ∧ Q(x)) (3-1) ∀xP (x) ∧ ∀xQ(x) =⇒ ∀x(P (x) ∧ Q(x)) 前提 前提 ∀xP (x) ∧ ∀xQ(x) ∀xP (x) ∧ ∀xQ(x) ∀xP (x) ∀xQ(x) P (a) Q(a) P (a) ∧ Q(a) ∀x(P (x) ∧ Q(x)) (3-2) ∀x(P (x) ∧ Q(x)) =⇒ ∀xP (x) ∧ ∀xQ(x) 前提 前提 ∀x(P (x) ∧ Q(x)) ∀x(P (x) ∧ Q(x)) P (a) ∧ Q(a) P (a) ∧ Q(a) P (a) Q(a) ∀xP (x) ∀xQ(x) ∀xP (x) ∧ ∀xQ(x) (4) ∃xP (x) ∨ ∃xQ(x) ⇐⇒ ∃x(P (x) ∨ Q(x)) (4-1) ∃xP (x) ∨ ∃xQ(x) =⇒ ∃x(P (x) ∨ Q(x)) 仮定(∗1) P (a) 前提 ∃xP (x) ∨ ∃xQ(x) P (a) ∨ Q(a) ∃x(P (x) ∨ Q(x)) ∃x(P (x) ∨ Q(x)) ∃x(P (x) ∨ Q(x)) 仮定(∗3) ∃xP (x) 仮定(∗2) Q(a) (∗1) P (a) ∨ Q(a) ∃x(P (x) ∨ Q(x)) ∃x(P (x) ∨ Q(x)) 仮定(∗3) ∃xQ(x) (∗3) (4-2) ∃x(P (x) ∨ Q(x)) =⇒ ∃xP (x) ∨ ∃xQ(x) 仮定(∗1) P (a) 仮定(∗1) Q(a) ∃xP (x) ∃xQ(x) ∃xP (x) ∨ ∃xQ(x) ∃xP (x) ∨ ∃xQ(x) 前提 ∃x(P (x) ∨ Q(x)) ∃xP (x) ∨ ∃xQ(x) (∗2) ∃xP (x) ∨ ∃xQ(x) 仮定(∗2) P (a) ∨ Q(a) 3 (∗1) (∗2) (5) ∀xP (x) ∨ ∀xQ(x) ⇐⇒ ∀x∀y(P (x) ∨ Q(y)) ( ⇐= は古典) (5’) ∀xP (x) ∨ ∀xQ(x) =⇒ ∀x(P (x) ∨ Q(x)) ( ⇐= は成り立たない) (5-1) ∀xP (x) ∨ ∀xQ(x) =⇒ ∀x∀y(P (x) ∨ Q(y)) 仮定(∗1) ∀xP (x) 仮定(∗1) ∀xQ(x) P (a) Q(b) 前提 ∀xP (x) ∨ ∀xQ(x) P (a) ∨ Q(b) P (a) ∨ Q(b) P (a) ∨ Q(b) ∀y(P (a) ∨ Q(y)) ∀x∀y(P (x) ∨ Q(y)) (5-2) ∀x∀y(P (x) ∨ Q(y)) =⇒ ∀xP (x) ∨ ∀xQ(x) 前提 ∀x∀y(P (x) ∨ Q(y)) ∀y(P (a) ∨ Q(y)) P (a) ∨ Q(b) 仮定(∗2) ¬P (a) ⊥ Q(b) (∗1) (古典) 仮定(∗1) P (a) 仮定(∗1) Q(b) (∗1) Q(b) ∀xQ(x) ∀xP (x) ∨ ∀xQ(x) 仮定(∗3) ¬(∀xP (x) ∨ ∀xQ(x)) ⊥ (∗2) ¬¬P (a) P (a) ∀xP (x) ∀xP (x) ∨ ∀xQ(x) 仮定(∗3) ¬(∀xP (x) ∨ ∀xQ(x)) ⊥ ¬¬∀xP (x) ∨ ∀xQ(x) ∀xP (x) ∨ ∀xQ(x) (5’-1) ∀xP (x) ∨ ∀xQ(x) =⇒ ∀x(P (x) ∨ Q(x)) (逆は成り立たない) 仮定(∗1) ∀xQ(x) 仮定(∗1) ∀xP (x) P (a) P (a) ∨ Q(a) P (a) ∨ Q(a) ∀x(P (x) ∨ Q(x)) 前提 ∀xP (x) ∨ ∀xQ(x) Q(a) P (a) ∨ Q(a) 4 (∗1) (∗3) (6) ∃xP (x) ∧ ∃xQ(x) ⇐⇒ ∃x∃y(P (x) ∧ Q(y)) (6’) ∃xP (x) ∧ ∃xQ(x) ⇐= ∃x(P (x) ∧ Q(x)) ( =⇒ は成り立たない) (6-1) ∃xP (x) ∧ ∃xQ(x) =⇒ ∃x∃y(P (x) ∧ Q(y)) 仮定(∗2) P (a) 仮定(∗1) Q(b) P (a) ∧ Q(b) ∃y(P (a) ∧ Q(y)) 前提 ∃x∃y(P (x) ∧ Q(y)) ∃xP (x) ∧ ∃xQ(x) 前提 ∃xQ(x) ∃xP (x) ∧ ∃xQ(x) (∗1) ∃xP (x) ∃x∃y(P (x) ∧ Q(y)) (∗2) ∃x∃y(P (x) ∧ Q(y)) (6-2) ∃x∃y(P (x) ∧ Q(y)) =⇒ ∃xP (x) ∧ ∃xQ(x) 仮定(∗1) P (a) ∧ Q(b) 仮定(∗1) P (a) ∧ Q(b) P (a) Q(b) ∃xP (x) ∃xQ(x) 仮定 ∃y(P (a) ∧ Q(y)) ∃xP (x) ∧ ∃xQ(x) 前提 (∗1) ∃x∃y(P (x) ∧ Q(y)) ∃xP (x) ∧ ∃xQ(x) (∗2) ∃xP (x) ∧ ∃xQ(x) (∗2) (6’-2) ∃x(P (x) ∧ Q(x)) =⇒ ∃xP (x) ∧ ∃xQ(x) (逆は成り立たない) 仮定(∗1) 仮定(∗1) P (a) ∧ Q(a) P (a) ∧ Q(a) P (a) Q(a) ∃xP (x) ∃xQ(x) 前提 ∃x(P (x) ∧ Q(x)) ∃xP (x) ∧ ∃xQ(x) (∗1) ∃xP (x) ∧ ∃xQ(x) 5 (7) ∀xP (x) → ∀xQ(x) ⇐⇒ ∃x∀y(P (x) → Q(y)) ( =⇒ は古典) (7-1) ∀xP (x) → ∀xQ(x) =⇒ ∃x∀y(P (x) → Q(y)) (古典) 仮定(∗2) ¬P (a) ⊥ Q(b) 仮定(∗1) P (a) (∗1) P (a) → Q(b) ∀y(P (a) → Q(y)) ∃x∀y(P (x) → Q(y)) 仮定(∗3) ¬∃x∀y(P (x) → Q(y)) ⊥ ¬¬P (a) P (a) ∀xP (x) (∗2) 前提 ∀xP (x) → ∀xQ(x) ∀xQ(x) Q(d) P (c) → Q(d) ∀y(P (c) → Q(y)) ∃x∀y(P (x) → Q(y)) 仮定(∗3) ¬∃x∀y(P (x) → Q(y)) ⊥ ¬¬∃x∀y(P (x) → Q(y)) ∃x∀y(P (x) → Q(y)) 6 (∗3) (8) ∃xP (x) → ∃xQ(x) ⇐⇒ ∃y∀x(P (x) → Q(y)) ( =⇒ は古典) (8-1) ∃xP (x) → ∃xQ(x) =⇒ ∃y∀x(P (x) → Q(y)) (古典) 仮定(∗1) P (a) 仮定(∗2) ¬∃xP (x) ⊥ Q(b) (∗1) P (a) → Q(b) ∀x(P (x) → Q(b)) ∃y∀x(P (x) → Q(y)) ∃xP (x) 仮定(∗3) Q(d) 仮定(∗4) ¬∃y∀x(P (x) → Q(y)) ⊥ ¬¬∃xP (x) ∃xP (x) (∗2) 前提 ∃xP (x) → ∃xQ(x) P (c) → Q(d) ∀x(P (x) → Q(d)) ∃y∀x(P (x) → Q(y)) ∃xQ(x) ⊥ ¬¬∃y∀x(P (x) → Q(y)) ∃y∀x(P (x) → Q(y)) (8-2) ∃y∀x(P (x) → Q(y)) =⇒ ∃xP (x) → ∃xQ(x) (∗1) 仮定 P (a) 仮定(∗2) ∃xP (x) 仮定(∗3) ∀x(P (x) → Q(b)) P (a) → Q(b) Q(b) ∃xQ(x) ∃xQ(x) ∃xP (x) → ∃xQ(x) ∃xP (x) → ∃xQ(x) 前提 ∃y∀x(P (x) → Q(y)) 7 (∗1) (∗2) (∗3) 仮定(∗4) ¬∃y∀x(P (x) → Q ⊥ (∗3) (∗4) (9) ∀xP (x) → ∃xQ(x) ⇐⇒ ∃x(P (x) → Q(x)) ( =⇒ は古典) (9-1) ∀xP (x) → ∃xQ(x) =⇒ ∃x(P (x) → Q(x)) (古典) 仮定(∗2) ¬P (a) ⊥ Q(a) 仮定(∗1) P (a) (∗1) P (a) → Q(a) ∃x(P (x) → Q(x)) 仮定(∗4) ¬∃x(P (x) → Q(x)) ⊥ ¬¬P (a) P (a) ∀xP (x) 仮定(∗3) Q(b) (∗2) 前提 ∀xP (x) → ∃xQ(x) P (b) → Q(b) ∃x(P (x) → Q(x)) ∃xQ(x) ⊥ ∃x(P (x) → Q(x)) ∃x(P (x) → Q(x)) (9-2) ∃x(P (x) → Q(x)) =⇒ ∀xP (x) → ∃xQ(x) 仮定(∗2) ∀xP (x) P (a) 前提 ∃x(P (x) → Q(x)) ∃xQ(x) ∀xP (x) → ∃xQ(x) 仮定(∗1) P (a) → Q(a) Q(a) ∃xQ(x) (∗1) (∗2) 8 仮定(∗4) ¬∃x(P (x) → Q(x)) ⊥ (∗3) (∗4) (10) ∃xP (x) → ∀xQ(x) ⇐⇒ ∀x∀y(P (x) → Q(y)) (10’) ∃xP (x) → ∀xQ(x) =⇒ ∀x(P (x) → Q(x)) ( ⇐= は成り立たない) (10-1) ∃xP (x) → ∀xQ(x) =⇒ ∀x∀y(P (x) → Q(y)) 仮定(∗1) P (a) 前提 ∃xP (x) → ∀xQ(x) ∀xQ(x) Q(b) (∗1) P (a) → Q(b)) ∀y(P (a) → Q(y)) ∀x∀y(P (x) → Q(y)) ∃xP (x) (10-2) ∀x∀y(P (x) → Q(y)) =⇒ ∃xP (x) → ∀xQ(x) 仮定(∗2) ∃xP (x) 仮定(∗1) P (a) 前提 ∀x∀y(P (x) → Q(y)) ∀y(P (a) → Q(y)) P (a) → Q(b) Q(b) Q(b) ∀xQ(x) ∃xP (x) → ∀xQ(x) (∗1) (∗2) (10’-1) ∃xP (x) → ∀xQ(x) =⇒ ∀x(P (x) → Q(x)) 仮定(∗1) P (a) 前提 ∃xP (x) → ∀xQ(x) ∀xQ(x) Q(a) (∗1) P (a) → Q(a)) ∀x(P (x) → Q(x)) ∃xP (x) 9 (11) ∀x∃y(P (x) → Q(y)) ⇐⇒ ∃y∀x(P (x) → Q(y)) ( =⇒ は古典) (11’) ∀x∃yP (x, y) ⇐= ∃y∀xP (x, y) ( =⇒ は成り立たない) (11-1) ∀x∃y(P (x) → Q(y)) =⇒ ∃y∀x(P (x) → Q(y)) (古典) 仮定(∗2) P (a) 前提 ∀x∃y(P (x) → Q(y)) ∃y(P (a) → Q(y)) 仮定(∗1) P (a) → Q(b) Q(b) P (a) → Q(b) ∀x(P (x) → Q(b)) ∃y∀x(P (x) → Q(y)) 仮定(∗3) ¬∃y∀x(P (x) → Q(y)) ⊥ Q(d) (∗1) Q(d) (∗2) P (a) → Q(d) ∀x(P (x) → Q(d)) ∃y∀x(P (x) → Q(y)) 仮定(∗3) ¬∃y∀x(P (x) → Q(y)) ⊥ ¬¬∃y∀x(P (x) → Q(y)) ∃y∀x(P (x) → Q(y)) (11-2) ∃y∀x(P (x) → Q(y)) =⇒ ∀x∃y(P (x) → Q(y)) 仮定(∗1) ∀x(P (x) → Q(b)) P (a) → Q(b) ∃y(P (a) → Q(y)) 前提 ∃y∀x(P (x) → Q(y)) ∀x∃y(P (x) → Q(y)) ∀x∃y(P (x) → Q(y)) (∗1) (11’) ∃y∀xP (x, y) =⇒ ∀x∃yP (x, y) (逆は成り立たない) 仮定(∗1) ∀xP (x, b) P (a, b) ∃yP (a, y) 前提 ∃y∀xP (x, y) ∀x∃yP (x, y) ∀x∃yP (x, y) (∗1) 10 (∗3)
© Copyright 2025 ExpyDoc