informações gerais
anterior próximo
An Indexed Approach to Modalities


The shape of the rules of standard proof-theoretical systems for modal logics is often an example of what a good rule should not be. The intensionality of the modal connectives forces the rules either to be non symmetric or to involve a global constraint on the shape of the deduction. To restore symmetry and locality we propose the framework of 2-sequents. This proposal is based on a notion of "indexed systems" (the idea goes back to Kripke and has been developed by many authors), where "indexes" (natural numbers) are used to mimic the interplay of variables and quantifiers in first-order logic. Different modal and linear logics are obtained with simple side conditions on indexes.