Let $\mathfrak{S}=(M_z,U_z)_{z\in\mathbb{Z}}$ be a sequence such that for each $z\in\mathbb{Z}$ we have
$M_z\models\mathsf{ZFC}+$ "$U_z$ is a nonprincipal ultrafilter on $\omega$" (so in particular $U_z\in M_z$),
$M_{z+1}\cong\left(\prod M_z/U_z\right)^{M_z}$, and
$j_z(U_z)=U_{z+1}$ where $j_z:M_z\rightarrow \left(\prod M_z/U_z\right)^{M_z}$ is the usual ultrapower embedding.
Such sequences can be built via compactness. Note that each $M_z$ thinks that $M_{z+1}$ is not an $\omega$-model.
Now letting ${\bf Graphs}_z$ be what $M_z$ thinks is the category of nonempty simple directed graphs with weak homomorphisms (there's a lot of flexibility here, I'm just picking something and sticking with it), we have obvious faithful functors $i_z: {\bf Graphs}_{z+1}\rightarrow{\bf Graphs}_z$ for each $z\in\mathbb{Z}$; while $M_{z+1}$ and $M_z$ disagree over complicated graph-theoretic properties such as well-foundedness, everything which $M_{z+1}$ thinks is a graph/graph homomorphism "is" also a graph/graph homomorphism in $M_z$ (once appropriately translated). Abusing language a bit, let $\mathfrak{S}_{-\infty}$ be the "union" of the ${\bf Graph}_z$s along the $i_z$s. Here I'm construing a category as a structure in the sense of first-order logic in the usual way (see e.g. here).
The structure $\mathfrak{S}_{-\infty}$ is rich enough to make sense of, and verify, statements like "there are infinite edgeless graphs not in bijection with each other" and "there is no infinite connected 2-regular graph" (the key first step is that we can categorically define the one-vertex graph and the two-vertices-one-edge graph). So we have at least a hint of a non-trivial theory of infinities without a "correct" version of the natural numbers, and thinking about such was the original motivation for this construction.
My question is:
What is the first-order theory of these $\mathfrak{S}_{-\infty}$s - that is, what is (or is there) a "reasonably nice" axiomatization of the set of sentences true in each $\mathfrak{S}_{-\infty}$?
