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)

形式演繹体系 LI,LK 証明例 述語編[PDF]