2
$\begingroup$

I need to prove the following predicate logic sequent using natural deduction:

$\exists y \forall x (P(x) \rightarrow x = y) \vdash \forall x \forall y (P(x) \land P(y) \rightarrow x = y)$

This is my half-finished proof. I hope I'm on the right track but there is something about box packing/unpacking I don't understand yet:

  1. $\exists y \forall x (P(x) \rightarrow x = y) \quad\mathrm{Premise}$
  2. $y_0: \forall x P(x) \rightarrow x = y_0) \quad\mathrm{Assumption}$
  3. $x_0: P(x_0) \rightarrow x_0 = y_0 \quad \forall x e2$
  4. $P(x_0) \land P(y_0) \quad \mathrm{Assumption}$
  5. $P(x_0) \quad \land e_1 4$
  6. $x_0 = y_0 \quad \rightarrow e 3, 5$
  7. $P(x_0) \land P(y_0) \rightarrow x_0 = y_0 \quad \rightarrow i 4-6$
  8. $\forall x (P(x) \land P(y_0) \rightarrow x = y_0 \quad \forall x i 3-7$

Then I can't go further because I can't use universal reintroduction on the $y$ variable.

Edit: I managed to finish it with the help from the answer!

  1. $\exists y \forall x (P(x) \rightarrow x = y) \quad\mathrm{Premise}$
  2. $z: \forall x P(x) \rightarrow x = z) \quad\mathrm{Assumption}$
  3. $a: P(a) \rightarrow a = z \quad \forall x e2$
  4. $b: P(b) \rightarrow b = z \quad \forall x e2$
  5. $P(a) \land P(b) \quad \mathrm{Assumption}$
  6. $P(a)\quad \land e_1 5$
  7. $P(b)\quad \land e_2 5$
  8. $a = z \quad \rightarrow e3,6$
  9. $b = z \quad \rightarrow e4,7$
  10. $b = b \quad =i$
  11. $z = b \quad =e 9,10$
  12. $a = b \quad =e 8,11$
  13. $P(a) \land P(b) \rightarrow a = b \quad \rightarrow i 5-12$
  14. $\forall y (P(a) \land P(y) \rightarrow a = y) \quad \forall y i 4-13$
  15. $\forall x \forall y (P(x) \land P(y) \rightarrow x = y) \quad \forall x i 3-14$
  16. $\forall x \forall y (P(x) \land P(y) \rightarrow x = y) \quad \exists z e 1,2-15$
$\endgroup$
  • $\begingroup$ In short: Since you wish to use Universal (Re)Introduction twice, this is a clue to first use Universal Elimination twice. $\endgroup$ – Graham Kemp Dec 28 '17 at 4:54
  • 1
    $\begingroup$ Short answer is, you want step 4 to be $P(x_0) \land P(z_0)$ $\endgroup$ – DanielV Dec 28 '17 at 7:20
2
$\begingroup$

You almost have it.   Do pretty much as you had, except use universal elimination twice, then conclude that the two arbitrary variables must be equal whenever they both make the predicate true, since they would both then equal the same witness.

$$\begin{array}{r|l:l}1&\exists y\forall x~(P(x)\to x=y)\\ 2&\quad\forall x~(P(x)\to x=c) & 1,\exists \text{Elimination }[y\backslash c]\\[0ex] 3 & \qquad P(a)\to a=c & 2,\forall\text{Elimination }[x\backslash a]\\[0ex] 4 & \qquad\quad P(b)\to b=c & 2,\forall\text{Elimination }[x\backslash b] \\[0ex] 5 & \qquad\qquad P(a)\wedge P(b) & \text{Assumption} \\[-1ex] 6 & \qquad\qquad\vdots & \\[-1ex] 7 & \qquad\qquad\vdots & \\[-1ex] 8 &\qquad\qquad\vdots & \\[-1ex] 9 & \qquad\qquad\vdots & \\[0ex] 10 & \qquad\qquad a=b & ~,~,=\text{Elimination}\\[0ex] 11 & \qquad\quad (P(a)\wedge P(b))\to(a=b) & 5,10,\to\text{Introduction}\\[-1ex] \vdots\end{array}$$

Well, you can fill in the missing details.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.