Infinitary Counting Logics: 1-sorted vs. 2-sorted framework
The answer to the question "Can we diretcly express graph canonization Grädel's way" is no.

However, we can substitute each $v&lt;w$ in a $\{E,&lt;\}$-formula with a $\{E\}$-formula (Libkin's wy) by Logical Transduction (also known as Logical Interpretation). This $\{E\}$ formula is a sentence without free variables. Hence, we can use a construction (by Grädel and Otto in the same paper) to eliminate all number variables which results in a Grädel-formula with the same number of vertex variables.