Most Properties are Undecidable for Transitive Tense Logics

Technical Summary: Most Properties are Undecidable for Transitive Tense Logics

Problem Statement
The paper addresses the algorithmic decidability of logical properties within the lattice of transitive tense logics, denoted as $NExtK4t$. While the decidability of properties (such as Kripke completeness, the finite model property, and decidability itself) is well-studied for unimodal logics and linear tense logics, the status of these properties in the intermediate class of transitive tense logics remains a critical open question. Specifically, the authors investigate whether the natural interaction between the future ($\Box$) and past ($\blacksquare$) modalities in transitive frames renders the decision problem for these properties undecidable. Previous work by Chagrov and Shehtman established the undecidability of tabularity and consistency in $NExtK4t$, but the decidability of Kripke completeness, the finite model property (FMP), and general decidability remained unresolved.

Methodology
The authors adapt a reduction technique originally developed by Chagrov for unimodal logics, extending it to the bimodal setting of tense logics. The core method involves constructing a computable reduction from the reachability problem of Minsky machines (a known undecidable problem equivalent to the halting problem for Turing machines) to the decision problem for specific logical properties.

1. Minsky Machine Encoding: The authors utilize a Minsky machine $M$ with two registers and a specific configuration $c_0 = \langle s, n, m \rangle$ such that the set of reachable configurations is undecidable.
2. General Frame Construction: A specific general frame $\mathcal{F} = (W, R, A)$ is constructed. The domain $W$ encodes the reachable configurations of $M$ alongside auxiliary points ($a_i, b_i, c_i$) representing the register values and a "counter" structure. The accessibility relation $R$ is defined to simulate the transitions of the Minsky machine and the increment/decrement operations on the registers.
3. Formula Construction: The authors define a set of variable-free formulas ($\phi_{c_n}, \phi_{a_n}, \phi_{b_n}$) that uniquely identify specific points in the frame $\mathcal{F}$. They further define formulas $\psi_A, \psi_B$ and their successors to simulate the $+1$ and $-1$ operations on the registers.
4. Logic Construction: For any configuration $c = \langle t, k, l \rangle$, a logic $L(c)$ is defined as an extension of $K4t$. This logic includes:
   • Axioms ($Ax_M$) encoding the transition rules of the Minsky machine.
   • A conditional axiom linking the initial configuration to the target configuration $c$.
   • A specific formula $\alpha$ (derived from a tabular logic) and a "trap" formula $\phi_0$ designed to ensure that if the target configuration is not reachable, the resulting logic is Kripke incomplete and undecidable.

Key Contributions and Results
The paper establishes a general criterion (Theorem 3.5) for the undecidability of properties in $NExtK4t$. The theorem states that if a property $P$ is contained within the union of Kripke completeness ($KC$) and decidability ($DEC$), and there exists a formula $\alpha$ such that $K4t \oplus \alpha \in P$ but the constructed frame $\mathcal{F}$ does not validate $\alpha$, then $P$ is undecidable.

Applying this theorem, the authors prove the following results (Corollary 3.13):

• The following sets of formulas are undecidable in $NExtK4t$:
  1. Kripke completeness.
  2. Canonicity.
  3. First-order definability.
  4. The finite model property (FMP).
  5. Local tabularity.
  6. Tabularity.
  7. Decidability (of the logic itself).
  8. Coincidence with a fixed tabular logic.
  9. Consistency (specifically, the complement, inconsistency, is undecidable).

Furthermore, via Proposition 2.2, the authors note that since $K4t$ is an extension of $Kt$ (the minimal tense logic), these undecidability results extend to the lattice $NExtKt$.

Significance and Claims
The paper claims to resolve the decidability status of major logical properties for transitive tense logics, demonstrating that "most properties are undecidable" in this class. The significance lies in clarifying how the interaction of modalities affects decidability:

• Contrast with Linear Time: While properties are decidable in the lattice of linear time flows ($NExtLint$), the introduction of transitivity without linearity ($NExtK4t$) leads to undecidability.
• Contrast with Unimodal Logics: The results highlight that the minimal tense extension map does not preserve properties like Kripke completeness or FMP, making the bimodal case fundamentally different and more complex than the unimodal case ($NExtK4$).
• General Scheme: The paper provides a general proof scheme for establishing undecidability in tense logics by reducing Minsky machine reachability to logical properties, filling a gap left by previous works that could not directly transfer unimodal undecidability results to the tense setting due to the non-injectivity of the tense extension map.

The authors conclude that the interactions of modalities in transitive tense logics make the decision problem for properties strictly harder than in linear tense logics and suggest that for properties like Kripke completeness, undecidability in a unimodal lattice likely implies undecidability in its minimal tense extension, though this remains a conjecture for future work.