不完全性定理(7)

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

「自分自身が証明できない」という論理式を定義することができれば真であり証明できない論理式になるということで『不完全性定理とはなにか 完全版 ゲーデルとチューリング 天才はなにを証明したのか (ブルーバックス B 2277)』に流れが書かれているので、できるだけこれに沿って ChatGPT で調べてみました。

入力1 (ラムダ計算)

をラムダ計算のラムダ抽象(右結合)、 をラムダ計算の関数適用(左結合)とします。 は式 の変数 を式 で置き換えたものとします。
と はあらかじめ定義されているとします。



とおくと

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

結果:

与えられた式をもとに証明を進めていきます。

の定義

1.
2.
3.

を証明する

Step 1: の定義を展開

まず、 を計算するために、 を展開します。

したがって、

Step 2: の定義を展開

次に、 を計算します。

したがって、

ここで、 に を代入すると、

Step 3: を元に戻す

これに を代入すると、

Step 4: と の等価性

なので、上式はそのまま にも当てはまります：

結論

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

入力2 (ラムダ計算のできるプログラミング言語)

ラムダ計算のできるプログラミング言語を考えます。
そのプログラミング言語では論理式を自然数で表すことができるとします。その自然数を論理式のコードと呼ぶことにします。
は、自然数を指定すると、「そのコードの論理式が証明できる」ということを表す論理式のコードを返す関数とします。
は、自然数を指定すると、「そのコードの論理式の否定」の論理式のコードを返す関数とします。
このとき

はどのような意味になりますか

結果:

与えられた条件をもとに、 の意味を解釈します。

前提

• コード: 各論理式は自然数で表され、その自然数を「コード」と呼びます。
• : 自然数 を指定すると、「コード に対応する論理式が証明可能である」という論理式のコードを返す関数。
  • : 「 が証明可能」の論理式のコード。
• : 自然数 を指定すると、「コード に対応する論理式の否定」の論理式のコードを返す関数。
  • : 「 の否定」の論理式のコード。

の解釈

この式を展開すると次のようになります：

つまり、 は次のような論理式のコードです：

• 「 が証明可能である」という命題の否定

意味の深掘り

1. 「 が証明可能である」

• は「 が証明可能である」という命題を表します。

2. その否定

• は「 が証明可能である」という命題の否定、つまり「 が証明可能でない」を表します。

3. 自己参照性

• 自身が「 が証明可能でない」という命題のコードであるため、これは自己参照的な構造を持っています。

関連する概念

このような自己参照的な構造は、ゲーデルの不完全性定理の一部に関連しています。ゲーデルは、自然数で表される命題が自らについて「証明可能でない」と主張するような形式的システムの文を構築できることを示しました。この文を「ゲーデル文」と呼びます。

具体的には、 は次のような意味を持つ可能性があります：

• に対応する論理式は「私は証明可能ではない」という自己参照的な命題を表している。

結論

は、「私は証明可能ではない」という自己参照的な論理式のコードを定義しています。このような構造は、形式的システムの限界や不完全性を示す重要な役割を果たします。

入力3: これを使って不完全性定理を証明してください

結果:

不完全性定理の証明を、提示された構造を用いて示します。ここでは第一不完全性定理に焦点を当てます。

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

形式的定理:
任意の無矛盾な一階算術の形式体系（例えばペアノ算術）において、次を満たす命題 が存在する：
1. は体系内で表現可能（つまり、その体系で記述できる）。
2. は体系内で証明も反証もできない（未解決）。

この命題 を「ゲーデル文」と呼びます。

構造と前提

• 論理式は自然数 に対応する「コード」として表現される。
• 関数 : の論理式が証明可能であることを表すコードを返す。
• 関数 : の論理式の否定のコードを返す。
• 式 : は「 が証明可能でない」という命題のコードを表す。

証明

1. ゲーデル文の構成

式 は次の自己参照的な命題を表しています：

これは、「 が証明可能」という命題の否定（つまり、「 が証明不可能」）を表しています。

2. が証明可能である場合の矛盾

仮に、 が証明可能であるとします。この場合：

• の内容は「私は証明可能ではない」であるため、 が証明可能であるという事実と矛盾します。

したがって、 が証明可能であることは無矛盾性を前提とした体系内では成立しません。

3. が反証可能である場合の矛盾

次に、仮に が反証可能（つまり、 の否定が証明可能）であるとします。この場合：

• の否定は「私は証明可能である」という命題を表します。
• しかし、もし「私は証明可能である」が証明可能であれば、これは 自体が証明可能であることを意味します。
• この場合も前述の矛盾が生じます。

したがって、 が反証可能であることも無矛盾性を前提とした体系内では成立しません。

4. は未解決である

上記の議論より、 は体系内で証明も反証もできません。

結論

これにより、形式体系の無矛盾性を仮定すると、自己参照的な命題 が体系内で証明も反証もできないことが示されました。このことは、ゲーデルの第一不完全性定理にほかならず、任意の無矛盾な形式体系には未解決の命題が存在することを示します。

入力4: は「真」であるといえますか

結果:

が「真」であるかどうかは、どのようなメタ理論の観点で考えるかによります。ただし、形式体系が無矛盾であることを前提にすると、次のように議論できます。

の内容

は次のような命題を表しています：

この命題の解釈を考えます。

1. 無矛盾性の前提

形式体系が無矛盾である場合、以下が成り立ちます：
1. を体系内で証明できない（さもなくば矛盾が生じます）。
2. を体系内で反証もできない（さもなくば矛盾が生じます）。

したがって、体系内では は「証明可能でも反証可能でもない」という未解決の命題です。

2. メタ理論の視点

形式体系の外部から（メタ理論の観点で）考えると：
1. が証明可能であると仮定すると、それは「 は証明可能でない」という主張と矛盾するため、この仮定は成立しません。
2. よって、実際に は証明可能ではありません。

この結論から、 の内容「私は証明可能ではない」は真であるといえます。

結論

形式体系が無矛盾であることを前提とすると、メタ理論の視点では は「真」であると解釈できます。ただし、体系内部では が「証明」も「反証」もできないため、体系内でその「真偽」を確定することはできません。

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

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

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

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

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

数学基礎論　増補版

論理学

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

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

数理論理学

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

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

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

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