Theory ScottVariantHOML

section‹Scott’s variant›
subsection‹ScottVariantHOML.thy (Figure 12 of \cite{J75})›
text‹Verification of Scott’s variant of Gödel’s ontological argument. Actualist 
quantifiers (avoiding existential import) are used for quantification over entities, otherwise possibilist quantifiers 
are used.›
theory ScottVariantHOML imports HOMLinHOL ModalFilter
begin 

consts PositiveProperty::"(e⇒σ)⇒σ" ("P") 

axiomatization where A1: "⌊❙¬P φ ❙↔ P ❙~φ⌋" 

axiomatization where A2: "⌊P φ ❙∧ ❙□(❙∀⇧Ey. φ y ❙⊃ ψ y) ❙⊃ P ψ⌋" 

theorem T1: "⌊P φ ❙⊃ ❙◇(❙∃⇧Ex. φ x)⌋" using A1 A2 by blast

definition God ("G") where "G x ≡ ❙∀φ. P φ ❙⊃ φ x"

axiomatization where A3: "⌊P G⌋" 

theorem Coro: "⌊❙◇(❙∃⇧Ex. G x)⌋" using A3 T1 by blast

axiomatization where A4: "⌊P φ ❙⊃ ❙□ P φ⌋" 

definition Ess ("_Ess._") where "φ Ess. x ≡ φ x ❙∧ (❙∀ψ. ψ x ❙⊃ ❙□(❙∀⇧Ey. φ y ❙⊃ ψ y))"

theorem T2: "⌊G x ❙⊃ G Ess. x⌋" using A1 A4 Ess_def God_def by fastforce

definition NecExist ("NE") where "NE x ≡ ❙∀φ. φ Ess. x ❙⊃ ❙□(❙∃⇧Ex. φ x)"

axiomatization where A5: "⌊P NE⌋"

lemma True nitpick[satisfy,card=1,eval="⌊P (λx.❙⊤)⌋"] oops ―‹One model found of cardinality one›

theorem T3: "⌊❙□(❙∃⇧Ex. G x)⌋" 
  ―‹sledgehammer(A5 Coro God\_def NecExist\_def Rsymm T2)› ―‹Proof found›
  proof -
    have 1: "⌊(G x ❙⊃ NE x) ❙∧ (G Ess. x ❙⊃ ❙□(❙∃⇧Ex. G x))⌋" using A5 Ess_def God_def NecExist_def by smt
    hence 2: "⌊(❙∃⇧Ex. G x) ❙⊃ ❙□(❙∃⇧Ex. G x)⌋" using A5 God_def NecExist_def T2 by smt
    hence 3: "⌊❙◇(❙∃⇧Ex. G x) ❙⊃ (❙◇(❙□(❙∃⇧Ex. G x)) ❙⊃ ❙□(❙∃⇧Ex. G x))⌋" using Rsymm by blast
    thus ?thesis using 2 Coro by blast
  qed

lemma MC: "⌊φ ❙⊃ ❙□φ⌋" 
  ―‹sledgehammer(A1 A4 God\_def Rsymm T3)› ―‹Proof found› 
  proof - {fix w fix Q
      have 1: "∀x.(G x w ⟶ (❙∀Z. Z x ❙⊃ ❙□(❙∀⇧Ez.((G z) ❙⊃ (Z z)))) w)" using A1 A4 God_def by smt
      have 2: "(∃x. G x w)⟶((Q ❙⊃ ❙□(❙∀⇧Ez.((G z) ❙⊃ Q))) w)" using 1 by force
      have 3: "(Q ❙⊃ ❙□Q) w" using 2 T3 Rsymm by blast} 
    thus ?thesis by auto 
  qed

lemma PosProps: "⌊P (λx.❙⊤) ❙∧ P (λx. x ❙= x)⌋" using A1 A2 by blast
lemma NegProps: "⌊❙¬P(λx.❙⊥) ❙∧ ❙¬P(λx. x ❙≠ x)⌋" using A1 A2 by blast
lemma UniqueEss1: "⌊φ Ess. x ❙∧ ψ Ess. x ❙⊃ ❙□(❙∀⇧Ey. φ y ❙↔ ψ y)⌋" using Ess_def by smt
lemma UniqueEss2: "⌊φ Ess. x ❙∧ ψ Ess. x ❙⊃ ❙□(φ ❙≡ ψ)⌋" nitpick[card i=1] oops ―‹Countermodel found›
lemma UniqueEss3: "⌊φ Ess. x ❙⊃ ❙□(❙∀⇧Ey. φ y ❙⊃ y ❙≡ x)⌋" using Ess_def MC by auto 
lemma Monotheism: "⌊G x ❙∧ G y ❙⊃ x ❙≡ y⌋" using A1 God_def by smt
lemma Filter: "⌊Filter P⌋" using A1 God_def Rsymm T1 T3 by (smt (verit, best))
lemma UltraFilter: "⌊UFilter P⌋" using Filter A1 by blast
lemma True nitpick[satisfy,card=1,eval="⌊P (λx.❙⊥)⌋"] oops ―‹One model found of cardinality one›

end