Finite Satisfiability of Two-Variable Logic with Arbitrarily Many Successors

Abstract

We study finite satisfiability of two-variable first-order logic over structures equipped with an arbitrary finite number of independent successor relations of linear orders. The number of successor relations is part of the input, and the vocabulary may contain further unrestricted unary and binary relations. We prove decidability in deterministic doubly exponential space together with a triply exponential bound on the size of a smallest finite model. This settles the unrestricted finite case beyond two successors.