Σ₁完全性定理
結論
参考文献
Remark
$ \mathscr{L}_\mathrm{A}は算術の言語とする． 当然$ \mathscr{L}_\mathrm{A}の理論である．
memo:
$ \sf PA^{-}は帰納法の公理図式を持たないPeano算術であるから$ \sf Qと同じとみなして良い（はず）． 1階述語論理における任意の論理式$ \varphiに対し，同値な冠頭標準形な論理式$ \varphi'が存在する． $ \psiは$ \Delta_0論理式とする．$ 0 \leq m
2. $ \varphiの冠頭標準形が$ \exists_{x_1,\dots,x_m}\psiであるとき，$ \varphiは$ \Sigma_1論理式であるとする．
3. $ \varphiの冠頭標準形が$ \forall_{x_1,\dots,x_m}\psiであるとき，$ \varphiは$ \Pi_1論理式であるとする．
remark:$ m=0でも構わないので，任意の$ \Delta_0論理式は$ \Sigma_1論理式及び$ \Pi_1論理式であることに注意．
更に，$ 0 \leq m
4. $ \psiが$ \Sigma_n論理式で，$ \varphiの冠頭標準形が$ \forall_{x_1,\dots,x_m}\psiであるとき，$ \psiは$ \Pi_{n+1}論理式であるとする．
5. $ \psiが$ \Pi_n論理式で，$ \varphiの冠頭標準形が$ \exists_{x_1,\dots,x_m}\psiであるとき，$ \psiは$ \Sigma_{n+1}論理式であるとする．
remark:
上の注意と同様に$ m=0でも構わないので，
任意の$ \Sigma_k論理式は$ \Pi_{n+1}論理式である
任意の$ \Pi_k論理式は$ \Sigma_{n+1}論理式である
6. $ \Sigma_n論理式かつ$ \Pi_n論理式でもある論理式は$ \Delta_k論理式という．
7. $ \mathscr{L}_\mathrm{A}の論理式の集合$ \Phi \sube \mathrm{Fml}_{\mathscr{L}_\mathrm{A}}について↓が成り立つとき，$ \Phiを$ \Delta_n,\Sigma_n,\Pi_nと言う．
$ \varphi \in \Phi$ \iff$ \varphiは$ \Delta_n,\Sigma_n,\Pi_n論理式
すなわち，$ \Phiは$ \mathscr{L}_\mathrm{A}の$ \Delta_n,\Sigma_n,\Pi_n論理式全体集合となっている．
8. 同様に，$ \mathscr{L}_\mathrm{A}の文の集合$ \Theta \sube \mathrm{Snt}_{\mathscr{L}_\mathrm{A}}について同じ条件が成り立つとき，$ \Thetaを$ \Delta_n,\Sigma_n,\Pi_nと言う．
Remark: 否定について
$ \lnot \exists_{\vec{x}}.\varphi \equiv \forall_{\vec{x}}.\lnot\varphi
$ \lnot \forall_{\vec{x}}.\varphi \equiv \exists_{\vec{x}}.\lnot\varphi
よって，
$ \Sigma_n論理式$ \varphiの否定$ \lnot\varphiは$ \Pi_n論理式である．
$ \Pi_n論理式$ \varphiの否定$ \lnot\varphiは$ \Sigma_n論理式である．
Remark
以降，論理式または文は必ず冠頭標準形であるものと約束する． Def. $ \Sigma_k完全性/$ \Pi_k完全性
文の集合$ \Theta \sube \mathrm{Snt}_{\mathscr{L}_\mathrm{A}}とする．
1. 全ての文$ \theta \in \Thetaに対して$ \mathcal{N} \vDash \theta \implies T \vdash \thetaであるとき，$ Tは$ \Theta完全であるという．
2. $ \Thetaが$ \Sigma_nであるとき$ Tは$ \Sigma_n完全であるという．
3. $ \Thetaが$ \Pi_nであるとき$ Tは$ \Pi_n完全であるという．
Def. $ \Sigma_k健全性/$ \Pi_k健全性
文の集合$ \Theta \sube \mathrm{Snt}_{\mathscr{L}_\mathrm{A}}とする．
1. 全ての文$ \theta \in \Thetaに対して$ T \vdash \theta \implies \mathcal{N} \vDash \thetaであるとき，$ Tは$ \Theta健全であるという．
2. $ \Thetaが$ \Sigma_nであるとき$ Tは$ \Sigma_n健全であるという．
3. $ \Thetaが$ \Pi_nであるとき$ Tは$ \Pi_n健全であるという．
Lem 1
$ Tが$ \Pi_n完全$ \implies$ Tは$ \Sigma_{n+1}完全
proof:
1. $ Tを$ \Pi_n完全とする
2. $ \thetaは$ \Sigma_{n+1}文であるとし，$ \mathcal{N} \vDash \thetaとする．$ \vdash \thetaを示す．
3. $ \theta \equiv \exists_{\vec{x}}.\xi(\vec{x})となるような$ \Pi_n文$ \xi(\vec{x})が存在する．
4. 2と3より$ \vDash \xi(\vec{a})となるような$ \vec{a}が存在する．
$ \vDashの定義より．
5. 1と4より$ \vdash \xi(\vec{a})となるような$ \vec{a}が存在する．
$ \xiは$ \Pi_n文であり$ \Pi_n完全性より．
6. よって，$ \vdash \exists_{\vec{x}}.\xi(\vec{x})．すなわち$ \vdash \theta．
Lem 2
$ Tが$ \Sigma_n健全$ \implies$ Tは$ \Pi_{n+1}健全
proof:
1. $ Tを$ \Sigma_n健全とする
2. $ \thetaは$ \Pi_{n+1}文であるとし，$ T \vdash \thetaとする．$ \mathcal{N} \vDash \thetaを示す．
3. $ \theta \equiv \forall_{\vec{x}}.\xi(\vec{x})となるような$ \Sigma_n文$ \xi(\vec{x})が存在する．
4. 2と3より任意の$ \vec{a}で$ \vdash \xi(\vec{a})．
5. 1と4より任意の$ \vec{a}で$ \vDash \xi(\vec{a})
6. よって，$ \vdash \forall_{\vec{x}}.\xi(\vec{x})．すなわち$ \vDash \theta．
$ Tが$ \Sigma_1健全なら，無矛盾である．
proof
1. $ Tが矛盾すると仮定すると破綻することを示す．
2. 算術の理論$ Tが矛盾しているとき，$ T \vdash 0=1である．
3. $ 0 = 1は$ \Sigma_1文である．
$ \Delta_0文である．
4. $ Tが$ \Sigma_1健全なら，2,3より$ \mathcal{N} \vDash 0 = 1である．
5. しかし実際には$ \mathcal{N} \nvDash 0 = 1である．
6. 5,6より破綻する．$ Tは無矛盾である．
Thm.3 $ \Sigma_1完全性定理
$ Tは$ \Sigma_1完全である．
すなわち，
任意の$ \Sigma_1文$ \thetaに対し，$ \mathcal{N} \vDash \theta \implies T \vdash \theta
proof:
1. Lem1より，$ Tが$ \Pi_0完全であるなら，$ Tは$ \Sigma_1完全である．
2. $ Tが$ \Pi_0完全であることと$ \Delta_0完全であることは同じである．
3. 以下で示されるCor 3.4より，$ Tは$ \Delta_0完全である．
4. したがって以上より，$ Tは$ \Sigma_1完全である．❏ Lem 3.1
$ \tau(\vec{x})を$ \mathscr{L}_\mathrm{A}の項とする．
$ a_1,\dots,a_m,b \in \Nとする．
$ a_1,\dots,a_m,bは自然数である．直接項$ \tauに入れることは出来ない．
$ \mathcal{N} \vDash \tau(\vec{\overline{a}}) = \overline{b} \implies T \vdash \tau(\vec{\overline{a}}) = \overline{b}
proof:項についての帰納法．
remark:
$ a \in \Nとしたとき，数項を$ \overline{a}として表す． $ a_1,\dots,a_n,b \in \Nと書いて暗黙の了解として項としているっぽいが，ややこしいのでちゃんと明記することにする．
Lem 3.2
$ \varphiを$ \Delta_0論理式とする．
$ tを閉じた（自由変数を持たない）$ \mathscr{L}_\mathrm{A}の項とする．
$ a \in \Nとする．
$ \mathcal{N} \vDash t = \overline{a}とする．
このとき，以下が成り立つ．
1. $ \mathcal{N} \vDash \forall_{x \leq t}. \varphi(x) \leftrightarrow (\varphi(\overline{0}) \land \dots \land \varphi(\overline{a}))
2. $ \mathcal{N} \vDash \exists_{x \leq t}. \varphi(x) \leftrightarrow (\varphi(\overline{0}) \lor \dots \lor \varphi(\overline{a}))
proof:自然数の帰納法で．
また，以下が成り立つ．
3. $ T \vdash \forall_{x \leq t}. \varphi(x) \leftrightarrow (\varphi(\overline{0}) \land \dots \land \varphi(\overline{a}))
4. $ T \vdash \forall_{x \leq t}. \varphi(x) \leftrightarrow (\varphi(\overline{0}) \lor \dots \lor \varphi(\overline{a}))
proof:1と2の証明を$ \sf Qで形式化する．
Lem 3.3
$ \thetaを$ \Delta_0文とする．
$ \mathcal{N} \vDash \theta \leftrightarrow \xiかつ$ T \vdash \theta \leftrightarrow \xiな，量化子を含まない文$ \xiが存在する．
proof:
Lem 3.2より．すなわち，限定量化は$ \landと$ \lorの連なりに変換出来る．
example:
$ \exists_{x \leq \overline{2}}.\varphi(x)という$ \Delta_0文は$ \varphi(\overline{0}) \lor \varphi(\overline{1}) \lor \varphi(\overline{2})という$ \Delta_0文と同値である．
Cor 3.4
$ \thetaを$ \Delta_0文とする
1. $ \mathcal{N} \vDash \theta \implies T \vdash \theta
2. $ Tが無矛盾なら，$ T \vdash \theta \implies \mathcal{N} \vDash \theta
proof:
Lem3.3より$ \thetaを量化子を含まない文$ \xiに変形する
更に$ \xiを適当に変形すると$ \mathcal{N} \vDash \xi \implies T \vdash \xiが言える．
すなわち定義より，
3. $ Tは$ \Delta_0完全である．
4. $ Tが無矛盾なら，$ Tは$ \Delta_0健全である．
Cor 4
$ Tが無矛盾なら，$ Tは$ \Pi_1健全である．
proof:
Cor 3.4とLem2より．
Cor 5
$ \thetaは$ \Delta_0文とする．
$ T \vdash \thetaまたは$ T \vdash \lnot\thetaのどちらか一方である．
proof:
以下の事実より．
1. $ \thetaが$ \Delta_0文ならば，$ \mathcal{N} \vDash \thetaまたは$ \mathcal{N} \vDash \lnot\thetaのどちらか一方である．
2. Cor3.4より$ Tは$ \Delta_0完全である．