6 Identity and existence
In the preceeding 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 nonexistent 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.
 Identity Reasoning with equations
 Definite Descriptions The logic of the word 'the'
 Nonexistence An outline of free logic
 Restricted quantifiers revisited The rules ∀I_{R}, ∀E_{R}, ∃I_{R} and ∃E_{R}

( Manysorted logic work in progress: subject to revision without notice ) 
Examples Proofs with restricted quantifiers and in free logic