Model existence in non-compact modal logic (Q5939997)

Segerberg has shown a model existence theorem for an infinitary modal logic in which the concept of common knowledge can be axiomatized and a non-compact set of formulas is constructed by making use of it. The author extends this to the first-order case in a generalized form on the base of classical first-order constant domain (multi) modal predicate logic K formalized in a sequent style. Therefore, the predicate modal logics to be discussed are characterized syntactically as a set of formulas derivable by the sequent system from a set of axiom sequent schemas satisfying some conditon in a general form. The main feature of the sequent system is that a pair of countable sets of formulas is employed for a sequent instead of the usual finite sequences of formulas. Thus the obtained theorem allows us to apply it for such a logic as constant domain first-order extension of the infinitary modal logic of common knowledge. The proof of the model-existence theorem is carried out by a respresentation of modal algebras for the basic modal predicate logic.