Prove $\exists x(P(x) \land \forall y(P(y) \to y=x)) \vdash \exists x \forall y(P(y) \leftrightarrow y=x)$.

Question

This is the skeleton for the proof of $\exists x(P(x) \land \forall y(P(y) \to y=x)) \vdash \exists x \forall y(P(y) \leftrightarrow y=x)$ using Fitch-style natural deduction system.

$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $ $ \fitch{1.\, \exists x(P(x) \land \forall y(P(y) \to y=x))}{ \fitch{2.\, P(a) \land \forall y(P(y) \to y=a)}{ 3.\, P(a) \ce{2} 4.\, \forall y(P(y) \to y=x) \ce{2} 5.\, P(b) \to b=a \Ae{4} \fitch{6.\, P(b)}{ b=a }\\ \fitch{7.\, b=a}{ \vdots\\ P(b) }\\ P(b) \leftrightarrow b=a\\ \vdots }\\ \exists x \forall y(P(y) \leftrightarrow y=x) } $

In order to use, $\mathbf{\leftrightarrow E}$, I need to show $P(b) \vdash b=a$ and $b=a \vdash P(b)$.

Is this the right approach? How can I justify $P(b)$ for the second subproof ?

EDIT:

Biconditional Introduction and Elimination Rules

$ \fitch{}{ \fitch{i.\, \mathcal{A}}{ j.\, \mathcal{B} }\\ \fitch{k.\, \mathcal{B}}{ l.\, \mathcal{A} }\\ \, \mathcal{A} \leftrightarrow \mathcal{B} \bi{i-j,k-l} } $

$ \fitch{}{ \mathcal{A} \leftrightarrow \mathcal{B}\\ \mathcal{A}\\ \mathcal{B} \be{m,n} } $

$ \fitch{}{ \mathcal{A} \leftrightarrow \mathcal{B}\\ \mathcal{B}\\ \mathcal{A} \be{m,n} } $

Identity elimination rules

$ \fitch{}{ \mathcal{a} = \mathcal{b}\\ \mathcal{A}(...\mathcal{a}...\mathcal{a}...)\\ \mathcal{A}(...\mathcal{b}...\mathcal{a}...) } \fitch{}{ \mathcal{a} = \mathcal{b}\\ \mathcal{A}(...\mathcal{b}...\mathcal{b}...)\\ \mathcal{A}(...\mathcal{a}...\mathcal{b}...) } $

Answer 1

$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad\mathbf{R} \: #1 \\} \def\ci#1{\qquad\mathbf{\land I} \: #1 \\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad\mathbf{\leftrightarrow I} \: #1 \\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad\mathbf{\neg E} \: #1 \\} \def\ni#1{\qquad\mathbf{\neg I} \: #1 \\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $

Your approach is correct, you just have to fill the dots (and fix a couple of typos in lines $2$ and $4$: $a$ should replace $x$).

To prove $b = a$ from $P(b)$ you just have to trivially apply modus ponens $\to \mathbf{E}$ from lines $5$ (i.e. $P(b) \to b = a$) and $6$ (i.e. $P(b)$).

Vice-versa, to prove $P(b)$ from $b = a$ you have to apply $= \mathbf{E}$ from lines 3 (i.e. $P(a)$) and 8 (i.e. $b = a$). Here we are using an obvious but important property of the identity $=$: if $P(a)$ and $b = a$ then $P(b)$.

So, you get $P(b) \leftrightarrow b = a$ by $\leftrightarrow \mathbf{I}$ and hence you are done by introducing first the universal quantifier and then the existential quantifier.

Note that the witness $a$ for both the existential quantifier in the hypothesis and the existential quantifier in the conclusion is the same. Indeed, the core of the proof is to prove that $P(a) \land \forall y \, (P(y) \to y = a) \vdash \forall y \, (P(y) \leftrightarrow y =a)$ (i.e. the derivation from the second line to the second to last line).

Below a complete proof in Fitch-style natural deduction.

$ \fitch{1.\, \exists x(P(x) \land \forall y(P(y) \to y=x))}{ \fitch{2.\, P(a) \land \forall y(P(y) \to y=a)}{ 3.\, P(a) \ce{2} 4.\, \forall y(P(y) \to y=a) \ce{2} 5.\, P(b) \to b=a \Ae{4} \fitch{6.\, P(b)}{ 7. \, b=a \ie{5,6} }\\ \fitch{8.\, b=a}{ 9. \, P(b) \qe{3, 8} }\\ 10. \, P(b) \leftrightarrow b=a \bi{6\text{-}7, 8\text{-}9} 11. \, \forall y \, (P(y) \leftrightarrow y = a) \Ai{10} 12. \, \exists x \forall y\, (P(y) \leftrightarrow y=x) \Ei{11} }\\ 13 .\, \exists x \forall y \, (P(y) \leftrightarrow y=x) \Ee{1,12} } $