Theory SimpleVariantSEinT

subsection‹Simplified Variant with Simple Entailment in Logic T (Fig.~9 in \<^cite>‹"C85"›)›

theory SimpleVariantSEinT imports 
  HOML 
  MFilter 
  BaseDefs
begin
text‹Axiom's of new variant based on ultrafilters.› 
axiomatization where 
  A1': "⌊❙¬(𝒫(λx.(x❙≠x)))⌋" and
  A2'': "⌊❙∀X Y.(((𝒫 X) ❙∧ (X❙⊑Y)) ❙→ (𝒫 Y))⌋" and
  T2:   "⌊𝒫 𝒢⌋" 

text‹Modal Logic T.› 
axiomatization where T: "⌊❙∀φ.((❙□φ) ❙→ φ)⌋" 
lemma T': "⌊❙∀φ.(φ ❙→ (❙◇φ))⌋" by (metis T)

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'' T') 
  have T3: "⌊❙◇(❙∃⇧E 𝒢)⌋" by (metis T1 T2)
  have T5: "⌊(❙◇(❙∃⇧E 𝒢)) ❙→ ❙□(❙∃⇧E 𝒢)⌋" by (metis A1' A2'' T2) 
  thus ?thesis using T3 by simp qed

text‹T6 again, with an alternative, simpler proof.›
theorem T6again: "⌊❙□(❙∃⇧E 𝒢)⌋"  
proof -
  have L1: "⌊(❙∃X.((𝒫 X)❙∧❙¬(❙∃⇧EX)))❙→(𝒫(λx.(x❙≠x)))⌋" 
    by (smt (z3) A2'') 
  have L2: "⌊❙¬(❙∃X.((𝒫 X) ❙∧ ❙¬(❙∃⇧E X)))⌋" by (metis L1 A1')
  have T1': "⌊❙∀X.((𝒫 X) ❙→ (❙∃⇧E X))⌋" by (metis L2)  
  have T3': "⌊❙∃⇧E 𝒢⌋" by (metis T1' T2)
  have L3: "⌊❙◇(❙∃⇧E 𝒢)⌋" by (metis T3' T') ―‹not needed›
  thus ?thesis using T3' by simp qed
end