Hurkensのパラドックス
#Fleeting_Notes
Hurkensのパラドックス(Hurkens's paradox)
ジラールのパラドックス
を簡略化したもの？
[Hurkens95]
『Simpliication of Girard's paradox』
Coq
の証明
Standard Library | The Coq Proof Assistant
Coq.Logic.Hurkens
Coq.Logic.Hurkens コードリーディング
Agda
の証明:
Hurkens.agda
Haskell
の証明？:
Language.PTS.Examples.Hurkens
Leanの証明:
mathlib4/Counterexamples/Girard.lean at f3731eaabfa91f8610f09b48be38213d6c16d171 · leanprover-community/mathlib4
Hurkens' paradox | PLS Lab
確認用
Q. Hurkensのパラドックス
参考
『 Martin-Lofの 理論とそのパラドックス 』あいまいな本日の私 blog
調査用
Google.icon
Hurkensのパラドックス(日)
Google.icon
Hurkens's paradox(英)
Wikipedia.icon
Hurkensのパラドックス - Wikipedia(日)
Hurkensのパラドックス(検索) - Wikipedia(日)
Wikipedia.icon
Hurkens's paradox - Wikipedia(英)
Hurkens's paradox(検索) - Wikipedia(英)