# 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. We also tidy up some loose ends by extending the calculus a little to accommodate restricted (binary) quantifiers along with the unrestricted ones used so far.

• Reasoning with equations
• The logic of the word 'the'
• Another view of definite descriptions
• An outline of free logic
• The rules ALLIR, ALLER, SOMEIR and SOMEER
• work in progress: subject to revision without notice )
•
Proofs with restricted quantifiers and in free logic