Discussion
Closed
不完全性定理のコンピュータモデル実装を探しています。
誰か、そういうプログラムの所在をご存知の方がいらっしゃいましたら、
お教え下さい。
自分でやろうとしましたが、自分の能力を超えるような気がして大変なので、
また、広い世の中、こういうことは必ずと言っていいほど誰かがやっているものだと思うし、
不完全性定理の証明は、単純にしたら、コンピュータのロジックモデルで再現可能なものだから、
すでにあるものだったら、再発明の労力が省けると思いまして。
よろしくお願いします。
回答ではありません。 不学にして、
不完全性定理のコンピュータモデル
というものがどういうものを指すのかわかりません。 どのようなもの指しているのでしょうか？
定理証明支援系である Isabelle を使ってゲーデルの第一・第二不完全定理を機械的に証明したという論文なら見つかりました https://arxiv.org/abs/2104.13792
uasiさん、どうもありがとうございます。
見てみます。
uasiさんのポストは、不完全性定理を機械的に証明したという話ですが、そういうものを求めていたということでしょうか？
「不完全性定理のコンピュータモデル実装」とはだいぶ趣が違うように思いますが。
同じです
Coqでもゲーデルの不完全性定理に関するパッケージがあるようです。
https://github.com/coq-community/goedel
@pt9999さん、
どうもありがとうございました。
Linuxでもできるコンピュータの証明モデルが示されたので、質問をクローズします。
