4
$\begingroup$

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$.

$\endgroup$
2
$\begingroup$

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}$

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

$\;$ 8. $P(x) \rightarrow x=b$, $\;\;\;\;\;\; \text{2-7, $\rightarrow$I}$

$\;$ 9. $\forall x (P(x) \rightarrow x=b)$, $\;\;\;\;\;\; \text{2-7, $\rightarrow$I}$

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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)}}$$

$\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.