代入
代入
論理式における代入
定義.
φ を論理式とするとき，φ に現れる自由変数 x を別の変数記号 y に置き換えてでき る論理式をここでは $ φ[x ⇝ y] と書く．
またこの操作を代入と呼ぶ．
例
φ が (∀x (x ∈ y)) ∧ (x = z) の場合，$ φ[x ⇝ y] は (∀x (x ∈ y)) ∧ (y = z) という論理式になる．
束縛変数と自由変数の衝突とかをしないように気をつける必要がある
alg-dでは「代入条件」と読んでおく
ここらへんの話は略
$ \varphi [ x \rightsquigarrow y]
\varphi [ x \rightsquigarrow y]
⇝
ここらへんのちゃんとした定式化は、放送大学の記号論理学の授業で見たんだっけ？miyamonz.icon
TAPLにもあったっけ？miyamonz.icon