Theory GoedelVariantHOML1

section‹Gödel’s ontological argument -- 1970 manuscript›
subsection‹GoedelVariantHOML1.thy (Figure 6 of \cite{J75})›
text‹Gödel’s axioms and definitions, as presented in the 1970 manuscript, are inconsistent. Actualist 
quantifiers (avoiding existential import) are used for quantification over entities, otherwise possibilist quantifiers 
are used.›
theory GoedelVariantHOML1 imports HOMLinHOL
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 ❙⊃ (φ ❙⊃⇩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,expect=unknown] oops ―‹No model found›

lemma EmptyEssL: "⌊(λy.❙⊥) Ess. x⌋" using Essence_def by auto

theorem Inconsistency: False
   ―‹sledgehammer(Ax2a Ax3 Ax4 EmptyEssL NecExist\_def)› ―‹Proof found›
  proof -
    have 1: "⌊❙¬(P (λx.❙⊥))⌋" using Ax2a Ax4 by blast
    have 2: "⌊P (λx.(λy.❙⊥) Ess. x ❙⊃ ❙□(❙∃⇧Ez. (λy.❙⊥)z))⌋" using Ax3 Ax4 NecExist_def by smt
    have 3: "⌊P (λx.❙□(❙∃⇧Ez. (λx.❙⊥) z))⌋" using 2 EmptyEssL by simp 
    have 4: "⌊P (λx.❙□❙⊥)⌋" using 3 by auto
    have 5: "⌊P (λx.❙⊥)⌋" using 4 Ax2a Ax4 by smt
    have 6: "⌊❙⊥⌋" using 1 5 by blast
    thus ?thesis by blast
  qed

end