Go backward to 2.3.2 Atomic Formulas Go up to 2.3 Predicate Logic Go forward to 2.3.4 Quantified Formulas |
x = x;
x = y => y = x;
(x = y /\ y = z) => x=z.
x = y => f(..., x, ...) = f(..., y, ...); x = y => p(..., x, ...) <=> p(..., y, ...).
If we know x=y, the equality axioms allow us to replace x by y in any phrase without changing the meaning of the phrase.