代入
2017/4/3
代入の定義を変更しました。
〇健全な研究室
さトぅー
「命題論理なら論理式を定義してすぐに論理的公理と推論規則の話ができた。
でも、一階述語論理は代入と自由変数の話をしないと先に進めない」
エーリル
「代入は今まで使ってきたのじゃダメなの？」
さトぅー
「ダメってわけじゃないんだけど、今ならそれなりに定義できる。ちょっと準備がいるけどね」
■項tに含まれる変数の集まりtv(t)の定義
nを1以上の自然数(1,...)とする。
(1) tが定数記号 ならば tv(t):={}
(2) tが変数記号 ならば tv(t):={t}
(3) t = f(t_1,...,t_n)のとき、fが項数nの関数記号でt_1,...,t_nが項 ならば
tv(t) := tv(t_1)∪...∪tv(t_n)
と定義し、tv(t)を項tに含まれる変数の集まり、と読むことにする。
エーリル
「{}や∪はわかるけど、:=ってなに？」
さトぅー
「:=の右側の記号列を使って、左側に右側と等しいって意味で記号列を定義するって意味」
エーリル
「へー、:⇔と似たような感じか。
じゃあ、= はなに？」
さトぅー
「えっ、天々城から教えてもらってない？」
エーリル
「教えてもらってない」
さトぅー
「 = は『等しい』って意味の記号。
一階述語論理だと項数2の関係記号なんだけど、今使った = はメタな記号ね」
エーリル
「使い方よくわからないから、例がほしい」
さトぅー
「いいわよ」
■例
耳,鼻:定数記号
y_1:変数記号
長い:項数1の関数記号
混ぜた:項数2の関数記号
・tv(耳)
= {} [tvの定義(1)]
・tv(y_1)
= {y_1} [tvの定義(2)]
・tv(長い(耳))
= tv(耳) [tvの定義(3)]
= {} [tvの定義(1)]
・tv(混ぜた(y_1,長い(耳)))
= tv(y_1)∪tv(長い(耳)) [tvの定義(3)]
= {y_1}∪{} [tvの定義(2)とtv(長い(耳))={}]
= {y_1} [集まりの中身を合わせた]
エーリル
「あ、なるほど。
等しいものを論理式みたいに並べて、ゴールまで行く感じか」
さトぅー
「そんな感じ。
とりあえず、これで代入の準備ができた」
■代入[ / ]の定義
tは項、xは変数記号、nを1以上の自然数(1,...)とする。
(1) cが定数記号 ならば (c[t/x]) := c
(2) (x[t/x]) := t
(3) yが変数記号でx = yでないならば (y[t/x]) := y
(4) fが項数nの関数記号でt_1,...,t_nが項 ならば
(f(t_1,...,t_n)[t/x]) := f((t_1[t/x]),...,(t_n[t/x]))
(5) Rが項数nの関係記号でt_1,...,t_nが項 ならば
(R(t_1,...,t_n)[t/x]) := R((t_1[t/x]),...,(t_n[t/x]))
φ,ψは論理式とする。
(6) ((φ⇒ψ)[t/x]) := ((φ[t/x])⇒(ψ[t/x]))
(7) ((￢φ)[t/x]) := (￢(φ[t/x]))
(8) 変数記号yがx = yでない かつ tv(t)に含まれない ならば
((∀y φ)[t/x]) := (∀y (φ[t/x]))
(9) 変数記号yがx = y または tv(t)に含まれる ならば
((∀y φ)[t/x]) := (∀y φ)
エーリル
「(9)まであるんだけど……」
さトぅー
「とりあえず、例をあげていくわ」
■例
耳,鼻:定数記号
y_1,x_0,z:変数記号
長い:項数1の関数記号
混ぜた:項数2の関数記号
・((耳)[鼻/y_1])
= 耳 [代入の定義(1)]
・((y_1)[鼻/y_1])
= 鼻 [代入の定義(2)]
・(x_0[鼻/y_1])
=x_0 [代入の定義(3)]
・(長い(y_1)[鼻/y_1])
= 長い((y_1[鼻/y_1])) [代入の定義(4)]
= 長い(鼻) [代入の定義(2)]
・(混ぜた(y_1,長い(耳))[鼻/y_1])
= 混ぜた((y_1[鼻/y_1]),(長い(耳)[鼻/y_1])) [代入の定義(5)]
= 混ぜた(鼻,長い((耳[鼻/y_1]))) [代入の定義(2),(4)]
= 混ぜた(鼻,長い(耳)) [代入の定義(1)]
・((混ぜた(y_1,長い(耳))⇒混ぜた(y_1,長い(耳)))[鼻/y_1])
= ((混ぜた(y_1,長い(耳))[鼻/y_1])⇒(混ぜた(y_1,長い(耳))[鼻/y_1]))
[代入の定義(6)]
= (混ぜた(鼻,長い(耳))⇒混ぜた(鼻,長い(耳)))
[(混ぜた(y_1,長い(耳))[鼻/y_1]) = 混ぜた(鼻,長い(耳)を2回使う]
・((￢混ぜた(y_1,長い(耳)))[鼻/y_1])
= (￢(混ぜた(y_1,長い(耳))[鼻/y_1])) [代入の定義(7)]
= (￢混ぜた(鼻,長い(耳)))
[(混ぜた(y_1,長い(耳))[鼻/y_1]) = 混ぜた(鼻,長い(耳)を使う]
・((∀x_0 混ぜた(y_1,長い(耳)))[鼻/y_1])
= (∀x_0 (混ぜた(y_1,長い(耳))[鼻/y_1])) [代入の定義(8)]
= (∀x_0 混ぜた(鼻,長い(耳)))
[(混ぜた(y_1,長い(耳))[鼻/y_1]) = 混ぜた(鼻,長い(耳)を使う]
・((∀y_1 混ぜた(y_1,長い(耳)))[鼻/y_1])
= (∀y_1 混ぜた(y_1,長い(耳))) [代入の定義(9)]
エーリル
「あれ、(9)って代入してないよね。
文字列そのままだし」
さトぅー
「(9)のときに論理式の文字を入れ替えると、大変なことになるの。
今はわからないと思うから、道具が揃ったら見せてあげる」
エーリル
「楽しみー」
