Theory GoedelVariantHOML2

subsection‹GoedelVariantHOML2.thy (Figure 7 of \cite{J75})›
text‹After an appropriate modification of the definition of essence in Gödel’s 1970 ontological proof,
the inconsistency revealed in Figure 6 is avoided, and the argument can be successfully verified in modal
logic S5 (indeed, as shown, only symmetry of the accessibility relation is actually needed). Actualist 
quantifiers (avoiding existential import) are used for quantification over entities, otherwise possibilist quantifiers 
are used.›
theory GoedelVariantHOML2 imports HOMLinHOL ModalFilter
begin 

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

axiomatization where Ax1: "⌊P φ ❙∧ P ψ ❙⊃ P (φ ❙. ψ)⌋"

axiomatization where Ax2a: "⌊P φ ❙∨⇧e P ❙~φ⌋" 

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

abbreviation PropertyInclusion ("_❙⊃⇩N_") where "φ ❙⊃⇩N ψ ≡ ❙□(❙∀⇧Ey. φ y ❙⊃ ψ y)" 

definition Essence ("_Ess._") where "φ Ess. x ≡ φ x ❙∧ (❙∀ψ. ψ x ❙⊃ (φ ❙⊃⇩N ψ))"

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

lemma Ax2b': "⌊❙¬P φ ❙⊃ ❙□(❙¬P φ)⌋" using Ax2a Ax2b by blast

theorem Th1: "⌊G x ❙⊃ G Ess. x⌋" using Ax2a Ax2b Essence_def God_def by (smt (verit))

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

axiomatization where Ax3: "⌊P E⌋"

theorem Th2: "⌊G x ❙⊃ ❙□(❙∃⇧Ey. G y)⌋" using Ax3 Th1 God_def NecExist_def by smt

theorem Th3: "⌊❙◇(❙∃⇧Ex. G x) ❙⊃ ❙□(❙∃⇧Ey. G y)⌋" 
  ―‹sledgehammer(Th2 Rsymm)› ―‹Proof found›
  proof -
    have 1: "⌊(❙∃⇧Ex. G x) ❙⊃ ❙□(❙∃⇧Ey. G y)⌋" using Th2 by blast
    have 2: "⌊❙◇(❙∃⇧Ex. G x) ❙⊃ ❙◇❙□(❙∃⇧Ey. G y)⌋" using 1 by blast
    have 3: "⌊❙◇(❙∃⇧Ex. G x) ❙⊃ ❙□(❙∃⇧Ey. G y)⌋" using 2 Rsymm by blast
    thus ?thesis by blast
  qed

axiomatization where Ax4: "⌊P φ ❙∧ (φ ❙⊃⇩N ψ) ❙⊃ P ψ⌋"

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

abbreviation "PosProps Φ ≡ ❙∀φ. Φ φ ❙⊃ P φ"
abbreviation "ConjOfPropsFrom φ Φ ≡ ❙□(❙∀⇧Ez. φ z ❙↔ (❙∀ψ. Φ ψ ❙⊃ ψ z))"
axiomatization where Ax1Gen: "⌊(PosProps Φ ❙∧ ConjOfPropsFrom φ Φ) ❙⊃ P φ⌋" 

lemma L: "⌊P G⌋" using Ax1Gen God_def by (smt (verit))

theorem Th4: "⌊❙◇(❙∃⇧Ex. G x)⌋" using Ax2a Ax4 L by blast

theorem Th5: "⌊❙□(❙∃⇧Ex. G x)⌋" using Th3 Th4 by blast

lemma MC: "⌊φ ❙⊃ ❙□φ⌋"
  ―‹sledgehammer(Ax2a Ax2b Th5 God\_def Rsymm)› ―‹Proof found›
  proof - 
    {fix w fix Q
      have 1: "∀x.(G x w ⟶ (❙∀Z. Z x ❙⊃ ❙□(❙∀⇧Ez. G z ❙⊃ Z z)) w)" using Ax2a Ax2b 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 Th5 Rsymm by blast} 
    thus ?thesis by auto 
  qed

lemma PosProps: "⌊P (λx.❙⊤) ❙∧ P (λx. x ❙= x)⌋" using Ax2a Ax4 by blast
lemma NegProps: "⌊❙¬P(λx.❙⊥) ❙∧ ❙¬P(λx. x ❙≠ x)⌋" using Ax2a Ax4 by blast
lemma UniqueEss1: "⌊φ Ess. x ❙∧ ψ Ess. x ❙⊃ ❙□(❙∀⇧Ey. φ y ❙↔ ψ y)⌋" using Essence_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 Essence_def MC by auto
lemma Monotheism: "⌊G x ❙∧ G y ❙⊃ x ❙≡ y⌋" using Ax2a God_def by smt
lemma Filter: "⌊Filter P⌋" using Ax1 Ax4 MC NegProps PosProps Rsymm by smt
lemma UltraFilter: "⌊UFilter P⌋" using Ax2a Filter by smt 
lemma True nitpick[satisfy,card=1,eval="⌊P (λx.❙⊥)⌋"] oops ―‹One model found of cardinality one›

end