Coqでカリーのパラドックス

カリーのパラドックス(英: Curry's paradox)は、素朴集合論や素朴論理学で見られるパラドックスであり、自己言及文といくつかの一見問題ない論理的推論規則から任意の文が派生されることを示す。名称の由来は論理学者のハスケル・カリーから。 カリーのパラドックス - Wikipedia これをCoqで解きました。自信作です。 Le…