時制論理の証明体系とブール代数の意味を結び付ける

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.