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

投稿日: 2022-08-14 日

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

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

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

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

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

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