2 Add the fact that the two classes are known to differ.

It is not the case. As an example, the following paper:

Kouck´y, M., Lautemann, C., Poloczek, S., Th´erien, D.: Circuit lower bounds via Ehrenfeucht-Fraiss´e games, 2006.

shows that, over words, FO[+, $\times$] with 2 variables is equivalent to AC$^0$ with linear size circuits --- while FO[+, $\times$] is equivalent to the whole class AC$^0$.

Those two classes are known to differ (S. Chaudhuri and J. Radhakrishnan: Deterministic restrictions in circuit complexity, 1996).

1

It is not the case. As an example, the following paper:

Kouck´y, M., Lautemann, C., Poloczek, S., Th´erien, D.: Circuit lower bounds via Ehrenfeucht-Fraiss´e games

shows that, over words, FO[+, $\times$] with 2 variables is equivalent to AC$^0$ with linear size circuits --- while FO[+, $\times$] is equivalent to the whole class AC$^0$.