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.
Edit
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))).$
Best Answer
Since the variable $x_i$ is free in the first but not the second formula, the formulae aren't equivalent.
To analyse just their logical form, your two formulae can be more readably rewritten: \begin{gather}∃x∀y\; Pxyy \quad∧\quad ∀z\; (∀y\; Pxyy \to Qxz)\tag1\\∃x∀y\; \Big(Pxyy \quad∧\quad ∀z\;(Pzyy \to Qxz)\Big).\tag2\end{gather} For easier comparison, here's a logical rewrite: \begin{gather}∃r∀s∀z∃y\; \Big(Prss \quad∧\quad (Pxyy \to Qxz)\Big)\tag1\\∃x∀z∀y\; \Big(Pxyy \quad∧\quad (Pzyy \to Qxz)\Big).\tag2\end{gather}
P.S. Note that \begin{align}&∀y\; Pxyy \to Qxz\\\equiv{}& (∀y\; Pxyy) \to Qxz\\\equiv{}& ∃y\;(Pxyy \to Qxz).\end{align}
Addendum (corresponding to the OP's Edit)
Considering its logical form: $$∃x\;\Big(∀y\; Pxyy \quad∧\quad ∀z\; (∀y\; Pzyy \to Qxz)\Big).\tag{1r}$$
Logical rewrite: $$∃x∀s∀z∃y\; \Big(Pxss \quad∧\quad (Pzyy \to Qxz)\Big).\tag{1r}$$
Unfortunately, $$∃x∀z∀y\; \Big(Pxyy \quad∧\quad (Pzyy \to Qxz)\Big)\tag2$$ (duplicated from above) is logically equivalent to neither $(1)$ nor $(1r).$