We study the two-variable fragment FO^2 of first-order logic over two-dimensional structures. Formulae may employ two linear orders <=_1, <=_2, their successor relations S_1, S_2, and auxiliary predicates of any arity. Despite two decades of work, three cases of finite satisfiability in this setting were still open; we settle all three. First, finite satisfiability of FO^2 with one linear order and one successor relation, of the same or of a different order, is NExpTime-complete, even with arbitrary auxiliary predicates and constant symbols. This closes a gap left open by Manuel and Zeume (CSL 2013). As an application, a reduction based on swaps of adjacent elements shows that order-invariance and order-successor-invariance of FO^2 are coNExpTime-complete. This reproves the main result of Zeume and Harwath (LICS 2016) and settles their question on order-successor-invariance. Second, finite satisfiability of FO^2 with two linear orders is ExpSpace-hard, already without auxiliary non-unary predicates, matching the upper bound known since 2010. Our reduction combines Kieronski's encoding of alternating Turing machines with the classical fact that the pre-order and post-order traversals of a tree define its descendant relation. Third, with two linear orders and the successor of one of them, finite satisfiability is in ExpSpace even with arbitrary auxiliary predicates, improving the previous 2NExpTime bound and confirming a conjecture of Zeume and Harwath. Together with known results, our theorems show that in two dimensions, auxiliary (non-unary) predicates and constants come for free: with or without them, the complexities coincide. All our proofs are simple.

翻译：暂无翻译