Theory ScottVariantHOMLinS4

subsection‹ScottVariantHOMLinS4.thy›
text‹›
theory ScottVariantHOMLinS4 imports HOMLinHOLonlyS4
begin 

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

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

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

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

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

axiomatization where A3: "⌊P G⌋"

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

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

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

axiomatization where A5: "⌊P NE⌋"

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

theorem T3: "⌊❙□(❙∃⇧Ex. 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