Modulo-Counting First-Order Logic on Bounded Expansion Classes

TL;DR

This paper demonstrates that on bounded expansion classes, first-order logic with modulo counting can be reduced to existential first-order logic in linear time, enabling efficient model checking and set size computations.

Contribution

It proves the equivalence of modulo-counting first-order formulas to existential formulas on bounded expansion classes, with applications to transductions, graph minors, and matrix calculus.

Findings

Modulo-counting FO logic reduces to existential FO logic in linear time.

First-order transductions with modulo counting have the same power as existential transductions.

Model checking and set size computation in modulo-counting FO are linear-time on bounded expansion classes.

Abstract

We prove that, on bounded expansion classes, every first-order formula with modulo counting is equivalent, in a linear-time computable monadic expansion, to an existential first-order formula. As a consequence, we derive, on bounded expansion classes, that first-order transductions with modulo counting have the same encoding power as existential first-order transductions. Also, modulo-counting first-order model checking and computation of the size of sets definable in modulo-counting first-order logic can be achieved in linear time on bounded expansion classes. As an application, we prove that a class has structurally bounded expansion if and only if it is a class of bounded depth vertex-minors of graphs in a bounded expansion class. We also show how our results can be used to implement fast matrix calculus on bounded expansion matrices over a finite field.