Theory GoedelVariantHOML3inS4

subsection‹GoedelVariantHOML3inS4.thy›
text‹The same as GoedelVariantHOML3, but now in logic S4, where the proof of theorem Th3 fails.›
theory GoedelVariantHOML3inS4 imports HOMLinHOLonlyS4 
begin 

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

axiomatization where Ax1: "⌊P φ ❙∧ P ψ ❙⊃ P (φ ❙. ψ)⌋"

abbreviation "PosProps Φ ≡ ❙∀φ. Φ φ ❙⊃ P φ"
abbreviation "ConjOfPropsFrom φ Φ ≡ ❙□(❙∀⇧Ez. φ z ❙↔ (❙∀ψ. Φ ψ ❙⊃ ψ z))"
axiomatization where Ax1Gen: "⌊(PosProps Φ ❙∧ ConjOfPropsFrom φ Φ) ❙⊃ P φ⌋" 

axiomatization where Ax2a: "⌊P φ ❙∨⇧e P ❙~φ⌋"

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

abbreviation PropertyInclusion ("_❙⊃⇩N_") where "φ ❙⊃⇩N ψ ≡ ❙□(φ ❙≠ (λx. ❙⊥) ❙∧ (❙∀⇧Ey. φ 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

axiomatization where Ax4: "⌊P φ ❙∧ (φ ❙⊃⇩N ψ) ❙⊃ P ψ⌋"

theorem Th3: "⌊❙◇(❙∃⇧Ex. G x) ❙⊃ ❙□(❙∃⇧Ey. G y)⌋" ―‹nitpick sledgehammer› oops ―‹Open problem›

end