2024.07.27
https://gyazo.com/78231b1a8e6a4194e7a5dcf622699151
当面の目標として、iehality氏は算術上のゲーデルの第2不完全性定理を、私はソロベイによる𝐆𝐋の算術的完全性定理を示すことを目標としています。
おそらく両方とも何らかの定理証明支援系によって形式化された事実ではなく、この点において新規性があるだろうと考えています。
G2の証明で重要なのは「算術で」というより $ \sf I\Sigma_1 上で示そうとしている点ですね(L. C. Paulson の結果は HF での G2を証明しているが,これは $ \sf PAと同等で,私はもっと強い結果を証明しようとしている)
なお,これは我々のプロジェクトでも終わった.C
メモ
メモ
いいね
思った
真面目な人たちにツイッターアーがフォローされて恐縮なのですが,わたしのGitHubプロフィール画面はこうなっています
https://gyazo.com/2213c20ea25a4da8475bad06bc607139
(照)
メモ