AI 中文总结
研究Grzegorczyk时态逻辑扩张格及自返传递时态逻辑格中性质的可判定性，将Chagrov方法从Minsky机器不可判定问题归约，证明表格性等多数性质在Grz_t扩张格中不可判定，相关结论可应用于双超直觉逻辑格，还分离出良赋值方法。
AI 中文摘要
我们研究了Grzegorczyk时态逻辑$\mathsf{Grz}_t$的扩张格$\mathop{\mathsf{NExt}} \mathsf{Grz}_t$以及自返传递时态逻辑的格$\mathop{\mathsf{NExt}} \mathsf{S4}_t$中性质的可判定性，相关结果可应用于双超直觉逻辑的格$\mathop{\mathsf{Ext}} \mathsf{biIPC}$。我们证明了一大类性质在$\mathop{\mathsf{NExt}} \mathsf{Grz}_t$中是不可判定的，包括表格性、Kripke完备性、有限模型性质和可判定性，这也意味着这些性质在$\mathop{\mathsf{NExt}} \mathsf{S4}_t$中同样不可判定。我们还构造了无穷多个$\mathsf{Grz}_t$（从而也是$\mathsf{S4}_t$）的表格扩张，其重合问题是不可判定的，同时给出了一个$\mathsf{Grz}_t$的表格扩张和无穷多个$\mathsf{S4}_t$的表格扩张，它们的重合问题是可判定的。由此，我们得出有限模型性质和表格性在$\mathop{\mathsf{Ext}} \mathsf{biIPC}$中是不可判定的，且存在无穷多个$\mathsf{biIPC}$的表格扩张，其重合问题是不可判定的。这些结果阐明了$\mathop{\mathsf{NExt}} \mathsf{Grz}_t$与$\mathop{\mathsf{NExt}} \mathsf{Grz}$、$\mathop{\mathsf{NExt}} \mathsf{S4}_t$与$\mathop{\mathsf{NExt}} \mathsf{S4}$，以及$\mathop{\mathsf{Ext}} \mathsf{biIPC}$与$\mathop{\mathsf{Ext}} \mathsf{IPC}$之间的一些异同。证明采用了Chagrov的方法，将其从Minsky机器的不可判定问题进行归约。我们分离并明确表述了“良赋值”方法，这是文献中多个使用大框架的证明所依赖的重复技术，可供进一步应用。
英文摘要
We investigate decidability of properties in the lattice $\mathop{\mathsf{NExt}} \mathsf{Grz}_t$ of extensions of the Grzegorczyk tense logic $\mathsf{Grz}_t$ and the lattice $\mathop{\mathsf{NExt}} \mathsf{S4}_t$ of reflexive and transitive tense logics, with applications to the lattice $\mathop{\mathsf{Ext}} \mathsf{biIPC}$ of bi-superintuitionistic logics. We prove that a broad class of properties is undecidable in $\mathop{\mathsf{NExt}} \mathsf{Grz}_t$, including tabularity, Kripke completeness, the finite model property, and decidability, which also yields their undecidability in $\mathop{\mathsf{NExt}} \mathsf{S4}_t$. We also construct infinitely many tabular extensions of $\mathsf{Grz}_t$ (and thus of $\mathsf{S4}_t$) whose coincidence problems are undecidable, while presenting one tabular extension of $\mathsf{Grz}_t$ and infinitely many ones of $\mathsf{S4}_t$ with a decidable coincidence problem. As a consequence, we obtain that the finite model property and tabularity are undecidable in $\mathop{\mathsf{Ext}} \mathsf{biIPC}$, and that there are infinitely many tabular extensions of $\mathsf{biIPC}$ whose coincidence problems are undecidable. These results clarify some similarities and differences between $\mathop{\mathsf{NExt}} \mathsf{Grz}_t$ and $\mathop{\mathsf{NExt}} \mathsf{Grz}$, $\mathop{\mathsf{NExt}} \mathsf{S4}_t$ and $\mathop{\mathsf{NExt}} \mathsf{S4}$, as well as $\mathop{\mathsf{Ext}} \mathsf{biIPC}$ and $\mathop{\mathsf{Ext}} \mathsf{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.
Comments28 pages, 4 figures, 2 tables
