Question:
A graph G is a 3-sparse graph if in every finite subgraph of $G$, the number of edges is at most 3 times the number of vertices. Prove that there doesn't exist a statement over the signature ${E^2}$ in first order logic which is valid in G iff G is a 3-sparse graph.
(I guess E means the relation of an edge in the graph)
Proof attempt
I'm trying to work with the compactness theorem ad absurdum schema.
Assume by contradiction that such a formula DOES exist and call it $b$
Denote the formula $a_{r,n}= \exists x_1...x_n \bigvee _{I \in A_r} \bigwedge _{(i,j)\in I} E(i,j)$, with the set $A_r= \lbrace K\subseteq [n]\times [n] : |K|=r \rbrace$ - which means that G has a subgraph with r edges over n nodes.
Define $T= \lbrace \neg a_{r,n} | r,n\in \mathbb N^+ \rbrace \cup ${b}.
T isn't satisfiable because it means that there are no subgraphs with any number of edges in G, while at the same time it means that G is 3-sparse.
$T$ is satisfiable from the compactness theorem because: let $T'\subset T$ a finite subset. $T'$ is satisfiable because if it includes a subset of the a's then it can be satisfied by a graph that has no edges. If $T'$={b} then it can be satisfied by a 3-sparse graph. If $T'$ is a mixture of those then it can be satisfied by a 3-sparse graph whose all subgraphs have more edges and vertices than the maximal r,n that appear in $T'$.
Therefore {b} cannot exist as T creates a contradiction.
I'm wondering if this idea is correct, I feel that this double-index definition is shaky, and also I think this might not work for 0 (that's why I've used $\mathbb N^+$) - and I don't know if this use doesn't mess the proof up.
There is no issue in general with a recursive set of axiom scheme defined with two indices. However, here one is sufficient.
The statement $a_{r,n}$ says there is a subset of $n$ vertices that has at least $r$ edges. Now a graph is 3-sparse if there is no subset with at least $3n$ edges, equivalently $\neg a_{r,n}$ for the smallest $ r \geq 3n$. So we can write $a'_n$ for the $a_{r,n}$ with the smallest such $r$. We can start at $n=7$ because ${n \choose 2} \geq 3n$ implies $n\geq 7$.
Now consider $T = \{\neg a'_n \mid n \geq 7\} \cup \{\neg b\}$. It says "the graph is not 3-sparse, and no subset of $n$ vertices has at least $3n$ edges".
Every finite subset $t$ of $T$ has a model, since you take the biggest $n^*$ such that $a'_{n^*}$, and you build a graph which has a subset of $n^*+1$ vertices with at least $3(n^*+1)$ edges, and no subset of at most $n^*$ vertices violates $a'_{n^*}$. As you observe, since by compactness $T$ has a model, $b$ cannot be defined in first-order logic.
The prototype of a similar proof is the undefinability of connectedness, which can be found in Spencer's 'Strange logic of random graphs'. Note that if you are interested of definability in the finite, you can't use compactness and can then rely on Ehrenfeucht-Fraïssé games to prove first-order undefinability.