Solovayの算術的完全性定理

Introduction

Solovayの構成法

有限推移木Kripkeフレームを算術の中に埋め込むという方向性を取る．

Robert M. Solovay; 1976; "Provability Interpretation of Modal Logic"

Story

証明可能性論理における難民のフォークロア

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:

ここでの$ \mathrm{Pr}_Tは標準的な証明可能性述語

すなわち導出可能性条件D1~D3を全て満たすようなものとする．

remark:

左辺は様相命題論理の言語$ \mathscr{L}_\mathrm{M}の論理式であり，右辺は算術の言語$ \mathscr{L}_\mathrm{A}の論理式である．

以下

$ \mathscr{L}_\mathrm{M}の論理式は$ A,B,\dots

$ \mathscr{L}_\mathrm{A}の論理式は$ \varphi,\psi,\dotsとして表す．

Thm: Solovayの算術的完全性定理

$ \vdash_\mathsf{GL} A$ \iff任意の変換$ fに対し$ T \vdash f_T(A)

$ \impliesは算術的健全性と呼ばれて形式化されたLöbの定理などから明らかになる．

$ \impliedbyが長い旅になる．

Def. Solovay Sentences

$ \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:

$ \beta(x)はSolovay Sentencesと呼ばれる．「$ xは$ hの極限値である」を意味する．

Gödelの不動点補題を用いて構成するが，どの様に構成するかは

新井敏康『数学基礎論』増補版やG. Boolos; "The Logic of Provability"を参照．

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:

数学における証明と真理第2部メモ参照！

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

#TODO

とはいっても↑をちょっと変えるだけでまあ明らかに

Lem 4