矛盾を示すときに使える方法としては主に以下の2つだと思う 命題 ¬P に P をぶつける 矛盾 ⊥ の特徴付けを使う 矛盾の特徴付けというのは, 例えばAgdaだと⊥は空集合の公理を満たすことが示せるから, 空集合の公理がそのまま矛盾の特徴付けになる. ∃ \(A : Se…