A Hypersequent Calculus for the System S5
S5 is undoubtedly one of the most important and well-known of all modal normal systems. When considered from the point of view of Kripke semantics, S5 is rather peculiar since it can be described in two different albeit equivalent ways. The first one specifies the properties (i.e. reflexiv- ity, transitivity and symmetry) that the accessibility relation of a Kripke frame should satisfy. A second and easier way to study S5 semantically exploits Kripke frames where the accessibility relation is absent: S5 is sound and complete with respect to the class of frames which are just non-empty sets of worlds. This second way is evidently simpler. In this chapter we aim at reflecting this simplicity at the syntactic level within a new and simple hypersequent calculus for the system S5.