§E16.29完全性と不完全性

最終更新

一階述語論理の完全性定理と Gödel の不完全性定理は、同じ「完全性」という語を用いるが、量化する対象が異なる。完全性定理は、任意の理論から意味論的に帰結する各文が形式的にも導出されることを述べる。第一不完全性定理は、算術を十分に表現する無矛盾かつ計算可能に列挙することができる各理論について、その理論が文と否定のどちらも証明しない文の存在を述べる。第二不完全性定理は、同じ種類の理論のうち Peano 算術を含むものについて、その理論自身の無矛盾性を表す特定の文が証明されないことを述べる。本記事では三つの主張を量化記号の順序まで明示して比較し、それらが矛盾せず、むしろモデルの存在を介して正確に対応することを証明する。

1 二種類の完全性

定義 1.1. 固定した一階述語論理の証明体系が意味論的に完全 (semantically complete) であるとは、任意の理論TTと任意の文φ\varphiについて

T⊨φ⟹T⊢φT\models\varphi\quad\Longrightarrow\quad T\vdash\varphi

が成り立つことをいう。健全性と合わせると、T⊨φT\models\varphiとT⊢φT\vdash\varphiは同値になる。

一方、固定した理論TTが構文論的に完全 (syntactically complete) であるとは、TTの言語の任意の文φ\varphiについて

T⊢φまたはT⊢¬φT\vdash\varphi\quad\text{または}\quad T\vdash\neg\varphi

が成り立つことをいう。

意味論的完全性は証明体系と意味論の対応に関する性質であり、構文論的完全性は一つの理論が各文を決定するか否かに関する性質である。「任意の理論TT」を量化する前者は、各TTが構文論的に完全であることを意味しない。

2 三つの定理の量化範囲

定理 2.1. 三つの定理は、次の形をもつ。

  1. 任意の集合サイズの有限項一階言語LL、任意のLL理論TT、任意のLL文φ\varphiについて、

    T⊨φ⟺T⊢φ.T\models\varphi\quad\Longleftrightarrow\quad T\vdash\varphi.

  2. 任意の無矛盾かつ計算可能に列挙することができるLAL_A理論T⊇QT\supseteq Qについて、あるLAL_A文RTR_Tが存在して、

    T⊬RTかつT⊬¬RT.T\nvdash R_T \quad\text{かつ}\quad T\nvdash\neg R_T.

  3. 任意の無矛盾かつ計算可能に列挙することができるLAL_A理論T⊇PAT\supseteq PAについて、標準証明述語に基づく無矛盾性文を

    Con⁡T=¬Prov⁡T(⌜0=S0⌝)\operatorname{Con}_T =\neg\operatorname{Prov}_T(\ulcorner0=S0\urcorner)

    とすると、

    T⊬Con⁡TT\nvdash\operatorname{Con}_T

    が成り立つ。

証明. 第一の主張は§E16.12 定理 5.2が与える双条件である。言語LLや理論TTの計算可能性を仮定せず、TTが算術を含むことも要求しない。

第二の主張は§E16.23 定理 4.2の Rosser 文に関する結論である。理論TTの無矛盾性、計算可能列挙可能性、およびQ⊆TQ\subseteq Tを仮定し、文RTR_Tの存在を結論する。

第三の主張は§E16.24 定理 10.1である。理論TT自身の標準証明述語によって定めた特定の文Con⁡T\operatorname{Con}_Tの非証明可能性を結論する。理論を量化する範囲は第二の主張より狭く、Q⊆TQ\subseteq TではなくPA⊆TPA\subseteq Tを仮定する。導出可能性条件 D2 と D3 の証明が対象理論の帰納法を用いるためである。▨

量化記号を略記すると、三つの主張の差は次のように表される。

定理 理論を量化する範囲 文の量化 結論
意味論的完全性 任意の一階理論TT 任意の文φ\varphi T⊨φ  ⟺  T⊢φT\models\varphi\iff T\vdash\varphi
第一不完全性 無矛盾かつ c.e. でT⊇QT\supseteq Q あるRTR_Tが存在 T⊬RTT\nvdash R_TかつT⊬¬RTT\nvdash\neg R_T
第二不完全性 無矛盾かつ c.e. でT⊇PAT\supseteq PA 特定のCon⁡T\operatorname{Con}_T T⊬Con⁡TT\nvdash\operatorname{Con}_T

第一行のTTは任意であるが、結論は「任意の文を証明するか、その否定を証明するか」ではない。結論は、TTのすべてのモデルで真になる文とTTから導出される文が一致するという主張である。

3 Rosser 文の両側にモデルが存在すること

不完全性定理が与える二つの非証明に強完全性を適用すると、Rosser 文を真にするモデルと偽にするモデルをそれぞれ得る。

定理 3.1.TTを無矛盾かつ計算可能に列挙することができるLAL_A理論とし、Q⊆TQ\subseteq Tとする。RTR_Tを

T⊬RTかつT⊬¬RTT\nvdash R_T \quad\text{かつ}\quad T\nvdash\neg R_T

を満たす Rosser 文とする。このとき、LAL_A構造M+\mathcal M_+とM−\mathcal M_-が存在して、

M+⊨T+RT,M−⊨T+¬RT\mathcal M_+\models T+R_T, \qquad \mathcal M_-\models T+\neg R_T

が成り立つ。特に、T+RTT+R_TとT+¬RTT+\neg R_Tはいずれも無矛盾である。

証明. まず、T⊬RTT\nvdash R_Tである。T⊨RTT\models R_Tを仮定すると、§E16.12 定理 5.2からT⊢RTT\vdash R_Tが得られ、非証明の仮定に反する。したがって、

T⊭RTT\not\models R_T

である。意味論的帰結の定義により、TTのモデルM−\mathcal M_-でM−⊭RT\mathcal M_-\not\models R_Tを満たすものが存在する。古典意味論ではRTR_Tは文なので、

M−⊨¬RT\mathcal M_-\models\neg R_T

である。ゆえに、M−⊨T+¬RT\mathcal M_-\models T+\neg R_Tである。

次に、T⊬¬RTT\nvdash\neg R_Tである。同じ議論を文¬RT\neg R_Tに適用すると、

T⊭¬RTT\not\models\neg R_T

を得る。したがって、TTのモデルM+\mathcal M_+でM+⊭¬RT\mathcal M_+\not\models\neg R_Tを満たすものが存在する。古典意味論によりM+⊨RT\mathcal M_+\models R_Tなので、M+⊨T+RT\mathcal M_+\models T+R_Tである。

モデルをもつ理論は、§E16.10 定理 6.1の健全性により無矛盾である。したがって、二つの拡大理論はいずれも無矛盾である。▨

二つのモデルは一般に同じモデルではない。RTR_TはM+\mathcal M_+で真であり、M−\mathcal M_-で偽であるため、同一の古典構造が両方の役割を担うことはできない。このモデルの分岐こそが、RTR_Tも¬RT\neg R_TもTTのすべてのモデルで真ではないことを表す。強完全性定理は、双方が意味論的帰結でないことを双方が証明不能であることに対応させるため、不完全性定理と矛盾しない。

4 第二不完全性が与えるモデル

第二不完全性定理にも、同じ意味論的な読み替えを一方向に適用することができる。

定理 4.1.TTを無矛盾かつ計算可能に列挙することができるLAL_A理論とし、PA⊆TPA\subseteq Tとする。このとき、あるLAL_A構造N\mathcal Nが存在して、

N⊨T+¬Con⁡T\mathcal N\models T+\neg\operatorname{Con}_T

が成り立つ。

証明. 第二不完全性定理により、T⊬Con⁡TT\nvdash\operatorname{Con}_Tである。もしT⊨Con⁡TT\models\operatorname{Con}_Tならば、§E16.12 定理 5.2からT⊢Con⁡TT\vdash\operatorname{Con}_Tが得られる。したがって、

T⊭Con⁡TT\not\models\operatorname{Con}_T

である。意味論的帰結の定義から、TTのモデルN\mathcal NでN⊭Con⁡T\mathcal N\not\models\operatorname{Con}_Tを満たすものが存在する。古典意味論によりN⊨¬Con⁡T\mathcal N\models\neg\operatorname{Con}_Tなので、N⊨T+¬Con⁡T\mathcal N\models T+\neg\operatorname{Con}_Tである。▨

外側のメタ理論でTTが無矛盾であるという仮定と、N⊨¬Con⁡T\mathcal N\models\neg\operatorname{Con}_Tという結論は矛盾しない。Con⁡T\operatorname{Con}_TはTTの標準証明述語を算術の内部で表した文であり、定理が得るN\mathcal Nを標準モデルと同一視する根拠はない。N\mathcal Nは、N\mathcal Nの内部で証明コードの条件を満たす要素をもつことがあり、その要素が外側の標準自然数に対応する有限証明コードであるとは限らない。

第二不完全性定理から直接得られる非証明はT⊬Con⁡TT\nvdash\operatorname{Con}_Tである。同じ仮定だけからT⊬¬Con⁡TT\nvdash\neg\operatorname{Con}_Tまで結論することはできないため、本節はT+¬Con⁡TT+\neg\operatorname{Con}_Tのモデルだけを主張する。 Rosser 文について両側のモデルを得た前節との違いは、上流の第一不完全性定理がT⊬RTT\nvdash R_TとT⊬¬RTT\nvdash\neg R_Tの二つを与える点にある。前節では二つの非証明の双方に強完全性定理を適用し、本節ではT⊬Con⁡TT\nvdash\operatorname{Con}_Tに強完全性定理を適用している。

理論を量化する範囲も前節と異なる。前節のTTはQQを含めばよいが、本節のTTはPAPAを含まなければならない。上流の第二不完全性定理が導出可能性条件を経由し、その証明が対象理論の帰納法を用いるからである。QQを含むがPAPAを含まない理論については、本記事はT+¬Con⁡TT+\neg\operatorname{Con}_Tのモデルの存在を主張しない。

5 演習

問題 5.1.

  1. 一階述語論理の意味論的完全性が、任意の理論の構文論的完全性を意味しない理由を、二つの量化の形を用いて説明せよ。
  2. T⊬RTT\nvdash R_TからT+¬RTT+\neg R_Tのモデルを得る論証を述べよ。
  3. T⊬Con⁡TT\nvdash\operatorname{Con}_Tから得られるモデルが、メタ理論においてTTが無矛盾でないことを示さない理由を述べよ。
解答 (確認問題の解答).
  1. 意味論的完全性は、任意のTTとφ\varphiについてT⊨φT\models\varphiならばT⊢φT\vdash\varphiであるという条件である。構文論的完全性は、固定したTTの任意の文φ\varphiについてT⊢φT\vdash\varphiまたはT⊢¬φT\vdash\neg\varphiであるという条件である。意味論的完全性は、T⊨φT\models\varphiまたはT⊨¬φT\models\neg\varphiのいずれかが必ず成り立つとは主張しない。
  2. T⊨RTT\models R_Tならば§E16.12 定理 5.2によりT⊢RTT\vdash R_Tとなるため、T⊬RTT\nvdash R_TからT⊭RTT\not\models R_Tを得る。したがって、TTのモデルでRTR_Tが偽になるものが存在し、そのモデルはT+¬RTT+\neg R_Tのモデルである。
  3. 得られるモデルは標準モデルであるとは限らない。モデルの内部で証明コードの条件を満たす要素が、外側の標準自然数による有限証明コードに対応するとは限らないため、N⊨¬Con⁡T\mathcal N\models\neg\operatorname{Con}_Tはメタ理論でTTの矛盾の証明が存在することを意味しない。

▨

参考文献

  1. Herbert B. Enderton, A Mathematical Introduction to Logic, 2nd ed., Academic Press, 2001.完全性定理と算術理論の不完全性を参考にした。
  2. Petr Hájek and Pavel Pudlák, Metamathematics of First-Order Arithmetic, Perspectives in Logic 3, Cambridge University Press, Cambridge, 2017, originally published 1993.算術理論の証明可能性述語、無矛盾性文、および不完全性定理の仮定を参考にした。

前提記事