=の式変形,[x/x]
〇健全な研究室
さトぅー
「代入の計算をするときにこんな書き方をしてたの覚えてる？」
・(長い(y_1)[鼻/y_1])
= 長い((y_1[鼻/y_1])) [代入の定義(4)]
= 長い(鼻) [代入の定義(2)]
エーリル
「なんかふわっとした感覚で=を使ってたのは覚えてる」
さトぅー
「=の項数って『2』でしょ？」
エーリル
「あっ、これ項数1みたいな書き方してる」
さトぅー
「そうね。普通に考えたら文法ミスだから、たぶんなにか定義して使ってるだろうって話になる。
実際これは書いてないところがあるの」
・省略なし
1 (長い(y_1)[鼻/y_1]) = 長い((y_1[鼻/y_1])) [代入の定義(4)]
2 長い((y_1[鼻/y_1])) = 長い(鼻) [代入の定義(2)]
3 (長い(y_1)[鼻/y_1]) = 長い(鼻) [=の推移性 1.2]
エーリル
「=の推移性……、感覚で使ってたのか」
さトぅー
「2行目の左側の項が、1行目と右側の項と同じだから省略。
=の推移性は1行目の左側と、3行目の右側を見ればわかるから書かなかったってわけね。
他の計算例はもっとたくさん変形してたけど、=の推移性を何回も使えば最初と最後が=で繋がってるとわかる。
=が出てきたときに毎回も毎回も同じ話をするのは面倒だし、定理にしてショートカットしようと思う」
■thm1.5(=のn推移性)
n:自然数(0,1,...)
t_1,...,t_(n+1):項
{(t_1 = t_2),(t_2 = t_3),...,(t_n = t_(n+1))} |- (t_1 = t_(n+1))
proof
数学的帰納法で示す。
------------------
さトぅー
「数学的帰納法はわかる？」
エーリル
「証明の長さに関する帰納法ならわかる」
さトぅー
「考え方は、証明の長さに関する帰納法と一緒」
エーリル
「連鎖的に敵を倒し続けるのか」
-------------------
・n=1のとき{(t_1 = t_2)} |- (t_1 = t_2)を証明すればよい。
1 (t_1 = t_2) [ax]
よって{(t_1 = t_2)} |- (t_1 = t_2)。
n=kのとき
{(t_1 = t_2),(t_2 = t_3),...,(t_k = t_(k+1))} |- (t_1 = t_(k+1))
とする。
・n=k+1のとき
1 (t_1 = t_2) [ax]
2 (t_2 = t_3) [ax]
:
:
k (t_k = t_(k+1)) [ax]
k+1 (t_1 = t_(k+1))
[{(t_1 = t_2),(t_2 = t_3),...,(t_k = t_(k+1))}の定理]
k+2 (t_(k+1) = t_(k+2)) [ax]
k+3 (t_1 = t_(k+2) [=の推移性 k+1,k+2]
よって{(t_1 = t_2),(t_2 = t_3),...,(t_k = t_(k+1)),(t_(k+1) = t_(k+2))} |- (t_1 = t_(k+2))。
ゆえに、すべての自然数nについて、{(t_1 = t_2),(t_2 = t_3),...,(t_n = t_(n+1))} |- (t_1 = t_(n+1))
■
さトぅー
「これをいちいち書くのは面倒くさいから定義して省略するわね」
■=の項の省略
n:自然数(0,1,...)
t_1,...,t_(n+1):項
R_i,..,R_n:推論規則,定理など
:
:
i t_1
= t_2 [R_1]
i+1 = t_3 [R_(i+1)]
:
:
n = t_(n+1) [R_n]
を次の論理式の列で定義する。
:
:
i (t_1 = t_2) [R_i]
i+1 (t_2 = t_3) [R_(i+1)]
:
:
n (t_n = t_(n+1)) [R_n]
さトぅー
「後出しで申し訳ないけど、これを=のn推移性と組み合わせれば、代入のときのような計算ができるわけね」
エーリル
「あくまで論理式の列なのか」
さトぅー
「そういうこと。
あと、代入についてやっておかないといけないことがある」
エーリル
「また代入か……」
■meta thm1.3
ρ:論理式
x:変数記号
(ρ[x/x]) = ρ
-------------------
さトぅー
「もちろん、この=はメタな=ね」
エーリル
「え、でもだってこれ当たり前じゃ……」
さトぅー
「証明はどういう流れになりそう？」
エーリル
「えっと、えっと……。
──おかしい、証明が思いつかない」
さトぅー
「証明の長さに関する帰納法、数学的帰納法と同じように帰納法で証明する流れになる。
証明の長さに関する帰納法は、まず証明のスタートを全パターンチェックする。
ある行から次の行への公理や推論規則を全パターンチェックして、問題ないなら証明できたって流れだったわよね」
エーリル
「⇒elとか∀inで場合分けしたのは覚えてる」
さトぅー
「代入って『何パターン』あったかしらね」
エーリル
「…………ちょ、ちょっと待っt」
-------------------
proof
t:項
x:変数記号
まず、項の複雑さに関する帰納法で(t[x/x]) = tを証明する。
--------------------
さトぅー
「項の複雑さに関する帰納法は、まず、項の一番小さな部品になる定数と変数を全パターンチェックする。
次に、適当に項を集めて作った新しい項を全パターンチェックして大丈夫なら、すべての項について証明できたことになる」
エーリル
「先が見えちゃったの、ほんときつい」
さトぅー
「同じようにして次は論理式の複雑さに関する帰納法を使う。
こっちは原子的論理式を全パターンチェックして、適当に論理式を集めて新しく作った論理式を全パターンチェックする流れね。
流れはわかりそう？」
エーリル
「未来予知できたけど、代入の魔境感しかわからなかった」
--------------------
・tが定数記号のとき
(t[x/x])
= t [代入の定義(1)]
よって(t[x/x]) = t
・tが変数記号でt=xのとき
(t[x/x])
= (x[x/x]) [t = x]
= x [代入の定義(2)]
= t [t = x]
よって(t[x/x]) = t
・tが変数記号でt=xでないとき
t[x/x]
= t [代入の定義(3)]
よって(t[x/x]) = t
fが項数nの関数記号でt_1,...,t_nが項で
(t_1[x/x]) = t_1,...,(t_n[x/x]) = t_n
とする。
・t = f(t_1,...,t_n)のとき
(t[x/x])
= (f(t_1,...,t_n)[x/x]) [t=f(t_1,...,t_n)]
= f((t_1[t/x]),...,(t_n[t/x])) [代入の定義(4)]
= f(t_1,...,t_n) [t_1[x/x]=t_1,...,t_n[x/x]=t_n]
= t [t=f(t_1,...,t_n)]
よって(t[x/x]) = t
よってすべての項tについてt[x/x] = t。
--------------------
さトぅー
「これで『項』の証明が終了」
エーリル
「あぁ……」
--------------------
論理式の複雑さに関する帰納法で(ρ[x/x]) = ρを証明する。
Rが項数nの関係記号で、
t_1,...,t_nを項とする。
・ρ=R(t_1,...,t_n)のとき
(ρ[x/x])
=(R(t_1,...,t_n)[x/x]) [ρ=R(t_1,...,t_n)]
=R((t_1[x/x]),...,(t_n[x/x])) [代入の定義(5)]
=R(t_1,...,t_n) [すべての項tについてt[x/x] = t]
=ρ [ρ=R(t_1,...,t_n)]
よって(ρ[x/x])=ρ
(φ[x/x])=φ,(ψ[x/x])=ψとする。
・ρ=(φ⇒ψ)のとき
(ρ[x/x])
=((φ⇒ψ)[x/x]) [ρ=(φ⇒ψ)]
=((φ[x/x])⇒(ψ[x/x])) [代入の定義(6)]
=(φ⇒ψ) [(φ[x/x])=φ,(ψ[x/x])=ψ]
=ρ [ρ=(φ⇒ψ)]
よって(ρ[x/x])=ρ
・ρ=(￢φ)のとき
(ρ[x/x])
=((￢φ)[x/x]) [ρ=(￢φ)]
=(￢(φ[x/x])) [代入の定義()]
=(￢φ) [(φ[x/x])=φ]
=ρ [ρ=(￢φ)]
よって(ρ[x/x])=ρ
yを変数記号とする。
・ρ=(∀y φ)で、x = yでないとき
tv(x)={x}だから、yはtv(x)に含まれない。
(ρ[x/x])
=((∀y φ)[x/x]) [ρ=(∀y φ)]
=(∀y (φ[x/x])) [代入の定義(8)]
=(∀y φ) [(φ[x/x])=φ]
=ρ [ρ=(∀y φ)]
よって(ρ[x/x])=ρ
・ρ=(∀y φ)で、x = yのとき
(ρ[x/x])
=(∀y φ)[x/x] [ρ=(∀y φ)]
=(∀y φ) [代入の定義(9)]
=ρ [ρ=(∀y φ)]
よって(ρ[x/x])=ρ
ゆえに、すべての論理式ρについて(ρ[x/x]) = ρ
■
さトぅー
「tが変数のときと、∀が絡んだときが面倒だけど、計算は道なりに進めば簡単ね」
エーリル
「これには流石の賢者も苦笑い」
