Requiring the isomorphism between two FOL interpretations to be a bijection when proving they are elementary equivalent Assume we have a formula $F$ with $k$ free variables of some signature, and we also have two isomorphic interpretations $M_1$ and $M_2$ of that signature with $\alpha$ being the corresponding isomorphism. Let's prove
$$
\forall m_1, \dots, m_k : M_1 \models F(m_1, \dots, m_k) \iff M_2 \models F(\alpha(m_1), \dots, \alpha(m_k)),
$$
which is a slightly more generic claim, but would allow us to prove the original one by induction on the structure.


*

*If $F$ is an atomic formula, then the claim follows from the fact that isomorphisms preserve predicates and functions.

*If $F$ is a logical combination of one (using $\lnot$) or two ($\lor, \land, \rightarrow$) formulas, then it follows easily from the inductive hypothesis.

*$\forall$ is expressible via $\exists$, so we proceed straight to that.

*If $F(\xi_1, \dots, \xi_n)$ is $\exists \xi G(\xi, \xi_1, \dots, \xi_n)$: this is the interesting part. Let's fix $m_1, \dots, m_k$ and consider two subcases:


*

*If $M_1 \models \exists \xi F(\xi, m_1, \dots, m_k)$, then, well, there exists some $m$ such that $M_1 \models F(m, m_1, \dots, m_k)$, and by the inductive hypothesis $M_2 \models F(\alpha(m), \alpha(m_1), \dots, \alpha(m_k))$, so $M_2 \models \exists \xi F(\xi, \alpha(m_1), \dots, \alpha(m_k))$.

*If $M_1 \not\models \exists \xi F(\xi, m_1, \dots, m_k)$, assume still $M_2 \models \exists \xi F(\xi, \alpha(m_1), \dots, \alpha(m_k))$, and $m'$ is the value of $\xi$ that makes it true. Since $\alpha$ is an isomorphism, then there exists $\alpha^{-1}(m')$, and by the inductive hypothesis $M_1 \models F(\alpha^{-1}(m'), m_1, \dots, m_k)$, contradicting the claim.



One might note that we haven't really used that $\alpha$ is an isomorphism. Instead, we have only used its surjectivity, which brings two questions:


*

*Is this proof correct?

*If it is, can the surjectivity requirement also be dropped as the injectivity is? The claim looks symmetrical, so it would be surprising if it couldn't.
 A: Let's identify the issue first, and then try to figure out where the omission occurs. 
We want to argue that $\alpha$ preserves all formulas. In particular, this means that somewhere along the line we'll need to show (something which implies) that $\alpha$ preserves the formula "$\neg x=y$." But clearly this is equivalent to the injectivity of $\alpha$. So we can see that there must in fact be a gap somewhere in your argument, since in order to show that $\alpha$ preserves all formulas we must use injectivity somewhere.

OK, so where's the gap?
As written, I would say you need to be more explicit at (2). Specifically, the negation case is important: think about e.g. "$\neg x=y$" (and the relation between preserving this and being injective). So technically you've given the correct "shape," but the injectivity assumption on $\alpha$ is buried in behind the word "easily."
Another option would be to be more explicit at (1). Maybe by "preserves atomic formulas" you mean "preserves and reflects atomic formulas," or equivalently "preserves atomic and negated atomic formulas." In this case you will need to actually give an argument: while preservation of atomic formulas is built into the hypotheses (other than injectivity) on $\alpha$, the reflection of atomic formulas isn't.
Either way, something needs to happen to cover the negated atomic case; this isn't present in your proof as written, and accounts for the apparent unnecessity of injectivity.
