Some Remarks on the Proof-Theory and the Semantics of Infinitary Modal Logic

We investigate the (multiagent) infinitary version Kω1 of the propositional modal logic K, in which conjunctions and disjunctions over countably infinite sets of formulas are allowed. It is known that the natural infinitary extension LK ω1 (here presented as a Tait-style calculus, TK] ω1) of the standard sequent calculus LK p for K is incomplete with respect 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 standard Kripke semantics, and prove that TK] ω1 is sound and complete with respect to it. By the same proof strategy, we show that the stronger system TKω1, allowing countably infinite sequents, axiomatizes Kω1, although it provably does not admit cut-elimination.