PaperlayerView exact revision on arXiv

Source-linked AI summary

Two-Variable Logic with Arbitrarily Many Successor Relations

Jakub Michaliszyn, Piotr Witkowski

arXiv:2610.09758v1cs.LO

TL;DR

Two-variable satisfiability with arbitrarily many exact successor relations must account for models that are necessarily infinite. The paper builds finite certificates for such structures and proves 2-NEXPTIME upper bounds for general and infinite satisfiability, while identifying open boundaries for complexity and finite models.

  • Problem

    Successor constraints can destroy the finite-model property, so satisfiability must account for formulas with infinite models and no finite model.

    Source: §1 · p. 2

  • Method

    Finite certificates separate bounded-multiplicity neighbourhoods and their witness requirements from the remaining successor structure, which is realized using integer heights and dense completion.

    Source: §8 · p. 16

  • Results

    Infinite satisfiability is in 2-NEXPTIME and NEXPTIME-hard for one successor, and every satisfiable infinite case has a countably infinite model.

    Source: §6.2 · p. 13

  • Takeaways & Limitations

    The certificates provide an effective doubly exponential threshold above which a finite model guarantees an infinite one, although explicit finite cores can themselves be doubly exponentially large.

    Source: §1 · p. 3

    The exact general-satisfiability complexity gap remains open, and adapting certificates to scattered or well-founded orders or controlling finite models with three or more successors remain unresolved.

    Source: §8 · p. 16

Abstract

from arXiv · show

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.

1 Introduction

The paper establishes decidability for two-variable logic with arbitrarily many exact successor relations, including cases that require infinite models. It gives finite certificates for these models and a separate finite-model result when successor adjacency disagreement is bounded.

1 Introduction

  • Infinite models are essential: successor constraints can destroy the finite-model property, as ∀x∃y S1(x, y) has a model over Z but no finite model.An empty successor relation is also realizable on at least two elements over Q, but not in a finite admissible model.Source: §1 · p. 2
  • Satisfiability with any finite number of exact successor relations is in 2-NEXPTIME, uniformly in their number, with arbitrary unary and binary predicates; the problem is NEXPTIME-hard with one successor.Each relation is the exact immediate-successor relation of an order on the common domain; the orders may have arbitrary order types and are absent from the signature.Source: §1 · p. 2
  • A finite certificate handles shared successor neighbours and finite-multiplicity neighbourhoods while consistently meeting witness obligations involving additional binary predicates.It separates bounded-multiplicity types into an explicit interface and uses integer heights to match whole neighbourhoods without cycles; dense ordering of path components recovers exact successors.Source: §1 · p. 2
  • The exact complexity remains open between the NEXPTIME lower bound and 2-NEXPTIME upper bound, and unrestricted finite satisfiability with three or more successors remains unresolved.A sentence of polynomial size in r can force a finite set of exactly 2^(2^r)−1 elements while requiring the whole model to be infinite.Source: §1 · p. 3
  • With a budget on reference adjacencies lost across other orders, finite satisfiability is NEXPTIME-complete, even when the successor count and binary-encoded budget are inputs.The bound places no restriction on domain size; the reduction uses binary ranks with O(log(b + 2)) unary bits per relation, while a separate argument bounds model size singly exponentially in b.Source: §1 · p. 3

1.1 Related work

  • Earlier results cover finite two-successor settings [14, 6, 4] and one-forest satisfiability [2]; arbitrary order types here enable dense ordering of components after successor edges are fixed.Related work on visible orders addresses different settings, while the paper uses invisible orders to complete successor components densely.Source: §1.1 · pp. 3–4

2 Preliminaries

The preliminaries define admissible successor structures and the local descriptions used to reason about them. They also specify how binary relations label pairs and how acyclic path graphs can be completed into exact successor relations.

2 Preliminaries

  • An admissible structure has a common domain and, for each distinguished predicate, a strict linear order whose immediate-successor pairs are exactly that predicate.The orders may have arbitrary order types and are not part of the signature.Source: §2 · p. 5
  • Scott normalization preserves the domain and original predicates while adding fresh unary predicates; each existential requirement becomes a witness obligation.The normalized formula has quantifier-free matrices.Source: §2 · p. 5
  • A neighbourhood records up to 2k predecessor and successor ports; a legal mask captures one neighbour shared across one or more successor colours.For example, {1+, 2−} means the neighbour is both the S1-successor and S2-predecessor of the source.Source: §2 · p. 5
  • Unary values and diagonal binary values form 1-types, while a binary assignment records directed truth values on a pair and completes its 2-type.A binary assignment uses 2a bits for a additional binary predicates; converse symbols encode the reverse direction.Source: §2 · pp. 5–6
  • A countable functional, inverse-functional acyclic graph with infinitely many components is an exact successor graph of a linear order.The components can be indexed by Q and ordered component-first, so elements in different components are never consecutive.Source: §2 · p. 6

3 Star types of bounded multiplicity

Star types encode complete successor neighbourhoods, and a closure operation distinguishes types with bounded multiplicity from regular types. The resulting bounds determine which elements must be stored explicitly and when the remaining types can support infinite realizations.

3 Star types of bounded multiplicity

  • A star type records an element’s 1-type and complete successor neighbourhood; its rays describe distinct neighbours.Each ray stores the neighbour’s 1-type, a nonempty legal mask, and a binary assignment.Source: §3 · p. 6
  • The closure marks a type bounded when it lacks a far assignment to a realized 1-type or requires a neighbour whose type is bounded.The closure adds a type when all matches for one of its rays are already bounded.Source: §3 · p. 7
  • Bounded star types have computable multiplicity bounds, while each regular type has nonempty far assignments and a regular match for every ray.A seed type has bound d + 1; later bounds follow from injectively mapping its realizations to a ray-neighbour.Source: §3 · p. 7
  • The sum of bounded-type multiplicities is at most (d + 1)2^|P| after at most |P| closure additions.Each closure step at most doubles the running bound.Source: §3 · p. 7
  • Star types with the same source 1-type can differ in boundedness because their successor neighbourhoods differ.A type requiring a bounded predecessor becomes bounded, while another type with the same source 1-type can remain regular.Source: §3 · p. 7
  • When no regular types remain, the multiplicity bounds cover the whole domain and a finite model can be guessed explicitly.Otherwise the construction proceeds using the regular types.Source: §3 · p. 7

4 The finite certificate

The finite certificate stores bounded elements and their neighbourhoods in an interface, then describes new regular elements with rows. Witness choices coordinate obligations across both parts while preserving consistent binary assignments.

4 The finite certificate

  • A certificate combines a finite interface, rows describing other elements, and witness choices for formula obligations.Its construction from a certificate and extraction from a model are treated as converse directions.Source: §4 · p. 8, §4.2 · p. 9

4.1 The finite interface

  • The interface contains all bounded elements and their neighbours, with a pair table recording masks and binary assignments between interface elements.The core contains bounded elements; boundary elements have a core neighbour, and all core rays must be realized.Source: §4.1 · p. 8

4.2 Rows and witnesses

  • A row fixes a regular element’s star type and one consistent binary assignment to every core element.The same row assignment must work across all witness obligations; the selected rows include every regular type and at most one additional row per interface obligation.Source: §4.2 · pp. 8–9
  • Each row obligation can be witnessed by the source, a neighbour, a far regular element, or a core element.Interface obligations likewise select a core element, a free ray neighbour, or a new far element; assignments for core sources must agree with the row.Source: §4.2 · pp. 8–9

5 Certificates and models

Accepting certificates are realized as admissible models by matching successor requirements and assigning remaining binary relations. Conversely, admissible models yield certificates; when regular types are present, the construction produces a countably infinite model.

5 Certificates and models

  • The construction gives every selected row infinitely many copies, matches successor requirements, then fills far pairs to satisfy remaining obligations.The converse direction extracts the interface and rows from an admissible model.Source: §5 · p. 9, §5.3 · p. 11

5.1 Matching rays at integer heights

  • Integer height vectors match whole successor neighbourhoods simultaneously while preventing loops and directed cycles.A mask determines a displacement; matching each ray with its inverse preserves shared neighbours and makes each colour graph functional and inverse-functional.Source: §5.1 · pp. 9–10
  • The construction uses infinitely many components and dense completion to obtain exact successor relations for the resulting path graphs.Each colour has infinitely many components, and each can be ordered independently.Source: §5.1 · p. 10

5.2 Assigning far pairs

  • For remaining witness obligations, distinct far targets are chosen in a higher group, and permitted binary assignments fill all unselected far pairs.Selections cannot conflict because they increase group number; regularity ensures permitted assignments are nonempty.Source: §5.2 · p. 11

5.3 From a model to a certificate

  • An accepting certificate exists exactly when an admissible model realizes its star types, and it yields a countably infinite model when regular types are present.Every regular star type is realized infinitely often; the construction does not generally guarantee a finite model or orders of type ω.Source: §5.3 · pp. 11–12

6 Decision procedures and consequences

The decision procedure handles bounded-only and regular-type cases separately, with certificate verification giving a doubly exponential time bound. Its infinite-model branch also yields an effective size threshold and shows that explicit cores can be doubly exponential.

6.1 Satisfiability and the complexity bound

  • The algorithm guesses realized star types and their boundedness closure, then uses either an explicit finite model or an accepting certificate.The certificate branch can accept star types extracted from a finite model and construct an infinite model with the same set.Source: §6.1 · p. 12
  • Certificate guessing and checking take at most doubly exponential time, while hardness follows from ordinary FO2.The finite-model branch obeys the same time bound.Source: §6.1 · p. 12

6.2 Infinite models and an effective size threshold

  • Infinite satisfiability belongs to 2-NEXPTIME, and every sentence with an infinite admissible model has a countably infinite admissible model.The infinite-model branch is precisely the branch with at least one regular star type.Source: §6.2 · pp. 12–13
  • A finite admissible model larger than FΦ = (d + 1)2^H guarantees an infinite admissible model.The threshold bounds finite models only when no infinite model exists; it is not a general small-model property for finite satisfiability.Source: §6.2 · p. 13

How large can the core be?

  • Polynomial-size sentences can force exactly 2^(2^r) − 1 bounded elements using two successors and unary predicates.This is a model-size lower bound, not a 2-NEXPTIME hardness result.Source: How large can the core be? · p. 13

7 Finite models with bounded adjacency disagreement

For finite models, the section bounds disagreement among successor paths by lost reference adjacencies, then reduces the decision problem to finite satisfiability with one distinguished successor. The problem is NEXPTIME-complete, and satisfiable instances have a size bound depending on the budget value.

7 Finite models with bounded adjacency disagreement

  • The budget bounds the total number of reference-order edges missing from the other paths; a lost edge shared by multiple orders is counted once per order.Each summand also equals the number of added edges and half the symmetric difference, since every finite successor has |A| − 1 edges.Source: §7 · p. 13
  • Budgeted finite satisfiability is NEXPTIME-complete for binary-encoded budgets, any input number of successors, and arbitrary additional unary and binary predicates.It is also NEXPTIME-complete for unary-encoded budgets and each fixed b ≥ 0.Source: §7 · p. 14

7.1 Reduction to one successor

  • Binary rank predicates encode how each other successor path advances beyond shared S1-edges, reducing the problem to finite satisfiability with one distinguished successor.The reduction uses counting quantifiers and bounds the total guessed added-edge counts by b.Source: §7.1 · p. 14

7.2 Correctness and complexity

  • The reduction is sound and complete: monotone ranks rule out cycles, while degree and root constraints make each successor a spanning path.The NEXPTIME procedure runs in time 2^{N^{O(1)}} and need not list a model explicitly.Source: §7.2 · p. 15

7.3 The finite-model size bound

  • A model of cost at most b splits at most b lost reference edges into at most b + 1 common blocks, whose orderings determine the path boundaries.The size bound is 2^{p(|φ|+k+b)} for a fixed polynomial p, so it depends on the value of b.Source: §7 · p. 14, §7.3 · p. 15

8 Conclusion

The conclusion presents certificates for arbitrary-model satisfiability and a separate bounded-disagreement approach for finite models. It identifies unresolved questions about complexity, order types, and finite interactions among successors.

8 Conclusion

  • Finite certificates separate bounded-multiplicity local types from infinitely repeated ones, then use integer heights and dense component ordering to realize successor structure.The same certificates decide infinite satisfiability and bound every model of a sentence that has only finite models.Source: §8 · p. 16
  • For finite models, a binary budget on adjacency disagreement keeps satisfiability NEXPTIME-complete, with common blocks and binary ranks controlling successor interactions.The result is uniform in the number of successors and permits arbitrary additional unary and binary predicates.Source: §8 · p. 16
  • Open questions include closing the NEXPTIME-to-2-NEXPTIME gap, adapting certificates to scattered or well-founded orders, and handling three or more finite successors without a budget.The forced doubly exponential core does not establish a matching lower bound.Source: §8 · p. 16

Use of generative AI.

The authors report using generative AI during problem-solving and manuscript preparation, while retaining responsibility for the final work.

Use of generative AI.

  • GPT-6 Astra proposed a complex proof argument based on the authors’ initial notes.The authors say they spent substantial effort deconstructing and simplifying it.Source: Use of generative AI · p. 18
  • The authors rewrote nearly the entire proof and independently verified its mathematical correctness.Source: Use of generative AI · p. 18
  • GPT-6 Astra and GPT-6.1 SOL also assisted with proofreading, stylistic refinement, and text reduction.The authors reviewed and edited the content and accept responsibility for its final accuracy and integrity.Source: Use of generative AI · p. 18

A Scott normalization on the same domain

The normalization introduces fresh unary predicates to name quantified subformulas, producing an equivalent sentence without changing the original structure.

A Scott normalization on the same domain

B The bounded part can be doubly exponential

Polynomial-size sentences can force a doubly exponentially large finite set of bounded star types, even though every admissible model is infinite. The construction grows levels from a unique root, while the explicit-core lower bound does not imply a 2-NEXPTIME hardness result.

B The bounded part can be doubly exponential

  • For every r ≥ 1, a polynomial-size sentence forces exactly 2^(2^r)−1 T-elements in every admissible model, and every such model is infinite.The elements of T realize bounded star types.Source: B The bounded part can be doubly… · p. 19
  • A unique root and two distinct children per element yield exactly 2^j elements at level j, across levels 0 through 2^r−1.Children are distinct because they disagree on L; inverse-functionality and the L-constraint prevent different parents from sharing a child.Source: B The bounded part can be doubly… · pp. 19–20
  • The full binary tree with countably many isolated elements outside T supplies an infinite model, while no finite model can contain those isolated elements.A finite admissible successor relation is a spanning path, which has no isolated vertex when the domain has more than one element.Source: B The bounded part can be doubly… · p. 20
  • The forced finite part shows that an explicit certificate interface need not have singly exponential size, but it is not a 2-NEXPTIME hardness result.A more succinct algorithm could represent the forced part without listing all its elements.Source: B The bounded part can be doubly… · p. 20

C A worked certificate

The worked certificate illustrates how shared successor requirements, bounded elements, and binary-predicate witnesses are handled together. It reserves compatible interface witnesses, matches remaining rays at integer heights, and completes the orders without adding successor pairs.

C A worked certificate

  • With S1 = S2, the example uses an asymmetric E relation to expose both boundedness propagation and the need for multiple rows of one star type.The clauses make K nonempty and unique, impose successor and predecessor requirements, and specify E-witness obligations for K and A elements.Source: C A worked certificate · pp. 20–21
  • The closure marks pK and p0 bounded but leaves pA and pV regular, despite p0 and pV sharing a 1-type.The predecessor ray of p0 matches only pK; the closure therefore operates on star types, not just 1-types.Source: C A worked certificate · p. 21
  • The interface stores c, v0, and a0, while rows encode consistent E-assignments to the core and provide distinct choices for witnesses.The reserved a⋆ uses row r⋆ to meet the K-element’s E-obligation; v+ attaches the free successor ray at a0.Source: C A worked certificate · p. 22
  • Integer heights attach v+ at (3, 3) and reserve a⋆ at (0, 0), with a far E-witness in another group.The remaining rays are matched at displacement (1, 1); dense completion recovers the orders without adding successor pairs.Source: C A worked certificate · pp. 22–23
  • Matching the two shared rays independently would violate S1 = S2, and choosing an incompatible row for a⋆ would conflict with the required E-assignment.Agreement on a single core pair is not enough to ensure feasibility when witness obligations are strengthened.Source: C A worked certificate · p. 23
Loading 2610.09758v1…