2
$\begingroup$

If I symbolize the argument in First-Order logic, I think this would be the argument (the conclusion is an expansion of $\exists!$ definition):

$\exists z \forall x(x+z=x) \vdash \exists y(\forall x(x+y=x) \land \forall z(\forall x(x+z=x) \to y=z)$

$ \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 z \forall x(x+z=x)}{ \fitch{2.\, a+0'=a}{ \fitch{3.\, \neg(0 = 0')}{ \fitch{4.\, \forall x(x+0=x)}{ 5.\, 0'+0=0' \Ae{3} 6.\, 0=0 \qi{} 7.\, 0+0'=0 \qe{5,2} 8.\, 0'=0 \qe{6,4} 9.\, \bot \ne{} }\\ 10.\, \bot \Ee{} }\\ 0=0' } } $

I have as an axiom: $\exists z \forall x(x+z=x)$, used here as a premise.

The problem I have is that I cannot instantiate z to $0$ (step 4), as it occurs in a previous undischarged assumptions (step 3).

Are there any routes to complete the proof and effectively use Existential Elimination ?

EDIT: based on comments, I rewrote the proof. I am a step forward, but still cannot close $\mathbf{\exists E}$ proof, since both $0$ and $0'$ appear in undischarged assumptions.

EDIT 2: $$ \fitch{1.\, \exists z \forall x(x+z=x)\\2.\, \forall x\forall y(x+y=y+x)}{ \fitch{2.\, \forall x(x+0'=x)}{ 3.\, 0+0'=0 \Ae{1} \fitch{4.\, ¬(0=0')}{ \fitch{5.\, \forall x(x+0=x)}{ 6.\, 0'+0=0' \Ae{4} 7.\, 0+0'=0'+0 \Ae{2} 8.\, 0+0'=0' \qe{6,5} 9.\, 0=0' \qe{3,7} 10.\, \bot \ne{4,8} }\\ 11.\, \bot \Ee{1,5-10} }\\ 12.\, 0=0' \IP{4-11} }\\ 13.\, \forall x(x+0'=x) \to 0=0' \ii{2-12} 14.\, \forall z(\forall x(x+z=x) \to 0=z) \Ai{13} 15.\, \exists y(\forall x(x+y=x) \land \forall z(\forall x(x+z=x) \to y=z) \Ei{14} } $$

$\endgroup$
10
  • $\begingroup$ $\exists !y [P(y)]$ is $\exists y[P(y) \land \forall z[P(z) \to z = y]$. In your case $P(y)$ is $\forall x[ x + y = x ]$, so your expansion is incorrect. $\endgroup$
    – Magdiragdag
    Apr 24, 2020 at 14:30
  • $\begingroup$ @Magdiragdag deleted. You were correct. $\endgroup$
    – David Reed
    Apr 24, 2020 at 15:02
  • $\begingroup$ Your conclusion should be $\exists y \forall x(x+y=x \land \forall z(\color{red}{\forall x} \ x+z=x \to y=z))$ which is equivalent to $\exists y (\forall x \ x+y=x \land \forall z(\forall x \ x+z=x \to y=z))$, which as a symbolization I like better $\endgroup$
    – Bram28
    Apr 24, 2020 at 15:22
  • $\begingroup$ Thank you very much, @Magdiragdag, Bram28 and David. Could you look at my updated proof ? $\endgroup$
    – F. Zer
    Apr 24, 2020 at 17:03
  • 1
    $\begingroup$ You still haven't fixed the statement you have to prove. And in line 3, instead of instantiating with an arbitrary element $a$, instantiate with $0$. Then, in line 5, don't instantiate with $a$, but with $0'$. You then need commutativity of $+$ to finish. $\endgroup$
    – Magdiragdag
    Apr 24, 2020 at 17:08

1 Answer 1

Reset to default
0
$\begingroup$

Second proof still not quite right ... you need to have:

$\forall x(x+0'=x) \land \forall z(\forall x(x+z=x) \to 0'=z)$

before introducing the existential at the end

... and so all that needs to go inside the subproof. Here is a proof in Fitch. The $\forall \ I$ rule works a little differently than yours: it is looking for a subproof where you introduce a new constant, i.e. the analogue to 'Let $b$ be an arbitrary object': enter image description here

$\endgroup$
1
  • $\begingroup$ Thank you. Going to rework it. $\endgroup$
    – F. Zer
    Apr 24, 2020 at 17:40

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .