Prove the following for a general binary operation, $\Delta$

Question

I would like somebody to confirm if my proof is correct or not, please.

The question below:

Prove the following for a general binary operation $\Delta$: \begin{equation} \left[ \forall_{x} \exists_{y} [y \Delta y = x] \right] \implies \left[ \forall_{x} \exists_{a} \exists_{b} \left[ (a \Delta a) \Delta b = x \right]\right] \end{equation}

My proof:

\begin{align} 1&. \quad \forall_{x} \exists_{y} [y \Delta y = x] \tag{assume} \\ 2&. \quad x \tag{declare} \\ 3&. \quad a = c \tag{choose} \\ 4&. \quad b = c \Delta c \tag{choose} \\ 5&. \quad ( c \Delta c ) \Delta ( c \Delta c ) = x \tag{1,3,4} \\ 6&. \quad \exists_{b} \left[ (a \Delta a) \Delta b = x \right] \tag{4,5} \\ 7&. \quad \exists_{a} \exists_{b} \left[ (a \Delta a) \Delta b = x \right] \tag{3 $\to$ 6} \\ 8&. \quad \forall_{x} \exists_{a} \exists_{b} \left[ (a \Delta a) \Delta b = x \right] \tag{2 $\to$ 7} \\ 9&. \quad \left[ \forall_{x} \exists_{y} [y \Delta y = x] \right] \implies \left[ \forall_{x} \exists_{a} \exists_{b} \left[ (a \Delta a) \Delta b = x \right]\right] \tag{1 $\to$ 8} \end{align}

An explanation of my thought process follows (line numbers correspond to that of the proof's):

1. We assume this part.
2. Because we can't continue due to the assumption's $ \forall $ we start working backwards. Thus, we start using the conclusion's $\forall_{x} \exists_{a} \exists_{b}$. With the first part being $\forall_{x}$, we declare $x$.
3. From the next $\exists_{a}$, we choose a value for $a$. Because we are working with a general set of objects as values, we assign it a specific value called $c$.
4. From the next $\exists_{b}$, we, similarly, choose a value for $b$. We choose it to be $(c \Delta c)$, because we will be using the fact that for all $x$ there exists a value $y$ such that $y \Delta y = x$.
5. Thus, the reason we choose $b$ to be $(c \Delta c)$, is because, when we substitute the values of $a$ and $b$ into $(a \Delta a) \Delta b = x$ we find that we get $(c \Delta c) \Delta (c \Delta c) = x$, which, by line $1$, we know is true.
6. From lines $4$ and $5$ we can conclude that there does indeed exist such a value $b$ for which the statement holds.
7. From lines $3$ to $6$ we can conclude similarly that there exists such a value $a$.
8. From lines $2$ to $7$ we can conclude that this works for all $x$.
9. QED

The reason I am skeptical is that I am basically using the statement in the conclusion to conclude itself. Is this allowed?

Answer 1

To prove the given implication you need to show that if the antecedent, $ \forall_{x} \exists_{y} [y \Delta y = x]\ $, is true then the consequent, $\ \forall_{x} \exists_{a} \exists_{b} \left[ (a \Delta a) \Delta b = x \right]\ $, must also be true—that is, given any $\ x\ $ you can find $\ a\ $ and $\ b\ $ such that $\ (a \Delta a) \Delta b = x\ $. The only assumption you're allowed to make in a valid proof is that the antecedent is true—that is, given any $\ x\ $ you can find a $\ y\ $ such that $\ y \Delta y = x\ $.

You're scepticism about the validity of your proposed proof is quite justified. You start off correctly by assuming the antecedent in step $1$, and choosing an arbitrary $\ x\ $ in step $2$. However, having chosen an (apparently arbitrary ) $\ c\ $ for the value of $\ a\ $ in step $3$ and then $\ c\Delta c\ $ for the value of $\ b\ $ in step $4$, you have no justification for assuming, as you appear to do in step $5$, that $\ (a\ \Delta a) \Delta b = x\ $ for those chosen values of $\ a\ $ and $\ b\ $.

What you need to do in step $3$ is use your assumption that the antecedent is true to pick some value of $\ y\ $ such that $\ y\Delta y = x\ $, then let $\ b=y\ $, so you have $\ b\Delta b=x\ $. But now, the antecedent also tells you that you can find another value, $\ y_1\ $, say, of $\ y\ $ such that $\ y_1\Delta y_1=b\ $, and putting $\ a=y_1\ $ gives you $\ a\Delta a=b\ $, and hence $\ (a\ \Delta a) \Delta b = x\ $.