Theory GoedelVariantHOML1AndersonQuant

section‹Further Appendices›
subsection‹GoedelVariantHOML1AndersonQuan.thy›
text‹The same as GoedelVariantHOML1, but now for a mixed use of actualist and possibilist quantifiers 
for entities; cf. Footnote 20 in \cite{J75}.›
theory GoedelVariantHOML1AndersonQuant 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 ψ ≡ ❙□(❙∀y::e. φ 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 (verit))
    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