arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2610.19943

Finite Satisfiability of Two-Variable Logic with Arbitrarily Many Successors

Artur Jeż·Jakub Michaliszyn·Piotr Witkowski
View original source ↗Read source document ↗Export metadata ↓

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.

Explore related subjects

cs.LO

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Artur Jeż, Jakub Michaliszyn, Piotr Witkowski. 2026-10-14. Finite Satisfiability of Two-Variable Logic with Arbitrarily Many Successors. https://arxiv.org/abs/2610.19943

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Algorithmic Unverifiability of Safety for Fixed and Recursively Self-Improving Systems

Existing impossibility results for AI verification concern a fixed system. Self-modifying systems (agents that rewrite their own code, recursive self-improvement loops) raise a different question: can a safety property that holds now be certified, in advance, to keep holding after the system rewrites itself? We model one step of self-modification as a total computable transformation of code, and preservation as 'safe now and safe after the step'. If the transformation depends only on behaviour, preservation is Rice's theorem one level up; if it reads the code, as self-modification does, preservation is no longer semantic, yet at least as hard as the halting problem, by the same s-m-n reduction carried out inside a class of behaviourally identical programs. One step is never harder than the property; persistence along the whole trajectory can be one arithmetical level higher. No tower of supervisors lowers the problem; every total supervisor errs on a set of systems it cannot locate. Every faithful scheme certifying on finite behavioural evidence admits, for properties not settled by any finite set of inputs, an evolution trace it certifies at every stage while the property is violated. Statically, we record the classical limits (Rice, Goedel, Trakhtenbrot) and add the resource face: over succinctly described finite environments, verifying a policy against an adversary is coNP-complete and synthesising one PSPACE-complete. These limits do not say self-modifying systems are unsafe; they locate where algorithmic guarantees break, at the expressivity a general system needs: Turing-completeness and unrestricted self-modification. What survives is exact: a monitor detects the first violation of a safety property, and no sound procedure certifies all safe systems; certification requires restricting rewrites by design; and a frozen reference keeps the question well posed.

cs.LO↗
arXiv2026

Cover Semantics for Intuitionistic Modalities

Intuitionistic modal logic (IML) has inspired several developments in programming languages including modal type systems for staging, computational effects and language-based security. IMLs are typically studied using Kripke-style relational semantics, which simplifies proofs of meta-theoretic properties, such as completeness and consistency, by making it easy to construct models. Kripke-style relational semantics, however, relies upon classical reasoning principles, which makes it unappealing from a computational perspective and unsuitable for formalization in a constructive type theory. Goldblatt provides an alternative semantics for IMLs by extending Beth-Kripke-Joyal-style "cover" semantics for intuitionistic propositional logic with relations to support modalities. Goldblatt's "relational cover" semantics overcomes classical reasoning but introduces a new limitation: it relies upon a "modal localization" condition that restricts the class of models and complicates model construction. Goldblatt bypasses this restriction by using intricate order-theoretic completion arguments to prove completeness. In this article, we present a conservative extension of relational cover semantics that alleviates this restriction and is amenable to simpler and standard model construction techniques. We formalize our semantics in Agda and prove completeness constructively in the style of Normalization by Evaluation for a variety of IMLs featuring independent box and diamond modalities.

cs.LO↗
arXiv2026

Formalizing Flag Algebras in Lean

Razborov's flag algebra method is one of the most successful tools for proving asymptotic density inequalities in extremal graph theory. It reduces an inequality about all large graphs avoiding a forbidden pattern to finitely many algebraic conditions, and a certificate satisfying them can be found by semidefinite programming. We formalize the method for finite simple graphs in Lean 4, building on Mathlib. The formalization covers flags and their densities, the flag algebra as a quotient vector space, positive homomorphisms as limits of graph sequences, Razborov's random extensions, and the downward operator that averages out labels. On top of this theory, we build verified computation of flag densities and a tactic that turns certificates found by semidefinite programming into Lean proofs. The certificate serves only as candidate data; Lean checks every fact the proof uses. With this development we verify seven Turán-type upper bounds. Adding lower-bound constructions proved in Lean yields the asymptotic form of Mantel's theorem and the asymptotic Erdős pentagon theorem $π(C_5;K_3)=24/625$; to our knowledge, the latter has not previously been formalized in a proof assistant. We also prove two inequalities of Goodman. All density theorems reported here depend only on the standard axioms of Lean's logic. Formalization also led us to treat forbidden subgraphs with a different semantics. Instead of building a separate flag algebra for each forbidden family, we keep a single algebra of all graphs and impose the constraint only when interpreting an inequality, through randomly labeled limits of graphs satisfying it. We prove that this ensemble semantics yields the intended density bounds, and that a condition we call root-plantability characterizes when it agrees with the standard semantics.

cs.LO↗