subsection‹ThereIsNoEvil2.thy (Figure 11 of \cite{J75})› text‹Importing Gödel’s modified axioms from Figure 8 we can prove that necessarily there exists no entity that possesses all non-positive (=negative) properties.› theory ThereIsNoEvil2 imports GoedelVariantHOML3 begin definition Evil ("Evil") where "Evil x ≡ ❙∀φ. ❙¬ P φ ❙⊃ φ x" theorem NecNoEvil: "⌊❙□(❙¬(❙∃⇧Ex. Evil x))⌋" ―‹sledgehammer(Ax1Gen Ax2a Evil\_def)› oops ―‹Proof found› end