# 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.

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

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

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

4. 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:

1. 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))$.
2. 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:

1. Is this proof correct?

2. 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.

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.

• Probably a dumb question, but why? In the negation case $F(\xi_1, \dots, \xi_n) = \lnot G(\xi_1, \dots, \xi_n)$, and $M_1 \models \lnot G(m_1, \dots, m_n) \iff M_1 \not\models G(m_1, \dots, m_n) \iff M_2 \not\models G(\alpha(m_1), \dots, \alpha(m_n)) \iff M_2 \models \lnot G(\alpha(m_1), \dots, \alpha(m_n))$, where the first and last equivalences are by definition of truthfulness in an interpretation, and the middle one is by the induction hypothesis. – 0xd34df00d Jun 23 '18 at 1:13
• @0xd34df00d It depends on exactly how you phrase the base case. What you've written is just that $\alpha$ preserves atomic formulas, but you also want it to reflect atomic formulas. (Or, maybe by "preserves" you mean "preserves in both directions.") The point is that when it comes time to argue that $\alpha$ preserves "$x\not=y$" (or if you prefer, reflects $x=y$) then you need the injectivity of $\alpha$. – Noah Schweber Jun 23 '18 at 15:44
• It might be easier to start at the beginning: do you see why, in order to argue that $\alpha$ preserves $x\not=y$, we will need to know that $\alpha$ is injective? – Noah Schweber Jun 23 '18 at 15:46
• @0xd34df00d I've edited my answer to be clearer; let me know if this doesn't improve things and I'll further edit or revert as preferred. – Noah Schweber Jun 23 '18 at 15:51
• Ah, I see what you're saying now, thank you for the clarification! Yes, I meant "preserves and reflects", so that the implication in both directions holds (sorry, the book I'm using is written in another language, so I might be translating incorrectly). Further, your argument indeed shows that this essentially requires $\alpha$ to be injective, but here you seem to assume the interpretations are normal — or, in other words, that $=$ is interpreted as a match between two elements. That wouldn't be necessarily the case for non-normal interpretations, would it? – 0xd34df00d Jun 23 '18 at 17:18