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

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

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

エラーが発生しました。

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

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

=の式変形,[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が変数のときと、∀が絡んだときが面倒だけど、計算は道なりに進めば簡単ね」


エーリル

「これには流石の賢者も苦笑い」

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

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

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

↑ページトップへ