命題論理のメモ１
○エルフの村-エーリルの家
常人なら発狂するような魔力を秘めたエーリルの家に、ドワーフの姫、ディアナが訪れていた。
家の中では紙切れをもったエーリルが発狂したようなステップで発狂していたので、こいつはもうダメ。
ディアナ
「エーリル、いますか？」
エーリル
「最強の言語」
ディアナ
「ちょっと落ち着いたらどうですか？」
エーリル
「これ見て。最強の言語の感覚が顔に出てる」
ディアナ
「わかりませんよ、そんな顔。
あ、これは天々城さんからですね。何か教わったんですか？」
エーリル
「最強の言語」
ディアナ
「それはもういいので、内容を聞かせてください」
～エーリル説明中～
ディアナ
「考えることは文を変形させること、ですか。
なるほど。文を変形させれば考えを形にできてしまう」
エーリル
「天々城さんの世界は恐ろしい言語力に満ちている」
ディアナ
「それを変数を使って圧縮し、必要なときに元に戻せばいい。
凄まじい発想ですね」
エーリル
「それを書いたのがこれ」
*********注意*********
次の順で書いた
定理の番号:例,thm5.7
証明したい定理:
例,{} |- ((φ)∧(ψ))→((ψ)∧(φ))
proof:
1 ρ [ax]
■
よく使う道具なので、覚えると強いよ？
by 天々城
*********************
■thm0.11(∧の結合性)
{} |- ((φ∧(ψ∧ρ))⇔((φ∧ψ)∧ρ))
proof
1 (φ∧(ψ∧ρ)) [ax]
2 (ψ∧ρ) [∧elL 1]
3 ρ [∧elL 2]
4 φ [∧elR 1]
5 ψ [∧elR 2]
6 (φ∧ψ) [∧in 4,5]
7 ((φ∧ψ)∧ρ) [∧in 6,3]
8 ((φ∧(ψ∧ρ))⇒((φ∧ψ)∧ρ)) [⇒in 7 el 1]
9 ((φ∧ψ)∧ρ) [ax]
10 (φ∧ψ) [∧elR 9]
11 φ [∧elR 10]
12 ψ [∧elL 10]
13 ρ [∧elL 9]
14 (ψ∧ρ) [∧in 12,13]
15 (φ∧(ψ∧ρ)) [∧in 11,14]
16 (((φ∧ψ)∧ρ)⇒(φ∧(ψ∧ρ))) [⇒in 9 el 15]
17 ((φ∧(ψ∧ρ))⇔((φ∧ψ)∧ρ)) [⇔in 8,16]
■
ディアナ
「∧は『かつ』ですよね」
エーリル
「∧が３連続で並んだら()をずらせるっぽいね」
ディアナ
「次が∨の３連続ですか」
■thm0.12(∨の結合性)
{} |- ((φ∨(ψ∨ρ))⇒((φ∨ψ)∨ρ))
proof
1 (φ∨(ψ∨ρ)) [ax]
2 φ [ax]
3 (φ∨ψ) [∨inR 2]
4 ((φ∨ψ)∨ρ) [∨inR 3]
5 (φ⇒((φ∨ψ)∨ρ)) [⇒in 4 el 2]
6 (ψ∨ρ) [ax]
7 ψ [ax]
8 (φ∨ψ) [∨inL 7]
9 ((φ∨ψ)∨ρ) [∨inR 8]
10 (ψ⇒((φ∨ψ)∨ρ)) [⇒in 9 el 7]
11 ρ [ax]
12 ((φ∨ψ)∨ρ) [∨inL 11]
13 (ρ⇒((φ∨ψ)∨ρ)) [⇒in 12 el 11]
14 ((φ∨ψ)∨ρ) [∨el 6,10,13]
15 ((ψ∨ρ)⇒((φ∨ψ)∨ρ)) [⇒in 14 el 6]
16 ((φ∨ψ)∨ρ) [∨el 1,5,15]
17 ((φ∨(ψ∨ρ))⇒((φ∨ψ)∨ρ)) [⇒in 16 el 1]
18 ((φ∨ψ)∨ρ) [ax]
19 (φ∨ψ) [ax]
20 φ [ax]
21 (φ∨(ψ∨ρ)) [∨inR 20]
22 (φ⇒(φ∨(ψ∨ρ))) [⇒in 21 el 20]
23 ψ [ax]
24 (ψ∨ρ) [∨inR 23]
25 (φ∨(ψ∨ρ)) [∨inL 24]
26 (ψ⇒(φ∨(ψ∨ρ))) [⇒in 25 el 23]
27 (φ∨(ψ∨ρ)) [∨el 19,22,26]
28 ((φ∨ψ)⇒(φ∨(ψ∨ρ))) [⇒in 27 el 19]
29 ρ [ax]
30 (ψ∨ρ) [∨inL 29]
31 (φ∨(ψ∨ρ)) [∨inL 30]
32 (ρ⇒(φ∨(ψ∨ρ))) [⇒in 31 el 29]
33 (φ∨(ψ∨ρ)) [∨el 19,28,32]
34 (((φ∨ψ)∨ρ)⇒(φ∨(ψ∨ρ))) [⇒in 33 el 18]
35 ((φ∨(ψ∨ρ))⇔((φ∨ψ)∨ρ)) [⇔in 17,34]
■
ディアナ
「∨は『または』でしたよね」
エーリル
「『場合分け』って言ってたから『もしも～なら』ってことかな。
３つの場合をしないといけない」
ディアナ
「それは長くなって当然ですね……」
■thm0.13(∧の可換性)
{(φ∧ψ)} |- (ψ∧φ)
proof
1 (φ∧ψ) [ax]
2 ψ [∧elL 1]
3 φ [∧elR 2]
4 (ψ∧φ) [∧in 2,3]
■
エーリル
「『『ディアナは姫』で『ディアナはドワーフ』』なら
『『ディアナはドワーフ』で『ディアナは姫』』だよね」
ディアナ
「なんで私……」
エーリル
「なんとなく」
■thm0.14(∨の可換性)
{(φ∨ψ)} |- (ψ∨φ)
proof
1 (φ∨ψ) [ax]
2 φ [ax]
3 (ψ∨φ) [∨inL 2]
4 (φ⇒(ψ∨φ)) [⇒in 3 el 1]
5 ψ [ax]
6 (ψ∨φ) [∨inR 5]
7 (ψ⇒(ψ∨φ)) [⇒in 6 el 5]
8 (ψ∨φ) [∨el 1,4,7]
■
ディアナ
「∨の両側の文字を入れ替えましたね」
エーリル
「これ、∧と∨を入れ替えたのをやってるみたい」
■thm0.15(∧∨の吸収 法則1)
{} |- ((φ∧(φ∨ψ))⇔φ)
proof
1 (φ∧(φ∨ψ)) [ax]
2 φ [∧elR 1]
3 ((φ∧(φ∨ψ))⇒φ) [⇒in 2 el 1]
4 φ [ax]
5 (φ∨ψ) [∨inR 4]
6 (φ∧(φ∨ψ)) [∧in 4,5]
7 (φ⇒(φ∧(φ∨ψ))) [⇒in 6 el 4]
8 ((φ∧(φ∨ψ))⇔φ) [⇔in 3,7]
■
■thm0.16(∧∨の吸収 法則2)
{} |- ((φ∨(φ∧ψ))⇔φ)
proof
1 (φ∨(φ∧ψ)) [ax]
2 (φ⇒φ) [thm0.0]
3 (φ∧ψ) [ax]
4 φ [∧elR 3]
5 ((φ∧ψ)⇒φ) [⇒in 4 el 3]
6 φ [∨el 1,2,5]
7 ((φ∨(φ∧ψ))⇒φ) [⇒in 6 el 1]
8 φ [ax]
9 (φ∨(φ∧ψ)) [∨inR 8]
10 (φ⇒(φ∨(φ∧ψ))) [⇒in 9 el 8]
11 ((φ∨(φ∧ψ))⇔φ) [⇔in 7,10]
■
ディアナ
「∧と∨って綺麗な関係を持ってるんですね」
エーリル
「たぶん、それを意識して∧と∨って記号を作ったんだと思う。
それにしても不思議だなあ……」
