We now formally define the notion of first order convergence.
This notion can be used for all relational structures and beyond, e.g., matroids [1]},
however, for simplicity, we limit our exposition to graphs, which may (but need not) be directed and edge-colored.
In particular, in the case of 2-edge-colored \(k\) -trees, we have \(k+2\)  binary relations,
\(k\)  of them encoding the relation between vertices and their \(i\) -parents, \(i\in [k]\) , and two encoding the edge-coloring.
If \(\psi \)  is a first order formula with \(\ell \)  free variables and \(G\)  is a (finite) graph,
then the Stone pairing \(\langle \psi ,G\rangle \)  is the probability that
a uniformly chosen \(\ell \) -tuple of vertices of \(G\)  satisfies \(\psi \) .
A sequence \((G_n)_{n\in {\mathbb {N}}}\)  of graphs is first order convergent
if the limit \(\lim \limits _{n\rightarrow \infty }\langle \psi ,G_n\rangle \)  exists for every first order formula \(\psi \) .
Every sequence of graphs has a first order convergent subsequence, see e.g. [2]}, [3]}, [4]}.
