I'm working with a 2-sorted theory of graphs, and would like to express the predicate $|E| \leq |V|$. In particular, I want to be able to say $\varphi \to |E| \leq |V|$, and then apply a $0$-$1$ law to conclude almost all graphs of interest (those satisfying $\varphi$) have $|E| \leq |V|$.
There is an "obvious" approach: add a function symbol $f : E \to V$ and assert that $f$ is an injection. The issue is that my graph models would now arbitrarily choose an $f$, many of which won't be injections, even if the model does have fewer edges than vertices... So $\varphi \to \text{ isInjection}(f)$ will incorrectly report $|E| \not \leq |V|$.
There's also the issue of $0$-$1$ laws interacting badly with function symbols - the results here are a lot more delicate than I would like, so avoiding function symbols would be convenient. If there's a way to express this in some weak MSO fragment, that's also OK provided we can recover a $0$-$1$-type result.
I'm not sure what I'm asking for is even possible, but I can't disprove the existence of such a predicate either. Any help is appreciated ^_^
This can't be done, by a standard compactness argument. It's basically the same idea as showing that there is no sentence whose finite models are exactly those structures of even cardinality.
Let $A$ be the graph with two vertices and one edge, and $B$ be the complete graph on four vertices with one edge removed (so four vertices and five edges). There is a first-order sentence $\theta$ true in exactly those graphs which are a disjoint union of $A$s and $B$s, and for each $i$ there is a sentence $\eta_i$ which is true in exactly those models of $\theta$ with at least $i$-many $A$s and at least $i$-many $B$s.
Now suppose $\varphi$ expressed "$\vert E\vert\le\vert V\vert$." For $M\models\theta$, we have $M\models\varphi$ iff $M$ has at least as many $A$s as $B$s. This plus compactness means that each of the theories $$S=\{\varphi\wedge\theta\}\cup\{\eta_j:j\in\mathbb{N}\}$$ and $$T=\{\neg\varphi\wedge\theta\}\cup\{\eta_j:j\in\mathbb{N}\}$$ is satisfiable.
Now let's think about their intersection $$U=\{\theta\}\cup\{\eta_i:i\in\mathbb{N}\}.$$ It's easy to check that $U$ has exactly one countable model up to isomorphism. But $S$ and $T$ must each have at least one countable model (Lowenheim-Skolem). This yields a contradiction.