Is non-connectedness of graphs first order axiomatizable?

Question

A recent question asked for graph properties that are first order axiomatizable but not finitely axiomatizable. Connectedness was mentioned in the context. Connectedness can be axiomatized in infinitary logic, but not in ordinary first order logic. Just take an ultraproduct of the paths $P_n$ of length $n$, $n\in\mathbb N$. The paths are connected, but the ultraproduct has exactly two vertices of degree 1 and these two are not joined by a path of any finite length. If connectedness was axiomatizable by a first order theory $\Phi$, then all the $P_n$ would satisfy $\Phi$ and hence the ultraproduct satisfies $\Phi$. But the ultraproduct is not connected, a contradiction.

I was wondering whether non-connectedness is first order axiomatizable. I guess it is not, but I don't have an argument for this right now.

An attempted proof goes as follows: Let $G_n$ be the disjoint union of two cycles of length $n$. Take an ultraproduct $H$ of the $G_n$. Now all vertices of $H$ have degree $2$ and there are no finite cycles. In other words, $H$ is the disjoint union of a family of infinite (in both directions) paths.
We were done if we could show that $H$ is elementary equivalent to the bi-infinite path (is there a notation for this graph?). I assume that this is the case, but I don't see why.

A different proof that non-connectedness is not first order axiomatizable would also be welcome (or an axiomatization).

Answer 1

Stefan's original idea is realized in the following observation, which shows that one $\mathbb{Z}$-chain is elementary equivalent to two such chains.

Theorem. The theory of nontrivial cycle-free graphs where every vertex has degree $2$ is complete.

Proof. All models of uncountable size $\kappa$ consist of $\kappa$ many $\mathbb{Z}$ chains, and hence are isomorphic. Thus, the theory is $\kappa$-categorical, and hence complete. QED

Thus, all cycle-free graphs with every vertex of degree $2$ have the same first order theory. In particular, the graph consisting of one $\mathbb{Z}$-chain is elementary equivalent to the graph consisting of any number of such $\mathbb{Z}$ chains. Since the first graph is connected and the latter are not, it follows that neither connectivity nor disconnectivity are first-order expressible as theories in the language of graph theory.

Answer 2

The class of non-connected graphs is not axiomatizable. To see this, consider $\mathbb{Z}$ as a graph with $i$, $j$ connected by an edge if and only if $|i-j|=1$. Then a simple compactness argument yields a non-connected graph $\Gamma$ such that $\Gamma$ is elementarily equivalent to $\mathbb{Z}$; ie $\Gamma$ and $\mathbb{Z}$ satisfy precisely the same first order sentences. Since $\mathbb{Z}$ is connected and $\Gamma$ is non-connected, the result follows.

Answer 3

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_i\in 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 \not\models f$.

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