Proof Using Natural Deduction (including '=' rules)

Question

I have a natural deduction proof that I'm stuck on. Obviously I'm not asking someone to just tell me the answer, but if anyone could help me with the next step/point out any mistakes I've made it would be much appreciated.

The proof is:

$P(b),\forall x\forall y(P(x)\wedge P(y) \rightarrow x=y) \vdash \forall x(P(x) \rightarrow x=b)$

and here is what I have so far:

$$1\;\;\;\;\;\;\;\;\;\;\;\;\; P(b)\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; premise \\ \;\;2\;\;\;\;\;\;\;\;\;\;\;\;\; \forall x \forall y(P(x)\wedge P(y) \rightarrow x=y) \;\;\;\;\;\;\;\;\;\;\;\;\;premise \\ 3\;|\;x_0\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \\ \;\;\;\;\;4\;|\;|\;\;\;\;\;\;\;\;\;P(x_0)\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;assumption \\ 5\;|\;|\;\;\;\;\;\;\;\;\; \forall y(P(x_0)\wedge P(y)\rightarrow x_0 = y)\;\;\;\;\;\;\;\;\;\;\;\;\;\forall e\;2\;\;\;\; \\ 6\;|\;|\;\;\;\;\;\;\;\;\; P(x_0)\wedge P(y_0) \rightarrow x_0 = y_0\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\forall e\;5\;\;\;\; \\ 7\;|\;|\;\;\;\;\;\;\;\;\;... \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;$$

I think from this point, I need to somehow show that $y_0 = b$ or $P(y_0)=P(b)$ or something, so that I can eliminate the $\rightarrow$ on line 6 and end up with $x_0=b$.

Answer 1

I wouldn't bother instantiating $x_0$ or $y_0$. I would instantiate the $y$ in your second premise to be $b$ itself. Then since you have $P(b)$ as a premise, you know that $P(x) \land P(b)$ is equivalent to just $P(x)$, and you're done.

More explicitly, start with

$$\forall x\forall y(P(x)\wedge P(y) \rightarrow x=y$$

Then since this is true for every $y$, it must be true for $b$ in particular, so

$$\forall x(P(x)\wedge P(b) \rightarrow x=b$$

And since $P(b)$ is true, $P(x)\wedge P(b) \iff P(x)\wedge \top \iff P(x)$, so we can substitute and get

$$\forall x(P(x) \rightarrow x=b)$$

and done.

Answer 2

You don't actually need to apply the identity rules. Note that in your givens you have $P(b)$ and $∀x∀y(P(x)∧P(y)→x=y)$, a sentence that merely asserts that one and only one object has $P$.

Now since $P$ is predicated of $b$ already, why don't try some instantiation of them?

You can try something simpler:

1. $P(b)$, $\;\;\;\;\;\; \text{premise}$
2. $∀x∀y(P(x)∧P(y)→x=y)$, $\;\;\;\;\;\; \text{premise}$
3. $\quad P(x)$, $\;\;\;\;\;\; \text{assumption}$
4. $\quad ∀y(P(x)\land P(y)→x=y)$, $\;\;\;\;\;\; \text{2, $\forall$E}$
5. $\quad P(x)\land P(b)→x=b$, $\;\;\;\;\;\; \text{4, $\forall$E}$
6. $\quad P(x)\land P(b)$, $\;\;\;\;\;\; \text{3, 1, $\land$I}$
7. $\quad x=b$, $\;\;\;\;\;\; \text{5, 6, $\rightarrow$E}$
8. $P(x) \rightarrow x=b$, $\;\;\;\;\;\; \text{3-7, $\rightarrow$I}$
9. $\forall x (P(x) \rightarrow x=b)$, $\;\;\;\;\;\; \text{2-8, $\forall$I}$

Answer 3

The 'trick' to remember is that when using universal elimination you can alpha-replace the bound entity with any entity, including a non-arbitrary entity.   If a predicate is true for all things it is true for any specific thing.   Just remember you can't use universal reintroduction when you don't choose an arbitrary entity.

You can use: $\forall y\; Q(y) \vdash Q(b)$

$$\def\fitch#1#2{~~\begin{array}{|l} #1\\\hline #2\end{array}}\fitch{~1.~P(b):\textsf{Premise (Constant Term)}\\~2.~\forall x\forall y~(P(x)\land P(y)\to x=y):\textsf{Premise}}{\fitch{~3.~[a]:\textsf{Arbitrary Term}}{~4.~\forall y~(P(a)\land P(y)\to a=y):\textsf{Universal Elimination (2,x:=a)}\\~5.~P(a)\land P(b)\to a=b:\textsf{Universal Elimination (4,y:=b)}\\\fitch{~6.~P(a):\textsf{Assumption}}{~7.~P(a)\land P(b):\textsf{Conjunction Introduction (1,6)}\\~8.~a=b:\textsf{Conditional Elimination (5,7)}}\\~9.~P(a)\to a=b:\textsf{Conditional Introduction (6-8)}}\\10.~\forall x~(P(x)\to x=b):\textsf{Universal Introduction (3-9)}}$$