不完全性定理(5)

『不完全性定理とはなにか』の新しい版(不完全性定理とはなにか 完全版 ゲーデルとチューリング 天才はなにを証明したのか (ブルーバックス B 2277))が出ていたので、旧版のわかりにくかったところが書き換えられているのかどうかを調べようと思ったのですが、書き換えられているかどうかはよくわかりませんでした。そこでそれを調べる前に、まずチューリング機械の停止問題について ChatGPT で調べてみました。

チューリング機械の停止問題

ChatGPT で以下のように入力しました。

プログラミング言語Cと同等の機能をもち、かつメモリー不足で停止することはなく永久に動き続けることができるプログラミング言語を「プログラミング言語Cω」とします。 「Cω」は以下の機能をもつとします。

• 「Cω」のコードはメモリー上で一つの自然数で表される(Cと同様)
• 「Cω」で「Cω」の構文解析ができる(Cと同様)
• 構文解析ができたとき「Cω」で「Cω」のコードを実行できる(Cと同様：Cコンパイラーでコンパイル後実行、またはCインタープリターで実行)

「Cω」のコードを実行すると、終了するか、または永久に動き続けるとします。実際のコンピューター上のプログラミング言語で実行すると、メモリー不足で終了してしまったり、動力を供給することができなくなって停止してしまったりすることもありますが、「Cω」はそのようなことが起こらない理想的なコンピューター上で動作しているのでそのようなことは起こらないとします。
このとき「Cω」で以下のような関数 h を書くことができたと仮定します：

• 一つの自然数を引数として受け取る
• この関数は必ず終了する
• 引数の自然数が「Cω」のコードのときは、コードを実行したとき終了するならば 1、終了しないならば 0 を返す
• 引数の自然数が「Cω」のコードではないときは 2 を返す

「Cω」でこのような関数 h を書くことができたと仮定するとどうなりますか

以下のような答えが戻ってきました。

このような関数 を「Cω」で書けると仮定すると、チューリング停止問題の解決が可能であることを意味します。しかし、この仮定は理論的には矛盾を引き起こします。以下に詳細を説明します。

1. 停止性判定問題の背景

停止性問題（Halting Problem）は、任意のプログラム（コード）とその入力が与えられたときに、そのプログラムが有限時間内に停止するかどうかを決定する問題です。この問題はアラン・チューリングによって1936年に理論的に解明され、停止性問題は一般には解決不可能であることが示されています。

「Cω」で定義された関数 は次のように停止性問題を解くための判定関数を提供します：

このような関数を記述できると仮定した場合、停止性問題を解けるため、チューリングの停止性問題の非決定可能性という理論と矛盾します。

2. 矛盾の具体例

矛盾を示すために、関数 を用いた自己参照的なプログラムを考えます。

の定義

以下のようなプログラム を考えます：

この のコード（自然数として表現される値）を とします。

矛盾の導出

1. ケース1: の場合

• であるということは、 が停止することを意味します。
• しかし、 の定義では の場合に無限ループするように書かれています。
• したがって矛盾します。

2. ケース2: の場合

• または を意味します。
• この場合、 は停止するように定義されています。
• しかし、 の定義では の場合に停止するので矛盾しません。
• ところが が停止すると、元の停止性判定の結果 が正しくなくなる場合が生じます。

3. 結論

この矛盾から、「Cω」でそのような を実装できるという仮定が間違っていることがわかります。具体的には、次のことが言えます：

• 理論的に停止性問題を解くような判定関数 を記述することは不可能である。
• 「Cω」が停止性問題を解決可能であるならば、「Cω」はチューリングマシンよりも強力な計算能力を持つ必要があるが、それは既存の計算理論と矛盾する。

このため、「Cω」の設計上、「h のような関数を記述できる」という仮定自体が成立しない、または「Cω」が現実的には存在し得ないという結論に至ります。

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

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

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

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

論理学

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

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

数理論理学

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

数学基礎論　増補版

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

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

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