Axiomatization and Decidability of Tense Information Logic
摘要
Knudstorp [3] axiomatizes modal information logic (MIL) with a supremum operator on posets. Since infima naturally complement suprema, this raises the question: Can this result be extended to a modal logic that includes both operators and, if so, what axioms would govern the interaction between the two modalities? In this paper, we prove soundness and completeness of tense information logic (TIL)—a modal logic with two binary modalities, \(\langle sup\rangle \) and \(\langle inf\rangle \) , interpreted as supremum and infimum operators over posets. Our axiomatization, which links \(\langle sup\rangle \) and \(\langle inf\rangle \) only through the standard tense-logic axioms, thereby resolves a question posed by van Benthem [6]. Completeness is proven using the step-by-step method [2] and as a corollary, we obtain completeness of TIL on preorders. Furthermore, we prove the finite model property (FMP) of TIL with respect to a generalized class of structures, which in turn establishes decidability of the logic. By introducing both fusion ( \(\langle sup\rangle \) ) and refinement ( \(\langle inf\rangle \) ) within one logical framework, TIL provides an expressive paradigm for information dynamics.