= Solution
Fix any structure and any assignment of the three quantified variables, writing their values as $a_0,a_1,a_2$. If either of the nested antecedents is false, the corresponding implication is true. If both are true, then $f^A(a_0)=a_1$ and $f^A(a_0)=a_2$. Actual identity is transitive, so $a_1=a_2$, making the consequent true as well.
Thus the unquantified matrix is true under every assignment in every structure. The universal-quantifier semantic clause then makes its universal closure true in every structure:
$$
\boxed{\models\forall x_0\forall x_1\forall x_2\,[f(x_0)=x_1\to(f(x_0)=x_2\to x_1=x_2)].}
$$
No assumption that $f$ is <injective> is used. The argument says that one value cannot equal two distinct elements, not that distinct inputs have distinct outputs.
Back to article page
