Theory ScottVariant

subsection‹Ultrafilter Analysis of Scott's Variant (Fig.~3 in \<^cite>‹"C85"›))›

theory ScottVariant imports 
  HOML 
  MFilter 
  BaseDefs
begin  
text‹Axioms of Scott's variant.›
axiomatization where 
  A1: "⌊❙∀X.((❙¬(𝒫 X)) ❙↔ (𝒫(❙⇁X)))⌋" and
  A2: "⌊❙∀X Y.(((𝒫 X) ❙∧ (X⇛Y)) ❙→ (𝒫 Y))⌋" and
  A3: "⌊❙∀𝒵.((𝒫𝗈𝗌 𝒵) ❙→ (❙∀X.((X⨅𝒵) ❙→ (𝒫 X))))⌋" and
  A4: "⌊❙∀X.((𝒫 X) ❙→ ❙□(𝒫 X))⌋" and
  A5: "⌊𝒫 𝒩ℰ⌋" and
  B:  "⌊❙∀φ.(φ ❙→ ❙□❙◇φ)⌋" ―‹Logic KB›

lemma B': "∀x y. ¬(x❙ry) ∨ (y❙rx)" using B by fastforce

text‹Necessary existence of a Godlike entity.›
theorem T6: "⌊❙□(❙∃⇧E 𝒢)⌋" 
proof -
  have T1: "⌊❙∀X.((𝒫 X) ❙→ ❙◇(❙∃⇧E X))⌋" using A1 A2 by blast
  have T2: "⌊𝒫 𝒢⌋" by (metis A3 G_def)
  have T3: "⌊❙◇(❙∃⇧E 𝒢)⌋" using T1 T2 by simp
  have T4: "⌊❙∀⇧Ex.((𝒢 x)❙→(ℰ 𝒢 x))⌋" unfolding G_def E_def using A1 A4 by metis
  have T5: "⌊(❙◇(❙∃⇧E𝒢))❙→ ❙□(❙∃⇧E𝒢)⌋" by (smt (z3) A5 G_def B' NE_def T4)
  thus ?thesis using T3 by blast qed

text‹Existence of a Godlike entity.›
lemma "⌊❙∃⇧E 𝒢⌋" using A1 A2 B' T6 by blast

text‹Consistency› 
lemma True nitpick[satisfy] oops ―‹Model found.›

text‹Modal collapse: holds.›
lemma MC: "⌊❙∀Φ.(Φ ❙→ ❙□Φ)⌋" 
proof - {
    fix w fix Q
    have 1: "∀x.((𝒢 x w) ⟶ (❙∀Z.((Z x) ❙→ ❙□(❙∀⇧Ez.((𝒢 z) ❙→ (Z z))))) w)" 
      by (metis A1 A4 G_def)
    have 2: "(∃x. 𝒢 x w)⟶((Q ❙→ ❙□(❙∀⇧Ez.((𝒢 z) ❙→ Q))) w)" 
      using 1 by force
    have 3: "(Q ❙→ ❙□Q) w" using B' T6 2 by blast} 
  thus ?thesis by auto qed

text‹Analysis of positive properties using ultrafilters.›
theorem U1: "⌊UFilter 𝒫⌋"  ―‹Proof found by sledgehammer›
proof - 
  have 1: "⌊(❙U❙∈𝒫) ❙∧ ❙¬(❙∅❙∈𝒫)⌋"  using A1 A2 by blast
  have 2: "⌊❙∀φ ψ.(((φ❙∈𝒫)❙∧(φ❙⊆ψ))❙→(ψ❙∈𝒫))⌋"  by (smt (z3) A2 B' MC)
  have 3: "⌊❙∀φ ψ.(((φ❙∈𝒫)❙∧(ψ❙∈𝒫))❙→((φ❙⊓ψ)❙∈𝒫))⌋" by (metis A1 A2 G_def B' T6)
  have 4: "⌊❙∀φ.((φ❙∈𝒫) ❙∨ ((¯φ)❙∈𝒫))⌋"  using A1 by blast
  thus ?thesis using 1 2 3 4 by simp qed

lemma L1: "⌊❙∀X Y.((X⇛Y) ❙→ (X❙⊑Y))⌋" by (metis A1 A2 MC)
lemma L2: "⌊❙∀X Y.(((𝒫 X) ❙∧ (X❙⊑Y)) ❙→ (𝒫 Y))⌋" by (smt (z3) A2 B' MC)

text‹Set of supersets of X, we call this HF X.›
abbreviation HF where "HF X ≡ λY.(X❙⊑Y)"

text‹‹HF 𝒢› is a filter; hence, ‹HF 𝒢› is Hauptfilter of ‹𝒢›.› 
lemma F1: "⌊Filter (HF 𝒢)⌋" by (metis A2 B' T6 U1)
lemma F2: "⌊UFilter (HF 𝒢)⌋" by (smt (z3) A1 F1 G_def)

text‹T6 follows directly from F1.› 
theorem T6again: "⌊❙□(❙∃⇧E 𝒢)⌋" using F1 by simp 
end