∃
〇健全な研究室
エーリル
「そろそろ魔力切れそう」
さトぅー
「ちょうど話のキリもいいし、次で最後にしましょうか」
エーリル
「わかった」
さトぅー
「この話を始める前に、エーリルさんがこんなことを言ってたわよね」
------------
なんで{(φ⇒ψ)} |- (ψ⇒φ)ではない論理式φ,ψが存在するってわかったの？
------------
エーリル
「言った言った」
さトぅー
「『存在する』は一階述語論理くらいの能力があれば定義できるの」
■∃の定義
φ:論理式
x:変数記号
(∃x φ) :⇔ (￢(∀x (￢φ)))
エーリル
「えっと、『すべてのxについてφじゃない、じゃない』か。
いまいちピンとこないけど」
さトぅー
「私は人間で、エーリルさんはエルフよね」
エーリル
「確かに」
さトぅー
「xには私かエーリルさんだけを代入していいとして、次の文章で試すわね」
・この研究室にいるxはエルフじゃない。
・この研究室にいるさトぅーはエルフじゃない。
・この研究室にいるエーリルはエルフじゃない。
エーリル
「最後が違う」
さトぅー
「そうね。だから次の文章は嘘になる」
・すべてのxについて、この研究室にいるxはエルフじゃない
さトぅー
「逆に考えて、この文章が正しかったら、『この研究室にはエルフはいない』ってことよね」
エーリル
「そんなの当たり前でしょ。
全員エルフじゃないなら、エルフはいな……あっ」
さトぅー
「いないってことは、『存在しない』ってことよね」
エーリル
「あっ、ああぁ！
なるほどなるほど、一番外側の￢はそういうことか！」
さトぅー
「ホントに研究室からエルフが存在しなくなる前に最後まで進めるわね」
■thm1.6
φ:論理式
x:変数記号
t:項
{(φ[t/x])} |- (∃x φ)
proof
1 (∀x (￢φ)) [ax]
2 (￢(φ[t/x])) [∀el]
3 (φ[t/x]) [ax]
4 (￢(∀x (￢φ))) [￢in 3,2 el 1]
5 (∃x φ) [def∃ in 4]
■
さトぅー
「これはうまく項tを見つけたら、存在すると言ってもいいよってことね」
エーリル
「さっきの文章だと、私がエルフだから、ここにエルフが存在するって言えるのか。
へー、圧倒的表現力だ」
さトぅー
「推論規則を追加しよう」
■∃in
φ:論理式
x:変数記号
t:項
(φ[t/x])
---------[∃in]
(∃x φ)
さトぅー
「証明で使うときは、色々頑張って項tを作って∃inを使う流れね。
でもうまく作れないときは、背理法や対偶を使って証明することが多いと思う」
エーリル
「まだ使ってないけど、大体想像はできた」
さトぅー
「次で最後にするわね」
■thm1.7
x,y:変数記号
φ,ψ:論理式
fv(ψ)はxを含まないとする。
{(∃x φ),(∀x (φ⇒ψ))} |- ψ
proof
1 (￢ψ) [ax]
2 (∀x (φ⇒ψ)) [ax]
------------
さトぅー
「次の行で2行目に∀elを使うと((φ⇒ψ)[x/x])を導けるわよね」
エーリル
「[x/x]って、まさか……!」
さトぅー
「((φ⇒ψ)[x/x]) = (φ⇒ψ)って証明してるから、3行目は(φ⇒ψ)と書ける」
------------
3 (φ⇒ψ) [∀el 2]
4 φ [ax]
5 ψ [⇒el 4,3]
6 (￢φ) [￢in 5,1 el 4]
7 (∀x (￢φ)) [∀in 6]
8 (∃x φ) [ax]
9 (￢(∀x (￢φ))) [def∃ el 8]
10 ψ [￢el 2,9 el 1]
■
さトぅー
「推論規則を追加しよう」
■∃el
fv(ψ)はxを含まないとする。
(∃x φ) (∀x (φ⇒ψ))
------------------------[∃el]
ψ
エーリル
「え、これが∃el？」
さトぅー
「やっぱりピンとこないかしら」
エーリル
「んー、なんか∨elに似てるけど」
さトぅー
「∨elって場合分けは2パターンよね」
(φ∨ψ) (φ⇒ρ) (ψ⇒ρ)
----------------------------[∨el]
ρ
さトぅー
「∃は∨の拡張版と考えた方が納得できると思う。
例えば、∃elは全パターンをチェックしてρが言えるならρって言ってもいい」
エーリル
「そう言われると、∃inは∨inR,∨inLに似てるように思えてきた」
さトぅー
「∀は∧の拡張版。∀inは∧inに、∀elは∧elR,∧elLに似てるでしょ？」
エーリル
「へー！ そんな感じがしてきた！」
さトぅー
「ということで、私からは以上。
あと、これは天々城からエーリルさんに」(メモ渡す
エーリル
「命題論理のときみたいな内容か。
でもこれ、いつ書いてるんだろう」
さトぅー
「天々城のヤツ、レポートの提出がやたら早いのよね。
授業の演習問題とか、すぐに終わらせて授業と関係ない計算してるし」
エーリル
「書き出すのが早いとか」
さトぅー
「かもね。私は論理学をやってるせいでイヤでも文法が気になるから、書くのが遅くなっちゃうのよね。
まあでも、お菓子の買い出しは天々城の方が遅い」
エーリル
「すぐ帰ってくるみたいな感じだったけど」
さトぅー
「どうだかね。歩き数学してたら溝に落ちたとかじゃない？」
エーリル
「歩き数学とは一体……」
