Prove the following for an addition binary operation

Question

I'm struggling to understand if my attempted proof is correct for the following question:

Prove the following formula when the binary operation is the addition of real numbers:

\begin{equation} \exists_{x}\forall_{y}[[x=1]\implies[x + y = y]] \end{equation}

My attempt follows: \begin{align} 1&. \quad \exists_{x}\forall_{y}[[x=1]\implies[x + y = y]] &(prove) \\ 2&. \quad x = 0 &(choose) \\ 3&. \quad y &(initialise) \\ 4&. \quad x = 1 &(given) \\ 5&. \quad 0 + y = y & \\ 6&. \quad x + y = y &(2,5) \\ 7&. \quad [x=1] \implies [x+y=y] &(5,6) \\ 8&. \quad \forall_{y} [[x=1] \implies [x+y=y]] &(3 \to 7) \\ 9&. \quad \exists_{x} \forall_{y} [[x=1] \implies [x+y=y]] &(2 \to 8) \end{align}

I always struggle to prove things that "don't make sense". By that, I mean that we expect to find that $x = 0$ because then $x+y=y$ would work for all $y$. The problem is that the question states that if $x=1$ then $x+y=y$ can be concluded. In my attempted proof, in line two, I chose $x$ to be equal to $0$ and then in line four I use the assumption that if $x=1$ the conclusion would hold.

Maybe if I wrote my logic out in English it would help to understand what I'm struggling with. According to me, the question reads as:
There exists an $x$ such that for all $y$, if $x=1$, then $x+y=y$.

Thus, as I understand it, my proof's explanation would be described by:

1. The $\exists$ and $\forall$ symbols exist outside of the implication's brackets, so we can use them as an assumption in our proof.
2. The first symbol is $\exists_{x}$. Therefore, we have to choose an $x$ in the proof such that the question can be proved. (line 2)
3. The $\forall_{y}$ follows, so we should initialise $y$ to be able to use it as a variable in the proof. (line 3)
4. Now we are "stuck" (can't make any more conclusions) and should move on to the next part, the implication contained in the brackets.
5. The implication reads as "if $x=1$ then $x+y=y$". Thus, we assume $x=1$ to be true so that we can use it in the rest of our proof. (??)
6. We know $0+y=y$ and it would satisfy the conclusion part of our implication, so we state it. (line 5)
7. Since $0+y=y$ and $x=0$ (line 2) we can conclude that $x+y=y$. (line 6)
8. From lines 5 and 6 we can conclude that if $x=1$ then $x+y=y$. (line 7)
9. We can conclude from initialising $y$ and the lines $3\to 7$ that the implication holds for all $y$. (line 8)
10. Because we chose an appropriate $x$ value where the content contained in lines $2\to 8$ holds, we can conclude there exists such an $x$. (line 9)

Any help would be appreciated!
Thanks in advance.

Answer 1

Sketch of a proof

If we start with the axioms for the reals we know that they are a field that means that there are two different elements $0$ and $1$.

Thus, assuming $0=1$ we have a contradiction with the previous axiom and we can use the tautology : $\lnot P \to (P \to Q)$ to derive directly : $(0+y=y)$

Then we discharge the assumption to get :

$0=1 \to (0+y=y)$

and the "generalize" it to get : $\forall y \ [0=1 \to (0+y=y)]$.

Finally, we use $\exists$-intro to conclude with :

$\exists x \ \forall y \ [x=1 \to (x+y=y)]$.

Answer 2

There are two ways to prove an implication $P\to Q$: you prove that the consequent $Q$ is true, or you prove that the antecedent $P$ is false. In other words, $P\to Q$ is equivalent to $\lnot P\lor Q$.

Therefore, your formula says as much as that there exists some number $x$ such that $x\neq 1$ or such that for all $y$ we have $x+y=y$. So informally there are two routes you could take:

• Show using the axioms of real arithmetic that there exists an element $x\neq 1$.
• Show using the axioms of real arithmetic that there exists an element $x$ such that for all $y$ we have $x+y=y$.

As you've noticed, taking $x=0$ does the job for both of these at the same time.

This shows we can prove even less intuitive statements, such as $\exists x\forall y(x=1\to x\neq y)$ (by showing the antecedent could be false) or $\exists x\forall y(x=1\land x=2\to y=y)$ (by showing the consequent is always true).

---

Note that in your proof, you start with $x=0$ and then assume $x=1$. If you prove $1\neq 0$, you get a contradiction, and thus by the Principle of Explosion you could then conclude any consequence.