一階述語論理のメモ1
2017/1/27
⊥の定義を変更しました
〇エルフの村-エーリルの家
エーリルが帰宅したのでディアナと合流。
さっきまでの話をディアナに伝えた。
ディアナ
「一階述語論理ですか。
命題論理と比べても記号が増えてますね」
エーリル
「表現力も強力に強くなってて凄い」
ディアナ
「記号が増えれば表現力も上がって当然でしょう」
エーリル
「強力な兵器感が半端ない」
■thm1.8(∀の変数記号の交換)
x,y:変数記号
φ:論理式
{(∀x (∀y φ))} |- (∀y (∀x φ))
proof
1 (∀x (∀y φ)) [ax]
2 (∀y φ) [∀el 1]
3 φ [∀el 2]
4 (∀y φ) [∀in 3]
5 (∀y (∀x φ)) [∀in 4]
■
ディアナ
「これは感覚とも一致してますね。
考えているときにもそれほど違いを気にしないですし」
エーリル
「あれ、さトぅーさんの書き込みがある」
ディアナ
「あちらの文字が読めないので、読み上げてください」
************
fv((∃x φ))と((∃y φ)[t/x])の話が間に合わなかった！
∀と同じような結果になるから、もし証明できたら今度来たときに教えて！
************
エーリル
「らしい」
ディアナ
「できるんですか？」
エーリル
「んー、とりあえずやってみる」
■(∃x φ)の自由変数
fv((∃x φ))
= fv((￢(∀x (￢φ)))) [∃の定義]
= fv((∀x (￢φ))) [fvの定義(3)]
= fv((￢φ))＼{x} [fvの定義(4)]
= fv(φ)＼{x} [fvの定義(3)]
エーリル
「お、できたできた」
ディアナ
「￢は無視なんですね」
エーリル
「fv((∃x φ))とfv((∀x φ))は同じなのか。
言われてみれば確かに」
ディアナ
「次は((∃y φ)[t/x])ですね」
エーリル
「∀と同じようなって、まさか……」
(8') 変数記号yがx = yでない かつ tv(t)に含まれない ならば
((∃y φ)[t/x])
= ((￢(∀y (￢φ)))[t/x]) [∃の定義]
= (￢((∀y (￢φ))[t/x])) [代入の定義(7)]
= (￢(∀y ((￢φ)[t/x]))) [代入の定義(8)]
= (￢(∀y (￢(φ[t/x])))) [代入の定義(7)]
= (∃y (φ[t/x])) [∃の定義]
(9') 変数記号yがx = yならば
((∃y φ)[t/x])
= ((￢(∀y (￢φ)))[t/x]) [∃の定義]
= (￢((∀y (￢φ))[t/x])) [代入の定義(7)]
= (￢(∀y (￢φ))) [代入の定義(9)]
= (∃y φ) [∃の定義]
(10') 変数記号yがx = yでない かつ tv(t)に含まれ、変数記号wがx = wでない かつ tv(t)に含まれない ならば
((∃y φ)[t/x])
= ((￢(∀y (￢φ)))[t/x]) [∃の定義]
= (￢((∀y (￢φ))[t/x])) [代入の定義(7)]
= (￢((∀w ((￢φ)[w/y]))[t/x])) [代入の定義(10)]
= (￢((∀w (￢(φ[w/y])))[t/x])) [代入の定義(7)]
= ((￢(∀w (￢(φ[w/y]))))[t/x]) [代入の定義(7)]
= ((∃w (φ[w/y]))[t/x]) [∃の定義]
ただし、wは使用する変数の列の中で、x = yでない かつ tv(t)に含まれない最初の変数記号とする。
もし使用する変数の列の中で、x = yでない かつ tv(t)に含まれない変数記号がない場合は、新しい変数記号wを追加する。
エーリル
「デスヨネー」
ディアナ
「∀の代入の定義が込み入ってますね」
エーリル
「いやでも、これも∀と∃を入れ替えるだけか。
そう考えたら概念が頭に流れ込んでくる感じがしてきた」
ディアナ
「その感覚はよくわからないですね」
■thm1.9(∃の変数記号の交換)
x,y:変数記号
φ:論理式
{(∃x (∃y φ))} |- (∃y (∃x φ))
proof
1 (∃x (∃y φ)) [ax]
2 (∃y φ) [ax]
3 φ [ax]
4 (∃x φ) [∃in 3]
5 (∃y (∃x φ)) [∃in 4]
6 (φ⇒(∃y (∃x φ))) [⇒in 5 el 3]
7 (∀y (φ⇒(∃y (∃x φ)))) [∀in 6]
8 (∃y (∃x φ)) [∃el 2,7]
9 ((∃y φ)⇒(∃y (∃x φ))) [⇒in 8 el 2]
10 (∀x ((∃y φ)⇒(∃y (∃x φ)))) [∀in 9]
11 (∃y (∃x φ)) [∃el 1,10]
■
エーリル
「そうか。∃inは代入を使うし、∃elは論理式の自由変数を気にしないといけない。それに気づいたさトぅーさんがメモに書いたのか」
ディアナ
「錬度の違いですかね。
たぶん私たちがこれを見ても気づかなかったと思います」
エーリル
「ぐぬぬ……」
■thm1.10
x,y:変数記号
φ:論理式
{(∃x (∀y φ))} |- (∀y (∃x φ))
proof
1 (∃x (∀y φ)) [ax]
2 (∀y φ) [ax]
3 φ [∀el 2]
4 (∃x φ) [∃in 3]
5 ((∀y φ)⇒(∃x φ)) [⇒in 4 el 2]
6 (∀x ((∀y φ)⇒(∃x φ))) [∀in 5]
7 (∃x φ) [∃el 1,6]
8 (∀y (∃x φ)) [∀in 7]
■
エーリル
「こっちは天々城さんの書き込みがある」
ディアナ
「なんとおっしゃっていますか？」
**********
逆の{(∀y (∃x φ))}|- (∃x (∀y φ))は証明できない。
証明できないことの証明はできないだろうから、試しに道なりに計算して詰まってみるのがいいだろう。
**********
エーリル
「詰まってみるのがいいだろう、だって」
ディアナ
「つまり問題点を探せということでしょうね」
エーリル
「じゃあやってみる」
proof
1 (∀y (∃x φ)) [ax]
2 (∃x φ) [∀el 1]
3 φ [ax]
4 (∀y φ) [?
エーリル
「あ、ダメだ」
ディアナ
「どうダメだったんですか？」
エーリル
「3行目に∀inを使って(∀y φ)をひねり出したかったんだけど、fv(φ)にyが含まれているときにダメになる。
(￢φ)を公理にして背理法を使うにしても、どうやって背理法に持ち込んでいいかわからない」
ディアナ
「なるほど。背理法なら(￢φ)から始めて、矛盾したときに(￢φ)が公理から消えるので変数を気にしなくていいということですか。
それも無理となると厳しいですね」
エーリル
「うーん、どうすればいいんだ……」
ディアナ
「例文を思いついたので、それで構いませんか？」
エーリル
「OK」
(∃x (∀y 村人yの王はx))
(∀y (∃x 村人yの王はx))
ディアナ
「これなら、全然違いますね。
(∃x (∀y 村人yの王はx))は、すべての村人を統治する王がいる。
(∀y (∃x 村人yの王はx))は、すべての村人に対して王がそれぞれいる。
前者は全世界を統一した王がいると言っていますが、後者はそれぞれの村の村長のような人が必ずいるというだけで、その者が全世界を統治しているとは限らない」
エーリル
「流石はドワーフの姫。格が違った」
ディアナ
「証明にはならないでしょうけど、理解の助けにはなるかと」
エーリル
「確かに」
■thm1.(￢∀∃のド・モルガンの法則1)
x:変数記号
φ:論理式
{} |- ((￢(∃x φ))⇔(∀x (￢φ)))
proof
1 (￢(∃x φ)) [ax]
2 φ [ax]
3 (∃x φ) [∃in 2]
4 (￢φ) [￢in 3,1 el 2]
5 (∀x (￢φ)) [∀in 4]
6 ((￢(∃x φ))⇒(∀x (￢φ))) [⇒in 5 el 1]
7 (∃x φ) [ax]
8 φ [ax]
9 (∀x (￢φ)) [ax]
10 (￢φ) [∀el 9]
11 ⊥ [⊥in 8,10]
12 (φ⇒⊥) [⇒in 11 el 8]
13 (∀x (φ⇒⊥)) [∀in 12]
14 ⊥ [∃el 7,13]
15 (￢(∃x φ)) [raa 14 el 7]
16 ((∀x (￢φ))⇒(￢(∃x φ))) [⇒in 15 el 9]
17 ((￢(∃x φ))⇔(∀x (￢φ))) [⇔in 6,16]
■
■thm1.(￢∀∃のド・モルガンの法則2)
x:変数記号
φ:論理式
{} |- ((￢(∀x φ))⇔(∃x (￢φ)))
proof
1 (￢(∃x (￢φ))) [ax]
2 (￢φ) [ax]
3 (∃x (￢φ)) [∃in 2]
4 φ [￢el 3,1 el 2]
5 (∀x φ) [∀in 3]
6 (￢(∀x φ)) [ax]
7 (∃x (￢φ)) [￢el 5,6 el 1]
8 ((￢(∀x φ))⇒(∃x (￢φ))) [⇒in 7 el 6]
9 (∃x (￢φ)) [ax]
10 (∀x φ) [ax]
11 φ [∀el 10]
12 (￢φ) [ax]
13 ⊥ [⊥in 11,12]
14 ((￢φ)⇒⊥) [⇒in 13 el 12]
15 (∀x ((￢φ)⇒⊥)) [∀in 14]
16 ⊥ [∃el 9,15]
17 (￢(∀x φ)) [raa 16 el 10]
18 ((∃x (￢φ))⇒(￢(∀x φ))) [⇒in 17 el 9]
19 ((￢(∀x φ))⇔(∃x (￢φ))) [⇔in 8,18]
■
エーリル
「これもド・モルガンの法則なのか」
ディアナ
「雰囲気は￢∧∨のときと似てますね」
エーリル
「あ、さトぅーさんの書き込みがある」
**********
このド・モルガンの法則の証明は⊥の自由変数、つまりfv(⊥)に変数xが含まれないようにしないと∃elが使えないわね。だから、
c:定数記号
⊥ :⇔ (￢(c = c))
と定義すれば自由変数が何もないから使いやすくなる。
ただ、命題論理のときと違うから、矛盾になってることを証明しないといけない)
それと∧∨⇔⊥の自由変数、代入を確かめた方がいいわね。
**********
ディアナ
「メモが終わりってことは、エーリルが自分で埋めるしかないですね」
エーリル
「賢者に不可能はない」
