=
〇健全な研究室
さトぅー
「そろそろメタじゃない=について話したいわね」
エーリル
「同じくらいの感覚でしか使ってない」
さトぅー
「一階述語論理くらいの能力があれば、きちんと書けるから大丈夫」
■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(関数的)
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)みたいな感じ」
さトぅー
「確かにこれを代入って言いたいけど、[/]と被るのよね。
しかも代入は変数の上書き限定だから、関数的とちょっと違う」
エーリル
「あー、代入は変数限定か」
さトぅー
「とりあえず、=が感覚の『等しい』みたいな機能をしてくれるってわかれば問題ないと思う」
エーリル
「それはバッチリ」
