Theory SimpleVariant

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

theory SimpleVariant imports 
  HOML 
  MFilter 
  BaseDefs
begin
text‹Axiom's of new, simplified variant.›
axiomatization where 
  A1': "⌊❙¬(𝒫(λx.(x❙≠x)))⌋" and 
  A2': "⌊❙∀X Y.(((𝒫 X) ❙∧ ((X❙⊑Y) ❙∨ (X⇛Y))) ❙→ (𝒫 Y))⌋" and
  A3:  "⌊❙∀𝒵.((𝒫𝗈𝗌 𝒵) ❙→ (❙∀X.((X⨅𝒵) ❙→ (𝒫 X))))⌋" 

lemma T2: "⌊𝒫 𝒢⌋" by (metis A3 G_def) ―‹From A3›
lemma L1: "⌊𝒫(λx.(x❙=x))⌋" by (metis A2' A3) 

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

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

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

text‹Gödel's A1, A4, A5: not implied anymore.›
lemma A1: "⌊❙∀X.((❙¬(𝒫 X))❙↔(𝒫(❙⇁X)))⌋" nitpick oops ―‹Countermodel›
lemma A4: "⌊❙∀X.((𝒫 X) ❙→ ❙□(𝒫 X))⌋" nitpick oops ―‹Countermodel›
lemma A5: "⌊𝒫 𝒩ℰ⌋" nitpick oops ―‹Countermodel›

text‹Checking filter and ultrafilter properties.› 
theorem F1: "⌊Filter 𝒫⌋" oops ―‹Proof found by sledgehammer, but reconstruction timeout›
theorem U1: "⌊UFilter 𝒫⌋" nitpick oops  ―‹Countermodel›
end