Abstract

We consider infinitary logic with only two variable symbols, both with and without counting quantifiers, i.e. L2 L∞ω2 and C2 L∞ω2mεω. The main result is that finite relational structures admit canonization with respect to L2 and C2: there are polynomial time com putable functors mapping finite relational structures to unique representatives of their equivalence class with respect to indistinguishability in either of these logics. In fact we exhibit in verses to the natural invariants that characterize structures up to L2- or C2-equivalence, respectively. As a corollary we obtain recursive presentations of the classes of all boolean queries that are closed with respect to L2- or C2-equivalence