Succinctness of Order-Invariant Logics on Depth-Bounded Structures

TL;DR

This paper investigates the expressive power and succinctness of order-invariant logic on structures with bounded tree-depth, showing equivalences with FO and MSO and analyzing translation sizes and optimality.

Contribution

It proves that order-invariant FO and MSO have the same expressive power as FO on bounded tree-depth structures and provides size bounds for translations between these logics.

Findings

Order-invariant FO has the same expressive power as FO on bounded tree-depth structures.

Translations from order-invariant FO and MSO to FO are elementary in size and have linear quantifier alternations.

Order-invariant MSO is equivalent to FO with modulo-counting quantifiers on these structures.

Abstract

We study the expressive power and succinctness of order-invariant sentences of first-order (FO) and monadic second-order (MSO) logic on structures of bounded tree-depth. Order- invariance is undecidable in general and, thus, one strives for logics with a decidable syntax that have the same expressive power as order-invariant sentences. We show that on structures of bounded tree-depth, order-invariant FO has the same expressive power as FO. Our proof technique allows for a fine-grained analysis of the succinctness of this translation. We show that for every order-invariant FO sentence there exists an FO sentence whose size is elementary in the size of the original sentence, and whose number of quantifier alternations is linear in the tree-depth. We obtain similar results for MSO. It is known that the expressive power of MSO and FO coincide on structures of bounded tree-depth. We provide a translation from MSO to FO and we show that this translation is essentially optimal regarding the formula size. As a further result, we show that order-invariant MSO has the same expressive power as FO with modulo-counting quantifiers on bounded tree-depth structures.