ゲーデルの神の存在証明を証明する
準備
クリプキフレーム$ F = \langle W, R\rangleを可能世界$ Wとその二項関係$ Rで定義する。命題$ \phiは可能世界$ Wの部分集合として定義する
code:kripke
structure kripke_frame :=
(world : Type u)
(rel : world → world → Prop)
abbreviation kripke_frame.prop := set F.world
命題$ \phiがフレーム$ Fで妥当である⊧ φとは任意の$ w \in Wで$ w \in \phiが真であることである
code:valid
def valid (φ : F.prop) : Prop := ∀ w, φ w
prefix ⊧ :30 := valid
各論理記号を適当に定義する
様相論理S5
証明は様相論理のS5で実行される。S5では以下のT, B, 4が成り立つ
T: $ \Box \phi \to \phi
$ Rは反射的
B: $ \phi \to \Box \Diamond \phi
$ Rは対称的
4: $ \Box \phi \to \Box \Box \phi
$ Rは推移的
とくに$ \Diamond \Box \phi \to \Box \phiが成り立つ
code:dia_box_implies_box
theorem dia_box_implies_box S5 F : ⊧ ◇□φ ⟶ □φ := λ w ⟨v, hv, h⟩ u hu, by { have : F.rel v u, from Four.transitive (B.symmetry hv) hu,
refine h u this }
証明
公理1: 任意の性質は肯定的(positive)かその否定が肯定的かのいずれかである
$ \forall \phi. P(\neg \phi) \leftrightarrow \neg P(\phi)
肯定的$ P, positiveとはなんらかの$ \alphaについての性質$ \varphiに関する述語
code:axiom1
axiom axiom1 : ⊧ positive (λ x, ¬ₘφ x) ⟷ ¬ₘpositive φ
公理2: φが肯定的なとき、必然的にφから導かれる性質は肯定的性質である
$ \forall \phi. \forall \psi. P(\phi) \to \Box \forall x. [\phi (x) \to \psi (x)] \to P(\psi)
code:axiom2
axiom axiom2 (φ ψ : α → F.prop) : ⊧ positive φ ⟶ (□ ∀ₘ x, φ x ⟶ ψ x) ⟶ positive ψ
定理1: 肯定的な性質は満たされうる
$ \forall \phi. P(\phi) \to \Diamond \exists x. \phi x
常に偽であるような性質が肯定的でないことを証明する。そのために$ P(\lambda x, \bot_m)に関する排中律を用いる
code:false_negatiive
lemma false_negative : ⊧ ¬ₘpositive (λ x : α, (⊥ₘ : F.prop)) := λ w,
begin
have : positive (λ x : α, ⊥ₘ) w ∨ (¬ₘpositive (λ x : α, ⊥ₘ)) w, from em w,
rcases this,
{ exfalso,
have h₁ : ¬positive (λ x : α, ⊤ₘ) w,
from ((axiom1 (λ x : α, (⊤ₘ : F.prop))) w).1 (by simpamnot, mverum using this ), have h₂ : positive (λ x : α, ⊤ₘ) w,
from axiom2 (λ x : α, (⊥ₘ : F.prop)) (λ x, ⊤ₘ) w this (λ v hv x, by simpmverum, (⟶)), exact h₁ h₂ },
{ exact this }
end
この結果と$ \lambda x, \bot_mを公理2のψに代入したものから定理1を得る
code:theorem1
theorem theorem1 : ⊧ positive φ ⟶ ◇∃ₘ x, φ x := λ w h,
begin
have : (¬ₘpositive (λ x : α, ⊥ₘ) ⟶ ¬ₘ(□∀ₘ x, φ x ⟶ ⊥ₘ)) w,
from mt (axiom2 φ (λ x : α, (⊥ₘ : F.prop)) w h),
have : (◇∃ₘ x, ¬ₘ(φ x ⟶ ⊥ₘ)) w,
end
定義1: 神的(God-Like)であるとはあらゆる肯定的な性質を持つことである
$ G(x) \leftrightarrow \forall \phi. [P(\phi) \to \phi(x)]
code:godlike
def godlike : α → F.prop := λ x, ∀ₘ φ, positive φ ⟶ φ x
公理3: 神性は肯定的である
$ P(G)
code:axiom3
axiom axiom3 : ⊧ positive godlike
定理2: 神的なものは存在しうる
$ \Diamond \exists x. G(x)
定理1と公理3からあきらか
code:theorem2
theorem theorem2 : ⊧ ◇∃ₘ x : α, godlike x
定義2: $ xが$ φを満たし、$ xについて成り立つあらゆる性質が$ φから必然的に導かれるものに限るとき、$ xは$ φの本質(essence)であるという
$ \phi \text{ ess } x \leftrightarrow \phi(x) \wedge \forall \psi. [\psi(x) \to \Box \forall y. [\phi(y) \to \psi(y)]]
code:essence
def essence (φ : α → F.prop) (x : α) : F.prop :=
φ x ∧ₘ ∀ₘ ψ, ψ x ⟶ □∀ₘ y, φ y ⟶ ψ y
infix ess :80 := essence
公理4: 肯定的な性質は必然的に肯定的である
$ \forall \phi. P(\phi) \to \Box P(\phi)
code:axiom4
axiom axiom4 : ⊧ positive φ ⟶ □positive φ
定理3: 神的なものは神性の本質である
$ \forall x. G(x) \to G \text{ ess } x
ある$ w \in Wで神的な$ xの持つ性質$ \psiは肯定的であることを証明する
肯定的でないならば公理1から$ \neg\psiは肯定的
神的な$ xはあらゆる肯定的な性質を持つから性質$ \neg \psiを持つ
矛盾
公理4より$ wRvなる$ vでも$ \psiは肯定的
よって任意の$ v \in W,$ wRvで任意の神的な$ yは性質$ \psiを持つ
$ xは$ Gの本質である
code: theorem3
theorem theorem3 : ⊧ ∀ₘ x, godlike x ⟶ godlike ess x := λ w x hg,
begin
refine ⟨hg, λ ψ hψ v hv y hy, _⟩,
have : positive ψ w,
{ by_contradiction A,
have : (positive (λ x, ¬ₘψ x)) w, from (axiom1 ψ w).mpr A,
have : ¬ψ x w, from hg (λ x, ¬ₘψ x) this,
contradiction },
have : positive ψ v, from axiom4 ψ w this v hv,
exact hy ψ this
end
定義3: $ xが本質であるあらゆる性質が、それを満たすものが必然的に存在する時、$ xは必然的存在(Necessary existence)である
$ \text{NE}(x) \leftrightarrow \forall \phi. [\phi \text{ ess } x \to \Box \exists y. \phi(y)]
code:NE
def necessary_existence (x : α) : F.prop := ∀ₘ φ, φ ess x ⟶ □∃ₘ y, φ y
公理5: 本質的存在性は肯定的である
code:axiom5
axiom axiom5 : ⊧ positive (necessary_existence : α → F.prop)
定理4: 神的なものは必然的に存在する
$ \Box \exists x.G(x)
$ \Diamond \Box \exists x. G(x)を証明する
任意の$ w \in Wを固定する
定理2から$ \Diamond \exists x. G(x)。$ wRvなる$ v, $ xが存在して$ vで$ xは神性$ Gをもつ
公理5より$ \text{NE}は肯定的。神的なものは汎ゆる肯定的な性質をもつので$ xは必然的存在
定理3より$ xは神性の本質なので、$ \text{NE}の定義より$ vで$ \Box \exists y.G(y)が成り立つ
S5の性質$ \Diamond \Box \phi \to \Box\phiより$ \Box \exists x.G(x)
S5の性質はここでしか使われない
code:god
theorem theorem4 : ⊧ □∃ₘ x, godlike x :=
begin
have : ⊧ ◇□∃ₘ x : α, (godlike x : F.prop),
{ intros w,
have : (◇∃ₘ x, godlike x) w, from (theorem2 : ⊧ ◇∃ₘ x : α, (godlike x : F.prop)) w,
rcases this with ⟨v, hv, x, gv⟩,
have nv : necessary_existence x v, from gv (necessary_existence : α → F.prop) (axiom5 v),
have : (□∃ₘ y, godlike y) v, from nv godlike (theorem3 v x gv),
refine ⟨v, hv, this⟩ },
exact λ w, dia_box_implies_box w (this w)
end
Modal collapse
$ \phi \leftrightarrow \Box \phi
$ \Longrightarrow
任意の$ w \in Wを固定する。$ w \models \phiを仮定する
$ w \models \Box \forall y.[G(y) \to \phi] を示す。
Tより$ wRwなので定理4から$ xが存在して$ w \models G(x)
$ \phiを性質($ wで恒真の性質)だとみなすと$ w \models \phi(x)
定理3より$ w \models G \text{ ess } x だから$ \text{ ess } の定義より$ w \models \Box \forall y.[G(y) \to \phi(x)]
定理4から$ xが存在して$ w \models \Box G(x)
よって$ w \models \Box \phi
$ \Longleftarrow
Tより明らか
code:modal_collapse
theorem modal_collapse {φ : F.prop} : ⊧ φ ⟷ □φ := λ w,
⟨λ hw v rv,
begin
have : (□∀ₘ y : α, godlike y ⟶ φ) w,
{ have : ∃ x : α, godlike x w, from theorem4 w w (T.reflexivity w),
rcases this with ⟨x, gw⟩,
have : (φ ⟶ □∀ₘ (y : α), godlike y ⟶ φ) w,
from (theorem3 w x gw).2 (λ _, φ),
exact this hw },
have : ∃ x : α, godlike x v, from theorem4 w v rv,
rcases this with ⟨x, gx⟩,
refine this v rv x gx
end, box_implies w⟩
参考