1.3.1 Equality Symbol

Adding an equality symbol to the syntax of FOL.

The first-order languages we have defined so far have an obvious expressive shortcoming: we have no way of asserting that two terms denote the same entity. Still, we may sometimes want to express such identities. So what are we to do?

Actually, the solution is perfectly straightforward. We can turn any language of first-order logic into a first-order language with equality by adding the special two place relation symbol . We use this relation symbol in the natural infix way: that is, if and are terms then we write rather than the unsightly .