Two constructions of non-equivalent modal formulas1

Abstract. We discuss two constructions of non-equivalent modal formulas for normal modal logics. One is basically same as the dual of the construction in Moss [Mos07] and the other is the construction in [Sas05], [Sas08] and [Sas09]. The former is useful for any normal modal logics, while as in [Sas09], the latter has much more information for modal logic S4. Here we define two constructions in sequent style and discuss the difference between them.