A recent 
[question](https://mathoverflow.net/questions/36956/graph-properties-and-fol)
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).



Is non-connectedness of graphs first order axiomatizable?
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.


