【一階述語論理4】モデルの存在定理と完全性


▼ すべて展開/縮小

無矛盾拡大の準備

補題4-1
\(L\)を言語とし\(\Sigma\)を\(L\)-閉論理式の集合とする. さらに\(c\)を\(L\)にない定数記号とし\(L’ = L \cup \{c\}\)とする. このとき, \(L’\)-論理式として\(\Sigma \vdash \varphi(c)\)ならば\(L\)-論理式として\(\Sigma \vdash \forall x \varphi(x)\).

(証明)
言語\(L’\)についての\(\Sigma\)からの\(\varphi(c)\)の証明を,

\(\varphi_1, \varphi_2, \cdots, \varphi_n, \)

とする. このとき, \(\varphi_n \equiv \varphi(c)\)である.
 各論理式\(\varphi_i (i = 1,2, \cdots ,n)\)において\(c\)が出現していれば\(\varphi_i (i = 1,2, \cdots ,n)\)に現れない変数記号\(x\)で書き換え, その各論理式を\(\psi_i(x)\)と表す. このとき, \(\psi_i(x)\)は\(L\)-論理式である. さらに, \(x\)が出現する論理式に全称量化子をつけて\(\forall x \psi_i(x)\)とする. こうしてできた新しい論理式を\(\varphi_i’\)と表すことにすると,

\(\varphi_1′, \varphi_2′, \cdots, \varphi_n’, \)

は言語\(L\)についての\(\Sigma\)からの\(\forall x \varphi(x)\)の証明である. ただし, \(\varphi_i’\)が各\(i\)について証明の条件を満たしていることは次のように確かめられる.

(I) \(\varphi_i\)が\(\Sigma\)に含まれるとき
 \(\Sigma\)は\(L\)-閉論理式の集合としたから\(\varphi_i\)に\(c\)は出現しない. よって, \(\varphi_i \equiv \varphi_i’\)となる. したがって, 示すことはない.

(II) \(\varphi_i\)が証明系\(\mathcal{H}\)の公理のとき
 証明系\(\mathcal{H}\)の公理の定義より, \(\psi_i(x)\)が\(\mathcal{H}\)の公理であればその全称閉包である\(\forall x \psi_i(x)\)も\(\mathcal{H}\)の公理であるからよい.

(III) \(\varphi_i\)が\(\varphi_j, \varphi_k (j, k \le i)\)からの(MP)の結論であるとき
 \(i, (i \ge 0)\)未満の論理式に関しては証明の条件が満たされていると仮定する. また, 与えられた証明において\(\varphi_k \equiv \varphi_j \rightarrow \varphi_i\)とする. このとき, 帰納法の仮定より\(\Sigma \vdash \forall x (\varphi_j(x) \rightarrow \varphi_i(x))\)が成り立つから公理(4)と(MP)により, \(\Sigma \vdash \forall x \varphi_j(x) \rightarrow \forall x \varphi_i(x)\)となる. また, 帰納法の仮定より\(\Sigma \vdash \forall x \varphi_j(x)\)であるからもう一度(MP)を用いて\(\Sigma \vdash \forall x \varphi_i(x)\)を得る.

補題4-2(Henkinの公理の無矛盾性)
\(L\)を言語とし\(\Sigma\)を\(L\)-閉論理式の集合とする. さらに, \(L\)の存在論理式\(\exists x \varphi(x)\)とそれに対応する\(C_{\exists x \varphi(x)}\)を新たな定数記号とする. \(L’ = L \cup \{C_{\exists x \varphi(x)}\}\)とし, \(\Sigma’ = \Sigma \cup \{\exists x \varphi(x) \rightarrow \varphi(C_{\exists x \varphi(x)})\}\)とすると, \(L\)-閉論理式の集合として\(\Sigma\)が無矛盾であれば, \(L’\)-閉論理式の集合として\(\Sigma’\)が無矛盾である.

(証明)
 演繹定理と否定の定義により\(\Sigma’ \vdash \bot \iff \Sigma \vdash \lnot (\exists x \varphi(x) \rightarrow \varphi(C_{\exists x \varphi(x)}))\)であるから, \(\Sigma’\)が矛盾すると仮定すると,

\( \Sigma \vdash \lnot \big(\exists x \varphi(x) \rightarrow \varphi(C_{\exists x \varphi(x)}) \big), \)
\( \Sigma \vdash \lnot \lnot \exists x \varphi(x) \land \lnot \varphi(C_{\exists x \varphi(x)}), \)
\( \Sigma \vdash \exists x \varphi(x),\)
\( \Sigma \vdash \lnot \varphi(C_{\exists x \varphi(x)}), \)
\( \Sigma \vdash \forall x \lnot \varphi(x), \) (補題3-1)
\( \quad \vdash \forall x \lnot \varphi(x) \rightarrow \lnot \exists x \varphi(x),\) (公理(5))
\( \Sigma \vdash \lnot \exists x \varphi(x), \) (前2つから(MP))
\( \Sigma \vdash \exists x \varphi(x) \rightarrow \bot, \) (否定の定義)
\( \Sigma \vdash \bot, \)

により, \(\Sigma\)の無矛盾性に矛盾する.

Henkin拡大

定義(Henkin拡大)
\(L\)を言語とし, \(L\)-閉論理式のうち存在量化記号\(\exists\)から始まる論理式の集合を\(\Gamma_0\)とする.

(1) \(\Gamma_0\)の元を一列に並べ, \(\varphi_1, \varphi_2, \cdots\),と表す. 定数記号の集合\(C_0\)を\(C_0 = \{c_{\varphi_1}, c_{\varphi_2}, \cdots\}\)と定める. このとき\( L \cup C_0 \)は新たな言語となるから, \(L \cup C_0\)の閉論理式のうち存在量化記号\(\exists\)から始まる論理式の集合を\(\Gamma_1\)とする.

(2) \(\Gamma_n \backslash \bigcup_{k=0}^{n-1} \Sigma_k\)の元を一列に並べ, \(\varphi_1^n, \varphi_2^n, \cdots\),と表す. 定数記号の集合\(C_n\)を\(C_n = \{c_{\varphi_1^n}, c_{\varphi_2^n}, \cdots\}\)と定める. このとき\(L \cup C_n\)は新たな言語となるから, \(L \cup C_n\)の閉論理式のうち存在量化記号\(\exists\)から始まる論理式の集合を\(\Gamma_{n+1}\)とする.

このとき, \(L \cup \bigcup C_n\)を\(L(C)\)と表し\(L\)のHenkin拡大という.

 たとえば, \(\Gamma_1 \backslash \Gamma_0\)は\(C_0\)の元である定数記号を含む\(\exists\)-閉論理式だけを集めたものである. すなわち, 言語\(L\)を\(L \cup C_0\)に拡張して初めて現れる\(\exists\)-閉論理式の集合である.

 このように定数記号が増えるたびに閉論理式も増えるため, 増えた分の\(\exists\)-閉論理式に対応する定数記号をさらに増やすという操作を繰り返すのである.

極大無矛盾集合

定義(極大無矛盾集合)
\(L\)を言語とし\(\Sigma^*\)を\(L\)-閉論理式の集合とする. 任意の\(L\)-閉論理式\(\varphi\)について\(\varphi \in \Sigma^*\)もしくは\(\lnot \varphi \in \Sigma^*\)のいずれか一方が成り立つとき\(\Sigma^*\)は極大無矛盾集合であるという.
補題4-3(極大無矛盾集合の構成)
\(L\)を言語とし\(\Sigma\)を\(L\)-閉論理式の無矛盾な集合とする. このとき, \(L(C)\)-閉論理式の極大無矛盾集合\(\Sigma^*\)で\(\Sigma \subset \Sigma^*\)なるものが存在する.

(証明)
 \(\Sigma\)に属さない\(L(C)\)-閉論理式を順に並べ,

\(\varphi_1, \varphi_2, \cdots,\)

のように自然数で添え字づける. \(\Sigma\)を次の規則によって拡大する.

\( \quad \Sigma_0 := \Sigma, \)
\(
\quad
\Sigma_{n+1} :=
\begin{cases}
\Sigma_{n} \cup \{ \varphi_n \} \quad (\Sigma_{n} \cup \{ \varphi_n \} \not\vdash \bot), \\\
\\\
\Sigma_{n} \cup \{ \lnot \varphi_n \} \quad (\Sigma_{n} \cup \{ \varphi_n \} \vdash \bot).
\end{cases}
\)

このとき, \(\Sigma^* = \bigcup_n \Sigma_n\)とすると\(\Sigma^*\)はその構成法から極大無矛盾集合となる.

モデルの存在定理

定理(モデルの存在定理)
\(L\)を言語とし\(\Sigma\)を\(L\)-閉論理式の無矛盾な集合とする. このとき, \(L\)-構造\(\mathcal{M}\)で\(\Sigma\)のモデルとなるものが存在する.

(証明)
 補題4-3より\(L(C)\)ー閉論理式の集合\(\Sigma^*\)で\(\Sigma \subset \Sigma^*\)なる極大無矛盾集合が存在する. これを用いて, 任意の\(L(C)\)-閉論理式\(\varphi\)について,

\(\mathcal{M}(\varphi) = 1 \iff \varphi \in \Sigma^*,\)

なるモデル\(\mathcal{M}\)を構成する.
 まず, モデルの対象領域を定める. \(L\)のHenkin拡大\(L(C)\)の閉項全体の集合を\(Ct(L(C))\)と表す. このとき\(Ct(L(C))\)上の同値関係\(\simeq\)を次で定める. \(t, s \in Ct(L(C))\)として,

\(t \simeq s :\iff (t = s) \in \Sigma^*,\)

とする. 等号公理より\(\simeq\)は同値関係になる. さて, 対象領域を\(M = Ct(L(C)) / \simeq \)で定め, \(t\)を代表元とする\(M\)の元を\([t]\)と表す.
 \(M\)を\(L(C)\)-構造にするために, 定数記号, 関数記号, 述語記号の解釈を次で与える. 以下, 特に断らない限り\(t, s, t_1, t_2, \cdots, t_n \in Ct(L(C))\)とする.
 
 (1)定数記号の解釈
 定数記号\(c\)は\(\)で解釈する.

 (2)関数記号の解釈
 \(f \in \mathcal{F}\)のとき\(f^\mathcal{M}([t_1], [t_2], \cdots, [t_n]) = [f(t_1, t_2, \cdots, t_n)]\)で定める.

 (3)述語記号の解釈
 \(R \in \mathcal{P}\)のとき\(([t_1], [t_2], \cdots, [t_n]) \in R^\mathcal{M} \iff R(t_1, t_2, \cdots, t_n) \in \Sigma^* \)で定める.

(2), (3)は等号公理よりwell-definedとなる.
 これらの解釈を写像\(F : L \to M \cup \bigcup_n P(M^n) \)で表すことにすれば, \(L(C)\)-構造\(\mathcal{M} = \langle M, F \rangle\)を得る. 以降では\(L(C)\)を\(\mathcal{M}\)の名前によって拡張しておく. ただし, 簡単のため\(L(C)\)と書く.

任意の\(L(C)\)-閉論理式\(\varphi\)について,\(\mathcal{M}(\varphi) = 1 \iff \varphi \in \Sigma^*\)が成り立つことは次の補題4-4で示す. これより, \(\mathcal{M} \vDash \Sigma^*\)がわかる.

\(\Sigma \subset \Sigma^*\)であるから\(\mathcal{M} \vDash \Sigma\)となり, よって\(\Sigma\)のモデルを得た.

補題4-4
各記号および仮定はモデルの存在定理に準じる. このとき, 任意の\(L(C)\)-閉論理式\(\varphi\)について,\(\mathcal{M}(\varphi) = 1 \iff \varphi \in \Sigma^*\)が成り立つ.

(証明)
定数記号と関数記号の解釈の定義より\(t^\mathcal{M} = [t]\)が成り立つことに注意する.

(1)原子閉論理式の場合
 ( i )\(\varphi \equiv (t = s)\)のとき

\(\mathcal{M}((t = s))=1 \)
\(\iff t^\mathcal{M} = s^\mathcal{M}\)
\(\iff [t] = [s]\)
\(\iff t \simeq s\)
\(\iff (t = s) \in \Sigma^*.\)

( ii )\(\varphi \equiv R(t_1, t_2, \cdots, t_n)\)のとき

\(\mathcal{M}(R(t_1, t_2, \cdots, t_n))=1 \)
\(\iff (t_1^\mathcal{M}, t_2^\mathcal{M}, \cdots, t_n^\mathcal{M}) \in R^\mathcal{M}\)
\(\iff ([t_1], [t_2], \cdots, [t_n]) \in R^\mathcal{M}\)
\(\iff R(t_1, t_2, \cdots, t_n) \in \Sigma^*.\)

(2)一般の閉論理式の場合
 記号\(\land, \lor, \rightarrow, \exists, \forall\)の個数に関する帰納法による. 記号が\(n (n \ge 0)\)未満の論理式については主張が成り立っていると仮定する. \(\land, \lor, \rightarrow\)に関しては\(\mathcal{M}(\varphi S \psi)\)の値の定め方により成り立つ(\(S\)は\(\land, \lor, \rightarrow\)のいずれか).

 存在量化子から始まる論理式\(\varphi \equiv \exists x \psi(x)\)について.
 まず, \(\varphi \in \Sigma^* \Longrightarrow \mathcal{M}(\varphi) = 1\)を示す. 補題4-2より\(\exists x \psi(x) \rightarrow \psi(C_{\exists x \psi(x)}) \in \Sigma^*\)であるから(MP)により\(\psi(C_{\exists x \psi(x)}) \in \Sigma^*\)である. 帰納法の仮定より, \(\mathcal{M}(\psi(C_{\exists x \psi(x)})) = 1\)となり, \(\mathcal{M}(\varphi)\)の定義より\(\mathcal{M}(\exists x \psi(x)) = 1\)が成り立つ.
 逆に, \(\mathcal{M}(\varphi) = 1 \Longrightarrow \varphi \in \Sigma^* \)を示す. \(\mathcal{M}(\varphi) = 1 \)のとき, ある\(m \in |\mathcal{M}|\)が存在して\(\mathcal{M}(\psi(c_m)) = 1\)となる. このとき, 適当な閉項\(t\)を用いて\(m = [t]\)と表せるから, \(t^\mathcal{M} = [t]\)より\(\mathcal{M}(\psi(t)) = 1\)となる. 帰納法の仮定より\(\psi(t) \in \Sigma^*\)となり, 公理(6)\((\varphi(t) \rightarrow \exists x \varphi(x)) \)より\(\varphi \in \Sigma^*\).

 次に, 全称量化子から始まる論理式\(\varphi \equiv \forall x \psi(x)\)について.
 まず, \(\varphi \in \Sigma^* \Longrightarrow \mathcal{M}(\varphi) = 1\)を示す. 補題3-3(対偶法)と公理(6)により任意の閉項\(t\)について\(\vdash \forall x \psi(x) \rightarrow \psi(t)\)が成り立つ. \(\forall x \psi(x) \in \Sigma^*\)と帰納法の仮定より, 任意の閉項\(t\)について\(\mathcal{M}(\psi(t)) = 1\)となる. したがって, \(\mathcal{M}(\forall x \psi(x)) = 1\).
 最後に, \(\varphi \not\in \Sigma^* \Longrightarrow \mathcal{M}(\varphi) = 0\)を示す. \(\varphi \not\in \Sigma^* \)および\(\Sigma^*\)の構成法より\(\lnot \varphi \in \Sigma^*\)が成り立つ. さらに, 補題3-3(対偶法)と公理(5)より\(\vdash \lnot \forall x \psi(x) \rightarrow \exists x \lnot \psi(x)\)であるから(MP)によって\(\exists x \lnot \psi(x) \in \Sigma^*\). 補題4-2より\(\exists x \lnot \psi(x) \rightarrow \lnot \psi(C_{\exists x \lnot \psi(x)}) \in \Sigma^*\)であるから(MP)より\(\lnot \psi(C_{\exists x \lnot \psi(x)}) \in \Sigma^*\)となる. よって帰納法の仮定より\(\mathcal{M}(\psi(C_{\exists x \lnot \psi(x)})) = 0\). よって, \(\mathcal{M}(\varphi)\)の定義より\(\mathcal{M}(\forall x \psi(x)) = 0\)が成り立つ.

完全性定理

定理(完全性定理)
\(L\)を言語とし\(\Sigma\)を\(L\)-閉論理式の集合, \(\varphi\)を\(L\)-閉論理式とする. このとき, 次が成り立つ.

\(\Sigma \vDash \varphi \Longrightarrow \Sigma \vdash \varphi\).

(証明)
 対偶を示すため, \(\Sigma \not\vdash \varphi\)を仮定する. 演繹定理から\(\Sigma \cup \{\lnot \varphi\} \vdash \bot \Longrightarrow \Sigma \vdash \varphi\)が成り立つからこれの対偶をとって\(\Sigma \not\vdash \varphi \Longrightarrow \Sigma \cup \{\lnot \varphi\} \not\vdash \bot\)が成り立つ. すなわち, \(\Sigma \cup \{\lnot \varphi\}\)が無矛盾となる. このとき, モデルの存在定理より\(\mathcal{M} \vDash \Sigma \cup \{\lnot \varphi\}\)なる\(\Sigma \cup \{\lnot \varphi\}\)のモデル\(\mathcal{M}\)が存在する. \(\mathcal{M}\)は\(\mathcal{M} \vDash \lnot \varphi\)より\(\mathcal{M} \not\vDash \varphi\)を満たす. すなわち, \(\Sigma \not\vDash \varphi\).

参考文献

[1] 新井敏康,数学基礎論 増補版,東京大学出版会,2021.

[2] ケネス・キューネン, キューネン数学基礎論講義, 日本評論社,2016.

[3] 鹿島亮, 現代基礎数学15 数理論理学, 朝倉書店, 2009.

[4] Stephen Cole Kleene, Introduction To Meta-Mathematics, Ishi Press Internal, 1952.

[5] Joseph R. Shoenfield, Mathematical Logic, CRC Press, 1967.

[6] Richard E. Hodel, An Introduction to Mathematical Logic, Dover Publications Inc, 1995.

コメントを残す