カリーのパラドックス（英: Curry's paradox）は、素朴集合論や素朴論理学で見られるパラドックスであり、自己言及文といくつかの一見問題ない論理的推論規則から任意の文が派生されることを示す。名称の由来は論理学者のハスケル・カリーから。
カリーのパラドックス - Wikipedia
これをCoqで解きました。自信作です。
Lemma l1: forall (X Y:Prop), (X->X->Y) -> X=(X->Y) -> X. Proof. intros. rewrite H0. intro. apply H in H1. apply H1. apply H1. Qed. Theorem curry's_paradox: forall (X Y:Prop), X=(X->Y) -> Y. Proof. intros. assert(X->X). auto. pattern X at 2 in H0. rewrite H in H0. apply (l1 X Y) in H0. pose H0. rewrite H in x. apply x in H0. apply H0. apply H. Qed.
でも、解けて良いのかな……
Coq全体が矛盾しちゃうとか……
