Cut-elimination theorems for some infinitary modal logics (Q2743647)

The well-known Gentzen systems of propositional modal logics K, T, K4, and S4 are extended naturally to their infinitary versions by adjoining the rules for (countably) infinite conjunction and disjunction preserving the cut-elimination property, according to which then the infinitary formula corresponding to the so-called Barcan axiom of predicate modal logic is shown not to be derivable in the sequential systems. Consequently the infinitary propositional modal logics are shown to be incomplete with respect to the Kripke semantics, for the infinitary formula is valid in the semantical frameworks for them respectively. On the other hand, it has already been proved by the author that the Kripke complete logics coincide in fact with the extensions by the infinitary version of the Barcan axiom. In this paper the Kripke complete logics are formulated in a kind of Gentzen style enjoying the cut-elimination property. The main feature of formulation is to employ a particular hypersequent, called tree sequent, such that the components are pairs of countable sets of formulas and constitute a finite tree. The proof of the cut-elimination theorem is carried out via the Kripke completeness. Analogous phenomena are found with respect to infinitary propositional intuitionistic logic as well, so that the Kripke complete infinitary propositional intuitionistic logic is shown to be formulated in a cut-free Gentzen system based on the same idea.