1 束縛変数の基本概念
1.1 量化記号と変数の結びつき
1.1.1 全称量化における束縛
全称量化（∀）では、量化子の直後に置かれる変数が、その量化された範囲で任意の要素として扱われる。例えば、式が「ある対象が任意の要素について成り立つ」ことを述べる形になっている場合、当該変数は、∀が指定する局所的な文脈の中で意味を固定される。これにより、式全体の真偽評価では、その変数に対する解釈が統一的に規定される。
1.1.2 存在量化における束縛
存在量化（∃）では、同様に量化子の直後の変数が、その範囲内で「条件を満たす具体例が存在する」ことに関わる。全称と異なり、存在量化は「少なくとも一つ」への言及を含むため、変数は量化スコープ内で成否の根拠となる対象として機能する。結果として、式の意味は、その変数に対する取り方が量化の範囲でのみ有効である点に支えられる。
1.2 スコープ（作用範囲）の考え方
1.2.1 量化子が及ぶ部分の定義
スコープとは、量化記号がその変数に対して意味を与える範囲（作用する部分）を指す。論理式は構文木として捉えられるため、量化子はその構文上の特定の部分式に対応して作用する。したがって、どの部分がスコープに入るかを明示するには、括弧や構文上の位置関係が重要になる。
1.2.2 スコープ内外での扱いの違い
スコープの内側では、量化子に結びついた変数は束縛変数として扱われ、解釈の対象としては量化子の指定に従う。一方、スコープの外側では同じ記号の変数が現れても、通常は別の意味として扱う必要がある。ここでの要点は、「変数の名前が同じであること」と「同じ束縛に属すること」は同一ではない、という区別である。
1.3 自由変数との対比
1.3.1 自由変数の定義
自由変数とは、いずれの量化子にも束縛されない変数である。したがって式を評価するには、自由変数に対応する値（割当）を外部から与える必要が生じる。外部条件に依存するため、自由変数を含む式は「開いた文」になり、全体の真偽は割当の仕方によって変化し得る。
1.3.2 束縛変数の位置づけ
束縛変数は、量化子によって局所的に意味が閉じられ、スコープ内で一貫した解釈規則を持つ。これにより、束縛された部分式の評価は、当該量化子が述べる性質に従って決定される。結果として、束縛変数は式の意味を「閉じる」方向に働き、自由変数のように外部割当へ委ねる度合いが小さくなる。
2 「用語F（束縛変数）」という表記の意味
2.1 用語Fの位置づけ
2.1.1 論理式における指定方法
表記の「F」は、束縛対象となる変数（記号）を一般化して示すために用いられる指定語として理解できる。すなわち、ある論理式中の特定の量化子が指定する変数記号が、束縛されていることを述べる文脈で使われる。重要なのは、ここでの記号Fが、常に特定の意味論的対象を直接指すのではなく、「量化子の結びつきが与える意味」に従って機能する点である。
2.1.1.1 例示：量化された変数の識別
例えば、∀x P(x) のように記号xが量化子の直後に置かれていれば、このxはその範囲で束縛変数である。一般に「量化された変数の識別」は、当該変数が量化子と同じ結びつきを持つかどうかを判定することで行われる。括弧や構造によってスコープが決まるため、どの部分式にxが現れているかも同時に確認する必要がある。
2.2 束縛変数を含む式の読み方
2.2.1 変数の意味が固定される条件
式の読解では、束縛変数はその量化子のスコープ内で固定された意味を持つと扱う。したがって、同じ変数記号があっても、その出現位置がスコープ内か外かで意味が変わり得る。固定の条件は「量化子により束縛されているか」に尽き、単なる文字列一致では判断しない。
2.2.2 解釈時の注意点
解釈では、束縛関係を構文から取り出してから意味論的評価に入ることが望ましい。特に、ネストした量化（量化子が量化子の中に現れる形）では、外側の量化と内側の量化が異なる束縛を作ることがある。そのため、どの量化子がどの出現に対応するかを追跡する注意が必要になる。
2.3 表記上の混同を避けるルール
2.3.1 量化の対応の取り違え防止
量化子の結びつきは、出現する位置の前後関係や括弧によって定まる。読解・記述の実務では、スコープを明確化するために括弧を省略しない、または読みやすい形に正規化することが混同防止に役立つ。対応の取り違えは、意図せず別の束縛に属する出現を同一視してしまうことで起こりやすい。
2.3.2 変数名の衝突（束縛のやり直し）
同じ変数名を異なる量化子が共有すると、見かけ上は衝突して見えることがある。実際には衝突というより、どの束縛に属するかという関係が曖昧にならないように取り扱う必要がある。衝突が起こりそうな場合は、変数名の付け替え（α変換）によって束縛の構造を保持したまま表記を整える。
3 形式操作における束縛変数の振る舞い
3.1 置換（代入）と束縛変数
3.1.1 自由変数の置換との違い
自由変数に対する置換（代入）は、その変数がスコープ外で外部に開いているため、定めた項に置き換える操作として意味が素直に定まる。対照的に、束縛変数を含む置換は注意を要する。なぜなら、束縛変数は量化子によって支配され、置換によってスコープ構造が変質したり、意図しない変数の挿入が起きたりし得るからである。
3.1.2 束縛変数を含む置換の制約
束縛変数を含む場合、通常は「量化子が生み出した範囲」を保つ形で置換を行う。具体的には、束縛変数そのものに対して置換を適用するのではなく、当該束縛に属さない位置に対してのみ操作を限定する、という設計が多い。加えて、置換対象の項がスコープ内の自由変数を新たに捕獲しないこと（後述の捕獲回避）が実務上の主要条件になる。
3.2 α変換（同値な変数名の取り替え）
3.2.1 変数名変更が意味を変えない理由
α変換は、束縛変数の名前を取り替える操作であり、同じ束縛構造を保つ限り論理式の意味は変わらない。理由は、量化子が与えるのは「特定の記号そのもの」ではなく、「スコープ内での束縛関係」であるためである。従って、束縛の影響を受ける出現箇所を一貫して改名するなら、評価結果は不変となる。
3.2.2 取り替えの実務的手順
実務では、改名したい束縛変数に対応する出現を全て同一の新記号に置換し、同時にスコープの境界を変えないようにする。さらに、他の束縛変数や自由変数と名前が衝突しないよう確認が必要である。衝突が想定される場合は、より安全な新記号を選んでからα変換を実行する手順が取られる。
3.3 捕獲回避（変数捕獲の防止）
3.3.1 変数捕獲が起こる状況
変数捕獲は、置換を行った結果として、ある自由変数が本来とは異なる量化子のスコープ内に入り込み、束縛されてしまう現象である。すると、元の意図は「自由のまま残るはずの変数」に対して、量化の規則が適用されてしまう。これは論理的意味の変更につながり得るため、注意が要る。
3.3.2 捕獲を避けるための手当て
捕獲回避の一般的な方法は、置換に入る前に必要に応じてα変換で変数名を調整し、スコープが絡む衝突を取り除くことである。具体的には、置換対象の項に含まれる自由変数と、置換先のスコープを構成する束縛変数名との干渉を検査し、問題があれば束縛変数の名前を安全なものに更新する。これにより、置換後も自由性・束縛性の関係が保持される。
4 重要性と関連概念
4.1 形式論理における意味論的役割
4.1.1 解釈（モデル）との関係
意味論では、量化子と束縛変数は、モデル内の要素集合に関する規則を組み立てる装置として機能する。全称は「対象の全てに対して成り立つ」ことを要求し、存在は「満たす要素が存在する」ことを要求する。束縛変数はこの要求の中心であり、モデルでの評価手続きにおいて量化の対象を確定させる。
4.1.2 真理条件の構成
束縛の有無は、真理条件の定義に直接影響する。自由変数がある場合、真偽は割当を固定しないと定まらないが、束縛がある場合は量化により割当依存が解消されることが多い。結果として、束縛構造は「式がいつ真になるか」を、モデル上の操作（全て・少なくとも一つの選択）として具体化する。
4.2 構文論的役割
4.2.1 証明操作での扱い
証明では、推論規則を適用する際に式の形を変形するが、その際に束縛変数の構造を壊さないことが重要になる。特に、量化を含む前提や結論を扱う場面では、置換・単置換・規則適用が束縛関係と整合する形で設計される。α変換や捕獲回避がここで実効性を持ち、誤った自由化や束縛の混入を防ぐ。
4.2.2 正規形・同値性との関係
束縛変数は、式の同値性を議論する際の基準にも関わる。例えば、α変換で得られる式は同一の束縛構造を持つため、同値として扱われることが多い。さらに、証明探索や正規化では、束縛変数の名前を整えて比較可能性を高める工夫がなされる。これにより、表記の違いによる見かけ上の相違が抑えられる。
4.3 近接する概念
4.3.1 束縛とスコープの拡張（多重量化）
多重量化では、単一の量化子に複数の要素型や複数の変数が関わるため、束縛の影響範囲をより注意深く管理する必要がある。とはいえ基本の考え方は共通で、スコープ内でのみ束縛が効き、外側では異なる振る舞いになる点が核となる。束縛の設計は、表現力と推論の扱いやすさの両立に関わる。
4.3.2 型理論・ラムダ計算との類似性
ラムダ計算では、λ抽象が変数を束縛し、その本体の中で変数の意味を固定する。これにより、自由変数・束縛変数、α変換（抽象変数名の付け替え）、捕獲回避（β簡約時の変数干渉の管理）といった概念が、述語論理の束縛変数と強く対応する。型理論でも同様に、束縛が式の構造と評価規則に組み込まれ、意味保持のための変数管理が中心的な技術となる。