Labelled sequent calculi for indexed modal logics

Indexed modal logics are a generalization of standard quantified modal logics obtained by indexing modal operators with sets of terms and by considering a counterpart-theoretic version of a Kripke-type semantics called transition semantics. This allows us to distinguish between ‘c is necessarily P’ and ‘it is neccessary that Pc’. Moreover, it gives us a better control of the interaction of the first-order machinery (substitutions, quantifers and identity) with modalities. This works provides a proof-theoretic study of indexed modal logics. It introduces labelled sequent calculi for all first-order definable classes of transition frames. It will be shown that the calculi introduced have good structural properties: invertibility of the rules, height-preserving admissibility of weakening and contraction and syntactic cut elimination. It will also be shown, in a completely modular way, that each calculus is sound and complete with respect to the appropriate class of transition frames.