Multidimensional tilings and MSO logic

TL;DR

The paper investigates the complexity of defining two-dimensional subshifts by MSO formulas and the associated languages of MSO-definable sets, organizing formulas by the number of second-order quantifier alternations in an MSO hierarchy. It establishes precise complexity bounds, showing $\mathrm{FOSUB}$ is $\Pi^0_4$-complete and that $\bar{\Pi}_n$-SUB and $\bar{\Sigma}_n$-SUB are $\Pi^1_n$-complete for all $n\ge 1$, while languages of $\bar{\Sigma}_n$-sets lie in $\Sigma^1_{n-1}$ (for $n\ge 2$) and $\Sigma^0_2$ (for $n\le 1$). The authors also demonstrate the existence of FO-definable subshifts with $\Sigma^0_2$-hard or $\Pi^0_3$-hard languages, mapping robust undecidability boundaries within multidimensional symbolic dynamics. These results illuminate the exact place of MSO definability in arithmetical and analytical hierarchies for 2D subshifts and have implications for computational tools like Griddy in handling multidimensional tilings. Overall, the work provides a comprehensive complexity landscape for MSO-definable 2D subshifts and their languages across quantifier alternation classes.

Abstract

We define sets of coulourings of the infinite discrete plane using monadic second order (MSO) formulas. We determine the complexity of deciding whether such a formula defines a subshift, parametrized on the quantifier alternation complexity of the formula. We also study the complexities of languages of MSO-definable sets, giving either an exact classification or upper and lower bounds for each quantifier alternation class.