中央研究院 資訊科學研究所

Compared with the standard possible world semantics, a path in a path model is a finite sequence of possible worlds in which each world, except the first, is accessible from the one it follows. So, roughly speaking, path models are a semantic framework adjusted from the standard possible world semantics such that the structure of frames is categorized by the set of paths rather than the relation between worlds. To further utilize the mechanism, truth values are then directly assigned to sequences of sequents of modal formulas, not to formulas, as normally done. Consequently, some style of Gentzen-type sequent calculi with sequences of sequents as the objects in a proof can be straightforwardly interpreted in accordance with path models. In this paper, we will demonstrate path models and their corresponding calculi of sequences of sequents for the normal modal logics extended from K by axioms D, T, 4, B, and 5, and prove the completeness theorem with respect to these models and calculi. Furthermore, for the logics extended from K by D, T and 4, we will discuss their cut-free versions of calculi.