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, ⟨sup⟩ and ⟨inf⟩, interpreted as supremum and infimum operators over posets. Our axiomatization, which links ⟨sup⟩ and ⟨inf⟩ 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 (⟨sup⟩) and refinement (⟨inf⟩) within one logical framework, TIL provides an expressive paradigm for information dynamics.