Theory GoedelVariantHOML3poss

subsection‹GoedelVariantHOML3poss.thy (Figure 18 of \cite{J75})›
text‹After an appropriate modification of the definition of necessary property implication, the
inconsistency shown in Figure 16 is avoided, and the argument can be successfully verified. As shown
here, this still holds when using possibilist quantifiers only.›
theory GoedelVariantHOML3poss 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 ψ ≡ ❙□(φ ❙≠ (λx. ❙⊥) ❙∧ (❙∀y::e. φ 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) ❙⊃ ❙□(❙∃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 (verit))

theorem Th4: "⌊❙◇(❙∃x. G x)⌋" 
  ―‹sledgehammer[timeout=200](Ax2a L Ax1Gen)› oops ―‹sorry› ―‹Proof found›

axiomatization where Th4: "⌊❙◇(❙∃x. G x)⌋"

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 L Th4 by smt
lemma NegProps: "⌊❙¬P(λx.❙⊥) ❙∧ ❙¬P(λx. x ❙≠ x)⌋" using Ax2a Ax4 L Th4 by smt
lemma UniqueEss1: "⌊φ Ess. x ❙∧ ψ Ess. x ❙⊃ ❙□(❙∀y. φ y ❙↔ ψ y)⌋" oops ―‹Unclear, open question› 
lemma UniqueEss2: "⌊φ Ess. x ❙∧ ψ Ess. x ❙⊃ ❙□(φ ❙≡ ψ)⌋" oops ―‹Unclear, open question› 
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