GLの算術的完全性定理の証明
Def
理論$ Tおよびその証明可能性述語$ \mathrm{Pr}_T(x)に対し,様相論理の論理式を算術の文に移す写像$ \mathrm{Form}_{\mathscr{L}_\mathrm{M}} \to \mathrm{Sent}_{\mathscr{L}_\mathrm{A}}を解釈$ *_{\mathrm{Pr}_T}と呼ぶ.
$ p^{*_{\mathrm{Pr}_T}} = \sigma_p($ \sigma_pは様相論理の命題変項$ pに対してそれぞれ適当に定める)
$ \bot^{*_{\mathrm{Pr}_T}} = \bot
$ (\Box A)^{*_{\mathrm{Pr}_T}} = \mathrm{Pr}_T(\ulcorner A^{*_{\mathrm{Pr}_T}} \urcorner)
特に明らかなら,$ *_{\mathrm{Pr}_T}で$ \mathrm{Pr}_Tは省略して単に$ *と書く.
Memo
ここでは面倒なのでこうしたが,本来は様相論理の命題変項$ \mathrm{Var}_{\mathscr{L}_\mathrm{M}} \to \mathrm{Sent}_{\mathscr{L}_\mathrm{A}}に移す写像を様相論理式に拡張して定義される.
また,算術の文である必要は特に無く,1階述語論理の文であればよい.
様相論理式$ A,$ \Sigma_1健全な理論$ T,導出可能性条件D1, D2, D3を満たす証明可能性述語$ \mathrm{Pr}_Tとする. $ \mathrm{Pr}_T上の任意の解釈$ *_{\mathrm{Pr}_T}に対し,$ T \vdash A^{*_{\mathrm{Pr}_T}}ならば$ \mathbf{GL} \vdash A
$ \mathbf{GL}は推移的かつ非反射的な有限フレームのクラスに対して(弱)完全
今後そのようなフレームを$ \bf GLフレームということにする.
Proof of Thm.1
対偶を示す.
すなわち,$ \mathbf{GL} \nvdash Aだとすると,$ T \nvdash A^{*}となる解釈$ *が取れることを示す.
今, $ \nvdash_\mathbf{GL} Aだから$ \bf GLのKripke完全性より,$ \bf GLフレームを持つモデル$ \mathcal{M_1} := \lang W_1, \prec_1, V_1 \rangとその世界$ w_1 \in W_1が取れて,$ \mathcal{M}_1, w_1 \nvDash Aである.
$ Aを固定しているため,$ W_1として興味がある部分は$ w_1以降である.
すなわち
$ W_1' := \{w_1\} \cup \{ v \mid w_1 \prec_1 v \}として削ぎ落とし,
当然有限であることに注意せよ.
ようするに$ w_1を根とするフレームみたいなものを考える
$ \prec_1を$ W_1'上のものに制限した$ \prec_1'として,
モデル$ \mathcal{M}_1' := \lang W_1', \prec_1', V_1 \rangとすると,やはり$ \mathcal{M}_1', w_1 \nvDash Aとなる.
今,$ w_0を適当に取ってきて
$ W := \{w_0\}\cup W_1'
やはり有限.$ |W| = nとする.
$ Rは$ w_0 R w_i(ただし$ 1 \leq iすなわち$ w_i \in W_1')かつ$ w \prec'_1 v \iff w \prec v
$ Vは$ V_1を$ w_0に適当に拡張して
$ \mathcal{M} := \lang W, \prec, V \rangとする.$ \mathcal{M}, w_1 \nvDash Aは据え置き.
略記として,自然数$ i \leq nで$ Wの$ i番目の要素$ w_iを同一視することとする.
すなわち$ \mathcal{M}, 1 \vDash Aとかと書く.
この略記の元で$ W = \{0,1,2,...,n\}.
$ 0 \prec 1
$ 1 < i \leq nで$ 1 \prec i
推移的だから$ 1 < i \leq nで$ 0 \prec i
$ n + 1個の算術の文$ \theta_0,\dots,\theta_nについて,以下の性質を($ T, \mathrm{Pr}_T, \mathcal{M}に対しての)Solovay条件と呼ぶことにする.
S1: $ T \vdash \bigvee_{0 \leq i \leq n} \theta_i
S2: $ i \neq jならば$ T \vdash \theta_i \to \lnot \theta_j
S3: $ i \neq 0ならば$ T \vdash \theta_i \to \mathrm{Pr}_T(\ulcorner \bigvee_{i \prec j} \theta_j \urcorner)
S4: $ i \prec jならば$ T \vdash \mathrm{Pr}_T(\ulcorner \lnot \theta_j \urcorner) \to \lnot \theta_i
Proof of Thm.1, cont.
Solovay条件を満たす$ \theta_0, \dots,\theta_nがとにかく構成できるものと仮定する.(後述)
今$ p^* := \bigvee_{i \vDash p} \theta_iとなるような解釈を構成する.この解釈が所望のものとなる.
このとき次のLem 3が成り立つ.
Lem.3
$ i \neq 0とし,$ Bを様相論理式としたとき,次が成り立つ.
1. $ i \vDash Bならば$ T \vdash \theta_i \to B^*
2. $ i \nvDash Bならば$ T \vdash \theta_i \to \lnot B^*
Proof of Lem.3
論理式の帰納法で1と2を同時に示す.
$ B \equiv pと$ B \equiv \Box Cのときだけ見る.他は帰納法の仮定より明らか.
$ B \equiv pの場合
$ i \vDash pとする.$ T \vdash \theta_i \to \bigvee_{j \vDash p} \theta_jを示せば良いが,これは明らか.
$ i \nvDash p.$ T \vdash \theta_i \to \lnot p^*と同値な$ T \vdash \theta_i \to \bigwedge_{j \vDash p} \lnot \theta_jを示せば良く,これはS2より明らか.
$ B \equiv \Box Cの場合
$ i \vDash \Box Cとする.
このとき充足関係の定義より任意な$ i \prec jで$ j \vDash Cである.
帰納法の仮定より$ T \vdash \theta_j \to C^*.よって$ T \vdash \bigvee_{i \prec j} \theta_i \to C^*.
D1, D2より$ T \vdash \mathrm{Pr}_T(\ulcorner \bigvee_{i \prec j} \theta_i \urcorner) \to \mathrm{Pr}_T(\ulcorner C^* \urcorner).
$ (\Box C)^* = \mathrm{Pr}_T(\ulcorner C^* \urcorner)だったことを思い出せば$ T \vdash \mathrm{Pr}_T(\ulcorner \bigvee_{i \prec j} \theta_i \urcorner) \to (\Box C)^*.
S3より,$ T \vdash \theta_i \to (\Box C)^*.よって示された.
$ i \nvDash \Box Cとする.
このとき充足関係の定義よりある$ i \prec jで$ j \nvDash Cである.
帰納法の仮定より$ T \vdash \theta_j \to \lnot C^*.
対偶を取り,D1とD2によって$ T \vdash \mathrm{Pr}_T(\ulcorner C^* \urcorner) \to \mathrm{Pr}_T(\ulcorner \lnot \theta_j \urcorner).先程の注意から$ T \vdash (\Box C)^* \to \mathrm{Pr}_T(\ulcorner \lnot \theta_j \urcorner)
S4より,$ T \vdash (\Box C)^* \to \lnot \theta_i.これの対偶を取って$ T \vdash \theta_i \to \lnot (\Box C)^*.よって示された.
Proof of Thm.1, cont.
さて今$ 1 \nvDash Aだったことを思い出すと$ T \vdash \theta_1 \to \lnot A^*,すなわち$ T \vdash A^* \to \lnot \theta_1がLem3.2より言える.
仮に,前提に反して$ T \vdash A^*だったとすると$ T \vdash \lnot \theta_1となる.これはおかしいことを示す.
$ T \vdash \lnot \theta_1にD1より$ T \vdash \mathrm{Pr}_T (\ulcorner \lnot \theta_1 \urcorner).
$ 0 \prec 1だったからS4の対偶より$ T \vdash \lnot \theta_0.
S1より,$ T \vdash \bigvee_{1 \leq i \leq n} \theta_i.
様相論理一般に成り立つ次のFact4をまず見ておく.
Fact 4
ある有限モデル$ \mathcal{M} = \lang W, \prec, V \rangとその世界$ w_0 \in Wに対し,
世界の有限の連鎖$ w_0 \prec w_1 \prec \cdots \prec w_nを$ w_0の鎖という.
$ w_0の鎖の内もっとも短いものの$ nを$ d(w_0) = nと書く.
すなわち,$ d(w_0) = nなら,$ w_0は少なくとも$ n回は遷移することが保証されている.
任意の論理式$ Aに対し,$ d(w) \leq n \implies \mathcal{M}, w \vDash \Box^{n+1} A
証明は帰納法を回せば良いので省くが,気持ち的には「$ \Box^{n+1} Aを評価するには$ n + 1回の遷移が必要だが,今そのような世界の連鎖は取ってこれない(最高でも$ n回までしか遷移しない)ため無条件に正しいとしてよい」と考えれば直ちに明らか.
Proof of Thm.1, cont.
$ i \neq 0とする.
今$ d(i) \leq d(1)であるからFact4より$ i \vDash \Box^{d(1) + 1} \bot.
任意の$ 1 \leq iで$ 1 \prec iであり,モデルは推移的であることを思い出す.
Lem3.1より,$ T \vdash \theta_i \to (\Box^{d(1) + 1} \bot)^*
$ T \vdash \bigvee_{1 \leq i \leq n} \theta_iだったから,$ T \vdash (\Box^{d(1) + 1} \bot)^*すなわち,$ T \vdash \underbrace{\mathrm{Pr}_T(\ulcorner \mathrm{Pr}_T(\ulcorner \cdots (\ulcorner}_{d(1) + 1} \bot \urcorner) \cdots \urcorner) \urcorner)である.
$ \bot, \mathrm{Pr}_T(\ulcorner \bot \urcorner), \mathrm{Pr}_T(\ulcorner \mathrm{Pr}_T(\ulcorner \bot \urcorner) \urcorner), \dotsたちは$ \Sigma_1文だから,$ \Sigma_1健全性より$ \botが$ T上で真となる.
しかしそのようなことはありえないため,元々の前提である$ T \vdash A^*がおかしい.よって$ T \nvdash A^*.
$ T \nvdash A^*となる解釈$ *が取れたので,これでSolovay条件を満たす関数たちが構成できると仮定すれば算術的完全性が示されたことになる.
Memo
Fact 4を用いた証明は$ \Sigma_1健全性を用いており明示的には意味論的帰結に関して触っていない.
もちろん$ \Sigma_1健全性は意味論的概念だから結局触っているのだが,形式化に関して$ \Sigma_1健全性を適当な形でラップする場合は便利である.
すなわち$ T \vdash {\mathrm{Pr}_T}^n(\ulcorner \bot \urcorner) \implies T \vdash \botという形さえ満たせば良い.
Memo
ここまでの証明を見ると,D3が使われていないように見える.
実際にはD3はSolovay条件を満たす関数たちを実際に構成する際に要請される.
Solovay条件を満たす文たち$ \theta_1, \dots, \theta_nは構成できる. Proof of Lem.5
Proof of Thm.1, cont.