Theory ScottVariantHOMLposs

subsection‹ScottVariantHOMLposs.thy (Figure 19 of \cite{J75})›
text‹Scott's variant of Gödel's ontological proof is still valid when using possibilist quantifiers only.›
theory ScottVariantHOMLposs imports HOMLinHOL ModalFilter
begin 

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

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

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

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

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

axiomatization where A3: "⌊P G⌋" 

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

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

definition Ess ("_Ess._") where "φ Ess. x ≡ φ x ❙∧ (❙∀ψ. ψ x ❙⊃ ❙□(❙∀y::e. φ 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 ❙⊃ ❙□(❙∃x. φ x)"

axiomatization where A5: "⌊P NE⌋"

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

theorem T3: "⌊❙□(❙∃x. G x)⌋" 
  ―‹sledgehammer(A5 Coro God\_def NecExist\_def Rsymm T2)› ―‹Proof found›
  proof -
    have 1: "⌊(G x ❙⊃ NE x) ❙∧ (G Ess. x ❙⊃ ❙□(❙∃x. G x))⌋" using A5 Ess_def God_def NecExist_def by smt
    hence 2: "⌊(❙∃x. G x) ❙⊃ ❙□(❙∃x. G x)⌋" using A5 God_def NecExist_def T2 by smt
    hence 3: "⌊❙◇(❙∃x. G x) ❙⊃ (❙◇(❙□(❙∃x. G x)) ❙⊃ ❙□(❙∃x. 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 ❙⊃ ❙□(❙∀z.((G z) ❙⊃ (Z z)))) w)" using A1 A4 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 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 ❙⊃ ❙□(❙∀y. φ y ❙↔ ψ y)⌋" using Ess_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 Ess_def MC by auto
lemma Monotheism: "⌊G x ❙∧ G y ❙⊃ x ❙≡ y⌋" using A1 God_def by smt
lemma Filter: "⌊FilterP P⌋" using A1 God_def Rsymm T1 T3 by (smt (verit, best))
lemma UltraFilter: "⌊UFilterP P⌋" using Filter A1 by blast
lemma True nitpick[satisfy,card=1,eval="⌊P (λx.❙⊥)⌋"] oops ―‹One model found of cardinality one›

end