lo.logic - Is non-connectedness of graphs first order axiomatizable?

I haven't thought about model theory in a while but I'll give this a shot. First, by bi-infinte graph, I assume that you mean $mathbb{Z}$ in which the only edges are those adjoining adjacent vertices, right?

Does the theory of cycle-free graphs admit quantifier elimination? If so, elementary equivalence follows from the fact that the isomorphism type of every finite substructure (or "type") in $H$ and $mathbb{Z}$ is expressible by a formula.

However, if I think about a direct back-and-forth argument, I'm worried about the following apparent obstruction. Say $H= H_0 cup H_1$, where $H_i$ are the paths. Suppose that one already has a partial isomorphism
${(h_0, z_0), (h_1, z_1)}$ starting a back-and-forth argument, where $h_iin H_i$. Now $mathbb{Z}$ satisfies a sentence, call it $f$, asserting that $z_0$ and $z_1$ are joined by a path of length $n$; clearly $H notmodels f$.

Did I just prove that the theory cannot not eliminate quantifiers? Sorry, I didn't mean to turn your question into another one.