pith. machine review for the scientific record. sign in

arxiv: 2605.06533 · v1 · submitted 2026-05-07 · 💻 cs.LO

Recognition: unknown

Relational Dualities and Bisimulation

Alex Kavvos, Piotr Kozicki

Authors on Pith no claims yet

Pith reviewed 2026-05-08 04:33 UTC · model grok-4.3

classification 💻 cs.LO
keywords Tarski dualityThomason dualitybisimulationrelational framesinfinitary logicKripke semanticscategorical dualityproof systems
0
0 comments X

The pith

Relational extensions of Tarski and Thomason dualities put relations between frames in correspondence with relations between their predicate algebras.

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

The paper sets out to extend standard categorical dualities so that relations on relational frames correspond to relations on the algebras of logical predicates. It constructs relational versions of Tarski duality for infinitary classical propositional logic and Thomason duality for infinitary classical modal logic. These extensions are meant to place well-behaved relations such as bisimulations on computational systems into direct correspondence with relations on the predicates that describe those systems. If successful, the dualities yield a proof system capable of relating formulae that hold in one system to formulae that hold in another.

Core claim

The paper constructs relational extensions of Tarski duality for infinitary classical propositional logic and Thomason duality for infinitary classical modal logic. These extensions establish a correspondence between relations on relational frames and relations on the algebras of logical predicates. The construction preserves the essential properties of the original dualities, so that relations between frames induce corresponding relations between predicates and thereby support a proof system that relates formulae across different systems.

What carries the argument

Relational extensions of Tarski duality and Thomason duality, which map relations on frames to relations on predicate algebras while preserving the original duality properties.

If this is right

  • Bisimulations between relational frames correspond directly to relations between the algebras of predicates on those frames.
  • A proof system is obtained that relates formulae holding in one logical system to formulae holding in another.
  • The correspondence applies to the infinitary versions of classical propositional logic and classical modal logic.
  • Well-behaved relations between systems are placed in exact correspondence with relations between their logical predicates.

Where Pith is reading between the lines

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

  • The same pattern of relational extension could be tried on dualities for other logics to obtain uniform treatments of bisimulation.
  • The resulting proof system might be used to transfer logical properties across bisimilar systems without direct semantic comparison.
  • Computational interpretations in which frames model machine states could inherit algebraic reasoning tools from the dualities.

Load-bearing premise

That relational extensions of the dualities exist while preserving the key properties of the original Tarski and Thomason dualities for the infinitary case, allowing correspondence between frame relations and predicate relations.

What would settle it

An explicit pair of relational frames and their predicate algebras in which a bisimulation on the frames fails to induce a corresponding relation on the predicates under any candidate extension of the duality.

read the original abstract

The Kripke semantics of various logics arises via categorical dualities between a category of relational frames and their maps, and a category of algebras and logical homomorphisms. When the relational frames are considered as computational systems (e.g. the states of a machine), the corresponding algebra is one of logical predicates on these systems (e.g. predicates on these states, i.e. program logics). Our aim is to extend this phenomenon to relations, putting well-behaved relations between systems (e.g. bisimulations) in correspondence with relations between predicates. This is achieved by constructing particular relational extensions of Tarski duality (for infinitary classical propositional logic) and Thomason duality (for infinitary classical modal logic). We sketch how these dualities give rise to a proof system that relates formulae between different systems.

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 constructs relational extensions of Tarski duality (for infinitary classical propositional logic) and Thomason duality (for infinitary classical modal logic). These extensions are intended to put well-behaved relations between relational frames (such as bisimulations) in correspondence with relations between the dual algebras of predicates. The manuscript sketches how the resulting dualities induce a proof system relating formulae across different systems.

Significance. If the constructions preserve the key adjunctions and object correspondences of the original dualities while adding relational structure, the work would supply a categorical bridge between frame-based and algebra-based accounts of bisimulation in infinitary logics. This could strengthen correspondence theory and provide a uniform way to derive relational proof rules from dualities, with potential applications to program logics and modal correspondence.

major comments (2)
  1. [§3] §3 (relational extension of Thomason duality): the claim that the construction preserves the original adjunction and object correspondence for infinitary modal logic is stated but not verified in detail; without an explicit check that the relational structure respects infinite conjunctions and the modal operators, the central correspondence between frame relations and predicate relations remains unestablished.
  2. [§5] §5 (induced proof system): the sketch of the proof system relating formulae between systems does not supply the explicit rules, the translation between the two sides, or a soundness argument with respect to the relational duality; this step is load-bearing for the claim that the dualities give rise to a usable proof system.
minor comments (2)
  1. Notation for the relational extensions (e.g., the functors and the lifted relations) is introduced without a consolidated table or diagram; a summary diagram would clarify the relationship to the classical Tarski and Thomason dualities.
  2. The paper should explicitly state the precise infinitary fragment under consideration (e.g., whether arbitrary or countable conjunctions are allowed) when extending the dualities, as this affects the preservation properties.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their thorough review and valuable comments on our paper. We address each major comment below and plan to incorporate the necessary revisions to strengthen the manuscript.

read point-by-point responses

  1. Referee: [§3] §3 (relational extension of Thomason duality): the claim that the construction preserves the original adjunction and object correspondence for infinitary modal logic is stated but not verified in detail; without an explicit check that the relational structure respects infinite conjunctions and the modal operators, the central correspondence between frame relations and predicate relations remains unestablished.

    Authors: We agree that the preservation of the adjunction and object correspondence requires a more detailed explicit verification, particularly regarding the handling of infinite conjunctions and modal operators. In the revised manuscript, we will add a subsection or appendix providing this verification to establish the central correspondence. revision: yes

  2. Referee: [§5] §5 (induced proof system): the sketch of the proof system relating formulae between systems does not supply the explicit rules, the translation between the two sides, or a soundness argument with respect to the relational duality; this step is load-bearing for the claim that the dualities give rise to a usable proof system.

    Authors: We recognize that the sketch in §5 lacks the explicit rules, translation, and soundness argument needed to fully support the claim. We will revise §5 to include these elements, deriving the proof rules directly from the relational duality and proving soundness. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper describes a direct categorical construction that extends the standard Tarski duality for infinitary propositional logic and Thomason duality for infinitary modal logic by adding relational structure to correspond bisimulations with predicate relations. No equations, definitions, or steps in the provided abstract or description reduce by construction to fitted parameters, self-referential definitions, or load-bearing self-citations. The central claim relies on preserving adjunctions and object correspondences from externally established dualities, with the relational extension presented as a sketch rather than a reduction to prior inputs. This is a self-contained theoretical development without the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work relies on standard category theory and existing dualities without introducing new free parameters or invented entities.

axioms (1)
  • standard math Standard axioms and properties of Tarski and Thomason dualities for infinitary logics
    The extensions presuppose the correctness of the base dualities in category theory and logic.

pith-pipeline@v0.9.0 · 5424 in / 1076 out tokens · 31368 ms · 2026-05-08T04:33:45.767396+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

12 extracted references · 12 canonical work pages

  1. [1]

    Abramsky

    1 Samson Abramsky. Domain theory in logical form.Annals of Pure and Applied Logic, 51(1):1–77, 1991.doi:10.1016/0168-0072(91)90065-T. 2Steve Awodey.Category Theory. Oxford Logic Guides. Oxford University Press,

    work page doi:10.1016/0168-0072(91)90065-t 1991

  2. [2]

    Monoidal extended stone duality

    3 Fabian Birkmann, Henning Urbat, and Stefan Milius. Monoidal extended stone duality. In Naoki Kobayashi and James Worrell, editors,Foundations of Software Science and Computation Structures, volume 14574 ofLecture Notes in Computer Science, pages 144–165. Springer Nature Switzerland, 2024.doi:10.1007/978-3-031-57228-9_8. 4 Patrick Blackburn, Maarten de R...

    work page doi:10.1007/978-3-031-57228-9_8 2024

  3. [3]

    Springer International Publishing, 2019.doi:10.1007/978-3-030-12096-2

    9 Leo Esakia.Heyting Algebras: Duality Theory, volume 50 ofTrends in Logic. Springer International Publishing, 2019.doi:10.1007/978-3-030-12096-2. 10 Mai Gehrke and Sam van Gool.Topological Duality for Distributive Lattices: Theory and Applications. Number 61 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press,

    work page doi:10.1007/978-3-030-12096-2 2019

  4. [4]

    11 Paul R

    URL:http://arxiv.org/abs/2203.03286. 11 Paul R. Halmos. Algebraic logic, I. Monadic boolean algebras.Compositio Mathematica, 12:217–249, 1954-1956. Publisher: Kraus Reprint. URL:https://www.numdam.org/item/CM_ 1954-1956__12__217_0/. 12 G. Hansoul. A duality for boolean algebras with operators.Algebra Universalis, 17(1):34–49, 1983.doi:10.1007/BF01194512. ...

    work page doi:10.1007/bf01194512 1954

  5. [5]

    Kozicki and G

    P. Kozicki and G. A. Kavvos 17 20 Bjarni Jonsson and Alfred Tarski. Boolean algebras with operators. part i.American Journal of Mathematics, 73(4):891, 1951.doi:10.2307/2372123. 21 G. A. Kavvos. Two-Dimensional Kripke Semantics I: Presheaves. In Jakob Rehof, editor, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024...

    work page doi:10.2307/2372123 1951

  6. [6]

    22 Kohei Kishida

    Schloss Dagstuhl – Leibniz-Zentrum für Informatik.doi: 10.4230/LIPIcs.FSCD.2024.14. 22 Kohei Kishida. Categories and modalities. In Elaine Landry, editor,Categories for the Working Philosopher. Oxford University Press, 2018.doi:10.1093/oso/9780198748991.003.0009. 23 Saul Kripke. Semantical Considerations on Modal Logic.Acta Philosophica Fennica, 16:83–94,...

    work page doi:10.4230/lipics.fscd.2024.14 2024

  7. [7]

    25 Saul A

    doi:10.1002/malq.19630090502. 25 Saul A. Kripke. Semantical Analysis of Intuitionistic Logic I. In J. N. Crossley and M. A. E. Dummett, editors,Formal Systems and Recursive Functions, volume 40 ofStudies in Logic and the Foundations of Mathematics, pages 92–130. Elsevier, 1965.doi:10.1016/S0049-237X(08) 71685-9. 26 Alexander Kurz, Andrew Moshier, and Achi...

    work page doi:10.1002/malq.19630090502 1965

  8. [8]

    27 Alexander Kurz and Jiri Rosicky

    doi:10.1007/978-3-031-24117-8_5. 27 Alexander Kurz and Jiri Rosicky. Strongly complete logics for coalgebras.Logical Methods in Computer Science, Volume 8, Issue 3:1231, 2012.doi:10.2168/LMCS-8(3:14)2012. 28 Alexander Kurz and Jiří Velebil. Relation lifting, a survey.Journal of Logical and Algebraic Methods in Programming, 85(4):475–499, 2016.doi:10.1016/...

    work page doi:10.1007/978-3-031-24117-8_5 2012

  9. [9]

    Mac Lane,Categories for the Working Mathematician, 2nd ed., Graduate Texts in Mathe- matics, Vol

    URL:https://ncatlab.org/nlab/files/LawvereComprehension.pdf. 30 Paul Blain Levy. Similarity quotients as final coalgebras. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures, volume 6604 ofLecture Notes in Computer Science, pages 27–41. Springer Berlin Heidelberg, 2011.doi:10.1007/ 978-3-642-19805-2_3. 31 Saunders Mac ...

    work page doi:10.1007/978-1-4757-4721-8 2011

  10. [10]

    35 Gordon D

    doi:10.1016/0304-3975(81) 90112-2. 35 Gordon D. Plotkin. A powerdomain construction.SIAM Journal on Computing, 5(3):452–487, 1976.doi:10.1137/0205035. 36 Emily Riehl.Category Theory in Context. Dover Publications,

    work page doi:10.1016/0304-3975(81 1976

  11. [11]

    jhu.edu/~eriehl/context.pdf

    URL:http://www.math. jhu.edu/~eriehl/context.pdf. 37 Giovanni Sambin and Virginia Vaccaro. Topology and duality in modal logic.Annals of Pure and Applied Logic, 37(3):249–296, 1988.doi:10.1016/0168-0072(88)90021-8. 38 Davide Sangiorgi. On the origins of bisimulation and coinduction.ACM Transactions on Programming Languages and Systems, 31(4):1–41, 2009.do...

    work page doi:10.1016/0168-0072(88)90021-8 1988

  12. [12]

    URL: https://hdl.handle.net/11370/ 13d08025-29ff-4193-a7f2-ea5bcd20f15d. 42 S. K. Thomason. Categories of frames for modal logic.The Journal of Symbolic Logic, 40(3):439–442, 1975.doi:10.2307/2272167

    work page doi:10.2307/2272167 1975