|| 知ってるけど考えてみるとよく分からんやつ
「なんでも（？）入れていい」もの
スポンサーリンク
目次
個体変数「変数全般を指す言葉」
変数と変項の違い「特にない」
束縛変数「値が定まっている個体変数」
自由変数「値が定まっていない個体変数」
開論理式「自由変数がそのままの論理式」
閉論理式「自由変数が固定された論理式」
個体変数 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}{lcl} \mathrm{Free}(φ) &=& \mathrm{Free}(\lnot φ) \\ \\ \mathrm{Free}(φ∨ψ) &=& \mathrm{Free}(φ)∪\mathrm{Free}(ψ) \\ \\ \mathrm{Free}(φ∧ψ) &=& \mathrm{Free}(φ)∪\mathrm{Free}(ψ) \\ \\ \mathrm{Free}(φ\to ψ) &=& \mathrm{Free}(φ)∪\mathrm{Free}(ψ) \\ \\ \mathrm{Free}(φ⇔ψ) &=& \mathrm{Free}(φ)∪\mathrm{Free}(ψ) \end{array}
「命題記号」でこうなると言えて
「量化」の段階で
\begin{array}{lcl} \mathrm{Free}(\forall x \,\, φ) &=& \mathrm{Free}(φ)\setminus \{x\} \\ \\ \mathrm{Free}(\exists x \,\, φ) &=& \mathrm{Free}(φ)\setminus \{x\} \end{array}
『量化された変数だけ』取り除かれることになるので
\begin{array}{ccc} 論理式全体 \\ \\ ↓ \\ \\ フィルター \\ \\ ↓ \\ \\ 分解された整論理式へ \end{array}
この操作を繰り返すと
結果的に自由変数を全て抜き取ることができます。
（最終的に原子論理式へと行き着く）
開論理式 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}{lllllllll} \displaystyle \mathrm{Thing} &←&\mathrm{book} \end{array}
実は日常でもよく見られる手順です。
（私たちは日常的に開式を閉式に変換している）