Theory UFilterVariant

subsection‹Ultrafilter Variant (Fig.~5 in \<^cite>‹"C85"›)›

theory UFilterVariant imports 
  HOML 
  MFilter 
  BaseDefs
begin
text‹Axiom's of ultrafilter variant.› 
axiomatization where 
  U1: "⌊UFilter 𝒫⌋" and
  A2: "⌊❙∀X Y.(((𝒫 X) ❙∧ (X⇛Y)) ❙→ (𝒫 Y))⌋" and
  A3: "⌊❙∀𝒵.((𝒫𝗈𝗌 𝒵) ❙→ (❙∀X.((X⨅𝒵) ❙→ (𝒫 X))))⌋" 

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

text‹Checking for consistency.›  
lemma True nitpick[satisfy] oops  ―‹Model found›

text‹Checking for modal collapse.›
lemma MC: "⌊❙∀Φ.(Φ ❙→ ❙□Φ)⌋" nitpick oops ―‹Countermodel›
end



(*
 definition ess ("ℰ") where "ℰ Y x ≡ Y x ❙∧ (❙∀Z.(Z x ❙→ (Y⇛Z)))" 
 definition NE ("NE") where "NE x ≡ λw.((❙∀Y.(ℰ Y x ❙→ ❙□❙∃⇧E Y)) w)"
 consts Godlike::γ UltraFilter::"(γ⇒σ)⇒σ" NeEx::γ
 axiomatization where 
  1: "Godlike = G" and 
  2: "UltraFilter = Ultrafilter" and
  3: "NeEx = NE"
 lemma True nitpick[satisfy] oops 
 lemma MC: "⌊❙∀Φ. Φ ❙→ ❙□Φ⌋" nitpick[format=8] oops (*Countermodel*)
 lemma A1: "⌊❙∀X. ❙¬(𝒫 X) ❙↔ 𝒫(❙⇁X)⌋" using U1 by fastforce
 lemma A4: "⌊(𝒫 X ❙→ ❙□(𝒫 X))⌋" nitpick [format=4] oops (*Countermodel*)
 lemma A5: "⌊𝒫 NE⌋" nitpick oops (*Countermodel*)
*)