Supplement to Actualism

Proof of NE in SQML

Theorem (NE):x□∃y(y=x)

Proof:

(1) x = x identity axiom
(2) y(yx) → xx quantifier axiom
(3) x = x → ¬∀y(yx) from (2), by propositional logic
(4) x = x → ∃y(y = x) from (3), by definition of ∃ and propositional logic
(5) y(y = x) from (1) and (4), by MP
(6) □∃y(y = x) from (5), by RN
(7) x□∃y(y = x) from (6), by GEN

Copyright © 2008 by
Christopher Menzel <cmenzel@tamu.edu>

Open access to the SEP is made possible by a world-wide funding initiative.
Please Read How You Can Help Keep the Encyclopedia Free