Prove the following by deduction rules for qualifiers and implication

Question

I am having trouble with the following proof. First, some basic definitions:

1. Def. Given two statements $\alpha$ and $\beta$, the statement \begin{equation}\alpha \implies \beta ,\end{equation} read as "$\alpha \ \mathrm{implies} \ \beta $ ", means \begin{equation}``\alpha \ \mathrm{implies} \ \beta " \end{equation} which is the same as to say \begin{equation}``\mathrm{if} \ \alpha \ \mathrm{then} \ \beta" .\end{equation}
2. Axm (Deduction Rules for Implication). From $\alpha$ and $\alpha \implies \beta$ we can conclude $\beta$. The statement $\alpha \implies \beta$ can be concluded after $\beta$ was concluded from $\alpha$.

We have to follow a very specific structure in our proofs. This is what's confusing me. We are supposed to give the proof in a nested manner where an inner block is proved first.

Prove the following, where variables represent natural numbers (including the number $0$): \begin{equation} \quad \forall_{x}\left[\left[ \forall_{y}\left[x+y=1+y\right]\right]\implies\left[\exists_{z}\left[x+z=2\right]\right]\right] \end{equation} My (updated) attempt:

\begin{align} 1&. \quad \forall_{x}\left[\left[ \forall_{y}\left[x+y=1+y\right]\right]\implies\left[\exists_{z}\left[x+z=2\right]\right]\right] \\ 2&. \quad x &(declare)\\ 3&. \quad \forall_{y} \left[ x+y=1+y \right] &(assumed)\\ 4&. \quad y=1 &(UI) \\ 5&. \quad x + 1 = 1 + 1 &(4,3)\\ 6&. \quad x + 1 = 2 &(5, Peano Ax.)\\ 7&. \quad z=1 &(choose)\\ 8&. \quad x+z=2 &(6,7) \\ 9&. \quad \left[\exists_{z}\left[x+z=2\right]\right] &(Exist.Gen.)\\ 10&. \quad\left[ \forall_{y} \left[ x+y=1+y \right] \implies \exists_{z}\left[x+z=2\right]\right] \\ 11&. \quad \forall_{x}\left[\left[ \forall_{y}\left[x+y=1+y\right]\right]\implies\left[\exists_{z}\left[x+z=2\right]\right]\right] &QED \end{align} We are given strict instruction to split deduction (conclusions) from the right-hand side's line corresponding numbers. If I understand correctly, it follows the rules of Natural Deduction but "baby-feeds" us with many additional comments so that we can start to understand it. We were told to draw lines between equations to show conclusions but I don't know how I could draw lines using the standard LaTeX functions. I'll "draw" conclusions via text:

1. Line 10 is concluded by line 2, because we have declared $x$ and thus, for all $x$ the statement holds
2. Line 9 is concluded by line 3, because, from the implication we assume that if $\forall_{y}\left[x + y = 1 + y\right]$ is true then $\left[\exists_{z}\left[x+z=2\right]\right]$ is also true.
3. Line 8 is concluded by line 4 because we instantiate $y$ to be equal to $1$ and thus, $x+z=2$.

I'll also include an (untidy) image on how to proof structure "should" look:

Apparently, according to my friend, this is wrong. His answer can be found here: \begin{align} 1&. \quad \forall_{x}\left[\left[ \forall_{y}\left[x+y=1+y\right]\right]\implies\left[\exists_{z}\left[x+z=2\right]\right]\right] \\ 2&. \quad x &(declare)\\ 3&. \quad \forall_{y} \left[ x+y=1+y \right] &(assumed)\\ 4&. \quad x=1 \\ 5&. \quad z = 1 &(choose)\\ 6&. \quad 1 + 1 = 2 &(Peano Ax.)\\ 7&. \quad x+z=2 &(6,4,5) \\ 8&. \quad \left[\exists_{z}\left[x+z=2\right]\right] &(5,7)\\ 9&. \quad\left[ \forall_{y} \left[ x+y=1+y \right] \implies \exists_{z}\left[x+z=2\right]\right] \\ 10&. \quad \forall_{x}\left[\left[ \forall_{y}\left[x+y=1+y\right]\right]\implies\left[\exists_{z}\left[x+z=2\right]\right]\right] &QED \end{align}

An image with his styling can be found here:

While he definitely gets better marks than me I'm struggling to see how his answer is better than mine.

Thanks so much for your help!

Sorry for the bad formatting. I'm still learning LaTeX. The images were added because of those lines we have to draw and I don't know how to add them while using basic LaTeX. I hope this conforms to the code of conduct. My hand writing is bad, I've been told - sorry!

Answer 1

Sketch of a proof, to be refined according to the proof system used.

We have to start assuming :

1) $∀y[x+y=1+y]$ --- start of sub-proof

Instantiating it with $y=1$ we get :

2) $x+1=1+1$

Now we need the laws of arithmetic, and specifically the law : $1+1=2$, provable from Peano axioms, and transitivity of equality to get :

3) $x+1=2$

Now we can conclude by Existential generalization with :

4) $∃z[x+z=2]$.

Now we use Conditional Proof :

$∀y[x+y=1+y] \to ∃z[x+z=2]$ --- end of sub-proof.

The result follows by Universal generalization :

$∀x \ (∀y \ [x+y=1+y] \to ∃z \ [x+z=2])$.