There are two ways to extend infinitary logic with counting:
We extend $L_{\infty\omega}$ by introducing a counting existential quantifier:
$$ \mathcal{A} \models \exists^{\geq m} x \varphi(x) \Leftrightarrow \textrm{There are at least $m$ $a \in A$ s.t. } \mathcal{A} \models \varphi(a).$$
Introducing such a quantifier for $\mathsf{FO}$ does not increase the expressive power because can easily define it with the usual $\exists$-quantifiers. However, $C^1_{\infty\omega} \not\leq L_{\infty\omega}$ (One variable is sufficient to express that $|A|$ is even in $C_{\infty\omega}$ yet it is not definable in $L_{\infty\omega}$).
We define a two-sorted framework. We have two kinds of variables now
- Number variables in $N^A = \{ x \in \mathbb{N} \mid 0 \leq x \leq |A|-1\}$
- Vertex variables (the old type) in $A$
Additionally, we have the natural ordering on the numbers. Furthermore, we introduce
$$ \#x.\varphi \in N^A$$
which represent the numeric value how many $x \in A$ satisfy $A \models \varphi(x)$.
Libkin's way is at least as expressive as Grädel's way, since for $\exists^{\geq m} x \varphi(x)$ we write
$$ \#x.\varphi \geq m.$$
Im trying to define Graph Canonization with Infinitary Counting Logics with finitely many variables. Libkin's way is easier on first glance since we have free numerical variables which can represent graph nodes, edges and so on. Graph Canonization with Fixed-Point Logics works very similar. However, for the Grädel way there are a lot of results like $k$-Pebble-Games and a connection the $k$-dimensional Weisfeiler-Lehman Algorithm which is a direct connection to the Graph-Isomorphism Problem.
Are the Libkin way and the Grädel way equivalent in expressiveness? Do the mentioned results work with the Libkin way? Are their respective restrictions with $k$ variables equivalent? How do I count the variables for the Libkin approach (numerical variables + vertex variables?)?
Any ideas how to define Graph Canonizations with the Grädel way?
