Theory SimpleVariantPG

subsection‹Simplified Variant with Axiom T2 (Fig.~7 in \<^cite>‹"C85"›)›

theory SimpleVariantPG imports 
  HOML 
  MFilter 
  BaseDefs
begin
text‹Axiom's of simplified variant with A3 replaced.› 
axiomatization where 
  A1': "⌊❙¬(𝒫(λx.(x❙≠x)))⌋" and
  A2': "⌊❙∀X Y.(((𝒫 X) ❙∧ ((X❙⊑Y)❙∨(X⇛Y))) ❙→ (𝒫 Y))⌋" and
  T2:  "⌊𝒫 𝒢⌋"

text‹Necessary existence of a Godlike entity.› 
theorem T6:  "⌊❙□(❙∃⇧E 𝒢)⌋"  ―‹Proof found by sledgehammer›
proof -
  have T1: "⌊❙∀X.((𝒫 X) ❙→ ❙◇(❙∃⇧E X))⌋" by (metis A1' A2') 
  have T3: "⌊❙◇(❙∃⇧E 𝒢)⌋" using T1 T2 by simp
  have T5: "⌊(❙◇(❙∃⇧E 𝒢)) ❙→ ❙□(❙∃⇧E 𝒢)⌋" by (metis A1' A2' T2)
  thus ?thesis using T3 by blast qed

lemma True nitpick[satisfy] oops  ―‹Consistency: model found›

text‹Modal collapse and Monotheism: not implied.›
lemma MC: "⌊❙∀Φ.(Φ ❙→ ❙□Φ)⌋" nitpick oops  ―‹Countermodel›
lemma MT: "⌊❙∀x y.(((𝒢 x)❙∧(𝒢 y))❙→(x❙=y))⌋" nitpick oops  ―‹Countermodel›
end