Typically we operate in a version of predicate logic that provides a binary
predicate constant `=' with the following properties (independently of the
domain being considered).
Proposition 14 (Equality)
For all x, y, and z, the following holds:
Furthermore, let f be a function constant and p be a predicate
constant. Then we have:
- Reflexivity (Reflexivität)
x = x;
- Symmetry (Symmetrie)
x = y => y = x;
- Transitivity (Transitivität)
(x = y /\ y = z)
- Equality Axioms (Gleichheitsaxiome)
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.
Author: Wolfgang Schreiner
Last Modification: October 4, 1999