Infinitary Modal Logic and Generalized Kripke Semantics

This paper deals with the infinitary modal propositional logic Kω1, featuring countable disjunctions and conjunc- tions. It is known that the natural infinitary extension LKω1 (here presented as a Tait-style calculus, TK♯ω1 ) of the standard sequent calculus LKp for the propositional modal logic K is incomplete w.r. to Kripke semantics. It is also known that in order to axiomatize Kω1 one has to add to LKω1 new initial sequents corresponding to the infinitary propositional counterpart BFω1 of the Barcan- formula. We introduce a generalization of Kripke seman- tics, and prove that TK♯ω1 is sound and complete w.r. to this generalized semantics. By the same proof strategy, we show that the stronger system TKω1 , allowing countably infinite sequents, axiomatizes Kω1, although it provably doesn’t admit cut-elimination