Go backward to 2.3.2 Atomic FormulasGo up to 2.3 Predicate LogicGo forward to 2.3.4 Quantified Formulas |

*Reflexivity (Reflexivität)*`x`=`x`;*Symmetry (Symmetrie)*`x`=`y`=>`y`=`x`;*Transitivity (Transitivität)*(

`x`=`y`/\`y`=`z`) =>`x`=`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