自由変数、一階述語論理の論理的公理、推論規則
2017/1/30
∀inの定義を修正しました
〇健全な研究室
さトぅー
「代入は定義した。
自由変数を定義すれば、論理的公理と推論規則の話ができるわね」
エーリル
「どんな定義？」
■自由変数fvの定義
nを1以上の自然数(1,...)とする。
(1) Rが項数nの関係記号でt_1,...,t_nが項 ならば
fv(R(t_1,...,t_n)) := tv(t_1)∪...∪tv(t_n)
φ,ψを論理式,xを変数記号とする。
(2) fv((φ⇒ψ)) := fv(φ)∪fv(ψ)
(3) fv((￢φ)) := fv(φ)
(4) fv((∀x φ)) := fv(φ)＼{x}
fv(φ)をφに含まれる自由変数と読むことにする。
エーリル
「tvは項に含まれる変数記号の集まりってわかるけど、＼ってなに？」
さトぅー
「直感的には左の集まりから右の集まりを引くの」
・例：変数x,y,zについて
{x,y,z}＼{x,y} = {z}
エーリル
「＼の右の集まりをキャンセルするのか。
……あれ、{x}＼{y}なんかはどうなるの？
左の集まりにキャンセルする相手がいないんだけど」
さトぅー
「相手がいないモノは無視するの。例えばこんな感じ」
・例：変数x,yについて
{x}＼{y} = {x}
エーリル
「代入に比べたら簡単か」
さトぅー
「いくつか自由変数の例を作るわね」
■例
y_1,z:変数記号
走った:項数1の関係記号
混ぜた:項数2の関数記号
・fv((∀z (￢混ぜた(y_0,z))))
= fv((￢混ぜた(y_0,z)))＼{z} [fvの定義(4)]
= fv(混ぜた(y_0,z))＼{z} [fvの定義(3)]
= (tv(y_0)∪tv(z))＼{z} [fvの定義(1)]
= ({y_0}∪{z})＼{z} [tvの定義(2)]
= {y_0,z}＼{z} [∪を計算]
= {y_0} [＼を計算]
・fv((走った(z)⇒(∀z 混ぜた(y_0,z))))
= fv(走った(z))∪fv((∀z 混ぜた(y_0,z))) [fvの定義(2)]
= tv(z)∪(fv(混ぜた(y_0,z))＼{z}) [fvの定義(2),fvの定義(4)]
= {z}∪(({y_0}∪{z})＼{z}) [tvの定義(2),fvの定義(1)]
= {z}∪({y_0,z}＼{z}) [∪を計算]
= {z}∪{y_0} [＼を計算]
= {z,y_0} [∪を計算]
さトぅー
「感覚的には∀がくっついてない変数を全部取ってくる感じかしら。
だたし、∀の外側で生き残っている場合は自由変数になるわね」
エーリル
「なるほどなるほど。
変数が∀に捕まったとしても、∀の外まで逃げ切ったら自由なのね」
さトぅー
「あとはメタじゃない一階述語論理の=。
今までの=はメタだったけど、ここからは違うことにするわね」
■項数2の関数記号、関係記号
項数2の関数記号、関係記号について、次のように定義し、都合によって使い分ける。
t,u:項
f:項数2の関係記号
(tfu) :⇔ f(t,u)
R:項数2の関係記号
(tRu) :⇔ R(t,u)
特に等号=は、以下のように定義される。
=:項数2の関係記号
(t = u) :⇔ =(t,u)
エーリル
「今まで=は2つの変数の間に書いたけど、定義しないと文法ミスになるのか。
言われてみれば当たり前だった」
さトぅー
「1+2とかもそうね。
文法に従うなら+(1,2)だけど、伝統とか読みやすさの都合でこんな並び方で書くこともある」
天々城
「できれば統一してほしいんだけど、不便になることもあるんだよナあ……」
さトぅー
「確認だけど、公理は自分で決めていいものだったわよね？」
エーリル
「うん、そうだった」
さトぅー
「ここからは公理系は公理の集まり、公理は公理系の中の一つとして言葉を使い分けるけど、大丈夫？」
エーリル
「OK」
さトぅー
「これですべての準備が整ったから、一階述語論理の論理的公理、推論規則を紹介できる」
エーリル
「長かった」
■一階述語論理G1の論理的公理
φ,ψ,ρ:論理式
x,y,z:変数記号
t:項
とする。
Ax1 (φ⇒(ψ⇒φ))
Ax2 ((φ⇒(ψ⇒ρ))⇒((φ⇒ψ)⇒(φ⇒ρ)))
Ax3 (((￢ψ)⇒(￢φ))⇒(φ⇒ψ))
Ax4 ((∀x φ)⇒(φ[t/x]))
Ax5 ((∀x (φ⇒ψ))⇒(φ⇒(∀x ψ))) [fv(φ)はxを含まない]
Ax6 (∀x (x = x))
Ax7 (∀x (∀y ((x = y)⇒((φ[x/z])⇒(φ[y/z])))))
■一階述語論理G1の推論規則
φ (φ⇒ψ)
-----------[⇒el]
ψ
φを結論とするすべての仮定かつ公理ψが、fv(ψ)がxを含まないとき
φ
--------[∀in]
(∀x φ)
エーリル
「Ax7まであるし、なんか括弧書きがある……。
いやでも、Ax1,Ax2,Ax3,⇒elは命題論理と一緒か」
さトぅー
「残りのAx4,Ax5,∀inは∀の扱いを、Ax6,Ax7は=の扱いを言っているわね。だから命題論理を拡張して、文章の内部まで扱えるようにしたのが一階述語論理になっている」
エーリル
「やっぱりパワーアップか。
じゃあ命題論理の定理って、一階述語論理でもいえるのかな」
さトぅー
「そうなんだけど、一つ修正しないといけない」
エーリル
「えっ、なに？」
さトぅー
「──演繹定理」
