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.
Labelled sequent calculi for indexed modal logics
Eugenio Orlandelli
2019
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.