A new formal logic links spatial reachability with motion through geometric spaces, setting out axiomatic systems that are sound and complete for corresponding topological, finite, Alexandroff and polyhedral model classes. In ordinary terms, the rules are designed to match exactly what is valid in each specified kind of model when the dynamics is invertible.
The paper also states completeness for a rotational subclass of the polyhedral models. Its aim is to bring together polyhedral semantics, spatial reachability and invertible dynamics in one formal framework, rather than treating those ingredients as separate questions.
The logic starts with a space
The formal models use a polyhedron as the underlying space and polyhedral sets as the admissible regions. The spatial modality is interpreted as interior, while the reachability operator describes passage through a region where one formula holds until reaching a point where another formula holds.
Time is added through a PL-homeomorphism and its inverse. That gives the formal language temporal modalities for both directions of the same reversible transformation. The study considers these h-dynamic extensions alongside the underlying reachability logics.
The scope covers topological, finite, Alexandroff and polyhedral reachability logics, together with their h-dynamic versions. The claimed results are therefore tied to named classes of spaces and transformations, rather than presented as a single unrestricted rule system.
Keeping the geometry intact
A key structural result concerns the regions themselves. The collection of polyhedral subsets forms a Boolean algebra and remains closed under interior and closure. In practical terms, the basic logical operations used by the system stay within the family of sets allowed by the polyhedral semantics.
The same kind of control holds for reachability. For polyhedral inputs, the truth set produced by the reachability operator remains polyhedral. A truth set is simply the collection of points at which a formula is true, so this result says that applying reachability does not take the interpretation outside the permitted geometric setting.
The paper also gives a structural transformation for formulas. Every formula can be translated into a provably equivalent form in which temporal operators occur only on propositional variables. The translation preserves the formula's formal meaning while putting its temporal content into a restricted shape.
From formulas to moving models
Model construction supplies another part of the result. When the starting model is finite, the construction preserves finiteness; when it has the Alexandroff property, the constructed model preserves that property as well. These preservation results allow the dynamic extensions to retain the relevant features of the original classes.
For the polyhedral case, satisfiability in a polyhedral model can be lifted to an h-dynamic polyhedral model whose dynamics is a rotation. This connects the formula-level translation with an explicit kind of geometric motion rather than leaving the temporal component purely symbolic.
Taken together, the theorem package has two directions. Soundness means that the axiomatic systems remain valid in their corresponding h-dynamic classes. Completeness means that the systems capture the formulas that are valid in those classes. The paper states both properties for the listed classes, including the rotational polyhedral subclass.
A precise boundary remains
The strongest claims have a clear boundary: the temporal setup uses an invertible map and its inverse. Completeness of the past-free fragment for continuous dynamics that is not necessarily invertible is left as a conjecture. Moving from reversible evolution to potentially one-way evolution therefore remains an unanswered part of the programme.
The paper identifies a separate challenge in an infinitary eventually operator. Its semantics involves an infinite union, and that union need not produce a polyhedral set. As a result, the closure properties established for the finite polyhedral operations do not resolve this infinitary case, which remains open.
The supplied document is an arXiv preprint, version 1, dated 26 Aug 2026. Its contribution is presented as a formal axiomatization and model-construction programme for the stated classes, with the unresolved cases marking the limits of the current results.
Paper data and sources
Original title: Dynamic Polyhedral Logic
Authors: Nick Bezhanishvili, Laura Bussi, Vincenzo Ciancia et al.
Journal/Repository: arXiv
Status: Preprint, not yet peer-reviewed
First online: 2026-08-26
DOI: Not available
Original paper · Full text