|| 知ってるけど考えてみるとよく分からんやつ
「なんでも（？）入れていい」もの
スポンサーリンク
目次
個体変数「変数全般を指す言葉」
変数と変項の違い「特にない」
束縛変数「値が定まっている個体変数」
自由変数「値が定まっていない個体変数」
開論理式「自由変数がそのままの論理式」
閉論理式「自由変数が固定された論理式」
個体変数 Individual Variable
|| 範囲内のどれかを取り得る空っぽの枠
これは『変数（変項）の総称』で
\begin{array}{ccc} 自由変数 &\subset& 個体変数 \\ \\ 束縛変数 &\subset& 個体変数 \end{array}
具体的にはこういうものを指しています。
（変数・変項は２つに分類できる）
個体と個体変数
一階述語論理の表現で
『個体の量化のみ許す』みたいな宣言があるんですが
（個体は定数と変数の両方を総称する用語）
\begin{array}{r} \forall x &A(x) \\ \\ \exists x&A(x) \end{array}
ここで使われている「個体」の意味は
正確には「個体変数」のみになります。
（この辺りちょっとややこしい）
変数と変項
変数にはこの２つの呼び方があるんですが
\begin{array}{c} 0&=&\{\} \\ \\ 1&=&\Bigl\{ \{\} \Bigr\} \\ \\ 2&=& \Bigl\{ \{\},\{\{\}\} \Bigr\} \\ \\ &\vdots \end{array}
「数」の定義や
（実態は集合で数字は名札）
\begin{array}{c} \mathrm{Constant}&\subset&\mathrm{Term} \\ \\ \mathrm{Variable}&\subset&\mathrm{Term} \\ \\ && \mathrm{Term}&\subset&\mathrm{Number} \end{array}
「項」の定義を考えると
\begin{array}{ccc} \mathrm{Constant}∪\mathrm{Variable}&=&\mathrm{Number} &&？ \end{array}
明確に区別する理由はほぼありません。
（実際ちゃんと区別して使われることはほぼ無い）
束縛変数 Bound Variable
|| 束縛されてるっていうワードセンス
「束縛されている個体変数」のことで
\begin{array}{ccc} ある操作がxを制限する &\Longleftrightarrow& xは束縛変数 \end{array}
厳密には「量化子」によって定義されています。
（原子論理式の量化された個体変数が最小限の定義）
\begin{array}{ccr} ∀x \,\, φ(x) &\Longleftrightarrow& xは束縛変数 \\ \\ ∃y \,\, ψ(x,y) &\Longleftrightarrow& yは束縛変数 \end{array}
この「量化」が「束縛子」のコアです。
（正確には量化子だけが束縛子だと言える）
束縛子
『条件によって範囲を狭める』やつのことで
\begin{array}{ccc} \forall x \,\, φ(x) &\Longleftrightarrow& 全てのxは条件φを満たす \end{array}
「量化子 ∀,∃ 」がこれの厳密な定義になります。
（ φ(x) が真になる x だけが集まる）
\begin{array}{lcr} \displaystyle\sum_{n=1}^{N}a_n && n が束縛変数 \\ \\ \displaystyle\prod_{n=1}^{N}a_n && nが束縛変数 \\ \\ \\ \displaystyle\lim_{x \to \infty}f(x) && xが束縛変数 \\ \\ \displaystyle\int_a^b f(x) \, dx && xが束縛変数 \end{array}
こういうやつらも「束縛子」と呼ばれますが
\begin{array}{ccc} \displaystyle\sum_{n=1}^{N}a_n=S &\Longleftrightarrow& \exists f:\{0,1,2,...,N\}\to R \,\, \Bigl( fの振る舞い \Bigr) \end{array}
\begin{array}{ccc} fの振る舞い & \left\{ \begin{array}{clcl} & f(0)&=&0 \\ \\ \forall n<N & f(n+1) & =& f(n)+a_{n+1} \\ \\ & f(N) &=& S \end{array} \right. \end{array}
呼ばれる根拠は結局「量化子」なので
「量化子のみ」を束縛子としても特に問題ありません。
（数学の操作は論理式で厳密に定義される）
原子論理式による最初の厳密な定義
これは「整論理式」の定義を知らないと
\begin{array}{lcc} \forall x \,\, φ &\in& \mathrm{Well}\text{-}\mathrm{Formed}\mathrm{Formula} \\ \\ \exists x \,\, φ &\in& \mathrm{Well}\text{-}\mathrm{Formed}\mathrm{Formula} \end{array}
よく分からないと思うんですが
（循環定義になってしまうのでそれを避けたい）
\begin{array}{ccc} xは束縛変数 &\Longleftrightarrow& \Bigl( φは原子論理式 \Bigr) ∧ \Bigl( \forall x \,\, φ ∨\exists x \,\, φ \Bigr) \end{array}
「初期の段階」での「束縛変数」の定義は
こんな感じになります。
束縛変数の厳密な定義
↓ を前提とした上で定義される
\begin{array}{ccc} xは束縛変数 &\Longleftrightarrow& \Bigl( φは原子論理式 \Bigr) ∧ \Bigl( \forall x \,\, φ ∨\exists x \,\, φ \Bigr) \end{array}
↓ のような形が
\begin{array}{ccc} xは束縛変数 &\Longleftrightarrow& \Bigl( φは整論理式 \Bigr) ∧ \Bigl( \forall x \,\, φ ∨\exists x \,\, φ \Bigr) \end{array}
「束縛変数」の厳密な定義になります。
（全体から下っていく感じで判定できる）
自由変数 Free Variable
|| 自由に値を取れる感じの変数
「束縛されてない個体変数」のことで
\begin{array}{ccc} 原子論理式 &\to& 量化されてない \\ \\ 量化されてない &\to& 個体変数は自由変数 \end{array}
「参照して良い範囲（ドメイン）」内なら
どのような値でも取ることができます。
自由変数を集めるフィルター
これについては
\begin{array}{ccc} \mathrm{Free}(φ) &\Longleftrightarrow& φに含まれる全ての自由変数 \end{array}
このような操作を考えると
（ \mathrm{Free}(φ) は φ の自由変数記号の集合を出力します）
\begin{array}{ccc} \mathrm{Free}(φ) &\Longleftrightarrow& φの全ての自由変数 \end{array}
まず「原子論理式 φ 」ではこうなり
（ φ の自由変数が全て要素になる）
\begin{array}{ccc} \mathrm{Free}(定数) &=& \{\} \\ \\ \mathrm{Free}(変数) &=& \{変数記号\} \end{array}
このシンプルな形の観察から
（論理式の定義前に定数か変数かは定義されてる）
\begin{array}{lcl} \mathrm{Free}\Bigl( f(t_1,...,t_n) \Bigr) &=& \mathrm{Free}(t_1)∪\cdots ∪\mathrm{Free}(t_n) \\ \\ \mathrm{Free}\Bigl( R(t_1,...,t_n) \Bigr) &=& \mathrm{Free}(t_1)∪\cdots ∪\mathrm{Free}(t_n) \end{array}
「項」については整理されるので
（項にまで分解されれば操作はほぼ終わる）
「整論理式 \phi,ψ 」の φ の分解操作は
\begin{array}{lcl} \mathrm{Free}(\lnot \phi) &=& \mathrm{Free}(\phi) \\ \\ \mathrm{Free}(\phi∨ψ) &=& \mathrm{Free}(\phi)∪\mathrm{Free}(\phi) \\ \\ \mathrm{Free}(\phi∧ψ) &=& \mathrm{Free}(\phi)∪\mathrm{Free}(ψ) \\ \\ \mathrm{Free}(\phi\to ψ) &=& \mathrm{Free}(\phi)∪\mathrm{Free}(ψ) \\ \\ \mathrm{Free}(\phi⇔ψ) &=& \mathrm{Free}(\phi)∪\mathrm{Free}(ψ) \end{array}
「命題記号」ではこうなると言えて
（この時の論理式全体は φ= \lnot \phi であるとします）
「量化」の分解操作は
\begin{array}{lcl} \mathrm{Free}(\forall x \,\, \phi) &=& \mathrm{Free}(\phi)\setminus \{x\} \\ \\ \mathrm{Free}(\exists x \,\, \phi) &=& \mathrm{Free}(\phi)\setminus \{x\} \end{array}
『量化された変数だけ』取り除かれることになるので
（この時は全体が φ=\forall x \,\, \phi という形です）
\begin{array}{ccc} 論理式全体 \\ \\ ↓ \\ \\ フィルター \\ \\ ↓ \\ \\ 分解された整論理式へ \end{array}
この操作を繰り返すと
結果的に自由変数を全て抜き取ることができます。
（量化されている個体変数以外は全て自由変数）
束縛変数を集めるフィルター
↑ とは逆の考え方をすれば
これも「量化されたものだけ」という形で
\begin{array}{ccc} \mathrm{Bound}(φ) &\Longleftrightarrow& φに含まれる全ての自由変数 \end{array}
「自由変数のフィルター外」のものとして
\begin{array}{lcl} \mathrm{Bound}(定数) &=& \{\} \\ \\ \mathrm{Bound}(自由変数) &=& \{\} \\ \\ \mathrm{Bound}(関数) &=& \{\} \\ \\ \mathrm{Bound}(原子論理式) &=& \{\} \end{array}
「原子論理式の量化」という形が来るまでは
「空集合になる」という形から
\begin{array}{lcl} \mathrm{Bound}(\lnot \phi) &=& \mathrm{Bound}(\phi) \\ \\ \mathrm{Bound}( \phi ∨ ψ ) &=& \mathrm{Bound}(\phi) ∪ \mathrm{Bound}(ψ) \\ \\ \mathrm{Bound}( \phi ∧ ψ ) &=& \mathrm{Bound}(\phi) ∪ \mathrm{Bound}(ψ) \\ \\ \mathrm{Bound}( \phi \to ψ ) &=& \mathrm{Bound}(\phi) ∪ \mathrm{Bound}(ψ) \\ \\ \mathrm{Bound}( \phi ↔ ψ ) &=& \mathrm{Bound}(\phi) ∪ \mathrm{Bound}(ψ) \end{array}
「命題論理」「述語論理」の記号で
（入力を論理式全体 φ とする）
\begin{array}{lcl} \mathrm{Bound}(\forall x \,\, \phi) &=& \{ x \} ∪ \mathrm{Bound}( \phi ) \\ \\ \mathrm{Bound}(\exists x \,\, \phi) &=& \{ x \} ∪ \mathrm{Bound}( \phi ) \end{array}
それぞれこのように定義することができます。
（ \mathrm{Bound}(φ) に入るのは述語論理の量化が来る場合だけ）
開論理式 Open Formula
「自由変数を含む論理式」のこと
\begin{array}{ccc} x &\in & \mathrm{FreeVariable} \\ \\ φ(x) &\in& \mathrm{AtomicFormula} \\ \\ φ(x) &\in& \mathrm{OpenFormula} \end{array}
核は「自由変数の有無」だけなので
そこだけ調べれば判別できます。
閉論理式 Closed Formula
「自由変数を含まない論理式」のこと
\begin{array}{ccc} φ(0) &\in& \mathrm{ClosedFormula} \\ \\ \forall x \,\, φ(x) &\in& \mathrm{ClosedFormula} \end{array}
これは『中身が確定している状態』にあります。
（ φ は ↑ と同じく１変数の原子論理式とします）
証明と自由変数
↑ の２つは証明に関わるもので
\begin{array}{c} x &←&\mathrm{Value} \end{array}
『証明における自由変数の扱い』を考える時
\begin{array}{ccc} 真偽不明 && 開論理式 \\ \\ 自由変数発見 && 開論理式 \\ \\ 自由変数排除 && 閉論理式 \\ \\ 真偽確定 && 閉論理式 \end{array}
「論理式の状態」を意味する用語として機能します。
（自由変数は定数を入れることで排除できる）
これは「論理式」というと難しく聞こえますが
\begin{array}{cc} 自由変数的概念 &\to& 具体的概念 \\ \\ もの &\to& 本 \end{array}
実は日常でもよく見られる手順です。
（私たちは日常的に開式を閉式に変換している）