Expressiveness of Infinitary Logic 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
&gt; \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}$?
There is a famous example of Cai, Fürer and Immerman, which shows that the $\mathcal{C}_{\infty\omega}^k$-hierarchy is strict and in particular that $\mathcal{C}_{\infty\omega}^\omega$ cannot express every query on finite structures. The paper is quite famous because it disproved a conjecture that IFP+C captures PTIME. Your proof that $\mathcal{L}_{\infty\omega}\equiv\mathcal{C}_{\infty\omega}$ is correct.