単項1階述語論理の決定可能性
はじめに
命題論理の充足可能性は決定可能だが，1階述語論理の充足可能性は一般に決定不能である． ところが，いくつかの一階述語論理の部分体系では決定可能である．
先に例を見たほうが理解はしやすいと思う
定理
定義
演算子は削除する．
述語のアリティは1である．すなわち，$ P(x)とかはあるが，$ Q(x,y)とかはない．
構文論は次のように与えられる．
単項述語論理の言語$ \mathscr{L}は以下．
定項: $ a_1,a_2,\dots
変項: $ v_1,v_2,\dots
単項述語: $ P_1,P_2,\dots
真理関数$ \to,\bot，量化子$ \exists，括弧など
項は以下のように再帰的に定める
1. 定項は項である．
2. 変項は項である．
論理式は以下のように再帰的に定める
1. 単項述語$ Pと項$ \tauに対し，$ P(\tau)は論理式である．
2. 論理式$ \varphi_1,\varphi_2に対し，$ \varphi_1 \to \varphi_2と$ \botは論理式である．
3. 論理式$ \varphiと変項$ vに対し，$ \exists v.\varphiは論理式である．
意味論を次のように与えられる．．
モデル$ \mathcal{M} = \lang U,F\rangと表す．
$ Uは領域と呼ばれ，非空集合とする．
$ Fは対応付けと呼ばれ，定項と単項述語を次の集合へ移す写像とする．
定項$ aに対し，$ F(a) \in U
単項述語$ Pに対し，$ F(P) \in \mathbb{B}^U
$ \mathbb{B} = \{1,0\}とし，$ 1は真に，$ 0は偽に対応するものとする．
解釈$ \mathcal{I} = \lang \mathcal{M},g\rangと表す．
モデルは$ \mathcal{M} = \lang U,F \rangとする．
$ gは付値関数と呼ばれ，変項に領域の要素を割り当てる関数であるとする．
すなわち，変項$ vに対して$ g(v) \in U
付値関数$ gの変異$ g_{\lbrack v \mapsto u \rbrack}を次のように定める．ただし$ u \in U．
$ g_{\lbrack v \mapsto u \rbrack}(v) = u \in U
$ g_{\lbrack v \mapsto u \rbrack}(v') = g(v')
ただし$ v' \neq vとする．
解釈$ \mathcal{I}の変異$ \mathcal{I}_{\lbrack v \mapsto u \rbrack} = \langle \mathcal{M},g_{\lbrack v \mapsto u \rbrack} \rangleとする．ただし$ u \in U．
記号の解釈
述語$ Pの解釈$ \llbracket P \rrbracket_\mathcal{I} = F(P) \in \mathbb{B}^Uとする．
真理関数$ \botの解釈$ \llbracket \bot \rrbracket_\mathcal{I} = \left\lbrack () \mapsto 1 \right\rbrackとする．
真理関数$ \toの解釈$ \llbracket \to \rrbracket_\mathcal{I} = \left\lbrack (1,1)\mapsto1 \mid (1,0)\mapsto0 \mid (0,1)\mapsto1 \mid (0,0)\mapsto1 \right\rbrackとする．
項の解釈
項$ \tauの解釈$ \llbracket \tau \rrbracket_\mathcal{I}は以下のように定める．
$ \tauが定項$ aなら，$ \llbracket a \rrbracket_\mathcal{I} = F(a) \in U
$ \tauが変項$ vなら，$ \llbracket v \rrbracket_\mathcal{I} = g(v) \in U
論理式の解釈
論理式$ \varphiの解釈$ \llbracket \varphi \rrbracket_\mathcal{I}は以下のように定める．
$ \varphiが単項述語$ Pと項$ \tauで$ P(\tau)であるなら，$ \llbracket P(\tau) \rrbracket_\mathcal{I} = \llbracket P \rrbracket_\mathcal{I} (\llbracket \tau \rrbracket_\mathcal{I}) \in \mathbb{B}
$ 1という定値の0引数関数とする．
$ \varphiが$ \botなら，$ \llbracket \bot \rrbracket_\mathcal{I} = \llbracket \bot \rrbracket_\mathcal{I}() = 1 \in \mathbb{B}
$ \varphiが論理式$ \psi_1,\psi_2として$ \psi_1 \to \psi_2なら，$ \llbracket \psi_1 \to \psi_2 \rrbracket_\mathcal{I} = \llbracket \to \rrbracket_\mathcal{I}(\llbracket\psi_1\rrbracket_\mathcal{I},\llbracket\psi_2\rrbracket_\mathcal{I}) \in \mathbb{B}
$ \varphiが変項$ vと論理式$ \psiとして$ \forall v.\psiなら，
$ \llbracket \forall v.\psi \rrbracket_\mathcal{I} = 1$ \iffすべての$ u \in Uに対し，$ \llbracket \psi \rrbracket_{\mathcal{I}_{\lbrack v \mapsto u \rbrack}} = 1
逆に，$ \llbracket \forall v.\psi \rrbracket_\mathcal{I} = 0$ \iffある$ u \in Uに対し，$ \llbracket \psi \rrbracket_{\mathcal{I}_{\lbrack v \mapsto u \rbrack}} = 0
定理の証明
モデル$ \mathcal{M} = \lang U,F\rang及び解釈$ \mathcal{I} = \lang \mathcal{M},g \rangを固定する．
$ \varphiは単項一階述語論理の論理式とする．
$ \varphiに現れる述語を$ P_{\varphi,1},\dots,P_{\varphi,n}とする．
領域$ Uの同値関係$ \approx_{\varphi}を次のように定める．
$ i = 1,\dots,n，$ u_1,u_2 \in Uとする．
$ u_1 \approx_\varphi u_2$ \iff
全ての$ P_{\varphi,i}に対し，$ \llbracket P_{\varphi,i} \rrbracket_\mathcal{I} (u_1) = 1 \iff \llbracket P_{\varphi,i} \rrbracket_\mathcal{I} (u_2) = 1
$ u \in Uの$ \mathbin{\approx_\varphi}同値類を$ \lbrack u \rbrack_{\mathbin{\approx_\varphi}}と表すことにする．
領域を$ U/\mathbin{\approx_\varphi}としたモデル$ \mathcal{M}' = \lang U/\mathbin{\approx_\varphi},F' \rang及び解釈$ \mathcal{I}' = \lang \mathcal{M}',g'\rangを置く．
$ \mathcal{M}'は有限のモデル，$ \mathcal{I}'は有限の解釈と呼ぶことにする．
対応$ F'は次のように定める
定項$ aに対して，$ F'(a) = \lbrack F(a) \rbrack_{\mathbin{\approx_\varphi}}
述語$ P_{\varphi,i}の対応付けは次のように定義する
$ F(P_{\varphi,i}) = \lbrack (u_1) \mapsto 0 \mid (u_2) \mapsto 1 \mid (u_3) \mapsto 0 \mid \cdots \rbrackとなっているとする．
ただし，$ u_1,u_2,u_3,\dots\in U
$ F'(P_{\varphi,i}) = \left\lbrack (\lbrack u_1 \rbrack_{\mathbin{\approx_{\varphi}}}) \mapsto 0 \mid (\lbrack u_2 \rbrack_{\mathbin{\approx_{\varphi}}}) \mapsto 1 \mid (\lbrack u_3 \rbrack_{\mathbin{\approx_{\varphi}}}) \mapsto 0 \mid \cdots \right\rbrackとする．
ただし，もちろん重複するので，この組は高々$ 2^n個しか存在しない．
付値関数$ g'は次のようになる．
$ vを変項として$ g'(v) = \lbrack g(v) \rbrack_{\mathbin{\approx_\varphi}}
元の解釈$ \mathcal{I}と有限の解釈$ \mathcal{I}'には次の関係が成り立つ．
$ P_{\varphi,i}を述語，$ u \in Uとして，$ \llbracket P_{\varphi,i} \rrbracket_{\mathcal{I}'} (\lbrack u \rbrack_{\mathbin{\approx_\varphi}}) = \llbracket P_{\varphi,i} \rrbracket_{\mathcal{I}} (u)
したがって，元の論理式$ \varphiについて
$ \llbracket \varphi \rrbracket_\mathcal{I'} = \llbracket \varphi \rrbracket_\mathcal{I}
すなわち，無限の可能性がある解釈$ \mathcal{I}を有限の（時間で計算可能な）解釈$ \mathcal{I}'に落とし込むことが出来る
ところで
領域$ U/\mathbin{\approx_\varphi}の要素の個数は高々$ 2^n以下である
すなわち，量化子については領域が有限個しかないので有限時間で計算可能である．
述語の対応付け$ F'(P_{\varphi,i})は述語一つあたり$ 2^{2^n}パターンある．
すなわち，全ての述語について高々$ \left(2^{2^n}\right)^nパターンしかない．
すなわち，有限のモデルは高々$ \left(2^{2^n}\right)^n個で全て列挙可能である．
有限のモデルを全部列挙し，それらについての解釈を一個一個行い，もし充足するものがあれば，論理式$ \varphiには何らかのモデルが存在することが示される．
例
以下
混乱を避けるために$ \mathbb{B} = \{ \mathbf{1},\mathbf{0} \}と太字で表すとする．
常識的な略記として$ \landを導入．表現的適格性など参照． $ \varphi = \exists v.(E(v) \land P(v))
天下り的には，偶数の素数が存在することを主張しているとする．
次のモデル$ \mathcal{M} = \lang \omega,F\rangで妥当になる．
$ \omega = \{1,2,3,\dots\}とする．
$ F(E) = \{(1) \mapsto \mathbf{0} \mid (2) \mapsto \mathbf{1} \mid (3) \mapsto \mathbf{0} \mid \cdots\}
偶数であるとき$ \mathbf{1}を，そうでないとき$ \mathbf{0}を返す写像$ \omega \mapsto \mathbb{B}
$ F(P) = \{(1) \mapsto \mathbf{0} \mid (2) \mapsto \mathbf{1} \mid (3) \mapsto \mathbf{1} \mid \cdots\}
素数であるとき$ \mathbf{1}を，そうでないとき$ \mathbf{0}を返す写像$ \omega \mapsto \mathbb{B}
このモデルでは，$ \llbracket \exists v. (E(v) \land P(v))\rrbracket = \mathbf{1}．
$ \llbracket E(v)\rrbracket_{\lbrack v \mapsto 2\rbrack} = \mathbf{1}，$ \llbracket P(v)\rrbracket_{\lbrack v \mapsto 2\rbrack} = \mathbf{1}，$ \llbracket \land \rrbracket_{\lbrack v \mapsto 2\rbrack}(\mathbf{1},\mathbf{1}) = \mathbf{1}より，
$ u = 2のとき$ \llbracket \land \rrbracket_{\lbrack v \mapsto 2\rbrack} \left(\llbracket E(v) \rrbracket_{\lbrack v \mapsto 2\rbrack},\llbracket P(v) \rrbracket_{\lbrack v \mapsto 2\rbrack} \right)= \mathbf{1}
$ \implies$ u = 2のとき$ \llbracket E(v) \land P(v) \rrbracket_{\lbrack v \mapsto 2\rbrack} = \mathbf{1}
$ \impliesある$ u \in Uについて$ \llbracket E(v) \land P(v) \rrbracket_{\lbrack v \mapsto u\rbrack} = \mathbf{1}
逆にたどれば$ \impliedbyは示すことが出来る
したがって，$ \llbracket \exists v. (E(v) \land P(v))\rrbracket = \mathbf{1}．
このモデルでの$ \approx_{\varphi}を考える
$ \omega/\mathbin{\approx_\varphi} = \left\{\{2\},\{3,5,7,\dots\},\{4,6,\dots\},\{1,9,\dots\}\right\}
$ F'(E) = \left\{ (\{2\}) \mapsto \mathbf{1} \mid (\{3,5,7,\dots\}) \mapsto \mathbf{0} \mid (\{4,6,\dots\}) \mapsto \mathbf{1} \mid (\{1,9,\dots\}) \mapsto \mathbf{0}\right\}
$ F'(P) = \left\{ (\{2\}) \mapsto \mathbf{1} \mid (\{3,5,7,\dots\}) \mapsto \mathbf{1} \mid (\{4,6,\dots\}) \mapsto \mathbf{0} \mid (\{1,9,\dots\}) \mapsto \mathbf{0}\right\}
$ \llbracket \exists v. (E(v) \land P(v))\rrbracket = \mathbf{1}
$ \iffある$ u \in U/\mathbin{\approx_\varphi}について$ \llbracket E(v) \land P(v) \rrbracket_{\lbrack v \mapsto u\rbrack} = \mathbf{1}
$ \iff$ u = \{2\}のとき$ \llbracket E(v) \land P(v) \rrbracket_{\lbrack v \mapsto \{2\}\rbrack} = \mathbf{1}
以下同じ
これは実質的には次の有限モデル$ \mathcal{M}^+ = \lang U^+, F^+ \rangで考えているのと同じことである
$ U^+=\{a,b,c,d\}
$ F^+(E) = \{ a \mapsto \mathbf{1} \mid b \mapsto \mathbf{0} \mid c \mapsto \mathbf{1} \mid d \mapsto \mathbf{0} \}
$ F^+(P) = \{ a \mapsto \mathbf{1} \mid b \mapsto \mathbf{1} \mid c \mapsto \mathbf{0} \mid d \mapsto \mathbf{0} \}
上の例では
述語は2個: $ n = 2
$ Uの個数は$ 2^n = 4個
$ F^+(E)のパターンは$ 2^{2^n} = 16パターン．
$ F^+(P)のパターンも$ 16パターン．
よって有限モデルは$ 16^2 = 256個で列挙可能．
後はこの256個のモデル一つ一つに対して
全ての$ u \in Uについて（4個しかない！）$ \llbracket E(v) \land P(v) \rrbracket_{\lbrack v \mapsto u\rbrack} = \mathbf{1}かどうかを検証する．
もちろん，有限の時間で可能
メモ: 演算子を入れてはいけない理由
上記の例で$ F(\times2): \lbrack (1) \mapsto 2 \mid (2) \mapsto 4 \mid \cdots \rbrack
のような演算子を考えるとどうやっても同値類に対しての対応付けの変換を考えることが出来ない
すなわち，$ F^+(\times 2) : \lbrack (\{2\}) \mapsto ? \mid (\{3,5,7,\dots\}) \mapsto ? \mid \cdots \rbrack
参考文献
が，いかんせん面倒くさく…
議論の大筋はここから持ってきている
ただし，意味論の与え方が分かりづらすぎるので，これは戸次のものを与えて書き直している
メモ
という観点から考えると，単項述語というのが様相演算子にも見えるというのがわかるだろう．