Solovayの算術的完全性定理
Introduction
Story
ここで述べられているが,この話がそもそも誰に由来するのかはわからないらしい.
以下引用.
地球の何処かに定住国を求める難民$ xがいる.
地球の国の数は有限である.
それぞれの国には渡航できる国は決まっているとする.
$ xは次のルールに沿って,母国から移住していく.
R1. 既に訪れた国には二度と戻れない.(非反射性)
R2. $ Aから渡航可能な国$ A'から渡航可能な国$ Bには,$ Aからでも渡航可能.(推移性)
R3. 今いる国から渡航可能な国には,「その国に定住しないこと」を証明したなら必ず移動する.
このとき,$ xは最終的にどうなるのか?
L1. $ xの定住国は必ずどこかに一国だけある.
R1と国の有限性より.
L2. 定住国が母国でない$ Aなら,「$ Aに定住しない」ことを証明しているはず.
R3より.
SnO2WMaN.icon「定住しない」と証明しておいて定住するってどういうことだよとは思うが,一旦受け入れる
L3. 定住国が$ Aで,$ Bが$ Aに渡航可能であるなら,「$ Bに定住しない」ことは証明できない.
もし証明出来たならR3より$ Bに移動しなければならない.ところが$ Aに定住しているのでそれはない.
L4. $ xが$ Aにいずれ渡航するが$ Aが定住国でない場合,$ Aから渡航可能などこかの国が定住国でなければならない.
R2より.
定住国となった場合$ xが幸せになれる国とそうでない国があるとする.$ xは自分が幸せになれることをなんとか証明したいとする.
母国でない$ Aが定住国とする.
H1. $ Aから渡航可能な国が全部幸せになれる国だったとする.
L2より,「$ Aには定住しない」ことは証明しているはず.
L4より,「$ A国から渡航可能などこかの国は定住可能である」ことが証明される.
仮定より,そのような国は全部幸せになれる国であることがわかっている.
結果,「$ xは幸せになれる」ことが証明できる.
H2. $ Aから渡航可能な国に幸せになれない国$ Bがある場合
仮に「$ xは幸せになれる」と証明できたとする.
このとき,「$ Bには定住しない」ということが証明されなければならない.
ところがそれはL3に反する.
なので「$ xは幸せになれる」ことは証明できない.
$ xは自分が証明した通りに動いて定住するとすると,結局母国からは一度も動くことは出来ない.
そのような$ xは一度移動すると延々に移動しなければならないが,国は有限だからそれは出来ない.
ここまでを纏めると
国$ Aを定住国とすれば$ xが幸せになれることを$ A \vDash Hと表す.
$ Aから移動可能な全ての国で幸せになれることは$ A \vDash \Box Hと表せる.
remark:$ A \vDash \Box H$ \iff$ A \rightsquigarrow A'な任意の$ A'で$ A' \vDash H
$ xが$ Aを定住国とすることを$ \beta_Aとする.
とすると
H1は$ \beta_Aかつ$ A \vDash \Box Hならば$ \mathrm{Pr}(H)
H2は$ \beta_Aかつ$ A \vDash \lnot\Box Hならば$ \lnot \mathrm{Pr}(H)
よって$ \Boxと$ \mathrm{Pr}が上手く対応する.
Notation
以下,$ \mathcal{M} \coloneqq \lang W,\rightsquigarrow,V \rangは有限推移木Kripkeモデルとする. $ W \coloneqq \{0,1,\dots,n\}とする.$ n \in \N.
様相論理の命題変数を算術の文に移す写像を,変換$ fと呼ぶ.(算術的変換) ある変換$ fについて,$ Tでの可証性を含めた算術の文に移す写像を$ T解釈とよび,$ f_Tで表す.算術的解釈 $ f_T(p) \equiv f(p)
$ f_T(\bot) \equiv \bot
$ f_T(A \to B) \equiv f_T(A) \to f_T(B)
$ f_T(\Box A) \equiv \mathrm{Pr}_T(\ulcorner f_T(A) \urcorner)
remark:
remark:
左辺は様相命題論理の言語$ \mathscr{L}_\mathrm{M}の論理式であり,右辺は算術の言語$ \mathscr{L}_\mathrm{A}の論理式である. 以下
$ \mathscr{L}_\mathrm{M}の論理式は$ A,B,\dots
$ \mathscr{L}_\mathrm{A}の論理式は$ \varphi,\psi,\dotsとして表す.
$ \vdash_\mathsf{GL} A$ \iff任意の変換$ fに対し$ T \vdash f_T(A)
$ \impliedbyが長い旅になる.
$ \Sigma_2論理式$ \beta(x)を以下のように構成する.
$ \beta(x) \equiv \exists_z.\forall_{y > z}. \lbrack h(y) = x \rbrack
ここで,$ h(x)とは次の原始再帰的関数であるとする.
$ h(0) = 0
$ h(k + 1)
$ = m,$ m \in Wかつ$ h(k) \rightsquigarrow mかつ,$ nが$ \lnot\beta(\overline{m})の$ Tでの証明のGödel数のとき
$ = h(k).そうでないとき.
remark:
example:
$ h(1)について
$ m = 0について調べる.
$ m \in Wかつ,$ h(0) \rightsquigarrow mかつ,$ 0が$ Tでの$ \lnot \beta(\overline{m})の証明のGödel数か?
このとき$ \lnot\beta(\overline{0}) \equiv \lnot\exists_z.\forall_{y > z}. \lbrack h(y) = \overline{0} \rbrack \equiv \forall_z.\exists_{y>z}.\lbrack h(y) \neq 0 \rbrack
そうでなかったとする.$ h(1) = h(0) = 0
$ h(2)について
$ m = 0,1について調べる.
どれでも成立しなかったとする.$ h(2) = h(1) = h(0) = 0
$ \vdots
いずれ$ h(k + 1) = mとなる最初の$ mが現れる.
$ 0 \rightsquigarrow mであり,$ kが$ \lnot\beta(\overline{m})の証明のGödel数となっている
最初の$ mなので任意の$ m' < mで$ h(m') = 0
「$ hが$ mでないときもある」ことの証明が得られたとき,$ hの値が変わる.
remark:
今いる国$ h(k) = \cdots = h(0) = 0から渡航可能な国$ mには
$ 0 \rightsquigarrow m
「$ mに定住しないこと$ \lnot \beta(\overline{m})」が証明できたなら,
移動する$ h(k+1) = m.
そして$ h(k + 2),h(k+3),\dotsへ
Lem 1
1. $ i \neq jなら$ \mathsf{PA} \vdash \beta(\overline{i}) \to \lnot\beta(\overline{j})
2. $ \mathsf{PA} \vdash \beta(\overline{1}) \lor \beta(\overline{1}) \cdots \lor \beta(\overline{n})
remark:1と2を合わせてL1になる.
3. $ i \rightsquigarrow jなら$ \mathsf{PA} \vdash \beta(\overline{i}) \to \lnot\mathrm{Pr}_T(\ulcorner \lnot\beta(\overline{j}) \urcorner)
remark: L3.
4. $ i \ge 1なら$ \mathsf{PA} \vdash \beta(\overline{i}) \to \mathrm{Pr}_T(\ulcorner \lnot\beta(\overline{i}) \urcorner)
remark: L2.
5. $ i \ge 1なら$ \mathsf{PA} \vdash \beta(\overline{i}) \to \mathrm{Pr}_T(\ulcorner \bigvee_{i \rightsquigarrow j} \beta(\overline{j}) \urcorner)
remark: L4.
proof:
Def 2
$ f(p) \equiv \bigvee_{i \in W \\ \mathcal{M},i \vDash p} \beta(\overline{i})とする.
Lem 3
$ i \in Wで$ i \ge 1.
1. $ \mathcal{M}, i \vDash A \implies \mathsf{PA} \vdash \beta(\overline{i}) \to f_T(A)
2. $ \mathcal{M}, i \nvDash A \implies \mathsf{PA} \vdash \beta(\overline{i}) \to \lnot f_T(A)
proof:
$ Aの構造帰納法.
$ A \equiv pのとき
$ \mathcal{M},i \vDash pなら$ \beta(\overline{i})は$ f(p)を構成する1要素.
よって少なくとも,$ f(p) \equiv \beta(\overline{i}).
ところで$ f_T(p) \equiv f(p).
よって$ \mathsf{PA} \vdash \beta(\overline{i}) \to f_T(p).
$ \mathcal{M},i \nvDash pなら$ \beta(\overline{i})は$ f(p)に含まれていない.
$ f(p)に含まれる全ての$ \beta(\overline{j})について
$ j \neq iなのでLem1.1より$ \mathsf{PA} \vdash \beta(\overline{i}) \to \lnot\beta(\overline{j})
ところで$ f_T(p) \equiv f(p).
よって$ \mathsf{PA} \vdash \beta(\overline{i}) \to \lnot f(p)
example:
$ \mathcal{M},1 \vDash pとする.
$ f(p) \equiv \beta(\overline{0}) \lor \beta(\overline{2})とする.定義より$ \beta(\overline{1})は含まれていない.
Lem1.1より
$ \mathsf{PA} \vdash \beta(\overline{1}) \to \lnot\beta(\overline{0})
$ \mathsf{PA} \vdash \beta(\overline{1}) \to \lnot\beta(\overline{2})
よって$ \mathsf{PA} \vdash \beta(\overline{1}) \to (\lnot\beta(\overline{0}) \land \lnot\beta(\overline{2}))
すなわち,$ \mathsf{PA} \vdash \beta(\overline{1}) \to \lnot(\beta(\overline{0}) \lor \beta(\overline{2}))
ところで$ \lnot(\beta(\overline{0}) \lor \beta(\overline{2})) \equiv \lnot f(p) \equiv \lnot f_T(p)
よって$ \mathcal{M},1 \vDash p \implies \mathsf{PA} \vdash \beta(\overline{1}) \to \lnot f_T(p)
$ A \equiv \bot,B \to Cは明らか.
$ A \equiv \Box Bの場合
$ \mathcal{M},i \vDash \Box Bなら
任意の$ i \rightsquigarrow jな$ j \leq nに対し,$ \mathcal{M},j \vDash B
IHより$ \mathsf{PA} \vdash \beta(\overline{j}) \to f_T(B)
よって$ \mathsf{PA} \vdash \bigvee_{i \rightsquigarrow j} \beta(\overline{j}) \to f_T(B)
導出可能性条件D1とD2より$ \mathsf{PA} \vdash \mathrm{Pr}_T (\ulcorner \bigvee_{i \rightsquigarrow j} \beta(\overline{j}) \urcorner) \to \mathrm{Pr}_T(\ulcorner f_T(B) \urcorner)
Lem1.5より$ \mathsf{PA} \vdash \beta(\overline{i}) \to \mathrm{Pr}_T (\ulcorner \bigvee_{i \rightsquigarrow j} \beta(\overline{j}) \urcorner)
よって$ \mathsf{PA} \vdash \beta(\overline{i}) \to \mathrm{Pr}_T(\ulcorner f_T(B) \urcorner)
ところで,$ \mathrm{Pr}_T(\ulcorner f_T(B) \urcorner) \equiv f_T(\Box B)
よって$ \mathsf{PA} \vdash \beta(\overline{i}) \to f_T(\Box B)
$ \mathcal{M},i \nvDash \Box B
とはいっても↑をちょっと変えるだけでまあ明らかに
Lem 4