#### 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 |