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

We investigate the (multiagent) infinitary version K-w1 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 LKw1 square (here presented as a Tait-style calculus, TKw1#) of the standard sequent calculus LKp square for K is incomplete with respect to Kripke semantics. It is also known that in order to axiomatize K-w1 one has to add to LKw1 square new initial sequents corresponding to the infinitary propositional counterpart BFw1 of the Barcan Formula. We introduce a generalization of standard Kripke semantics, and prove that K-w1(#) is sound and complete with respect to it. By the same proof strategy, we show that the stronger system TKw1, allowing countably infinite sequents, axiomatizes K-w1 although it provably does not admit cut-elimination.