表示調整
閉じる
挿絵表示切替ボタン
▼配色
▼行間
▼文字サイズ
▼メニューバー
×閉じる

ブックマークに追加しました

設定
0/400
設定を保存しました
エラーが発生しました
※文字以内
ブックマークを解除しました。

エラーが発生しました。

エラーの原因がわからない場合はヘルプセンターをご確認ください。

ブックマーク機能を使うにはログインしてください。
エルフに数学を装備するだけ  作者: めいぜんおーえす
三章:一階述語論理
36/51

=

〇健全な研究室



さトぅー

「そろそろメタじゃない=について話したいわね」


エーリル

「同じくらいの感覚でしか使ってない」


さトぅー

「一階述語論理くらいの能力があれば、きちんと書けるから大丈夫」



■thm1.1(=の反射性)

t:項


{}|-(t = t)


proof

x:変数記号


1 (∀x (x = x)) [Ax6]

2 (t = t) [∀el 1]




エーリル

「あれ、∀elって結論に代入を使ってなかった?」


さトぅー

「((x = x)[t/x])は(t = t)ってわかるわよね。

 でも、(φ[t/x])はどう?」


エーリル

「そんなのφがわからないとわかるわけ……。

 あ、そういうことか」


さトぅー

「そうね。わかるときは証明で省略する。

 代入そのものは推論規則じゃないし、メタな計算をしてるから、論理式の列で計算するのはあんまりしたくない。

 だから今回みたいに代入が具体的に計算できるときは代入を省略して、計算できないときは放置するわね」


エーリル

「今までは代入は感覚だったけど、アレはメタで計算してたのか」



■thm1.2(=の可換性)

t,u:項


{(t = u)}|- (u = t)


proof


x,y:tv(t),tv(u)に含まれない変数記号



1 (∀x (∀y ((x = y)⇒((x = x)⇒(y = x))))) [Ax7]


-------------

エーリル

「1行目が納得いかない。

 だって、Ax7ってこんな形だったよね。」


Ax7 (∀x (∀y ((x = y)⇒((φ[x/z])⇒(φ[y/z])))))


さトぅー

「これはx,zを変数記号として、φに(z = x)って論理式を選んだの。

 そうすれば((z = x)[x/z])は(x = x)に、((z = x)[y/z])は(y = x)になるでしょ」


エーリル

「φの選び方が大事なのか。

 x,yがtv(t),t(u)に含まれない変数記号にしてるのは、代入の定義(10)を避けるためかな」


さトぅー

「そういうこと。代入の(10)のパターンにならないからね」

-------------


2 (∀y ((t = y)⇒((t = t)⇒(y = t)))) [∀el 1]

3 ((t = u)⇒((t = t)⇒(u = t))) [∀el 2]

4 (t = u) [ax]

5 ((t = t)⇒(u = t)) [⇒el 4,3]

6 (t = t) [=の反射性]

7 (u = t) [⇒el 6,5]




エーリル

「へー、=の反射性が仕事した」


さトぅー

「もちろん、{} |- (∀x (∀y (x = y)⇒(y = x)))の形で証明してもいいわよ。

 ただ使う局面が多いから、毎回∀elを使って式の中身を呼び出さないといけないけどね」


エーリル

「それはそれで面倒くさいけど、{} |- (∀x (∀y (x = y)⇒(y = x)))も綺麗さで捨てがたい」




■thm1.3(=の推移性)

t,u,v:項

{(t = u),(u = v)}|- (t = v)


proof

x,y,z:tv(t),tv(u),tv(v)に含まれない変数記号


1 (∀x (∀y ((x = y)⇒((x = v)⇒(y = v))))) [Ax7]

2 (∀y ((u = y)⇒((u = v)⇒(y = v)))) [∀el 1]

3 ((u = t)⇒((u = v)⇒(t = v))) [∀el 2]

4 (t = u) [ax]

5 (u = t) [=の可換性 4]

6 ((u = v)⇒(t = v)) [⇒el 5,3]

7 (u = v) [ax]

8 (t = v) [⇒el 7,6]



さトぅー

「これも{} |- (∀x (∀y (∀z ((x = y)⇒((y = z)⇒(x = z))))))を証明してもいいわね。

 むしろこっちの方が好まれると思う」


エーリル

「反射性,可換性,推移性が揃ってたの、確か⇔もそうだった気がする」


さトぅー

「⇔は同値って読むし、=は等しいって読むから自然言語での感覚は近いわね。

 でも⇔は論理式を結んで、=は項を結ぶから、⇔と=はまったく別物」


エーリル

「今ならすごいよくわかる。

 私は違いがわかるエルフだもんね」




■thm1.4(関数(funct)(ional))

t,u:項

f:項数1の関数記号


{(t = u)} |- (f(t) = f(u))


proof

x,y:tv(t),tv(u)に含まれない変数記号


1 (∀x (∀y ((x = y)⇒((f(x) = f(x))⇒(f(y) = f(x)))))) [Ax7]

2 (∀y ((t = y)⇒((f(t) = f(t))⇒(f(y) = f(t))))) [∀el 1]

3 ((t = u)⇒((f(t) = f(t))⇒(f(u) = f(t)))) [∀el 2]

4 (t = u) [ax]

5 ((f(t) = f(t))⇒(f(u) = f(t))) [⇒el 4,3]

6 (f(t) = f(t)) [=の反射性]

7 (f(u) = f(t)) [⇒el 6,5]

8 (f(t) = f(u)) [=の可換性 7]




さトぅー

「これもできれば(∀x (∀y ((x = y)⇒(f(x) = f(y)))))で証明したいけど、使いやすさはこっちの方がいいと思う」


エーリル

「これ代入っぽくない?

 (f(t)[t/u])=f(u)みたいな感じ」


さトぅー

「確かにこれを代入って言いたいけど、[/]と被るのよね。

 しかも代入は変数の上書き限定だから、関数的とちょっと違う」


エーリル

「あー、代入は変数限定か」


さトぅー

「とりあえず、=が感覚の『等しい』みたいな機能をしてくれるってわかれば問題ないと思う」


エーリル

「それはバッチリ」

評価をするにはログインしてください。
ブックマークに追加
ブックマーク機能を使うにはログインしてください。
― 新着の感想 ―
このエピソードに感想はまだ書かれていません。
感想一覧
+注意+

特に記載なき場合、掲載されている作品はすべてフィクションであり実在の人物・団体等とは一切関係ありません。
特に記載なき場合、掲載されている作品の著作権は作者にあります(一部作品除く)。
作者以外の方による作品の引用を超える無断転載は禁止しており、行った場合、著作権法の違反となります。

この作品はリンクフリーです。ご自由にリンク(紹介)してください。
この作品はスマートフォン対応です。スマートフォンかパソコンかを自動で判別し、適切なページを表示します。

↑ページトップへ