Most properties are undecidable even in mathopNExt Grzt
Abstract
We investigate decidability of properties in the lattice mathopNExt Grzt of extensions of the Grzegorczyk tense logic Grzt and the lattice mathopNExt S4t of reflexive and transitive tense logics, with applications to the lattice mathopExt biIPC of bi-superintuitionistic logics. We prove that a broad class of properties is undecidable in mathopNExt Grzt, including tabularity, Kripke completeness, the finite model property, and decidability, which also yields their undecidability in mathopNExt S4t. We also construct infinitely many tabular extensions of Grzt (and thus of S4t) whose coincidence problems are undecidable, while presenting one tabular extension of Grzt and infinitely many ones of S4t with a decidable coincidence problem. As a consequence, we obtain that the finite model property and tabularity are undecidable in mathopExt biIPC, and that there are infinitely many tabular extensions of biIPC whose coincidence problems are undecidable. These results clarify some similarities and differences between mathopNExt Grzt and mathopNExt Grz, mathopNExt S4t and mathopNExt S4, as well as mathopExt biIPC and mathopExt IPC. The proofs adapt Chagrov's method of reducing from an undecidable problem for Minsky machines. We isolate and explicitly formulate the method of good valuations, a recurring technique underlying several proofs in the literature that use large frames, making it available for further applications.
Related
BibTeX
@misc{chen2026most,
title = {{Most properties are undecidable even in $\mathop\mathsfNExt \mathsfGrz_t$}},
author = {Qian Chen and Tenyo Takahashi},
howpublished = {arXiv},
year = {2026},
month = aug,
doi = {10.48550/arxiv.2608.30816},
eprint = {2608.30816},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2608.30816},
note = {CC BY-NC-SA 4.0},
}
RIS
TY - UNPB
TI - Most properties are undecidable even in mathopNExt Grz_t
AU - Qian Chen
AU - Tenyo Takahashi
PY - 2026
DA - 2026/08/31
PB - arXiv
DO - 10.48550/arxiv.2608.30816
UR - https://arxiv.org/abs/2608.30816
AB - We investigate decidability of properties in the lattice mathopNExt Grz_t of extensions of the Grzegorczyk tense logic Grz_t and the lattice mathopNExt S4_t of reflexive and transitive tense logics, with applications to the lattice mathopExt biIPC of bi-superintuitionistic logics. We prove that a broad class of properties is undecidable in mathopNExt Grz_t, including tabularity, Kripke completeness, the finite model property, and decidability, which also yields their undecidability in mathopNExt S4_t. We also construct infinitely many tabular extensions of Grz_t (and thus of S4_t) whose coincidence problems are undecidable, while presenting one tabular extension of Grz_t and infinitely many ones of S4_t with a decidable coincidence problem. As a consequence, we obtain that the finite model property and tabularity are undecidable in mathopExt biIPC, and that there are infinitely many tabular extensions of biIPC whose coincidence problems are undecidable. These results clarify some similarities and differences between mathopNExt Grz_t and mathopNExt Grz, mathopNExt S4_t and mathopNExt S4, as well as mathopExt biIPC and mathopExt IPC. The proofs adapt Chagrov's method of reducing from an undecidable problem for Minsky machines. We isolate and explicitly formulate the method of good valuations, a recurring technique underlying several proofs in the literature that use large frames, making it available for further applications.
ER -