Theory EvilDerivable

subsection‹EvilDerivable.thy (Figure 20 of \cite{J75})›
text‹The necessary existence of an Evil-like entity proved from (controversially) modified assumptions.
By rejecting Gödel’s assumptions and instead postulating corresponding negative versions of them, 
as shown in the Figure 20, the necessary existence of Evil becomes derivable. 
The non-positive properties of this Evil-like entity are however identical to the positive 
properties of Gödel’s God-like entity.›
theory EvilDerivable imports HOMLinHOL ModalFilter
begin 

consts PositiveProperty::"(e⇒σ)⇒σ" ("P") 

definition Evil ("Evil") where "Evil x ≡ ❙∀φ. ❙¬ P φ ❙⊃ φ x"

definition Essence ("_Ess._") where "φ Ess. x ≡ φ x ❙∧ (❙∀ψ. ψ x ❙⊃ ❙□(❙∀⇧Ey. φ y ❙⊃ ψ y))"

definition NecExist ("E") where "E x ≡ ❙∀φ. φ Ess. x ❙⊃ ❙□(❙∃⇧Ex. φ x)"

axiomatization where A1: "⌊❙¬P φ ❙↔ P ❙~φ⌋"

axiomatization where A2: "⌊❙¬P φ ❙∧ ❙□(❙∀⇧Ey. φ y ❙⊃ ψ y) ❙⊃ ❙¬P ψ⌋"

axiomatization where A4: "⌊❙¬P Evil⌋"

axiomatization where A3: "⌊❙¬P φ ❙⊃ ❙□ (❙¬P φ)⌋"

axiomatization where A5: "⌊❙¬P E⌋"

lemma True nitpick[satisfy,card i=1,eval="⌊P (λx.❙⊥)⌋",eval="⌊P (λx.❙⊤)⌋"] oops ―‹Model found›

theorem T1: "⌊❙¬P φ ❙⊃ ❙◇(❙∃⇧Ex. φ x)⌋" using A1 A2 by blast

theorem T2: "⌊❙◇(❙∃⇧Ex. Evil x)⌋" using A4 T1 by blast

theorem T3: "⌊Evil x ❙⊃ Evil Ess. x⌋" using A1 A3 Essence_def Evil_def by (smt (verit, best))

theorem T4: "⌊❙◇(❙∃⇧Ex. Evil x) ❙⊃ ❙□(❙∃⇧Ey. Evil y)⌋" using A5 Evil_def NecExist_def Rsymm T3 by smt

theorem T5: "⌊❙□(❙∃⇧Ex. Evil x)⌋" using T2 T4 by presburger

lemma MC: "⌊φ ❙⊃ ❙□φ⌋" 
  ―‹sledgehammer(A1 A3 T5 Evil\_def Rsymm)› oops ―‹proof found›

lemma PosProps: "⌊P (λx.❙⊥) ❙∧ P (λx. x ❙≠ x)⌋" using A1 A2 by blast
lemma NegProps: "⌊❙¬P(λx.❙⊤) ❙∧ ❙¬P(λx. x ❙= x)⌋" using A1 A2 by blast
lemma UniqueEss1: "⌊φ Ess. x ❙∧ ψ Ess. x ❙⊃ ❙□(❙∀⇧Ey. φ y ❙↔ ψ y)⌋" using Essence_def by smt
lemma UniqueEss2: "⌊φ Ess. x ❙∧ ψ Ess. x ❙⊃ ❙□(φ ❙= ψ)⌋" nitpick[card i=2] oops ―‹Countermodel found›
lemma Monoevilism: "⌊Evil x ❙∧ Evil y ❙⊃ x ❙≡ y⌋" using A1 Evil_def by smt
lemma Filter: "⌊Filter (λ φ. ❙¬P φ)⌋" using A1 Evil_def Rsymm T1 T5 by (smt (verit, best))
lemma UltraFilter: "⌊UFilter (λ φ. ❙¬P φ)⌋" using Filter A1 by blast

end