pith. sign in

arxiv: 2606.31887 · v1 · pith:ET6MLTN6new · submitted 2026-06-30 · 💻 cs.LO

Uniform Interpolation of Basic Tense Logic

Katsuhiko Sano (Hokkaido University) This is my paper

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

classification 💻 cs.LO
keywords uniform interpolationbasic tense logicmodal logiclayered bisimulationconverse modalityKripke semanticsinterpolation theorem
0
0 comments X

The pith

Basic tense logic has the uniform interpolation property.

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

This paper proves that basic tense logic possesses the uniform interpolation property. Basic tense logic adds a converse modality to basic modal logic, with the accessibility relation defined as the reverse in Kripke models. The proof extends Visser's layered bisimulation argument to cover both directions of the relation. If the extension succeeds, the property holds for this logic introduced by Prior. A reader would care because it supplies the missing case for two-way modal logics.

Core claim

This paper establishes the uniform interpolation theorem for basic tense logic by extending Visser's semantic argument formulated in terms of layered bisimulation to the converse accessibility relation.

What carries the argument

Layered bisimulation construction adapted to the converse accessibility relation in Kripke models.

If this is right

  • Basic tense logic satisfies uniform interpolation.
  • The layered bisimulation method generalizes from one-way modal logic to two-way variants.
  • No extra frame conditions are imposed by the result.
  • The uniform interpolation property is preserved under addition of the converse operator.

Where Pith is reading between the lines

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

  • The same adaptation might apply to other operators in temporal logics.
  • This could support algorithms that compute uniform interpolants for tense logic formulas.
  • Comparisons of interpolation strength become possible across modal logics with and without converse.

Load-bearing premise

Visser's layered bisimulation construction extends directly to the converse accessibility relation without requiring additional semantic conditions or adjustments.

What would settle it

A concrete formula in basic tense logic that lacks any uniform interpolant in the common variables would disprove the theorem.

Figures

Figures reproduced from arXiv: 2606.31887 by Katsuhiko Sano (Hokkaido University).

Figure 1
Figure 1. Figure 1: A model M in the proof of Lemma 7.8, with reflexive loops and transitive compositions omitted. The following result extends Ghilardi and Zawadowski’s [23] theorem on the failure of the uniform interpolation property in S4 to a tense-logical setting. Our proof builds upon the one given in [43, Theorem 16.4], which provides an alternative proof of their theorem. The model used in our proof (see [PITH_FULL_I… view at source ↗
read the original abstract

This paper establishes the uniform interpolation theorem for basic tense logic, which is also known as two-way modal logic or modal logic with converse. First introduced by Arthur Prior, basic tense logic is a syntactic expansion of basic modal logic with a converse modality. Its corresponding accessibility relation is defined as the converse of the standard accessibility relation in a given Kripke model. Although basic tense logic has been widely studied since its introduction, its uniform interpolation property has yet to be fully established. For basic modal logic K, Albert Visser (1996) provided a semantic argument formulated in terms of layered (or bounded) bisimulation, explicitly attributing the uniform interpolation property of K to Silvio Ghilardi. This paper extends Visser's semantic argument to demonstrate that basic tense logic also enjoys the uniform interpolation 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

1 major / 2 minor

Summary. The paper claims to establish the uniform interpolation theorem for basic tense logic (K_t) by extending Visser's 1996 layered-bisimulation semantic argument from basic modal logic K, taking the accessibility relation to be bidirectional to accommodate the converse (past) modality introduced by Prior.

Significance. If the extension holds, the result fills a documented gap for tense logic and shows that the layered-bisimulation technique scales symmetrically to two-way models without new semantic conditions or parameters. The argument is presented as a direct adaptation of an existing, non-circular construction.

major comments (1)
  1. [proof of the main theorem (around the extension of the layered bisimulation)] The central claim rests on the assertion that Visser's construction extends directly once accessibility is made bidirectional. The manuscript should include an explicit check (perhaps in the proof of the main theorem) that the bisimulation clauses for the converse modality preserve the layered depth bounds and the interpolation extraction step; without this verification the adaptation step remains unexamined even if the one-directional case is sound.
minor comments (2)
  1. [Introduction / abstract] The abstract and introduction cite Visser (1996) and Ghilardi but do not give a precise pointer to the theorem or section of Visser's paper that is being adapted; adding the reference would aid readers.
  2. [preliminaries] Notation for the two accessibility relations (R and R^{-1}) and the corresponding modalities should be introduced once and used consistently; occasional shifts between 'future'/'past' and 'forward'/'backward' reduce clarity.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the detailed reading and the helpful suggestion regarding the proof presentation. We address the comment below and will revise accordingly.

read point-by-point responses

  1. Referee: [proof of the main theorem (around the extension of the layered bisimulation)] The central claim rests on the assertion that Visser's construction extends directly once accessibility is made bidirectional. The manuscript should include an explicit check (perhaps in the proof of the main theorem) that the bisimulation clauses for the converse modality preserve the layered depth bounds and the interpolation extraction step; without this verification the adaptation step remains unexamined even if the one-directional case is sound.

    Authors: We agree that an explicit verification would make the adaptation clearer. In the revised manuscript we will insert, immediately after the statement of the main theorem, a short paragraph that checks the two required properties: (i) that the additional bisimulation clause for the converse modality respects the layered depth bound (by symmetry with the forward clause), and (ii) that the interpolation extraction step carries over verbatim once the accessibility relation is treated as bidirectional. The argument relies only on the fact that the layered bisimulation relation is defined symmetrically for both directions and that the depth bound is preserved under the converse relation; no new semantic parameters are introduced. revision: yes

Circularity Check

0 steps flagged

No significant circularity; derivation extends external semantic argument

full rationale

The paper's central result is an extension of Visser's 1996 layered-bisimulation argument (explicitly attributed to Ghilardi) from modal logic K to basic tense logic K_t. The construction is described as carrying over once the accessibility relation is treated as bidirectional, with no equations, parameters, or definitions that reduce the target theorem to the paper's own inputs by construction. No self-citations appear; the cited sources are independent prior work. The argument is therefore self-contained against the external benchmark of Visser's construction and does not exhibit any of the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The claim rests on standard Kripke semantics for tense logic and the validity of extending the bisimulation argument; no new free parameters or invented entities are introduced.

axioms (1)
  • domain assumption Kripke models with converse accessibility relation for the tense modalities
    The paper assumes the standard semantic definition where the accessibility for the converse modality is the inverse of the forward relation.

pith-pipeline@v0.9.1-grok · 5652 in / 1072 out tokens · 56558 ms · 2026-07-01T02:32:22.744421+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

45 extracted references · 23 canonical work pages · 1 internal anchor

  1. [1]

    Akbar Tabatabai, R

    A. Akbar Tabatabai, R. Iemhoff & R. Jalali (2022): Uniform Lyndon interpolation for intuitionistic mono- tone modal logic . In D. Fernández-Duque, A. Palmigiano & S. Pinchinat, editors: Advances in Modal Logic, 14, Colledge Publications, pp. 77–96. Available at http://www.aiml.net/volumes/volume14/ 09-AkbarTabatabai-Iemhoff-Jalali.pdf

    2022

  2. [2]

    Akbar Tabatabai, R

    A. Akbar Tabatabai, R. Iemhoff & R. Jalali (2024): Uniform lyndon interpolation for basic non-normal modal and conditional logics. Journal of Logic and Computation, doi:10.1093/logcom/exae057. 672 Uniform Interpolation of Basic Tense Logic

    work page doi:10.1093/logcom/exae057 2024

  3. [3]

    van Benthem (1991): The Logic of Time, 2 edition

    J. van Benthem (1991): The Logic of Time, 2 edition. Synthese Library 156, Reidel, Dordrecht

    1991

  4. [4]

    arXiv (2023)

    N. Bezhanishvili, B. ten Cate & R. Iemhoff (2025): Six Proofs of Interpolation for the Modal Logic K, doi:10.48550/ARXIV .2510.16398

    work page internal anchor Pith review doi:10.48550/arxiv 2025

  5. [5]

    Bílková (2007): Uniform Interpolation and Propositional Quantifiers in Modal Logics

    M. Bílková (2007): Uniform Interpolation and Propositional Quantifiers in Modal Logics. Studia Logica 85, pp. 1–31, doi:10.1007/s11225-007-9021-5

    work page doi:10.1007/s11225-007-9021-5 2007

  6. [6]

    Blackburn (1990): Nominal Tense Logic and Other Sorted Intensional Frameworks

    P. Blackburn (1990): Nominal Tense Logic and Other Sorted Intensional Frameworks. Ph.D. thesis, Centre for Cognitive Science, University of Edinburgh

    1990

  7. [7]

    Blackburn, M

    P. Blackburn, M. de Rijke & Y . Venema (2001): Modal Logic. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge

    2001

  8. [8]

    Blackburn, T

    P. Blackburn, T. Braüner & J. L. Kofod (2023): An Axiom System for Basic Hybrid Logic with Propositional Quantifiers. In: Logic, Language, Information, and Computation, Springer Nature Switzerland, pp. 118–134, doi:10.1007/978-3-031-39784-4_8

    work page doi:10.1007/978-3-031-39784-4_8 2023

  9. [9]

    P. R. Blackburn, T. Braüner & J. L. Kofod (2020): Remarks on Hybrid Modal Logic with Propositional Quantfiers. In P. Hasle, D. Jakobsen & P. Øhrstrøm, editors: The Metaphysics of Time: Themes from Prior, Logic and Philosophy of Time 4, Aalborg Universitetsforlag, pp. 401–426

    2020

  10. [10]

    J. P. Burgess (1984): Basic Tense Logic. In D. Gabbay & F. Guenthner, editors: Handbook of Philosophical Logic, II, Reidel, Dordrecht, pp. 89–133

    1984

  11. [11]

    ten Cate (2005): Model theory for extended modal languages

    B. ten Cate (2005): Model theory for extended modal languages . Ph.D. thesis, University of Amsterdam, Institute for Logic, Language and Computation

    2005

  12. [12]

    ten Cate, E

    B. ten Cate, E. Franconi & I. Seylan (2013): Beth Definability in Expressive Description Logics. Journal of Artificial Intelligence Research 48, pp. 347–414, doi:10.1613/jair.4057

    work page doi:10.1613/jair.4057 2013

  13. [13]

    Chagrov & M

    A. Chagrov & M. Zakharyaschev (1997): Modal Logic. Oxford Logic Guides 35, Oxford Science Publica- tions, Oxford

    1997

  14. [14]

    D’Agostino (2008): Interpolation in non-classical logics

    G. D’Agostino (2008): Interpolation in non-classical logics . Synthese 164(3), pp. 421–435, doi:10.1007/s11229-008-9359-x

    work page doi:10.1007/s11229-008-9359-x 2008

  15. [15]

    D’Agostino & G

    G. D’Agostino & G. Lenzi (2015): Bisimulation quantifiers and uniform interpolation for guarded first order logic. Theoretical Computer Science 563, pp. 75–85, doi:10.1016/j.tcs.2014.08.015

    work page doi:10.1016/j.tcs.2014.08.015 2015

  16. [16]

    D’Agostino, G

    G. D’Agostino, G. Lenzi & T. French (2006):µ-programs, uniform interpolation and bisimulation quantifiers for modal logics. Journal of Applied Non-Classical Logics 16(3-4), pp. 297–309, doi:10.3166/jancl.16.297- 309

    work page doi:10.3166/jancl.16.297- 2006

  17. [17]

    L. Fang, Y . Liu & H. van Ditmarsch (2019): Forgetting in multi-agent modal logics. Artificial Intelligence 266, pp. 51–80, doi:10.1016/j.artint.2018.08.003

    work page doi:10.1016/j.artint.2018.08.003 2019

  18. [18]

    34 SEAN COTNER [Ken87] S

    H. Férée, I. van der Giessen, S. van Gool & I. Shillito (2024): Mechanised Uniform Interpolation for Modal Logics K, GL, and iSL. In: Automated Reasoning, Springer Nature Switzerland, pp. 43–60, doi:10.1007/978- 3-031-63501-4_3

    work page doi:10.1007/978- 2024

  19. [19]

    Fine (1975): Normal forms in modal logic

    K. Fine (1975): Normal forms in modal logic. Notre Dame Journal of Formal Logic 16(2), pp. 229–237, doi:10.1305/ndjfl/1093891703

    work page doi:10.1305/ndjfl/1093891703 1975

  20. [20]

    T. N. French (2006): Bisimulation Quantifiers for Modal Logics . Ph.D. thesis, The University of Western Australia

    2006

  21. [21]

    D. M. Gabbay, I. M. Hodkinson & M. Reynolds (1994): Temporal Logic: Mathematical Foundations and Computational Aspects. Oxford Logic Guides 1, Oxford University Press

    1994

  22. [22]

    Ghilardi & M

    S. Ghilardi & M. Zawadowski (1995): A sheaf representation and duality for finitely presented Heyting algebras. Journal of Symbolic Logic 60(3), pp. 911–939, doi:10.2307/2275765

    work page doi:10.2307/2275765 1995

  23. [23]

    Ghilardi & M

    S. Ghilardi & M. Zawadowski (1995): Undefinability of propositional quantifiers in the modal system S4 . Studia Logica 55(2), pp. 259–271, doi:10.1007/bf01061237

    work page doi:10.1007/bf01061237 1995

  24. [24]

    Goldblatt (1992): Logics of Time and Computation, 2 edition

    R. Goldblatt (1992): Logics of Time and Computation, 2 edition. CSLI Publications. K. Sano 673

    1992

  25. [25]

    Harel, D

    D. Harel, D. Kozen & J. Tiuryn (2000): Dynamic Logic. MIT press

    2000

  26. [26]

    Iemhoff (2019): Uniform interpolation and the existence of sequent calculi

    R. Iemhoff (2019): Uniform interpolation and the existence of sequent calculi . Annals of Pure and Applied Logic 170(11), p. 102711, doi:10.1016/j.apal.2019.05.008

    work page doi:10.1016/j.apal.2019.05.008 2019

  27. [27]

    Kamp (1968): Tense Logic and the Theory of Linear Order

    H. Kamp (1968): Tense Logic and the Theory of Linear Order . Ph.D. thesis, University of California, Los Angeles, CA, USA

    1968

  28. [28]

    Kurahashi (2020): Uniform Lyndon interpolation property in propositional modal logics

    T. Kurahashi (2020): Uniform Lyndon interpolation property in propositional modal logics . Archive for Mathematical Logic 59(5-6), pp. 659–678, doi:10.1007/s00153-020-00713-y

    work page doi:10.1007/s00153-020-00713-y 2020

  29. [29]

    T. Lyon, A. Tiu, R. Goré & R. Clouston (2020): Syntactic Interpolation for Tense Logics and Bi- Intuitionistic Logic via Nested Sequents . In M. Fernández & A. Muscholl, editors: 28th EACSL An- nual Conference on Computer Science Logic (CSL 2020) , Leibniz International Proceedings in Informat- ics (LIPIcs) 152, Schloss Dagstuhl–Leibniz-Zentrum fuer Infor...

    work page doi:10.4230/lipics.csl.2020.28 2020

  30. [30]

    Maehara (1961): Craig no Interpolation Theorem

    S. Maehara (1961): Craig no Interpolation Theorem . Sugaku 12, pp. 235–237, doi:10.11429/sugaku1947.12.235

    work page doi:10.11429/sugaku1947.12.235 1961

  31. [31]

    Maruyama, S

    A. Maruyama, S. Tojo & H. Ono (2001): Decidability of temporal epistemic logics for multi-agent models . Proceedings of the ICLP’01 Workshop on Computational Logic in Multi-Agent Systems (CLIMA-01) , pp. 31–40

    2001

  32. [32]

    R. P. McArthur (1976): Tense Logic. Reidel Publishing Company, Dordrecht, Boston

    1976

  33. [33]

    L. S. Moss (2007): Finte Models Constructed From Canonical Formulas . Journal of Philosophical Logic 36(6), pp. 605–640, doi:10.1007/s10992-007-9052-4

    work page doi:10.1007/s10992-007-9052-4 2007

  34. [34]

    A. M. Pitts (1992): On an interpretation of second order quantification in first order intuitionistic proposi- tional logic. Journal of Symbolic Logic 57(1), pp. 33–52, doi:10.2307/2275175

    work page doi:10.2307/2275175 1992

  35. [35]

    A. N. Prior (1957): Time and Modality. Clarendon Press, Oxford

    1957

  36. [36]

    A. N. Prior (1967): Past, Present and Future. Clarendon Press, Oxford

    1967

  37. [37]

    A. N. Prior (1968): Papers on Time and Tense. Clarendon Press, Oxford

    1968

  38. [38]

    A. N. Prior (2003): Papers on Time and Tense, new edition. Oxford University Press

    2003

  39. [39]

    Rautenberg (1983): Modal tableau calculi and interpolation

    W. Rautenberg (1983): Modal tableau calculi and interpolation . Journal of Philosophical Logic 12(4), pp. 403–423, doi:10.1007/bf00249258

    work page doi:10.1007/bf00249258 1983

  40. [40]

    Sano & S

    K. Sano & S. Yamasaki (2020): Subformula property and Craig interpolation theorem of sequent cal- culi for tense logics . In N. Olivetti & R. Verbrugge, editors: Short Papers of Advances in Modal Logic (AiML 2020), pp. 97–101. Available at https://rinekeverbrugge.nl/wp-content/uploads/2024/ 09/FinalShortPaperMain-AiML2020.pdf

    2020

  41. [41]

    V . Y . Shavrukov (1993):Subalgebras of diagonalizable algebras of theories containing arithmetic. Disserta- tiones Mathematicae (Rozprawy Matematyczne) 323, pp. 1–82

    1993

  42. [42]

    Visser (1996): Uniform Interpolation and Layered Bisimulation

    A. Visser (1996): Uniform Interpolation and Layered Bisimulation . In: Gödel’96: Logical founda- tions of mathematics, computer science and physics—Kurt Gödel’s legacy, Brno, Czech Republic, August 1996, Spriinger-Verlag, Berlin, pp. 139–164. Available at http://projecteuclid.org/euclid.lnl/ 1235417019

    1996

  43. [43]

    Visser (1996): Bisimulations, model descriptions and propositional quantifiers

    A. Visser (1996): Bisimulations, model descriptions and propositional quantifiers . Logic Group Preprint Series, No. 161, Utrecht University10.1006/inco.1997.2627. Available at https://dspace.library.uu. nl/handle/1874/26710

    work page arXiv 1996

  44. [44]

    Journal of Philosophical Logic 26(5), pp

    F. Wolter (1997): A Note on the Interpolation Property in Tense Logic. Journal of Philosophical Logic 26(5), pp. 545–551, doi:10.1023/a:1017956722866

    work page doi:10.1023/a:1017956722866 1997

  45. [45]

    Zakharyaschev, F

    M. Zakharyaschev, F. Wolter & A. Chagrov (2001): Advanced Modal Logic. In: Handbook of Philosophical Logic, 3, Springer Netherlands, pp. 83–266, doi:10.1007/978-94-017-0454-0_2

    work page doi:10.1007/978-94-017-0454-0_2 2001