previous up next
Go backward to 2.3.2 Atomic Formulas
Go up to 2.3 Predicate Logic
Go forward to 2.3.4 Quantified Formulas
RISC-Linz logo

2.3.3 Equality

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:
 Reflexivity (Reflexivität)

x = x;

 Symmetry (Symmetrie)

x = y => y = x;

 Transitivity (Transitivität)

(x = y /\  y = z) => x=z.

Furthermore, let f be a function constant and p be a predicate constant. Then we have:
 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

previous up next