pith. sign in

arxiv: 2606.31863 · v1 · pith:H5GITLQEnew · submitted 2026-06-30 · 💻 cs.LO

Most Properties are Undecidable for Transitive Tense Logics

Qian Chen (The Tsinghua-UvA JRC for Logic , Department of Philosophy , Tsinghua University) , Tenyo Takahashi (Institute for Logic , Language , Computation , University of Amsterdam) This is my paper

Pith reviewed 2026-07-01 03:15 UTC · model grok-4.3

classification 💻 cs.LO
keywords transitive tense logicsundecidabilityKripke completenessfinite model propertyMinsky machinesNExt(K4t)bimodal logicsdecidability of properties
0
0 comments X

The pith

Most properties of transitive tense logics are undecidable.

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

The paper establishes that no algorithm exists to decide, for a finitely axiomatizable transitive tense logic, whether it is Kripke complete, has the finite model property, or is decidable. This undecidability holds across the lattice NExt(K4t) of all normal extensions of K4t. The argument adapts Chagrov's reduction from the halting problem for Minsky machines, transferring undecidability to the meta-level properties of these bimodal logics. The result separates transitive tense logics from linear tense logics, where some of the same properties remain decidable.

Core claim

In the lattice NExt(K4t) of transitive tense logics, the problems of determining Kripke completeness, the finite model property, and decidability itself are undecidable. The proof adapts Chagrov's reduction from the undecidable Minsky machine problem, constructing a general scheme that shows these properties cannot be decided by any algorithm on finite axiomatizations.

What carries the argument

The reduction from the undecidable Minsky machine halting problem to the decision problems for properties of logics in NExt(K4t).

If this is right

  • No algorithm decides Kripke completeness for finitely axiomatizable logics in NExt(K4t).
  • The finite model property cannot be decided algorithmically for logics in this class.
  • Decidability of the logic is itself an undecidable meta-property in NExt(K4t).
  • The same undecidability holds for other common properties of logics via the same reduction scheme.

Where Pith is reading between the lines

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

  • The contrast with decidable cases in linear tense logics points to the specific interaction of the two modalities as the source of undecidability.
  • The reduction method may apply to other bimodal or multimodal classes beyond transitive tense logics.
  • Even when the general decision problem is undecidable, individual concrete logics in the class may still admit direct verification of the properties.
  • The result suggests that adding transitivity to tense logics is enough to push many meta-properties into undecidability.

Load-bearing premise

Chagrov's reduction from the Minsky machine problem can be adapted to transitive tense logics while preserving undecidability for the target properties.

What would settle it

An algorithm that decides Kripke completeness for every finitely axiomatizable logic in NExt(K4t), or a demonstration that the adapted reduction fails to transfer undecidability to one of the listed properties.

Figures

Figures reproduced from arXiv: 2606.31863 by Computation, Department of Philosophy, Language, Qian Chen (The Tsinghua-UvA JRC for Logic, Tenyo Takahashi (Institute for Logic, Tsinghua University), University of Amsterdam).

Figure 1
Figure 1. Figure 1: The underlying frame of F Before studying properties of the general frame F, let us introduce a set of new modal operators ∆ ≤n and their duals ∇ ≤n , which will play an important role in our proofs. Definition 3.2. For each n ∈ ω and ϕ,ψ ∈ Lt , we define the formula ∆ ≤nϕ by: ∆ ≤0ϕ = ϕ and ∆ ≤k+1ϕ = ∆ ≤kϕ ∨♢∆ ≤kϕ ∨♦∆ ≤kϕ. As usual, we define the dual operator ∇ ≤n of ∆ ≤n by ∇ ≤nϕ := ¬∆ ≤n¬ϕ. For each Kri… view at source ↗
read the original abstract

A logics' property is decidable in a class of logics if there exists an algorithm that decides whether a finitely axiomatizable logic in the class has the property. Many properties are undecidable for bimodal logics but decidable for linear tense logics, which leads to a general question on how the interactions of modalities affect the decidability of properties. In this paper, we study the decidability of properties for transitive tense logics and show that most properties are undecidable in the lattice NExt(K4t) of transitive tense logics, including Kripke completeness, the finite model property, and decidability. Our proof method adapts Chagrov's approach of constructing a reduction from an undecidable problem of Minsky machines to the decision problem for logics' properties, yielding a general scheme of proving the undecidability of these properties.

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 / 1 minor

Summary. The paper claims that most properties of logics, including Kripke completeness, the finite model property, and decidability itself, are undecidable over the lattice NExt(K4t) of normal extensions of the transitive tense logic K4t. The proof adapts Chagrov's reduction from the undecidable halting problem for Minsky machines, constructing for each machine M a finitely axiomatizable extension L_M such that L_M has the target property iff M halts.

Significance. If the adaptation succeeds without the tense operators and transitivity axioms collapsing the reduction, the result would extend known undecidability theorems from unimodal and bimodal logics to the tense setting, showing that converse modalities do not restore decidability for these meta-properties (in contrast to linear tense logics). The general scheme for such reductions would be a useful technical contribution.

major comments (2)
  1. [§3] §3 (reduction construction): the manuscript asserts that Chagrov's one-directional accessibility encoding can be lifted to K4t but supplies no explicit verification that the added past-modality axioms and transitivity do not create 'shortcuts' or additional frames making every L_M Kripke complete (or decidable) independently of whether M halts.
  2. [§3.1] §3.1 (interaction axioms): no argument is given that the family {L_M} remains uniformly undecidable for the target properties once the tense interaction rules are enforced; the original Minsky-machine reduction relies on directed frames whose converse may introduce a uniform decision procedure across the family.
minor comments (1)
  1. [Introduction] The abstract states the result but the introduction could more clearly delineate which properties are covered by the general scheme versus those left open.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and the identification of points where the reduction requires more explicit justification. We will revise the manuscript to supply the missing verifications while preserving the core adaptation of Chagrov's construction.

read point-by-point responses

  1. Referee: [§3] §3 (reduction construction): the manuscript asserts that Chagrov's one-directional accessibility encoding can be lifted to K4t but supplies no explicit verification that the added past-modality axioms and transitivity do not create 'shortcuts' or additional frames making every L_M Kripke complete (or decidable) independently of whether M halts.

    Authors: We agree that an explicit verification is required. In the revised manuscript we will add a dedicated lemma (placed after the definition of L_M) that enumerates the possible accessibility relations compatible with the axioms of L_M. The argument proceeds by showing that any frame satisfying the transitivity and tense-interaction axioms of L_M must still encode exactly the one-directional computation steps of the Minsky machine; the converse accessibility relation cannot create shortcuts that would force Kripke completeness or decidability independently of halting, because any such shortcut would violate the specific modal formulas used to encode the machine's transition rules. revision: yes

  2. Referee: [§3.1] §3.1 (interaction axioms): no argument is given that the family {L_M} remains uniformly undecidable for the target properties once the tense interaction rules are enforced; the original Minsky-machine reduction relies on directed frames whose converse may introduce a uniform decision procedure across the family.

    Authors: We will insert a new paragraph immediately following the construction of the family {L_M} that addresses the interaction axioms directly. The argument establishes that any decision procedure uniform across {L_M} would still decide the halting problem for Minsky machines: the tense-interaction rules are satisfied by the intended frames, yet the reduction formulas remain independent of the converse direction in a way that prevents a single algorithm from deciding all instances. This is shown by proving that if a uniform procedure existed, it could be used to solve the original undecidable problem, contradicting the known undecidability of the halting problem. revision: yes

Circularity Check

0 steps flagged

No circularity; derivation adapts external Chagrov reduction from Minsky machines

full rationale

The paper's proof adapts Chagrov's reduction from the undecidable Minsky machine halting problem to establish undecidability results for properties in NExt(K4t). This relies on an externally established undecidable problem rather than any self-definitional construction, fitted parameters renamed as predictions, or load-bearing self-citations. The derivation chain is self-contained against external benchmarks with no reductions by construction to the paper's own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the validity of adapting Chagrov's reduction construction; abstract provides no further parameters or entities.

axioms (1)
  • standard math Minsky machines have undecidable properties such as halting
    Serves as the external source of undecidability transferred via reduction.

pith-pipeline@v0.9.1-grok · 5694 in / 1244 out tokens · 58783 ms · 2026-07-01T03:15:44.900335+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

33 extracted references · 26 canonical work pages

  1. [1]

    Pure and Applied Mathe- matics : A Series of Monographs and Textbooks, CRC Press, Boca Raton, doi:10.1201/9781439851302

    Clifford Bergman (2011): Universal Algebra: Fundamentals and Selected Topics. Pure and Applied Mathe- matics : A Series of Monographs and Textbooks, CRC Press, Boca Raton, doi:10.1201/9781439851302

    work page doi:10.1201/9781439851302 2011

  2. [2]

    Mathematical Proceedings of the Cambridge Philosophical Society 31(4), pp

    Garrett Birkhoff (1935): On the Structure of Abstract Algebras. Mathematical Proceedings of the Cambridge Philosophical Society 31(4), pp. 433–454, doi:10.1017/S0305004100013463

    work page doi:10.1017/s0305004100013463 1935

  3. [3]

    Blok (1980): Pretabular Varieties of Modal Algebras

    Willem J. Blok (1980): Pretabular Varieties of Modal Algebras. Studia Logica: An International Journal for Symbolic Logic 39(2/3), pp. 101–124, doi:10.1007/BF00370315

    work page doi:10.1007/bf00370315 1980

  4. [4]

    Oxford Uni- versity Press, United States, 2017.doi:10.1093/oso/9780198701347.001.0001

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

    work page doi:10.1093/oso/9780198537793.001.0001 1997

  5. [5]

    Chagrov (1990): Undecidable Properties of Extensions of a Provability Logic

    Alexander V . Chagrov (1990): Undecidable Properties of Extensions of a Provability Logic. I. Algebra and Logic 29(3), pp. 231–243, doi:10.1007/BF01979939

    work page doi:10.1007/bf01979939 1990

  6. [6]

    Chagrov (1990): Undecidable Properties of Extensions of a Provability Logic

    Alexander V . Chagrov (1990): Undecidable Properties of Extensions of a Provability Logic. II. Algebra and Logic 29(5), pp. 406–413, doi:10.1007/BF02215288

    work page doi:10.1007/bf02215288 1990

  7. [7]

    Chagrov (2002):The Algorithmic Problem of Axiomatising a Tabular Normal Modal Logic

    Alexander V . Chagrov (2002):The Algorithmic Problem of Axiomatising a Tabular Normal Modal Logic. In: Logical Investigations, Nauka, Moscow, pp. 251–263

    2002

  8. [8]

    Chagrov & Lilia A

    Alexander V . Chagrov & Lilia A. Chagrova (1995): Algorithmic Problems Concerning First-Order De- finability of Modal Formulas on the Class of All Finite Frames . Studia Logica 55(3), pp. 421–448, doi:10.1007/BF01057806. Q. Chen & T. Takahashi 201

    work page doi:10.1007/bf01057806 1995

  9. [9]

    Chagrov & Valentin B

    Alexander V . Chagrov & Valentin B. Shehtman (1995): Algorithmic Aspects of Propositional Tense Logics. In Gerhard Goos, Juris Hartmanis, Jan Van Leeuwen, Leszek Pacholski & Jerzy Tiuryn, editors: Computer Science Logic, 933, Springer Berlin Heidelberg, pp. 442–455, doi:10.1007/BFb0022274

    work page doi:10.1007/bfb0022274 1995

  10. [10]

    Chagrov & Michael Zakharyaschev (1993): The Undecidability of the Disjunction Property of Propositional Logics and Other Related Problems

    Alexander V . Chagrov & Michael Zakharyaschev (1993): The Undecidability of the Disjunction Property of Propositional Logics and Other Related Problems. The Journal of Symbolic Logic 58(3), pp. 967–1002, doi:10.2307/2275108

    work page doi:10.2307/2275108 1993

  11. [11]

    Studia Logica: An International Journal for Symbolic Logic 109(5), pp

    Qian Chen & Minghui Ma (2021): Lattices of Finitely Alternative Normal Tense Logics. Studia Logica: An International Journal for Symbolic Logic 109(5), pp. 1093–1118, doi:10.1007/s11225-021-09942-5

    work page doi:10.1007/s11225-021-09942-5 2021

  12. [12]

    Studia Logica: An International Journal for Symbolic Logic 111(2), pp

    Qian Chen & Minghui Ma (2023): Finite Model Property in Weakly Transitive Tense Logics. Studia Logica: An International Journal for Symbolic Logic 111(2), pp. 217–250, doi:10.1007/s11225-022-10027-0

    work page doi:10.1007/s11225-022-10027-0 2023

  13. [13]

    The Review of Symbolic Logic 17(2), pp

    Qian Chen & Minghui Ma (2024): Tabularity and Post-completeness in Tense Logic. The Review of Symbolic Logic 17(2), pp. 475–492, doi:10.1017/S1755020322000132

    work page doi:10.1017/s1755020322000132 2024

  14. [14]

    Jankov (1968): The construction of a sequence of strongly independent superintuitionistic propo- sitional calculi

    Vadim A. Jankov (1968): The construction of a sequence of strongly independent superintuitionistic propo- sitional calculi. Doklady Akademii Nauk SSSR 181(1), pp. 33–34

    1968

  15. [15]

    Archive for Mathematical Logic 31(4), pp

    Marcus Kracht (1992): Even More about the Lattice of Tense Logics. Archive for Mathematical Logic 31(4), pp. 243–257, doi:10.1007/BF01794981

    work page doi:10.1007/bf01794981 1992

  16. [16]

    The Journal of Symbolic Logic 64(1), pp

    Marcus Kracht & Frank Wolter (1999): Normal Monomodal Logics Can Simulate All Others. The Journal of Symbolic Logic 64(1), pp. 99–138, doi:10.2307/2586754

    work page doi:10.2307/2586754 1999

  17. [17]

    Notre Dame Journal of Formal Logic 12(2), pp

    David Makinson (1971): Some Embedding Theorems for Modal Logic. Notre Dame Journal of Formal Logic 12(2), pp. 252–254, doi:10.1305/ndjfl/1093894226

    work page doi:10.1305/ndjfl/1093894226 1971

  18. [18]

    Marvin Minsky (1967): Computation: Finite and Infinite Machines, rev. edition. Prentice-Hall

    1967

  19. [19]

    Prior (1967): Past, Present and Future

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

    1967

  20. [20]

    Prior (1968): Papers on Time and Tense

    Arthur N. Prior (1968): Papers on Time and Tense. Oxford University Press

    1968

  21. [21]

    Vieweg+Teubner Verlag, Wiesbaden, doi:10.1007/978-3-322-85796-5

    Wolfgang Rautenberg (1979): Klassische und Nichtklassische Aussagenlogik . Vieweg+Teubner Verlag, Wiesbaden, doi:10.1007/978-3-322-85796-5

    work page doi:10.1007/978-3-322-85796-5 1979

  22. [22]

    Studia Logica: An International Journal for Symbolic Logic 83(1-3), pp

    Wolfgang Rautenberg, Michael Zakharyaschev & Frank Wolter (2006):Willem Blok and Modal Logic. Studia Logica: An International Journal for Symbolic Logic 83(1-3), pp. 15–30, doi:10.1007/s11225-006-8296-2

    work page doi:10.1007/s11225-006-8296-2 2006

  23. [23]

    Master’s thesis, Institute for Logic, Language and Computation, University of Amsterdam

    Tenyo Takahashi (2025): Union-splittings, the Axiomatization Problem, and the Rule Dichotomy Property in Modal Logic. Master’s thesis, Institute for Logic, Language and Computation, University of Amsterdam

    2025

  24. [24]

    The Journal of Symbolic Logic , p

    Tenyo Takahashi (2026): Decidability of Being a Union-splitting. The Journal of Symbolic Logic , p. 1–14, doi:10.1017/jsl.2026.10187. Published online

    work page doi:10.1017/jsl.2026.10187 2026

  25. [25]

    Thomason (1974): Reduction of Tense Logic to Modal Logic

    Steven K. Thomason (1974): Reduction of Tense Logic to Modal Logic. I. Journal of Symbolic Logic 39(3), pp. 549–551, doi:10.2307/2272895

    work page doi:10.2307/2272895 1974

  26. [26]

    Thomason (1975): Reduction of Tense Logic to Modal Logic II

    Steven K. Thomason (1975): Reduction of Tense Logic to Modal Logic II . Theoria 41(3), pp. 154–169, doi:10.1111/j.1755-2567.1975.tb00555.x

    work page doi:10.1111/j.1755-2567.1975.tb00555.x 1975

  27. [27]

    Thomason (1982): Undecidability of the Completeness Problem of Modal Logic

    Steven K. Thomason (1982): Undecidability of the Completeness Problem of Modal Logic . Banach Center Publications 9(1), pp. 341–345, doi:10.4064/-9-1-341-345

    work page doi:10.4064/-9-1-341-345 1982

  28. [28]

    Frank Wolter (1993): Lattices Of Modal Logic. Ph.D. thesis, Freien Universität Berlin

    1993

  29. [29]

    Notre Dame Journal of Formal Logic 37(2), pp

    Frank Wolter (1996): A Counterexample in Tense Logic . Notre Dame Journal of Formal Logic 37(2), pp. 167–173, doi:10.1305/ndjfl/1040046085

    work page doi:10.1305/ndjfl/1040046085 1996

  30. [30]

    Mathematical Logic Quarterly 42(1), pp

    Frank Wolter (1996): Properties of Tense Logics . Mathematical Logic Quarterly 42(1), pp. 481–500, doi:10.1002/malq.19960420140

    work page doi:10.1002/malq.19960420140 1996

  31. [31]

    Journal of Symbolic Logic 62(1), pp

    Frank Wolter (1997): Completeness and Decidability of Tense Logics Closely Related to Logics above K4 . Journal of Symbolic Logic 62(1), pp. 131–158, doi:10.2307/2275736

    work page doi:10.2307/2275736 1997

  32. [32]

    Journal of Philosophical Logic 26(5), pp

    Frank 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. 202 Most Properties are Undecidable for Transitive Tense Logics

    work page doi:10.1023/a:1017956722866 1997

  33. [33]

    In Patrick Blackburn, Johan Van Benthem & Frank Wolter, editors: Handbook of Modal Logic , Studies in Logic and Practical Reasoning 3, Elsevier, pp

    Frank Wolter & Michael Zakharyaschev (2007): Modal Decision Problems. In Patrick Blackburn, Johan Van Benthem & Frank Wolter, editors: Handbook of Modal Logic , Studies in Logic and Practical Reasoning 3, Elsevier, pp. 427–489, doi:10.1016/S1570-2464(07)80010-3

    work page doi:10.1016/s1570-2464(07)80010-3 2007