グッドスタインの定理をACL2で証明できるか気になってる

投稿日: 2022-08-14 日
ACL2

グッドスタインの定理はペアノ算術の範囲では証明できないことが示されている定理らしく順序数を使うと証明できるらしい。

下記の動画でこの定理の名前を知り Wikipedia で調べて順序数と関係のある定理であると知った。

【雑学】正しいとも間違いとも言えない数学の命題が存在する【ゆっくり解説】 - YouTube

グッドスタインの定理 - Wikipedia

ペアノ算術の範囲で証明できないことを証明するのは難しそうだが、 Wikipedia に載っている順序数を使った証明は ACL2 で可能かもしれないと思って調べてみた。

すると、グットスタインの定理を ACL2 で表現しているコードが、 ACL2 の books に misc/goodstein.lisp として掲載されていた。

acl2/goodstein.lisp at master · acl2/acl2 · GitHub

関数は :program モードで定義されているため、 このファイルを読み込んでもファイル中の goodstein 関数の停止性が自動証明されるわけではない。 コメントで何故停止するのかの説明がなされているがそれぞの関数の定義をよく読み込まないと理解できなそう。

順序数の勉強にもなりそうだし、余裕があったらとり組んでみようと思う。

日記の一覧に戻る