Canonization for two variables and puzzles on the square Original Research Article

We consider infinitary logic with only two variable symbols, both with and without counting quantifiers, i.e. L2 ≔ L∞ω2 and C2 ≔ L∞ω2(∃⩾m)mϵω. The main result is that finite relational structures admit Ptime 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 Ptime in verses to the natural Ptime invariants that characterize structures up to L2- or C2-equivalence, respectively. As a corollary we obtain recursive presentations of the classes of all P time boolean queries that are closed with respect to L2- or C2-equivalence.