6   Identity and existence

In the preceding chapters we have set up a theory of first order logic allowing us to reason with descriptions of domains of things, given a vocabulary for representing relationships between them and expressions for quantifying over them. The logical system has been developed both syntactically as a calculus of natural deduction and semantically in terms of interpretations, with semantic tableaux and the sequent calculus to facilitate semantic reasoning.

All of that is fine and good, but to express much of what we would like to say, we need to extend the language by adding a notation for equations. This is familiar from Logic for Fun, where the very first thing we express is that x+2 = 4: equations are everywhere in practically useful applications of logic. In this chapter, we consider adding the obvious notation for identity, and go on to examine some related issues concerning existence, and especially how it is possible to reason about non-existent things.