プログラミング言語版不完全性定理(8) 第2不完全性定理の証明を書き直していきます。 証明関数 論理式と証明図をプログラミング言語のコードとして表すことができるシステムについて考えます。このシステムで論理式が証明できるかどうかを調べるプログラミン…

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

プログラミング言語版不完全性定理(6) 「不完全性定理(8) - エレファント・ビジュアライザー調査記録」では第2不完全性定理の式の計算を抽出して、そこから ChatGPT を使って第2不完全性定理の証明を書いてもらおうとしました。第1不完全性定理の式の計算は…

プログラミング言語版不完全性定理(5) 「不完全性定理(7) - エレファント・ビジュアライザー調査記録」の計算が間違っていたので書き直します。「コード化」と「逆コード化」を導入します。 を論理式全体の集合とします。 を自然数全体から論理式全体への写…

プログラミング言語版不完全性定理(4) 以下は『不完全性定理とはなにか 完全版 ゲーデルとチューリング 天才はなにを証明したのか (ブルーバックス B 2277)』の190ページ(様相論理)にある「ブーロスによる第2不完全性定理の証明『LOGIC, LOGIC, AND, LOGIC」…

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

プログラミング言語版不完全性定理(2) 「自分自身が証明できない」という論理式を定義することができれば真であり証明できない論理式になるということで『不完全性定理とはなにか 完全版 ゲーデルとチューリング 天才はなにを証明したのか (ブルーバックス B…

前回の「Cω」に以下の機能を追加することにします。 「Cω」では任意の長さの自然数を扱うことができる プログラミング言語Cでも配列を使うことで実現できるので必要ない(メモリー不足にはならないとしているので任意の長さの配列を使うことができる)のですが…

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

『不完全性定理とはなにか (ブルーバックス)』の不完全性定理の証明とチューリング機械の停止問題の証明について考えると、チューリング機械の停止問題の証明ではチューリング機械が停止するかどうか判定できると仮定したのに対して、不完全性定理の証明では…

『不完全性定理とはなにか (ブルーバックス)』の不完全性定理の証明をプログラミング言語を使って書き直していきます。しかし、すべてプログラミング言語のようにはできないので、まずはデータをプログラミング言語の式のように表すことを考えます。 不完全…

『不完全性定理とはなにか (ブルーバックス)』では「チューリング機械の停止問題」を参考にして「不完全性定理」を考えるということなので、前回は「チューリング機械の停止問題」について調べてみました。チューリング機械を扱うのではなく、無限のメモリー…

『不完全性定理とはなにか (ブルーバックス)』という本を見ると、不完全性定理について調べるためのヒントがいろいろ書かれていたので少し調べてみようと思います。また、ビジュアルプログラミングで何かやる例にすることができるかもしれないと考えています…