I have a sentence in natural language: "the sum has a neutral element and it is unique", which I have to write in a first order language that has a binary relationship symbol of equality $='$ and a binary function symbol $f_1$ which represents the sum. We were told not to bother with left and right identity, just check one. So what I did is:
$(\exists x_i)(\forall x_j)f_1(x_i,x_j) =' x_j \land (\forall x_k)( (\forall x_j)f_1(x_i,x_j) =' x_j \to (x_i =' x_k)).$
Someone in the class came up with this other one which looks equivalent but at the same time, it doesn't seem to say the same (which of course it makes no sense, is either equivalent and it says the same or its not equivalent):
$(\exists x_i)(\forall x_j)(f_1(x_i,x_j) =' x_j \land (\forall x_k)(f_1(x_k,x_j) =' x_j \to (x_i =' x_k))).$
Notice that now every occurrence of $x_j$ is under the influence of the same quantifier. So my understanding is that I can change the order of the $(\forall x_k)(\forall x_j)$ in my formula and then apply that universal quantifier distributes over conjunction, and I get his formula, and so they are equivalent. Is that correct?
And of course, if there's something wrong with my formula, please do point it out.
As ryang pointed out, there is a problem in my formula, since only the first occurrence of $x_i$ is under the influence of the existential quantifier. Reading it again, I noticed another typo, where it says $x_i$ instead of $x_k$. So, the corrected version of my formula is:
$(\exists x_i)((\forall x_j)f_1(x_i,x_j) =' x_j \land (\forall x_k)( (\forall x_j)f_1(x_k,x_j) =' x_j \to (x_i =' x_k))).$