Prove that a logic can not distinguish two models

Question

In order to prove unequal expressivity between two logics $L_1$ and $L_2$, one may provide two models which $L_1$ can distinguish, i.e. $L_1$ has a formula $\phi$ which is true in the one but false in the other, but $L_2$ can not distinguish those models. How shall you prove that $L_2$ can not distinguish those models ?

Answer 1

EDIT: a source you might be interested in, with information about tons of different logics, is the collection "Model-theoretic logics".

Well, it depends on what $L_2$ is - different logics have different properties, and there's no "one-size-fits-all" technique.

The standard example, just because it's so well understood, is when $L_2$ is first-order logic. Here we have lots of tools:

• Ehrenfeucht-Fraisse games can be used to show that two structures are elementarily (= first-order) equivalent; for instance, $(\mathbb{Z},<)$ and $(\mathbb{Z}\oplus \mathbb{Z},<)$.

• First-order theories are preserved under ultrapowers: if one structure is an ultrapower of the other, they will be elementarily equivalent.

• It's often easy to find the quantifier-free (resp. existential) theories of the two structures involved and show that they are equal; if we can then prove the appropriate quantifier-elimination (resp. model-completeness), this shows that the two structures are elementarily equivalent.

• And so forth.

Other logics, as I said above, require different techniques. E.g.:

• For appropriate fragments of infinitary logic $L_{\omega_1\omega}$, we have the Barwise compactness theorem.

• For the class-sized infinitary logic $L_{\infty\omega}$, we have back-and-forth systems (due to Karp), or equivalently the property of being isomorphic in some forcing extension (due to Barwise).

• And there are times when there is no easy tool available, and we have to argue "sentence-by-sentence" - e.g. by induction on complexity. This is often the case when working with set-theoretically "badly behaved" logics like second-order logic, and equivalence with respect to such logics can be extremely complicated to deal with.

---

Another important point is that we don't always need to make the two structures precise. For example, suppose we make a new logic $L_W$ by augmenting first-order logic with a well-foundedness quantifier, $\mathbb{W}$ (I really want this to be an upside-down "W," in keeping with "$\forall$" and "$\exists$," but don't know how - if you can get this to happen, feel free to edit and then delete this parenthetical), which behaves as follows: for a formula $\varphi(x, y, \overline{z})$ and with free variables $x, y,$ and possibly others $\overline{z}$, we interpret "$\mathbb{W}x, y(\varphi(x, y,\overline{z}))$" as saying "there is no infinite sequence $a_1, a_2, a_3, ...$ satisfying $\varphi(a_i, a_{i+1},\overline{z})$ for all $i\in\mathbb{N}$."

This logic pins down the structure "$\mathcal{N}=(\mathbb{N}, <)$" up to isomorphism: take the usual first-order theory of $\mathcal{N}$ and add the sentence "$\mathbb{W}x, y(y<x)$." But first-order logic does not pin down $\mathcal{N}$ up to isomorphism, by the compactness theorem! This means that there must be a structure first-order equivalent to $\mathcal{N}$, but not $L_W$-equivalent; and we don't need to know exactly what it is. A lot of the time we can in fact build explicit examples (e.g. $(\mathbb{N}\oplus\mathbb{Z},<)$), but (a) not needing to can save us time, and (b) sometimes we can't (although I'm not aware of any important case where we really can't give some description of the culprit).