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

（証明）
　補題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))\)とする.
　
　（１）定数記号の解釈
　定数記号\(c\)は\(\)で解釈する.

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

　（３）述語記号の解釈
　\(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^* \)で定める.

（２）, （３）は等号公理より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\)のモデルを得た.

□

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

（１）原子閉論理式の場合
　（ 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^*.\)

（２）一般の閉論理式の場合
　記号\(\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^*\)となり, 公理（６）\((\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（対偶法）と公理（６）により任意の閉項\(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（対偶法）と公理（５）より\(\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\)が成り立つ.

□