I'm trying to put together a general picture of the expressiveness of some logics: First-Order Logics, Fixed-Point Logics, (Finite Variable) Infinitary Logics and the respected versions with Counting. (Source)
$\mathcal{L}^k_{\infty\omega}$ is infinitary logic with $k$ distinct variables and
$$\mathcal{L}^\omega_{\infty\omega} := \bigcup_{k \in \omega} \mathcal{L}^k_{\infty\omega}$$
is finite variable infinitary logic. (Analog for Counting)
This is in the context of Finite Model Theory so in general all structures are finite.
We say $\varphi$ and $\varphi'$ are equivalent if for every structure $\mathcal A$
$$ \mathcal A \models_\mathcal L \varphi \Leftrightarrow \mathcal A > \models_{\mathcal {L'}} \varphi'.$$
If for every $\mathcal L$-sentence there is a equivalent $\mathcal L'$-sentence we write
$$ \mathcal L \leqq \mathcal L'.$$
Most of the relations are relatively straight-forward. $\mathcal{L}^\omega_{\infty\omega}$ cannot express that a graph has an even number of nodes. Hence, both $\mathcal{L}_{\infty\omega}$ and $\mathcal{C}^\omega_{\infty\omega}$ are strictly stronger because they can express any predicate over finite structures.
A though one is $\mathcal{L}_{\infty\omega} \equiv \mathcal{C}_{\infty\omega}$. I think this is correct since $\mathcal{L}_{\infty\omega}$ can express every predicate, thus adding counting should not make it more powerful. This it far from a proof but at most an intuition. Any ideas?
The other one I don't know is $\mathcal{C}^\omega_{\infty\omega} \lneqq \mathcal{C}_{\infty\omega}$. Again my intuition is that it is correct: How can we express any predicate with finite variables even with Counting? Any ideas on that? Maybe an example which is not expressible in $\mathcal{C}^\omega_{\infty\omega}$?
