束縛変数
bound variable
つまり、限量子($ \forall,\exists)の対象になっている変数
関数の実引数てきなやつ
function(x) {return x}のx
function(x) {return x}(x)の最後のxは自由変数
言っていることはわかるが名前の由来？がわからないmrsekut.icon
$ \mathrm{BVar}(\phi)
束縛変数全体の集合
$ \phi[t/x_i]
論理式$ \phiの自由変数$ x_iに、項$ tを代入して得られる論理式