Theory ThereIsNoEvil1

subsection‹ThereIsNoEvil1.thy (Figure 10 of \cite{J75})›
text‹Importing Gödel's modified axioms from Figure 7 we can prove that necessarily there exists
no entity that possesses all non-positive (=negative) properties.›
theory ThereIsNoEvil1 imports GoedelVariantHOML2
begin  

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

theorem NecNoEvil: "⌊❙□(❙¬(❙∃⇧Ex.  Evil x))⌋" 
  ―‹sledgehammer(Ax2a Ax4 Evil\_def)›  ―‹Proof found›
  proof -
    have    "⌊❙¬P(λy.❙⊥)⌋"  using Ax2a Ax4 by blast
    hence  "⌊(❙∀⇧Ex.  Evil x ❙⊃ (λy.❙⊥) x)⌋" using Evil_def by auto
    hence  "⌊(❙∀⇧Ex.  Evil x ❙⊃ ❙⊥)⌋" by auto
    hence  "⌊(❙∃⇧Ex.  Evil x) ❙⊃ ❙⊥⌋" by auto
    hence  "⌊❙¬(❙∃⇧Ex. Evil x)⌋" by blast
    thus ?thesis by blast
  qed

end