sequent calculi for indexed epistemic logics

Indexed epistemic logics constitute a well-structured class of quantified epistemic logics with great expressive power and a well-behaved semantics based on the notion of epistemic transition model. It follows that they generalize term-modal logics. As to proof theory, the only axiomatic system for which we have a completeness theorem is the minimal system Q.Ke, whether with classical or with free quantification. This paper proposes a different approach by introducing labelled sequent calculi. This approach turns out to be very flexible and modular: for each class of epistemic transition structures C* considered in the literature, we introduce a G3-style labelled calculus GE.*. We show that these calculi have very good structural properties insofar as all rules are height-preserving invertible (hp-invertible), weakening and contraction are height-preserving admissible (hp-admissible) and cut is admissible. We will also prove that each calculus GE.* characterizes the class C* of indexed epistemic structures