2024.07.23
https://gyazo.com/5ef0be9e13afac71e1590f3c38486386
形式化した
Classicalな理論が完全なら選言特性を持ち,逆も成り立つ.
思った
Boolosのやつでは代入規則が入っているため使えるが私のやつは公理図式だから微妙に証明が通らない
メモ
「このプロジェクトが引用先のような目的を志向しているのかは知らない/おそらく違う」の部分は実際その通りで、MetaCoq はゲーデルの不完全性定理を理由にCoq内でCoqを全て形式化するというアプローチはとっていないようです
Note that because of Gödel’s incompleteness theorem, there is no hope to prove completely the correctness of the specification of Coq inside Coq (in particular strong normalisation or canonicity),
そういえば System Fω で Self-Interpreter (∀A.Exp(A)→A) を実装できるという話があって、これもいかにも関連しそうな話題ですね(と思ったけど論文には不完全性定理への言及がなかった🤔)