不完全性定理(9)

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

以下は『不完全性定理とはなにか 完全版 ゲーデルとチューリング 天才はなにを証明したのか (ブルーバックス B 2277)』の190ページ(様相論理)にある「ブーロスによる第2不完全性定理の証明『LOGIC, LOGIC, AND, LOGIC」 413ページより」という表です。

公理

• (i) もしも ならば
• (ii)
• (iii)

第2不完全性定理の証明

• 1.
• 2.
• 3.
• 4.
• 5.
• 6.
• 7.
• 8.
• 9.
• 10.
• 11.

この結論が第二不完全性定理を表しているのかどうかよくわからないのでまた ChatGPT で調べてみました。

入力1:

演算 を

• 
• 右結合

とします。

はどうなりますか

結果:

演算 とその定義

与えられた演算 は以下のように定義されています：

• （ラムダ計算の関数適用と同じ）
• 右結合（つまり、 は と解釈される）

これを踏まえて、与えられた式

を具体的に解釈・評価します。

与えられた式の展開

1.

• これは右結合の規則に従って と解釈されます。
• は、与えられたコードの否定を表す関数です。

2.

• これは と解釈されます。
• と の組み合わせが再帰的に適用されています。

3.

• これは「 ならば 」を意味します。
• 演算としては「論理式のコードを得る」という形になります。

4.

• 最後に、この論理式のコードの「値」を によって評価します。

具体的な評価

• は「コード の論理式が証明可能」という命題のコードを表します。
• は「コード の論理式が証明可能でない」という命題のコードを表します。

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

全体の論理式

この論理式を評価します：
1. 前提 :

• が証明可能でないことを意味します。

2. 結論 :

• が証明可能でないことが証明不可能である、ということを意味します。

3. 全体の意味:

• 「 が証明可能でないならば、 が証明可能でないことが証明不可能である」という論理式を表します。

結論

の意味は：

つまり、論理式 に関して：

• 「 が証明可能でない」ことが成り立つならば、
• 「 が証明可能でないことが証明不可能である」という性質を評価するものです。

これは、証明可能性と否定的証明可能性に関する直観主義的な性質を反映しています。

入力2: これは第二不完全性定理の証明といえますか

結果:

はい、この評価は第二不完全性定理の証明の核心部分を含んでいます。ただし、第二不完全性定理そのものを完全に証明するには、この評価の結果を形式的な無矛盾性の証明不可能性に結びつけるさらなる議論が必要です。

評価の確認と第二不完全性定理との関連

与えられた式：

を分析すると、以下のような意味を持ちます：

1. 式の前提:

• 「論理式 が証明可能ではない」を意味します。

2. 式の結論:

• 「論理式 が証明可能でないことが証明不可能である」を意味します。

3. 全体の意味:

• 「 が証明可能でないならば、 が証明可能でないことが証明不可能である」という命題の評価です。

この結果は、自己言及的な命題に関連する性質を示しており、特に形式体系内での証明可能性に制限があることを反映しています。

第二不完全性定理との関係

第二不完全性定理の内容

第二不完全性定理は、無矛盾な形式体系 において、体系自身の無矛盾性（）を体系内で証明することができないことを主張します。

この議論において、

• を と置くと、
• は「 が証明可能でない」という命題を表します。

もし が体系内で証明可能であるとすると、上記の議論に矛盾が生じるため、 内で を証明することができないことが示されます。

必要な補足議論

この評価だけでは、形式的には第二不完全性定理の証明全体とはいえません。以下の追加の議論が必要です：

1. 形式体系 の自己反映性:
が自身の証明可能性や命題を適切に符号化できることを明示的に示す必要があります。

2. 命題の構築:
無矛盾性命題 を具体的に定義し、上記の評価がそれに適用できることを示します。

3. 矛盾の回避:
無矛盾な体系であれば、上記の評価から「体系内で無矛盾性を証明することができない」という結論を導くことができます。

結論

与えられた式 は、第二不完全性定理を証明するための核心的な性質を含んでいます。ただし、完全な証明とするためには形式体系の自己反映性や無矛盾性命題 との対応を詳細に議論する必要があります。その補足が整えば、この議論は第二不完全性定理の証明と見なすことができます。

前回の結論が第二不完全性定理の主張だと思うのですが、この様相論理バージョンの結論をラムダ計算風に書き直したものは違っているのでどうなのかということが知りたいのですが、これではまだよくわかりません。

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

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

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

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

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

数学基礎論　増補版

論理学

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

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

数理論理学

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

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

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

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