Theory GoedelVariantHOML2possInS4

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

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

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

abbreviation "PosProps Φ ≡ ❙∀φ. Φ φ ❙⊃ P φ"

abbreviation "ConjOfPropsFrom φ Φ ≡ ❙□(❙∀z. φ 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 ψ ≡ ❙□(❙∀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 ❙⊃ ❙□(❙∃x. φ x)"

axiomatization where Ax3: "⌊P E⌋"

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

theorem Th2: "⌊G x ❙⊃ ❙□(❙∃y. G y)⌋" using Ax3 Th1 God_def NecExist_def by smt

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

end