Summary
This work looks at a type of logical language that uses only two variables but includes multiple "next" relationships that must correspond exactly to immediate successors in some linear order. The authors prove that checking whether statements in this logic can be satisfied can be done within a very large but well-defined time complexity, even when many such successor relations are involved. They create a method that breaks down possible models into manageable pieces to decide satisfiability, providing ways to handle both finite and infinite structures. Their results also describe when large finite models guarantee infinite ones and clarify complexity limits when restricting models in certain ways.
What this means in practice
- •For automated reasoning developers: Decide satisfiability in logical systems with multiple exact successor relations efficiently using the complexity bounds provided.
- •For database query engines: Optimize queries involving sequences or chains by understanding complexity limits when handling multiple successor-like relations.
A theory result. No direct application yet.
Abstract
We study two-variable first-order logic with a finite, input-dependent number of distinguished successor relations and arbitrary additional unary and binary predicates. Each distinguished relation must be the exact immediate-successor relation of some linear order on the common domain; the orders themselves are not available in the language and may have arbitrary order types. We prove that satisfiability belongs to 2NEXPTIME, uniformly in the number of successors. The proof gives finite certificates for possibly infinite models. A closure operation separates local neighbourhood descriptions, called star types, into those of bounded multiplicity and those that can be realized infinitely often. The bounded part is represented explicitly. Outside it, integer height vectors allow overlapping successor requirements to be matched without creating cycles or unintended identifications. Ordering the resulting path components densely then recovers exact successor relations. Consistent assignments of the additional binary predicates handle witnesses involving the bounded part. The same certificates decide infinite satisfiability in 2NEXPTIME and give a doubly exponential threshold above which a finite model guarantees an infinite model. A doubly exponentially large finite core can be forced with only two successors and unary predicates. For finite models, we prove that satisfiability subject to a bound on the total number of reference adjacencies lost by the other orders is NEXPTIME-complete, even when the budget is encoded in binary and the number of successors is part of the input.