pith. sign in

arxiv: 2606.31874 · v1 · pith:D64SJXTSnew · submitted 2026-06-30 · 💻 cs.LO

Topological Logics of Path-Reachability

Aleksandr Gagarin , David Fern\'andez-Duque This is my paper

Pith reviewed 2026-07-01 02:54 UTC · model grok-4.3

classification 💻 cs.LO
keywords topological semanticsmodal logicpath-reachabilityCantor derivativeT1 topologymetric spacedecidabilityfinite model property
0
0 comments X

The pith

An axiomatic system is sound and complete for path-reachability logic in both T1 topologies and metric spaces, and decidable.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper studies a modal language that adds an Until-like path-reachability operator to the Cantor derivative modality. It supplies a single set of axioms that is sound and complete for the topological semantics on all T1 spaces and, separately, on all metric spaces. Decidability follows once an equivalent neighborhood semantics is shown to enjoy the finite model property. A weaker language that replaces the derivative with the closure operator also receives a complete axiomatization over arbitrary topological models.

Core claim

The authors exhibit an axiomatic system sound and complete both for the class of T1 topologies and for the class of all metric spaces, and establish its decidability. They also axiomatize the logic of all topological models in a weaker language obtained by substituting the closure modality for the Cantor derivative. The proofs rely on an equivalent neighborhood-like semantics that admits the finite model property.

What carries the argument

The neighborhood-like semantics, shown equivalent to the original topological semantics and used to obtain the finite model property.

If this is right

  • The same axioms are complete for metric spaces as for T1 spaces.
  • The logic is decidable.
  • The weaker language with the closure modality has a complete axiomatization over all topological models.
  • Finite models suffice to decide validity once the neighborhood semantics is in use.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Decidability may transfer to other classes of spaces once an equivalent finite-model semantics is found for them.
  • The neighborhood semantics offers a route to algorithmic checking of path properties in continuous spaces.
  • The approach separates the choice of axioms from the choice of topological class, which may simplify comparisons across different spatial logics.

Load-bearing premise

The introduced neighborhood-like semantics is equivalent to the original topological semantics.

What would settle it

A formula that is valid under the topological semantics on every T1 space but is not derivable from the given axioms, or a concrete model pair demonstrating that the neighborhood semantics and topological semantics validate different formulas.

read the original abstract

The topological semantics of modal logic has been an active area of research ever since their introduction in the 1940s, with attention shifting in recent years from standard unimodal logic to more expressive frameworks. In particular, an Until-like path-reachability modality has recently been studied in Bezhanishvili et al. (2024) in polyhedral semantics; this paper investigates its topological counterpart. Focusing on the language combining said modality with the classical Cantor derivative modality, we exhibit an axiomatic system sound and complete both for the class of T1 topologies and for the class of all metric spaces, and establish its decidability. We also axiomatize the logic of all topological models in a weaker language obtained by substituting the closure modality for the Cantor derivative. To prove our results, we introduce an equivalent neighborhood-like semantics allowing for the finite model property.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper develops a modal logic combining a path-reachability (Until-like) modality with the Cantor derivative operator. It presents an axiomatic system claimed to be sound and complete for both the class of T1 topologies and the class of all metric spaces, proves decidability by introducing an equivalent neighborhood-like semantics that admits the finite model property, and separately axiomatizes the logic of all topological models in the weaker language obtained by replacing the Cantor derivative with the closure operator.

Significance. If the central results hold, the work extends the topological semantics program to path-reachability modalities, supplying completeness theorems for two important classes (T1 and metric) and a decidability result via finite-model transfer. The neighborhood semantics construction, if verified, would be a reusable technical device for obtaining decidability in related topological logics.

major comments (2)
  1. [Abstract, §4] Abstract and §4 (neighborhood semantics): the assertion that the introduced neighborhood-like semantics is equivalent to the original topological semantics is load-bearing for the finite-model-property transfer and hence for the decidability claim. No explicit verification is supplied that the equivalence preserves the path-reachability modality and its interaction with the Cantor derivative on arbitrary T1 or metric models; if the equivalence fails on even one such model, the decidability argument does not go through.
  2. [§3] §3 (soundness/completeness): the manuscript states that the axiomatic system is sound and complete for T1 topologies and for metric spaces, yet supplies no proof sketches, counter-model constructions, or verification artifacts for either class. Because these are the two central completeness results, the absence of even outline arguments leaves the claims unexamined.
minor comments (2)
  1. [§2] Notation for the path-reachability modality is introduced without an explicit comparison table to the polyhedral Until operator of Bezhanishvili et al. (2024); a side-by-side definition would clarify the topological adaptation.
  2. [§4] The finite-model-property argument for the neighborhood semantics is stated at a high level; an explicit bound on model size or a reference to the standard filtration construction would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive report. The two major comments correctly identify places where the manuscript's presentation of key technical arguments is insufficiently detailed. We address each point below and will revise the paper accordingly.

read point-by-point responses

  1. Referee: [Abstract, §4] Abstract and §4 (neighborhood semantics): the assertion that the introduced neighborhood-like semantics is equivalent to the original topological semantics is load-bearing for the finite-model-property transfer and hence for the decidability claim. No explicit verification is supplied that the equivalence preserves the path-reachability modality and its interaction with the Cantor derivative on arbitrary T1 or metric models; if the equivalence fails on even one such model, the decidability argument does not go through.

    Authors: The referee is right that the equivalence between the original topological semantics and the neighborhood semantics must be verified explicitly for the path-reachability modality (and its interaction with the Cantor derivative) on T1 and metric models. While the manuscript asserts equivalence and uses it to transfer the finite model property, the detailed preservation argument for this modality was not supplied in §4. We will add a new subsection to §4 containing the missing verification, including the inductive argument that the path-reachability operator is preserved under the neighborhood translation for both classes of models. revision: yes

  2. Referee: [§3] §3 (soundness/completeness): the manuscript states that the axiomatic system is sound and complete for T1 topologies and for metric spaces, yet supplies no proof sketches, counter-model constructions, or verification artifacts for either class. Because these are the two central completeness results, the absence of even outline arguments leaves the claims unexamined.

    Authors: We agree that §3 states the soundness and completeness theorems for the two classes without providing even outline arguments or key proof ideas. The full proofs exist in the authors' notes but were omitted from the submitted version. In the revision we will insert concise proof sketches into §3 for both the T1 case (via canonical models adapted to T1 separation) and the metric case (via a filtration argument that respects the metric topology), together with brief indications of where counter-models are ruled out. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation self-contained against external classes

full rationale

The paper presents an axiomatic system claimed sound and complete for the external classes of T1 topologies and all metric spaces, then introduces a neighborhood-like semantics asserted equivalent to the original topological semantics in order to transfer the finite model property and obtain decidability. No quoted step reduces a prediction or completeness result to a self-definition, a fitted input, or a self-citation chain; the equivalence is introduced as a technical device whose correctness is external to the axiomatization itself. The central claims therefore rest on independent verification against the stated topological classes rather than on any internal renaming or construction that would force the outcome by definition.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the equivalence between topological and neighborhood semantics plus the standard background of modal logic and topology; no free parameters or new invented entities are introduced in the abstract.

axioms (1)
  • standard math Standard axioms and rules of modal logic with derivative operator
    The system extends classical modal logic; invoked implicitly when presenting the new axiomatic system.

pith-pipeline@v0.9.1-grok · 5670 in / 1230 out tokens · 56327 ms · 2026-07-01T02:54:00.308516+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

9 extracted references · 7 canonical work pages

  1. [1]

    In Marco Aiello, Ian Pratt- Hartmann & Johan van Benthem, editors: Handbook of Spatial Logics , Springer Netherlands, Dordrecht, pp

    Johan van Benthem & Guram Bezhanishvili (2007): Modal Logics of Space . In Marco Aiello, Ian Pratt- Hartmann & Johan van Benthem, editors: Handbook of Spatial Logics , Springer Netherlands, Dordrecht, pp. 217–298, doi:10.1007/978-1-4020-5587-4_5

    work page doi:10.1007/978-1-4020-5587-4_5 2007

  2. [2]

    The Review of Symbolic Logic 3, pp

    Guram Bezhanishvili, Leo Esakia & David Gabelaia (2010): The modal logic of stone spaces: Diamond as derivative. The Review of Symbolic Logic 3, pp. 26–40, doi:10.1017/S1755020309990335

    work page doi:10.1017/s1755020309990335 2010

  3. [3]

    In Agata Ciabattoni, David Gabelaia & Igor Sedlár, editors: Advances in Modal Logic, AiML 2024, Prague, Czech Republic, August 19-23, 2024 , College Publications, pp

    Nick Bezhanishvili, Laura Bussi, Vincenzo Ciancia, David Fernández-Duque & David Gabelaia (2024): Log- ics of Polyhedral Reachability . In Agata Ciabattoni, David Gabelaia & Igor Sedlár, editors: Advances in Modal Logic, AiML 2024, Prague, Czech Republic, August 19-23, 2024 , College Publications, pp. 187–204. Available at http://www.aiml.net/volumes/volu...

    2024

  4. [4]

    2022 , month = Nov, keywords =

    Nick Bezhanishvili, Vincenzo Ciancia, David Gabelaia, Gianluca Grilletti, Diego Latella & Mieke Massink (2022): Geometric Model Checking of Continuous Space . Logical Methods in Computer Science 18(4), doi:10.46298/LMCS-18(4:7)2022. arXiv:2105.06194. 406 Topological Logics of Path-Reachability

    work page doi:10.46298/lmcs-18(4:7)2022 2022

  5. [5]

    Oxford University Press, 01 1998

    Alexander Chagrov & Michael Zakharyaschev (1997): Modal Logic. Oxford University Press, New York, doi:10.1093/oso/9780198537793.001.0001

    work page doi:10.1093/oso/9780198537793.001.0001 1997

  6. [6]

    Sigma Series in Pure Mathematics 6, Heldermann, Berlin

    Ryszard Engelking (1989): General Topology. Sigma Series in Pure Mathematics 6, Heldermann, Berlin

    1989

  7. [7]

    arXiv:2303.07920

    Svante Janson (2023): Real trees. arXiv:2303.07920

    work page arXiv 2023

  8. [8]

    J. C. C. McKinsey & Alfred Tarski (1944): The Algebra of Topology. Annals of Mathematics, Second Series 45, pp. 141–191, doi:10.2307/2267577

    work page doi:10.2307/2267577 1944

  9. [9]

    Springer Publishing Company, Incorporated, doi:10.1007/978-3-319-67149-9

    Eric Pacuit (2017): Neighborhood Semantics for Modal Logic , 1st edition. Springer Publishing Company, Incorporated, doi:10.1007/978-3-319-67149-9

    work page doi:10.1007/978-3-319-67149-9 2017