Supplement to Actualism
Proof of NE in SQML
Theorem (NE): ∀x□∃y(y=x)
Proof:
| (1) | x = x | identity axiom |
| (2) | ∀y(y ≠ x) → x ≠ x | quantifier axiom |
| (3) | x = x → ¬∀y(y ≠ x) | 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 |