Theory GoedelVariantHOML2AndersonQuant

subsection‹GoedelVariantHOML2AndersonQuan.thy›
text‹The same as GoedelVariantHOML2, but now for a mixed use of actualist and possibilist quantifiers 
for entities; cf. Footnote 20 in \cite{J75}.›
theory GoedelVariantHOML2AndersonQuant 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 ψ ≡ ❙□(❙∀y::e. φ 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 φ Φ ≡ ❙□(❙∀z. φ z ❙↔ (❙∀ψ. Φ ψ ❙⊃ ψ z))"
axiomatization where Ax1Gen: "⌊(PosProps Φ ❙∧ ConjOfPropsFrom φ Φ) ❙⊃ P φ⌋" 

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

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

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 ❙⊃ ❙□(❙∀z. G z ❙⊃ Z z)) w)" using Ax2a Ax2b God_def by smt
    have 2: "(∃x. G x w)⟶((Q ❙⊃ ❙□(❙∀z. 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 ❙⊃ ❙□(❙∀y. φ y ❙↔ ψ y)⌋" using Essence_def by smt
lemma UniqueEss2: "⌊φ Ess. x ❙∧ ψ Ess. x ❙⊃ ❙□(φ ❙≡ ψ)⌋" nitpick[card i=2] oops ―‹Countermodel found›
lemma UniqueEss3: "⌊φ Ess. x ❙⊃ ❙□(❙∀y. φ 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 Ax2a God_def Th5 by (smt (verit, ccfv_threshold))
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