Infinitary Modal Logic and Generalized Kripke Semantics

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