Prove that $(\mathbb{Z}, =, <)$ is elementarily equivalent to $(\mathbb{Z} + \mathbb{Z}, =, <)$

Question

Prove that $(\mathbb{Z}, =, <)$ is elementarily equivalent to $(\mathbb{Z} + \mathbb{Z}, =, <)$. Interpretations are called elementarily equivalent if they satisfy the same predicate folmulas without free variables. I know that in $(\mathbb{Z}, =, <, S)$, where $S(x) = x + 1$ we can eliminate quantifiers. Can this fact help to solve the problem? Can you give me a hint how to start, please?

Answer 1

In order to establish elementary equivalence, one usually uses a criterion such as Tarski–Vaught test. This test is indeed easier to check if you have quantifier elimination.

(edit)Write $\mathbb{Z} + \mathbb{Z} = Z_1 + Z_2$, where $Z_i$ is a copy of $\mathbb{Z}$.
It is enough to check that $A:=(\mathbb{Z}, =, <, S) \equiv (\mathbb{Z}+\mathbb{Z}, =, <, S)=:B$, where $S^B$ is just the successor function on each copy of $\mathbb{Z}$.

plan A (don't do this!) Here's my hint : consider $A$ as a substructure of $B$ ($A$ is isomorphic to the first copy of $\mathbb{Z}$ in $B$), and use Tarski-Vaught test to prove that $A$ is an elementary substructure of $B$ (written$A\preccurlyeq B$).

problem with this hint It's OK to assume that the theory of $(\mathbb{Z},<,S)$ has QE, but we don't know if the theory of $(Z_1 > \sqcup Z_2,<,S)$ does!

This try also fails... Sorry!

Plan B (also wrong, see Noah's comment below) Make an infinite back and forth between both structures in order to show that they are $\omega$-equivalent (and hence equivalent).

a last try, back to plan A
Consider the partial type $\pi(x,y) := \{x<y \wedge S^n(x) \neq y\wedge \neg S^n(y)\neq x\}_{n \in \mathbb{N}}$. There are $a,b$ in an elementary extension, say $Z'$, of $(\mathbb{Z},<,S)$ such that $Z'\models \pi(a,b)$.
Now, let $M:=\langle a,b\rangle$ be the substructure of $Z'$ generated by $a,b$.

$M$ is isomorphic to $(Z_1\sqcup Z_2)$.

Now all is well : you can apply Tarsky Vaught test to show that $M$ is an elementary substructure of $Z'$ and you have QE.

Answer 2

There is a way to use quantifier elimination, but it works best not directly in the structure $(\mathbb Z,<,S),$ but rather in the theory $T_{disc}$ of discrete linear orders without endpoints, given in the signature with $<,S$ and the predecessor function $S^{-1}$, which is just a finite set of axioms that say $<$ is a total order, that every element has a direct successor and predecessor in the ordering, that $S$ and $S^{-1}$ are functions taking an element to its direct successor and predecessor, and that there is no greatest or least element.

The models of $T_{disc}$ are easy to characterize. By partitioning the domain into equivalence classes of elements that are a finite "distance" away from one another (i.e. $x\sim y$ iff $x=S^n y$ for some $n\in \mathbb Z$), you can see that models of $T_{disc}$ are exactly structures of the form $L\times \mathbb Z$ where $L$ is a linear order and the ordering on $L\times Z$ is lexicographic. So the two models in your question are the two simplest: $1\times \mathbb Z$ and $2\times \mathbb Z.$

So if we can show $T_{disc}$ is complete, then we are done: this will show that not only are the two models in question elementarily equivalent, but that any model of the form $L\times \mathbb Z$ is. Completeness will follow from quantifier elimination, since there are no closed terms, so the only quantifier-free sentences are $\top$ and $\bot.$

There are a number of tests to show quantifier elimination for this theory, and I'm not sure what your course uses, so I'll sketch a direct syntactic proof. It is a bit of a slog, but elementary. You can fill in a more elegant method if you wish. By induction on formulas it suffices to show we can eliminate an existential quantifier from a conjunction of atomic sentences: at the existential step of the induction the formula is equivalent to $\exists x \phi'(x)$ where $\phi'$ is quantifier free by the induction hypothesis. Then we can write $\phi'$ in disjunctive normal form and distribute the $\exists x$ over the disjunction so that we have a disjunction of formulas like $\exists x(\bigwedge_i \psi_i)$ where $\psi_i$ are literals.

Any negated literals have the form $\lnot(t_1=t_2)$ or $\lnot(t_1<t_2)$ and these can be replaced with the equivalent $t_1<t_2\lor t_2<t_1$ and $t_1=t_2\lor t_2<t_1,$ and then you can refactor the result into DNF, distribute the $\exists x$ and wind up in the same place, only now all the $\psi_i$ in each clause are atomic (i.e. not negated).

Then you can eliminate the $\exists x$ as follows: any $\psi_i$ that have no $x$ can just be factored out. The theory can decide anything like $S^2x=S^3x$ (false) or $S^{-5} x< S^{31} x$ (true) so any atomics like that trivialize and we don't need to worry about them. Also, any equalities in general trivialize. For instance if we have $S^3 x = S^7(y),$ we can just replace $x$ everywhere in the clause by $S^4y$ and remove the $\exists x$ and we're done.

So we just need to figure out what to do with a bunch of inequalities like $S^n x< S^m y.$ Write them all in the form $x < S^ky_j$ or $S^k y_j < x.$ The existence of an $x$ satisfying such a conjunction is equivalent to having all of the $S^k y_j$ in a certain order so that the $x$ fits between them in the right way. For instance $\exists x(S^2y < x\land x<S^6 z)$ is equivalent to $S^2 y < S^7 z$ and $\exists x(S^2y < x\land S^6 z<x)$ is just equivalent to $\top.$

It's a little bit of work to think through it and confirm that this is the case and theory has the power to prove this equivalence.

---

This is just one solution. If you have Ehrenfeucht–Fraïssé games available, then that is probably the easiest. (Eloise just needs to make sure she maps infinitely far apart things in $2\times \mathbb Z$ far enough away from each other in $\mathbb Z$ to survive $n$ rounds.)

There are other fancier ways involving saturated models, but these probably aren't available at this stage in the course.