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).