非専門的シンギュラリティー研究所

無限に動き続けるシステムを表す方法を AI なども使って考えていきます。

不完全性定理(12)

不完全性定理

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

「不完全性定理(8) - エレファント・ビジュアライザー調査記録」の式の計算は『数学基礎論 (ちくま学芸文庫)』に基づいて考えたと思うのですが、うまく対応しているかどうかわかりません。式をどうやって導いたかやり直してみます。

そこで『数学基礎論 (ちくま学芸文庫)』の「第2不完全性定理について」の記述を引用します。計算を元にこのように書いてほしかったのですがうまくいきませんでした。

第2不完全性定理について

「ZFが矛盾する」というのは「 $\bot$ が［ZFで］証明できる」ということである。 $\bot$ のゲーデル数は $13$ であり、記号の列と考えたときの $\bot$ のゲーデル数は $2^{13}$ であるから、formula
$\mathrm{Prov}(\mathbf{2}^{13})$
は「ZFが矛盾する」という命題を表わす formula である。
したがって、
（17） $\mathrm{Consis} \equiv \lnot \mathrm{Prov}(\mathbf{2}^{13})$
として定義される $\mathrm{Consis}$ は「ZFは無矛盾（consistent）である」という命題を表わす formulaである。
さて、第1不完全性定理の2）は
ZFが無矛盾ならば、 $U$ はZFで証明できない
ということであったが、これは
（18） $\mathrm{Consis} \to \lnot \mathrm{Prov}(\mathbf{q})$
という formulaで表わされる。何となれば、（12）の後半によれば、 $U$ のゲーデル数が $q$ だったからである。
第1不完全性定理の全証明を形式化してZFの証明図として書くと、formula（18）の証明図が得られ，（18）は証明できる。したがって、（14）によれば、formula
（19） $\mathrm{Consis} \to U$
が証明できることもわかる。そして、このことから、ZFが無矛盾ならば $\mathrm{Consis}$ は証明できない、ということがわかる．何となれば、もし $\mathrm{Consis}$ が証明できたとすれば、（19）により、 $U$ も証明できることになり、第1不完全性定理の2）に反するからである.

『不完全性定理: 数学的体系のあゆみ (ちくま学芸文庫ノ 4-1 Math&Science)』に「第2不完全性定理の証明のあらまし」の記述があります。これは参考にしなかったと思うのですが、引用しておきます。

第2不完全性定理の証明のあらまし

論理式 $\mathrm{Consis}$ は、254～256ページで紹介した論理式と関数を使えば我々にも書ける：
どんな $m$ についても、けっして

$[\mathrm{Provable}(m)$ でしかも $\mathrm{Provable}(\mathrm{neg}(m))]$ にはならない

ほかにもいろいろな書き方ができるが、これだけ念のため、記号論理の記法でも書いておこう。

$(\forall m) \lnot [\mathrm{Provable}(m) \land \mathrm{Provable}(\mathrm{neg}(m))]$

なお $\mathrm{Consis}$ の否定 $\lnot \mathrm{Consis}$ は、もちろん「矛盾の発生」を意味している：ある $m$ について、

$[\mathrm{Provable}(m)$ でしかも $\mathrm{Provable}(\mathrm{neg}(m))]$

さて定理4は、定理3の（超）証明の一部分（251ページ、①）

「もし $G$ が証明可能だとすると、 $G$ 自身がいっていることと矛盾する」

を形式化することによって導かれる。ただその前に準備として、ひとつ注意をしておかなければならない。具体的な自然数 $k$ に対して、論理式

$\mathrm{Provable}(k)$

のゲーデル数を $p(k)$ とすると、次のことが一般的・形式的に証明できる。

① $\mathrm{Provable}(k) → \mathrm{Provable}(p(k))$

これは内容的に、ひらたくいえば

文☆が証明できるならば、「文☆は証明できる」という文も証明できる

ということである（これはけっして自明ではなく、証明を要することであるが、証明はあんがい複雑である）。
さて

$k = \mathrm{sub}(1117,17, g(1117))$

とおくと、これはゲーデル文 $G$ ，すなわち $G(1117)$ のゲーデル数であり、
$\begin{eqnarray*} G & = & G(1117) \\ & = & \lnot \mathrm{Provable}(\mathrm{sub}(1117, 17, g (1117))) \\ & = & \lnot \mathrm{Provable}(k) \end{eqnarray*}$
であるから、
$k$ は“ $\lnot \mathrm{Provable}(k)$ ”のゲーデル数である，
ともいえる。一方“ $\mathrm{Provable}(k)$ ”のゲーデル数は $p(k)$ なので
$\begin{eqnarray*} k & = & “ \lnot \mathrm{Provable}(k) ”のゲーデル数 \\ & = & \mathrm{neg}(“ \mathrm{Provable}(k)”のゲーデル数 ) \\ & = & \mathrm{neg}(p(k)) \end{eqnarray*}$
が成り立つ。したがって、同語反復

② $\mathrm{Provable}(k) → \mathrm{Provable}(k)$

の右辺の $k$ を、それと等しい $\mathrm{neg}(p(k))$ におきかえることができ（ライプニッツの法則），

③ $\mathrm{Provable}(k) → \mathrm{Provable}(\mathrm{neg}(p(k)))$

が得られる。
このように、 $\mathrm{Provable}(k)$ を前提とすると、①と③から

$\mathrm{Provable}(p(k))$ と $\mathrm{Provable}(\mathrm{neg}(p(k)))$

が両方とも導かれることになる（矛盾発生！）。これは

④ $\mathrm{Provable}(k) → \lnot \mathrm{Consis}$

を意味している。したがって、対側の法則（の拡張版）によって

⑤ $\mathrm{Consis}→ \lnot \mathrm{Provable}(k)$

が得られる。ところが右辺の“ $\lnot \mathrm{Provable}(k)$ ”はゲーデル文 $G$ であるから、これは

$\mathrm{Consis}→ G$

ということである。
このように $\mathrm{Consis}→G$ が証明できるから、もし $\mathrm{Consis}$ まで証明できたとすると、推論規則「切断」によって $G$ が導かれる。しかしそれは、体系 $Z$ が無矛盾のときはありえない（第1不完全性定理）。したがって、もし体系 $Z$ が無盾ならば、論理式 $\mathrm{Consis}$ を体系内で形式的に証明することは不可能である。
なお $Z$ の無盾性を表現する論理式は、この $\mathrm{Consis}$ 以外にもある。

ある $m$ について、 $\lnot \mathrm{Provable}(m)$

もそのひとつであるーこれも $Z$ が無矛盾ならば、 $Z$ の中では証明できない。しかし

$Z$ が無矛盾だとすれば、 $\mathrm{Consis}$ と内容的に同値になる論理式

まで含めると、 $Z$ の中で証明できるものがある（クライゼル）。「無盾性を（ある弱い意味で）表現している論理式の中には、 $Z$ の中で形式的に証明できるものもある」というわけである。

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

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

作者:竹内薫
講談社

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

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

作者:高岡詠子
講談社

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

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

作者:野崎昭弘
筑摩書房

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

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

作者:本橋信義
講談社

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

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

作者:前原昭二,竹内外史
筑摩書房

数学基礎論　増補版

数学基礎論　増補版

作者:新井敏康
東京大学出版会

論理学

作者:野矢茂樹
東京大学出版会

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

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

作者:小島寛之
技術評論社

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

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

作者:萩原学,アフェルト・レナルド
森北出版

数理論理学

数理論理学

作者:戸次大介
東京大学出版会

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

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

作者:加藤暢
コロナ社

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

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

作者:Michael Sipser
共立出版

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

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

作者:Michael Sipser
共立出版

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

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

作者:Michael Sipser
共立出版