二重否定シフトと排中律との関係

$$\begin{array}{}\text{(A)}& \mathrm{\neg }\mathrm{\neg }(\mathrm{\forall }P.P\vee \mathrm{\neg }P)\end{array}$$

が成り立ち、任意の$Q$について

$$\begin{array}{}\text{(B)}& \mathrm{\forall }x.\mathrm{\neg }\mathrm{\neg }Q(x)\end{array}$$

が成り立つときに

$$\begin{array}{}\text{(C)}& \mathrm{\neg }\mathrm{\forall }x.Q(x)\end{array}$$

の成立を仮定して矛盾を導けばよい。

つまり、$(A),(B),(C)$の仮定の下で

$$\begin{array}{}\text{(D)}& \mathrm{\forall }P.P\vee \mathrm{\neg }P\end{array}$$

を仮定して

$$\begin{array}{}\text{(E)}& \mathrm{\forall }x.Q(x)\end{array}$$

が成り立つことを示せばよい。
※$(D)$の仮定の下で$(E)$が成り立つとき、これは$(C)$に矛盾する。したがって$\mathrm{\neg }(D)$であるが、これは$(A)$に矛盾する。

排中律と二重否定の除去規則は同値であるので、$(D)$により、

$$\begin{array}{}\text{(F)}& \mathrm{\forall }P.\mathrm{\neg }\mathrm{\neg }P⟹P\end{array}$$

が成り立つ。

最後に、$(B),(F)$の仮定の下で$(E)$が成り立つことを示す。

$(B)$により、すべての$x$に対して$\mathrm{\neg }\mathrm{\neg }Q(x)$が成り立つ。
このとき、$(F)$により$Q(x)$が成り立つ。つまり$(E)$が成り立つ。$◻$

任意の$\mathcal{F}$について

$$\begin{array}{}\text{(A)}& (\mathrm{\forall }P.\mathrm{\neg }\mathrm{\neg }\mathcal{F}(P))⟹\mathrm{\neg }\mathrm{\neg }\mathrm{\forall }P.\mathcal{F}(P)\end{array}$$

が成り立つときに

$$\begin{array}{}\text{(B)}& \mathrm{\neg }(\mathrm{\forall }P.P\vee \mathrm{\neg }P)\end{array}$$

の成立を仮定して矛盾を導けばよい。

ここで$\mathcal{F}$は任意なので

$$\mathcal{F}(P)=P\vee \mathrm{\neg }P$$

とすると、$(A)$は

$$(\mathrm{\forall }P.\mathrm{\neg }\mathrm{\neg }(P\vee \mathrm{\neg }P))⟹\mathrm{\neg }\mathrm{\neg }\mathrm{\forall }P.P\vee \mathrm{\neg }P$$

となる。
ここで、$\mathrm{\forall }P.\mathrm{\neg }\mathrm{\neg }(P\vee \mathrm{\neg }P)$は直観主義論理でも成り立つので、$\mathrm{\neg }\mathrm{\neg }\mathrm{\forall }P.P\vee \mathrm{\neg }P$も成り立つ。
しかし、これは$(B)$に矛盾する。$◻$