不完全性定理(8)

プログラミング言語版不完全性定理(3)

『不完全性定理とはなにか 完全版 ゲーデルとチューリング 天才はなにを証明したのか (ブルーバックス B 2277)』の様相論理の項の第二不完全性定理の証明の計算をラムダ計算のように書き直せないかということで ChatGPT で調べてみました。

入力1: 第二不完全性定理はどのようなものですか

結果:

ゲーデルの第二不完全性定理

定理の内容

任意の無矛盾な一階算術の形式体系 において、

• 自身の無矛盾性を の内部で証明することはできない。

直感的な説明

第二不完全性定理は、第一不完全性定理をより強化したものです。第一不完全性定理では、形式体系 内で表現可能な「特定の命題（ゲーデル文）」が、体系内で証明も反証もできないことを示しました。一方で、第二不完全性定理は、さらに強い主張をします：

• が無矛盾であると仮定しても、その無矛盾性を 自身の中で証明することはできません。

つまり、形式体系が自身の安全性を保証することは不可能です。

定理の重要性

第二不完全性定理が示すことは以下の通りです：

1. 形式体系の限界

• いかに強力な形式体系であっても、自分自身の無矛盾性を内部で証明することはできません。
• よって、形式体系が信頼できるかどうかを確かめるためには、その体系外の「より強い体系」や「直観」に依存する必要があります。

2. 形式主義への打撃

• ヒルベルトの「数学の完全な形式化と無矛盾性の証明」というプログラム（Hilbert Program）は、第二不完全性定理によって達成不可能であることが明確になりました。

証明の概要

ゲーデルの第二不完全性定理の証明は、第一不完全性定理と深く関連しています。以下にその概略を示します：

1. 無矛盾性を表す命題

• の無矛盾性は、形式的に「 の中で矛盾を導けない」という命題 として表されます。

2. 自己参照的構造の利用

• 第一不完全性定理で示された方法により、自己参照的な命題を構築します。この命題は「私が証明されると矛盾が生じる」という性質を持ちます。

3. 無矛盾性の証明不可能性

• が無矛盾であるならば、ゲーデル文の反証は 内で不可能です。一方で、無矛盾性が証明可能ならゲーデル文も証明可能である必要があります。この矛盾により、 内で無矛盾性を証明することはできないことが示されます。

意味すること

第二不完全性定理の意味は次のようにまとめられます：

1. 無矛盾性を仮定して数学を進めることは可能ですが、その無矛盾性を体系の内部で保証することはできません。
2. 形式的体系が信頼できるかどうかは、外部の観点や直観に依存する必要があります。

例と応用

• 算術の形式体系
  • ペアノ算術（PA）は無矛盾だと信じられていますが、その無矛盾性をペアノ算術自身で証明することはできません。

• 信頼性の連鎖
  • 形式体系 の無矛盾性を証明するには、より強力な体系 に頼る必要があります。しかし、この も自身の無矛盾性を証明することはできないため、無限の信頼の連鎖が必要になります。

第二不完全性定理は、数学の基礎論や形式主義の限界を示す深遠な結果であり、数学的思考や論理学の根幹を形作る概念です。

入力2:

を(論理式のコードを指定して)論理式の「値」を得る関数とします。
を論理式のコード と から「 ならば 」という論理式のコードを得る演算とします。
以前定義したのと同様
は、自然数を指定すると、「そのコードの論理式が証明できる」ということを表す論理式のコードを返す関数とします。
は、自然数を指定すると、「そのコードの論理式の否定」の論理式のコードを返す関数とします。
これらは

• 
• 

を満たすとします。このとき

が成り立つことを証明してください

結果:

与えられた関係式をもとに、 を証明します。

前提条件の整理

1. 関数と演算の定義

• : 論理式のコード の論理値（「真」か「偽」）を返す関数。
• : 論理式のコード と を元に、「 ならば 」という論理式のコードを生成する演算。

2. 与えられた性質

• 
• 

目標

以下の式が成立することを証明します：

証明

Step 1: の性質を利用

与えられた および から、次が成り立ちます：


よって、 は両式の共通の値を持つことがわかります。

Step 2: と の関係

および に対応する論理式について考えると、「」は次の形に分解できます：
1. の「証明可能性」に基づく：

• : 「 が証明可能ならば も証明可能」という形。

2. の「否定」に基づく：

• : 「 が証明不可能ならば も証明不可能」という形。

これらは直観主義論理において等価であることが知られています。

Step 3: の意味

は、「 が証明可能でないことが証明可能である」という論理式のコードを表します。

• これは直観主義論理において、 が持つ性質を符号化したものです。

Step 4: 結合の置き換え

において、 と の関係を利用して次を置き換えます：

結論

これにより、目標とする式

が成り立つことが証明されました。

様相論理の項に出ていた計算をラムダ計算の形に書き直すということがやりたかったのですが、これはちゃんと証明できているのかどうか不明です。

入力3:

は以前定義したものとします。
は任意の論理式のコードとします。
によって第二不完全性定理を証明することはできますか

結果:

はい、 を用いることで第二不完全性定理を証明する枠組みを構築できます。以下にその方法を説明します。

背景と前提の整理

1. の定義

以前定義した は以下を表します：

これは、 が「 自身が証明可能ではない」という命題を表す自己言及的な構造を持つことを意味します。

2. の任意性

は任意の論理式のコードとします。特に、形式体系 の無矛盾性を表す命題 を表すコードを選ぶことができます。

3. と

は、「もし が成り立つならば が成り立つ」という命題の「値」を評価する関数です。この値を使って体系 の無矛盾性について議論します。

第二不完全性定理の証明の流れ

1. の定義

形式体系 の無矛盾性を表す命題 は、「体系 では矛盾を導けない」ということを表します。記号的には次のように定義されます：

ここで は矛盾を表すコードです。

2. の解釈

は「 が証明可能ではない」という命題を表しています。よって、 は「 が成り立つならば は無矛盾である」という意味を持ちます。

3. の評価

を考えると、次のように評価されます：

1. が証明可能である場合：

• の定義から、これは「 が証明可能ではない」と矛盾するため、無矛盾な体系では成立しません。

2. が証明不可能である場合：

• は「 が証明可能でない」という命題そのものであるため、真であると考えられます。
• このとき、 は真であるため、 は「真」を返します。

4. 第二不完全性定理の結論

形式体系 内で無矛盾性 を証明するには、少なくとも を体系内で証明可能でなければなりません。しかし、次のことが成り立ちます：

1. を証明するためには、 の真偽が体系内で確定される必要があります。
2. しかし、 の自己言及的な性質により、 が体系内で証明可能であると仮定すると矛盾が生じます。
3. 結果として、 も体系内で証明することができません。

これにより、形式体系 内で を証明することができないことが示されました。

結論

を用いることで、形式体系 が無矛盾であること（つまり ）をその体系内で証明できないことを示す枠組みを提供できます。これは、ゲーデルの第二不完全性定理そのものです。

「入力2」の計算を使って第二不完全性定理が証明できるかどうかという質問だったのですが、「入力2」の結果は使われていないようですし証明ができているのかどうか不明です。

不完全性定理とはなにか 完全版 ゲーデルとチューリング 天才はなにを証明したのか (ブルーバックス B 2277)

チューリングの計算理論入門　チューリング・マシンからコンピュータへ (ブルーバックス)

不完全性定理: 数学的体系のあゆみ (ちくま学芸文庫 ノ 4-1 Math&Science)

今度こそわかるゲーデル不完全性定理 (今度こそわかるシリーズ)

数学基礎論 (ちくま学芸文庫)

数学基礎論　増補版

論理学

証明と論理に強くなる ～論理式の読み方から，ゲーデルの門前まで～

Coq/SSReflect/MathCompによる定理証明:フリーソフトではじめる数学の形式化

数理論理学

数理論理学: 合理的エ-ジェントへの応用に向けて

計算理論の基礎 [原著第3版] 1.オートマトンと言語

計算理論の基礎 [原著第3版] 2.計算可能性の理論

計算理論の基礎 [原著第3版] 3.複雑さの理論