# Natural Deduction and Identity

In Logic and Structure, p. 99, Van Dalen gives a brief summary of the rules for predicate logic involving identity. Now, I would like to think of myself as quite proficient in terms of constructing tree proofs, both in propositional logic and predicate logic as well. However, for some reason (most probably due to lack of exposure), I find the introduction of identity somewhat difficult to handle. For instance, consider the following problem (which is not in the book):

Derive in natural deduction, without any undischarged assumptions, the following formula: $$\exists x_{0} \forall x_{1} (x_{0} \dot{=}x_{1}) \to \forall x_{0} \forall x_{1} (x_{0} \dot{=}x_{1})$$

Now, if I would want to construct a proof tree of this, then I reckon by its form that the last rule should be $\to I$ and the rule above $\forall I$. However, once we reach this step I go completely blank. A part of me wants to use the $\exists E$, take $\exists x_{0} \forall x_{1} (x_{0}\dot{=}x_{1})$ as the main premise and derive $\forall x_{1}(x_{0} \dot{=} x_{1})$. But, another part simply says this reasoning would not be valid. Could anyone help me out, by explaining this example and/or provide more information about how one should approach derivations involving identity in general.

Let's think through a proof (I'll use $x$ and $y$ rather than $x_0$ and $x_1$ for ease of typing and readability)!

We need to prove a conditional proposition. So, as typical in an ND system, we assume the antecedent and aim to derive the consequent, then use CP (conditional proof) to discharge the antecedent and infer the desired conditional. What else could we do?? So the proof should have the shape:

$\quad\quad|\quad \exists x\forall y\, x = y\\ \quad\quad|\quad\ldots\\ \quad\quad|\quad\forall x\forall y\, x = y\\ \exists x\forall y\, x = y\ \to\ \forall x\forall y\, x = y\quad\quad\quad\text{By Conditional Proof}$

And now there's only one way to use an existential assumption $\exists x\varphi(x)$ if that's all we've got to work with ... We temporarily assume $\varphi(a)$ for some new name $a$, and derive some conclusion $C$ which doesn't involve $a$. Then we can use the original existential assumption and discharge the temporary assumption to derive $C$. So the proof has to go:

$\quad\quad|\quad \exists x\forall y\, x = y\\ \quad\quad|\quad\quad|\quad \forall y\, a = y\\ \quad\quad|\quad\quad|\quad\ldots\\ \quad\quad|\quad\quad|\quad\forall x\forall y\, x = y\\ \quad\quad|\quad\forall x\forall y\, x = y\quad\quad\quad\quad\quad\quad\text{By EE}\\ \exists x\forall y\, x = y\ \to\ \forall x\forall y\, x = y$

So far, so automatic, yes???

What now? We obviously have to use the universal. So let's instantiate with an new name: to get

$\quad\quad|\quad \exists x\forall y\, x = y\\ \quad\quad|\quad\quad|\quad \forall y\, a = y\\ \quad\quad|\quad\quad|\quad a = b\\ \quad\quad|\quad\quad|\quad\ldots\\ \quad\quad|\quad\quad|\quad\forall x\forall y\, x = y\\ \quad\quad|\quad\forall x\forall y\, x = y\\ \exists x\forall y\, x = y\ \to\ \forall x\forall y\, x = y$

But we can't get from that alone to the desired doubly quantified conclusion, because we can't generalize on $a$. [MAJOR REALITY CHECK: why can't we generalize on $a$?? If you don't understand that, you need to revise the ND rules for the quantifiers!!!] But we need two names we can generalize on get to the desired conclusion. Ok .... well, nothing stops us introducing another one using our temporary assumption at line 2: so we have

$\quad\quad|\quad \exists x\forall y\, x = y\\ \quad\quad|\quad\quad|\quad \forall y\, a = y\\ \quad\quad|\quad\quad|\quad a = b\\ \quad\quad|\quad\quad|\quad a = c\\ \quad\quad|\quad\quad|\quad\ldots\\ \quad\quad|\quad\quad|\quad\forall x\forall y\, x = y\\ \quad\quad|\quad\forall x\forall y\, x = y\\ \exists x\forall y\, x = y\ \to\ \forall x\forall y\, x = y$

Ah hah! Now if should be obvious how to proceed ....

$\quad\quad|\quad \exists x\forall y\, x = y\\ \quad\quad|\quad\quad|\quad \forall y\, a = y\\ \quad\quad|\quad\quad|\quad a = b\\ \quad\quad|\quad\quad|\quad a = c\\ \quad\quad|\quad\quad|\quad b = c \quad\quad\quad\quad\quad \text{By Leibniz's Law}\\ \quad\quad|\quad\quad|\quad \forall y\, b = y \quad\quad\quad\quad \text{By Univ. quantifier introduction}\\ \quad\quad|\quad\quad|\quad\forall x\forall y\, x = y\quad\quad\quad \text{By Univ. quantifier introduction again}\\ \quad\quad|\quad\forall x\forall y\, x = y\\ \exists x\forall y\, x = y\ \to\ \forall x\forall y\, x = y$

Just ensure you really understand the use of the quantifier rules here, and why the applications of the universal quantifier introduction moves are legitimate.

In my usual system of natural deduction, here is how I would prove this:

$$\begin{array}{lr} 1. & \exists (x) \forall (y) (x = y) & \text{Assumption} \\ 2. & \neg \forall(x) \forall(y)(x=y) & \text{Assumption} \\ 3. & \exists(x) \exists(y) \neg(x=y) & \text{Quantifier Negation 2} \\ 4. & \exists(y) \neg(a=y) & \text{Existential Instantiation 3} \\ 5. & \neg(a=b) & \text{Existential Instantiation 4} \\ 6. & \forall (y) (c = y) & \text{Existential Instantiation 1} \\ 7. & (c = a) & \text{Universal Instantiation 6} \\ 8. & (c = b) & \text{Universal Instantiation 6} \\ 9. & (a = b) & \text{Transitivity of Identity 7,8} \\ 10.& \forall(x) \forall(y)(x=y) & \text{Reductio 2, 5, 9} \\ 11.& \exists (x) \forall (y) (x = y) \rightarrow\forall(x) \forall(y)(x=y) & \text{Discharge 1, 10} \\ \end{array}$$

Proof by tableau would follow a similar scheme: start with premises 1 and 2, use 3 rounds of existential instantiation, 2 rounds of universal instantiation, and then the replacement for identity until you get a contradiction. Using reductio here gets around some tricky question about universal generalization. If you don't have a rule for the transitivity of identity, you could insert $c=c$ as a tautology and then replace.

• The notation $\exists(x)$ etc for the quantifiers is very non-standard. And in no system I know are you allowed to move a negation past two quantifiers at once as a basic rule. And in any case, there is no need to go round the houses like this .. Oct 10, 2013 at 12:30
• @PeterSmith I've seen $\forall x$, $(\forall x)$, and $\forall (x)$. I don't know your background, but mine is from philosophy. I have no idea what is standard in actual journals, etc. I did two steps at once to save time and space. I avoid introducing universals if I can, just so I know I didn't make a mistake. It doesn't seem roundabout to me. No more than introducing a new constant to quantify over. Oct 10, 2013 at 22:25
• I'd be interested to see a reference to a standard logic textbook that uses $\forall(x)$. None of the fifty or so I know does ... Oct 10, 2013 at 22:41
• @PeterSmith So would I at this point...... I spent a while looking through some on Amazon and trying to remember which ones I used, but it was years ago. Oct 11, 2013 at 0:04