Theory SimpleVariantSE

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

theory SimpleVariantSE 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‹Necessary existence of a Godlike entity.›  
theorem T6: "⌊❙□(❙∃⇧E 𝒢)⌋" using A1' A2'' T2 by blast 
theorem T7: "⌊❙∃⇧E 𝒢⌋" using A1' A2'' T2 by blast 

text‹Possible existence of a Godlike: has counterodel.›  
lemma T3: "⌊❙◇(❙∃⇧E 𝒢)⌋" nitpick oops ―‹Countermodel›

lemma T3': assumes T: "⌊❙∀φ.((❙□φ) ❙→ φ)⌋" 
  shows "⌊❙◇(❙∃⇧E 𝒢)⌋" 
  using A1' A2'' T2 T by metis
end