束縛変数と自由変数：変数のスコープを理解する - 記号論理学
量化子を使う際に重要なのが、束縛変数と自由変数の区別です。変数が量化子によって「縛られている」かどうかで、論理式の意味が大きく変わります。プログラミングにおける変数のスコープと類似した概念です。
束縛変数と自由変数
束縛変数（bound variable）は、量化子によって束縛されている変数です。∀x や ∃x の直後に来る式の中の x が束縛変数です。
自由変数（free variable）は、量化子によって束縛されていない変数です。式の外側から値を受け取る「空きスロット」のようなものです。
量化子のスコープ内にあり、特定の値を持たない。∀x P(x) の x は束縛変数。
量化子に縛られず、外部から値が与えられる。P(x) ∧ Q(y) の x, y は自由変数。
具体例
∀x(P(x) → Q(x)) では、x はすべて束縛変数です。「すべての x について」という量化子のスコープが式全体に及んでいます。
∀x P(x) → Q(y) では、x は束縛変数ですが、y は自由変数です。量化子 ∀x のスコープは P(x) だけであり、Q(y) には及びません。
「すべての x について P(x)」ならば「Q(y)」。y は外部から与えられる値。
量化子の直後の括弧が、そのスコープを示す。括弧がない場合は最も近い部分式だけがスコープ。
同じ変数名の異なる出現
同じ変数名でも、出現箇所によって束縛状況が異なることがあります。
∀x P(x) ∧ Q(x) という式を考えましょう。最初の x は ∀x に束縛されていますが、Q(x) の x は自由変数です（量化子のスコープが P(x) だけなので）。
このような混乱を避けるため、通常は異なる変数名を使うか、括弧を明示して ∀x(P(x) ∧ Q(x)) のようにスコープを明確にします。
閉じた式と開いた式
自由変数を含まない式を閉じた式（closed formula）または文（sentence）と呼びます。閉じた式は真か偽かが確定します。
自由変数を含む式を開いた式（open formula）と呼びます。開いた式は、自由変数に値を代入しない限り、真偽が定まりません。
∀x P(x)、∃x∃y L(x,y) など。自由変数がない。真偽が確定する。
P(x)、∀x L(x,y) など。自由変数がある。真偽は変数への代入に依存する。
代入と束縛変数
変数に値（項）を代入する操作は、自由出現にのみ適用されます。束縛出現には代入できません。
φ(x) に項 t を代入した結果を φ(t/x) や φ[t/x] と書きます。これは、φ の中の x の自由出現をすべて t で置き換えたものです。
たとえば P(x) ∧ ∀x Q(x) に t を代入すると、P(t) ∧ ∀x Q(x) になります。∀x Q(x) の中の x は束縛されているので置き換わりません。
自由出現を特定する
自由出現のみを項 t で置き換える
束縛出現はそのまま残る
変数の捕獲
代入の際に注意すべきことがあります。代入した項 t に含まれる変数が、代入先で束縛されてしまう現象を「変数の捕獲」（variable capture）といいます。
∀y P(x, y) に y を代入して ∀y P(y, y) とすると、代入した y が ∀y に捕獲されてしまい、意図した意味と異なります。
これを避けるには、代入前に束縛変数の名前を変更します。∀y P(x, y) を ∀z P(x, z) と書き換えてから y を代入すれば、∀z P(y, z) となり問題ありません。
このように、変数のスコープを正確に理解することは、述語論理を正しく扱う上で必須です。次回は、述語論理の形式化の全体像を見ていきます。
