*So far, equality has been treated as just another binary predicate that may be interpreted arbitrarily. However, the role of equality is so central that often we only want to consider interpretations where ‘equality means equality’. The previous logical theory and programmed proof procedures are easily modified for the new circumstances, but there are also more efficient and specialized ways of handling equality.*

4.1 Equality axioms

In many applications of logic, particularly to mathematical reasoning, equations play a central role. We’ve partly recognized this by supporting the usual infix notion ‘*s* = *t*’ instead of ‘= (*s, t*)’. Moreover, we can define various handy syntax operations for testing if a formula is an equation and ...

Start Free Trial

No credit card required