Theory GoedelVariantHOML2poss

subsection‹GoedelVariantHOML2poss.thy (Figure 17 of \cite{J75})›
text‹After an appropriate modification of the definition of essence, the inconsistency revealed in
Figure 16 is avoided, and the argument can be successfully verified in modal logic S5 (indeed, as shown,
only the modal schema B is actually needed). In contrast to Figure 7 we here use only possibilist
quantifiers to obtain these results.›
theory GoedelVariantHOML2poss imports HOMLinHOL ModalFilter
begin 

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

axiomatization where Ax1: "⌊P φ ❙∧ P ψ ❙⊃ 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⌋"

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

theorem Th3: "⌊❙◇(❙∃x. G x) ❙⊃ ❙□(❙∃y. G y)⌋" 
  ―‹sledgehammer(Th2 Rsymm)› ―‹Proof found›
  proof -
    have 1: "⌊(❙∃x. G x) ❙⊃ ❙□(❙∃y. G y)⌋" using Th2 by blast
    have 2: "⌊❙◇(❙∃x. G x) ❙⊃ ❙◇❙□(❙∃y. G y)⌋" using 1 by blast
    have 3: "⌊❙◇(❙∃x. G x) ❙⊃ ❙□(❙∃y. G y)⌋" using 2 Rsymm by blast
    thus ?thesis by blast
  qed

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

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

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

lemma L: "⌊P G⌋" using Ax1Gen God_def by smt

theorem Th4: "⌊❙◇(❙∃x. G x)⌋" using Ax2a Ax4 L by blast

theorem Th5: "⌊❙□(❙∃x. G x)⌋" using Th3 Th4 by blast

lemma MC: "⌊φ ❙⊃ ❙□φ⌋" 
  ―‹sledgehammer(Ax2a Ax2b Th5 God\_def Rsymm)› ―‹Proof found›
  proof - {fix w fix Q
    have 1: "∀x.(G x w ⟶ (❙∀Z. Z x ❙⊃ ❙□(❙∀z. G z ❙⊃ Z z)) w)" using Ax2a Ax2b 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 Th5 Rsymm by blast} 
   thus ?thesis by auto 
 qed

lemma PosProps: "⌊P (λx.❙⊤) ❙∧ P (λx. x ❙= x)⌋" using Ax2a Ax4 by blast
lemma NegProps: "⌊❙¬P(λx.❙⊥) ❙∧ ❙¬P(λx. x ❙≠ x)⌋" using Ax2a Ax4 by blast
lemma UniqueEss1: "⌊φ Ess. x ❙∧ ψ Ess. x ❙⊃ ❙□(❙∀y. φ y ❙↔ ψ y)⌋" using Essence_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 Essence_def MC by auto
lemma Monotheism: "⌊G x ❙∧ G y ❙⊃ x ❙≡ y⌋" using Ax2a God_def by smt
lemma Filter: "⌊FilterP P⌋" using Ax1 Ax4 MC NegProps PosProps Rsymm by smt
lemma UltraFilter: "⌊UFilterP P⌋" using Ax2a Filter by smt 
lemma True nitpick[satisfy,card=1,eval="⌊P (λx.❙⊥)⌋"] oops ―‹One model found of cardinality one›

end