Theory SimpleVariantHF

subsection‹Hauptfiltervariant (Fig.~10 in \<^cite>‹"C85"›)›

theory SimpleVariantHF imports
  HOML 
  MFilter 
  BaseDefs
begin
text‹Definition: Set of supersets of ‹X›, we call this ‹ℋℱ X›.›
abbreviation HF::"γ⇒(γ⇒σ)"  where "HF X ≡ λY.(X❙⊑Y)"

text‹Postulate: ‹ℋℱ 𝒢› is a filter; i.e., Hauptfilter of ‹𝒢›.› 
axiomatization where F1: "⌊Filter (HF 𝒢)⌋" 

text‹Necessary existence of a Godlike entity.› 
theorem T6: "⌊❙□(❙∃⇧E 𝒢)⌋" using F1 by auto ―‹Proof found›

theorem T6again: "⌊❙□(❙∃⇧E 𝒢)⌋"  
proof -
 have T3': "⌊❙∃⇧E 𝒢⌋" using F1 by auto
 have T6:  "⌊❙□(❙∃⇧E 𝒢)⌋" using T3' by blast 
 thus ?thesis by simp qed

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

text‹Axiom T enforces possible existence of Godlike entity.›
axiomatization 
lemma T3: assumes T: "⌊❙∀φ.((❙□φ) ❙→ φ)⌋"
          shows "⌊❙◇(❙∃⇧E 𝒢)⌋" using F1 T by auto

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

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