§A3.12述語と自由変数・束縛変数

1 自由変数と束縛変数

$P(x)$の$x$は自由変数であり、$P(4)$のように具体的な値を入れることができます。$\forall x\,P(x)$の$x$は量化子$\forall$のスコープにある束縛変数であり、量化の対象を走るための名前です。

2 束縛変数は名前を替えても主張が変わらない

束縛変数の改名は、$\displaystyle\sum_{k=1}^n a_k$の添字$k$を$j$に改名して$\displaystyle\sum_{j=1}^n a_j$と書くことや、$\displaystyle\int_0^1 f(x)\,dx$の積分変数$x$を別の文字に改名することに対応します。総和の添字と積分変数は、束縛変数を理解するための類比であり、量化子と同一の記号ではありません。

一方、自由変数の名前だけを替えると、どの値を固定しているかが変わるため、一般に別の述語になります。$P(x)$と$P(y)$の$x,y$が別の対象を指す場合に、二つの述語を同じものとして扱うことはできません。

3 自由変数を固定するか、量化するか

同じ述語から出発しても、自由変数をどう扱うかによって、得られる主張が変わります。

全称命題$\forall x\in X\,Q(x)$を証明するときは、任意の$a\in X$を一つとり、議論の間は$a$を固定します。この操作は証明内で対象を局所的に固定することであり、式の量化子が変数を束縛することとは区別します。$a\in X$以外の追加条件を仮定せずに$Q(a)$を導くことができれば、$a$の任意性から、すべての$x\in X$について$Q(x)$と結論することができます。反対に、議論の途中で$a$に追加条件を課すと、その条件を満たす対象についてしか$Q(a)$を示していないため、全称命題を結論することはできません。

4 束縛変数はその場限りの名前である

束縛変数の名前は、そのスコープの内側でだけ通用します。したがって、外側で使っている文字と束縛変数の名前が重なると、変数の衝突が生じます。束縛変数を改名するときは、定理 2.1の衝突しないという条件を確かめます。プログラムでも、変数名が有効なスコープを区別し、内側の変数が外側の変数を覆い隠さないようにします。これは論理式のスコープを理解する類比であり、プログラムの変数と論理式の変数を同一視するものではありません。数式処理系も、束縛変数のスコープと変数の衝突を区別して式を扱います。