发表机构
Universidad Nacional del Sur; Universidad Nacional de San Juan（南方大学; 圣胡安国立大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文从代数和证明论角度研究最小时态逻辑K_t，引入保真度逻辑及相继式演算，并通过Lindenbaum--Tarski构造改编，为Kashima演算建立了代数完备性定理，连接其嵌套相继式表述与时态布尔代数语义。
AI 中文摘要
我们从代数和证明论的角度研究最小时态逻辑$K_t$。我们引入了与一类时态布尔代数相关联的保真度逻辑。接着，我们为该逻辑引入了一个相继式演算，并通过Lindenbaum--Tarski构造的改编，建立了该演算相对于时态布尔代数的可靠性和完备性。因此，该演算为最小时态逻辑$K_t$提供了一种额外的语法表述。我们还给出了第二个纯语法的完备性证明。此外，我们为Kashima的Gentzen风格演算建立了代数可靠性和完备性定理。为此，我们将Lindenbaum--Tarski构造改编到Kashima的嵌套相继式框架中，从而能够直接从证明论系统构造代数语义。这为Kashima的演算提供了一个直接的代数完备性证明，并将其嵌套相继式表述与时态布尔代数的代数语义联系起来。
英文摘要
We study the minimal tense logic $K_t$ from an algebraic and proof-theoretic perspective. We introduce the degree-of-truth-preserving logic associated with the class of tense Boolean algebras. We then introduce a sequent calculus for this logic and establish its soundness and completeness with respect to tense Boolean algebras by means of an adaptation of the Lindenbaum--Tarski construction. Consequently, this calculus provides an additional syntactic presentation of the minimal tense logic $K_t$. We also provide a second, purely syntactic proof of completeness. Furthermore, we establish an algebraic soundness and completeness theorem for Kashima's Gentzen-style calculus. To this end, we develop an adaptation of the Lindenbaum--Tarski construction to Kashima's nested sequent framework, which allows us to construct the algebraic semantics directly from the proof-theoretic system. This yields a direct algebraic completeness proof for Kashima's calculus and connects its nested-sequent formulation with the algebraic semantics of tense Boolean algebras.
