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

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

• Which are the rules $\leftrightarrow_\mathrm{intro}$ and $\leftrightarrow_\mathrm{elim}$ in your system? Commented Apr 25, 2020 at 22:58
• Just updated the post. Commented Apr 25, 2020 at 23:19
• Which is the precise formulation of the rule $= \mathbf{E}$? Depending on that, I possibly have to add a line between lines 8 and 9 in my derivation. Commented Apr 26, 2020 at 0:45
• I will update the post to include that piece of data. Commented Apr 26, 2020 at 0:54
• @Taroccoesbrocco, your use of $= \mathbf{E}$ is perfectly in line with my book. Commented Apr 26, 2020 at 1:02

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

• Thank you very much, @Taroccoesbrocco ! Two little things in your proof. First, you didn't close the subproof you opened in line 2 for the existential quantifier. And, in order to use $\mathbf{\exists E}$ (to close the subproof), witness a cannot appear in the last line of the subproof. Commented Apr 26, 2020 at 0:53
• I really appreciate your dedication and explanation. Commented Apr 26, 2020 at 0:56
• @F.Zer - Thank you for your remark, both issues are fixed by adding line 12 to my derivation, which I had forgotten. Commented Apr 26, 2020 at 1:07
• It's perfect ! Thanks for the fixes. Commented Apr 26, 2020 at 1:09