Theory ScottVariantHOMLpossInS4

subsection‹ScottVariantHOMLpossInS4.thy›
text‹›
theory ScottVariantHOMLpossInS4 imports HOMLinHOLonlyS4 
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)⌋" nitpick[card e=1, card i=2] oops ―‹Countermodel found›

lemma MC: "⌊φ ❙⊃ ❙□φ⌋" nitpick[card e=1, card i=2] oops ―‹Countermodel found›

end