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.
sequent calculi for indexed epistemic logics / Corsi, Giovanna; Orlandelli, Eugenio. - ELETTRONICO. - 1770:(2016), pp. 2.21-2.35. (Intervento presentato al convegno 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016) tenutosi a Coimbra, Portugal nel 1-07-2016).
sequent calculi for indexed epistemic logics
CORSI, GIOVANNA;ORLANDELLI, EUGENIO
2016
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.