命題論理のメモ2
○エルフの村-エーリルの家
メモの後半になると難易度が化けてきた。
なお、基本が簡単とは限らない。
エーリル
「ディアナは何しにきたの？」
ディアナ
「ああ、文字を広めるようドワーフの民に働きかけていたんですが、このメモのせいでどうでもよくなりました」
エーリル
「わかる」
■thm0.17(∧∨の分配 法則1)
{} |- ((φ∧(ψ∨ρ))⇔((φ∧ψ)∨(φ∧ρ)))
proof
1 (φ∧(ψ∨ρ)) [ax]
2 (ψ∨ρ) [∧elL 1]
3 ψ [ax]
4 φ [∧elR 1]
5 (φ∧ψ) [∧in 4,3]
6 ((φ∧ψ)∨(φ∧ρ)) [∨inR 5]
7 (ψ⇒((φ∧ψ)∨(φ∧ρ))) [⇒in 6 el 3]
8 ρ [ax]
9 (φ∧ρ) [∧in 4,8]
10 ((φ∧ψ)∨(φ∧ρ)) [∨inL 9]
11 (ρ⇒((φ∧ψ)∨(φ∧ρ))) [⇒in 10 el 8]
12 ((φ∧ψ)∨(φ∧ρ)) [∨el 2,7,11]
13 ((φ∧(ψ∨ρ))⇒((φ∧ψ)∨(φ∧ρ))) [⇒in 12 el 1]
14 ((φ∧ψ)∨(φ∧ρ)) [ax]
15 (φ∧ψ) [ax]
16 φ [∧elR 15]
17 ψ [∧elL 15]
18 (ψ∨ρ) [∨inR 17]
19 (φ∧(ψ∨ρ)) [∧in 16,18]
20 ((φ∧ψ)⇒(φ∧(ψ∨ρ))) [⇒in 19 el 15]
21 (φ∧ρ) [ax]
22 φ [∧elR 21]
23 ρ [∧elL 23]
24 (ψ∨ρ) [∨inL 23]
25 (φ∧(ψ∨ρ)) [∧in 22,24]
26 ((φ∧ρ)⇒(φ∧(ψ∨ρ))) [⇒in 25 el 21]
27 (φ∧(ψ∨ρ)) [∨el 14,20,26]
28 (((φ∧ψ)∨(φ∧ρ))⇒(φ∧(ψ∨ρ))) [⇒in 27 el 14]
29 ((φ∧(ψ∨ρ))⇔((φ∧ψ)∨(φ∧ρ))) [⇔in 13,28]
■
エーリル
「∧と∨ってことは」
ディアナ
「やっぱりね。次も∨と∧を入れ替えている」
■thm0.18(∧∨の分配 法則2)
{} |- ((φ∨(ψ∧ρ))⇔((φ∨ψ)∧(φ∨ρ)))
proof
1 (φ∨(ψ∧ρ)) [ax]
2 φ [ax]
3 (φ∨ψ) [∨inR 2]
4 (φ∨ρ) [∨inR 2]
5 ((φ∨ψ)∧(φ∨ρ)) [∧in 3,4]
6 (φ⇒((φ∨ψ)∧(φ∨ρ))) [⇒in 5 el 2]
7 (ψ∧ρ) [ax]
8 ψ [∧elR 7]
9 (φ∨ψ) [∨inL 8]
10 ρ [∧elL 7]
11 (φ∨ρ) [∨inL 10]
12 ((φ∨ψ)∧(φ∨ρ)) [∧in 9,11]
13 ((ψ∧ρ)⇒((φ∨ψ)∧(φ∨ρ))) [⇒in 12 el 7]
14 ((φ∨ψ)∧(φ∨ρ)) [∨el 1,6,13]
15 ((φ∨(ψ∧ρ))⇒((φ∨ψ)∧(φ∨ρ))) [⇒in 14 el 1]
16 ((φ∨ψ)∧(φ∨ρ)) [ax]
17 (φ∨ψ) [∧elR 16]
18 (φ∨ρ) [∧elL 16]
19 φ [ax]
20 (φ∨(ψ∧ρ)) [∨inR 19]
21 (φ⇒(φ∨(ψ∧ρ))) [⇒in 20 el 19]
22 ψ [ax]
23 ρ [ax]
24 (ψ∧ρ) [∧in 22,23]
25 (φ∨(ψ∧ρ)) [∨inL 24]
26 (ψ⇒(φ∨(ψ∧ρ))) [⇒in 25 el 22]
27 (φ∨(ψ∧ρ)) [∨el 17,21,26]
28 (ρ⇒(φ∨(ψ∧ρ))) [⇒in 27 el 23]
29 (φ∨(ψ∧ρ)) [∨el 18,21,28]
30 (((φ∨ψ)∧(φ∨ρ))⇒(φ∨(ψ∧ρ))) [⇒in 29 el 16]
31 ((φ∨(ψ∧ρ))⇔((φ∨ψ)∧(φ∨ρ))) [⇔in 15,30]
■
エーリル
「φをψとρに分けるの、確かに分配って感じ」
ディアナ
「証明の難易度が上がってますよ」
エーリル
「天々城さんは容赦しない人」
■thm0.19(排中律)
{} |- (φ∨(￢φ))
proof
1 (￢(φ∨(￢φ))) [ax]
2 φ [ax]
3 (φ∨(￢φ)) [∨inR 2]
4 (￢φ) [￢in 3,1 el 2]
5 (φ∨(￢φ)) [∨inL 4]
6 (φ∨(￢φ)) [￢el 5,1 el 1]
■
エーリル
「天々城さんは手加減もしてくれる優しい人」
ディアナ
「￢ははじめてですね。
『でない』の意味ですか？」
エーリル
「うん。言われてみれば『ディアナはドワーフか、ディアナはドワーフじゃない』は合ってるのか。へー」
■thm0.20(無矛盾律)
{} |- (￢(φ∧(￢φ)))
proof
1 (φ∧(￢φ)) [ax]
2 φ [∧elR 1]
3 (￢φ) [∧elL 1]
4 (￢(φ∧(￢φ))) [￢in 2,3 el 1]
■
エーリル
「『ディアナはドワーフで、ディアナはドワーフじゃない』じゃないも言われてみれば確かに合ってる」
ディアナ
「それ私じゃなくてもいいでしょう？」
■thm0.21(￢の対合)
{} |- (φ⇔(￢(￢φ)))
proof
1 φ [ax]
2 (￢φ) [ax]
3 (￢(￢φ)) [￢in 1,2 el 2]
4 (φ⇒(￢(￢φ))) [⇒in 3 el 1]
5 (￢(￢φ)) [ax]
6 (￢φ) [ax]
7 φ [￢el 6,5 el 6]
8 ((￢(￢φ))⇒φ) [⇒in 7 el 5]
9 (φ⇔(￢(￢φ))) [⇔in 4,8]
■
エーリル
「『ディアナは姫じゃない』じゃない」
ディアナ
「姫です」
■thm0.22(対偶)
{} |- ((φ⇒ψ)⇔((￢ψ)⇒(￢φ)))
proof
1 (φ⇒ψ) [ax]
2 φ [ax]
3 ψ [⇒el 2,1]
4 (￢ψ) [ax]
5 (￢φ) [￢in 3,4 el 2]
6 ((￢ψ)⇒(￢φ)) [⇒in 5 el 4]
7 ((φ⇒ψ)⇒((￢ψ)⇒(￢φ))) [⇒in 6 el 2]
8 (((￢ψ)⇒(￢φ))⇒(φ⇒ψ)) [Ax3]
9 ((φ⇒ψ)⇔((￢ψ)⇒(￢φ))) [⇔in 7,8]
■
エーリル
「Ax3の逆、だと……？」
ディアナ
「私はよくわからないですけど、びっくりしたのはわかりました」
■thm0.23(￢∧∨のド・モルガンの法則1)
{} |- ((￢(φ∧ψ))⇔((￢φ)∨(￢ψ)))
proof
1 ￢((φ∧ψ)) [ax]
2 (￢((￢φ)∨(￢ψ))) [ax]
3 φ [ax]
4 ψ [ax]
5 (φ∧ψ) [∧in 3,4]
6 (￢φ) [￢in 5,1 el 3]
7 ((￢φ)∨(￢ψ)) [∨inR 6]
8 (￢ψ) [￢in 7,2 el 4]
9 ((￢φ)∨(￢ψ)) [∨inL 8]
10 ((￢φ)∨(￢ψ)) [￢el 9,2 el 2]
11 ((￢(φ∧ψ))⇒((￢φ)∨(￢ψ))) [⇒in 10 el 1]
12 ((￢φ)∨(￢ψ)) [ax]
13 (￢φ) [ax]
14 (φ∧ψ) [ax]
15 φ [∧elR 14]
16 (￢(φ∧ψ)) [￢in 15,13 el 14]
17 ((￢φ)⇒(￢(φ∧ψ))) [⇒in 16 el 13]
18 (￢ψ) [ax]
19 (φ∧ψ) [ax]
20 ψ [∧elL 19]
21 (￢(φ∧ψ)) [￢in 20,18 el 19]
22 ((￢ψ)⇒(￢(φ∧ψ))) [⇒in 21 el 18]
23 (￢(φ∧ψ)) [∨el 12,17,22]
24 (((￢φ)∨(￢ψ))⇒(￢(φ∧ψ))) [⇒in 23 el 12]
25 ((￢(φ∧ψ))⇔((￢φ)∨(￢ψ))) [⇔in 11,24]
■
エーリル
「なにこれスタイリッシュ」
ディアナ
「￢が()の中に入ったら∨と∧が入れ替わる感じですね」
エーリル
「これは思いつかないので、賢者引退します」
ディアナ
（こんなのやってる時点で十分賢者してると思います）
■thm0.24(￢∧∨のド・モルガンの法則 2)
{} |- ((￢(φ∨ψ))⇔((￢φ)∧(￢ψ)))
1 (￢(φ∨ψ)) [ax]
2 φ [ax]
3 (φ∨ψ) [∨inR 2]
4 (￢φ) [￢in 3,1 el 2]
5 ψ [ax]
6 (φ∨ψ) [∨inL 5]
7 (￢ψ) [￢in 6,1 el 5]
8 ((￢φ)∧(￢ψ)) [∧in 4,7]
9 ((￢(φ)∨(ψ))⇒((￢φ)∧(￢ψ))) [⇒in 8 el 1]
10 ((￢φ)∧(￢ψ)) [ax]
11 (φ∨ψ) [ax]
12 φ [ax]
13 (￢φ) [∧elR 10]
14 ⊥ [⊥in 12,13]
15 (φ⇒⊥) [⇒in 14 el 12]
16 ψ [ax]
17 (￢ψ) [∧elL 10]
18 ⊥ [⊥in 16,17]
19 (ψ⇒⊥) [⇒in 18 el 16]
20 ⊥ [∨el 11,15,19]
21 (￢(φ∨ψ)) [raa 20 el 11]
22 (((￢φ)∧(￢ψ))⇒(￢(φ∨ψ))) [⇒in 21 el 10]
23 ((￢(φ∨ψ))⇔((￢φ)∧(￢ψ))) [⇔in 9,22]
■
ディアナ
「ほんと誰がこれを思いついたんでしょうね」
エーリル
「やっぱり思いつかないので、賢者引退します」
ディアナ
「raaと⊥inはメモの中ではじめて使いましたね」
エーリル
「RAAとraaは使い道ないと思ってたけど……。
そうか、これはどちらに場合分けしても矛盾するって証明か。
矛盾したときにexplosionで(φ∧(￢φ))を証明して、∧elでφと(￢φ)から￢elの流れになるけど、それだと行数も文字数も増えてしまう。
なるほどなー、RAAとraaは欲しくなる」
ディアナ
「賢者引退しなくて大丈夫じゃないですか」
