Natural Deduction and Identity

Question

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.

Answer 1

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.

Answer 2

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.