This space is reserved for the EPiC Series header, do not use it Sequent Calculi for Indexed Epistemic Logics Giovanna Corsi1 and Eugenio Orlandelli2 1 University of Bologna, Bologna, Italy giovanna.corsi@unibo.it 2 University of Bologna, Bologna, Italy eugenio.orlandelli@unibo.it 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. 1 Introduction Indexed epistemic logics (IEL) are quantified multi-agent epistemic logics characterized by the fact that epistemic formulas are expressions like |t : sx |P x (1) meaning ‘the agent (denoted by) t knows of (the denotation of) s that it is a P ’, see [1, 2]. As in term-modal logics (TML), [3], agents are denoted by terms, and therefore it is possible to quantify on agents and reason about groups of agents, e.g. ‘every Q knows of s that it is P ’ is expressed as ∀y(Qy → |y : sx | P x), and ‘every Q knows that P s’ is expressed as ∀y(Qy → |y : ?| P s). IEL are more general than TML in many respects: (i) they allow for non-rigid designators, i.e. the denotation of a term can vary from world to world, thus the logic doesn’t impose that the agents know every true identity; (ii) they are based on a counterpart- theoretic semantics, which, as shown in [1], permits a better treatment of de re modalities. In [1, 2] many interesting IEL are semantically introduced, but almost no complete proof- theoretic characterization is given, the only exception is an axiomatic characterization of the formulas valid on all structures. As is well known, axiomatic systems are not well suited for automated reasoning and, in the case of quantified modal logics, they do not allow modular proofs of completeness. For these aspects the labelled G3-style calculi studied in [4, 5, 7] behave ARQNL 2016 21 CEUR-WS.org/Vol-1770 Sequent Calculi for IEL Corsi, Orlandelli better: they allow cut-free sequent calculi for a wide class of modal logics and to give modular proofs of completeness obtained by a mechanical procedure that determines a derivation for every valid sequent and an appropriate countermodel for every invalid one. This paper applies the methodology of labelled calculi to IEL: for every IEL semantically defined in [1, 2] a labelled calculus is introduced and proved complete. A constructive proof that the structural rules of inference are admissible is given, thus solving a problem left open in [1, p. 1182], where it was raised the question of finding ‘a cut free sequent calculus of the classically quantified epistemic logic Qe.K + GF’. In the sequel to this section the language and the semantics of IEL are sketched. Section 2 introduces labelled sequent calculi for IEL. Section 3 shows that the calculi introduced have the good structural features that are distinctive of G3-style calculi: all rules are hp-invertible, the structural rules of weakening and contraction are hp-admissible and the rule of cut is admissible. Section 4 deals with soundness and completeness. Language. Consider a first-order language L whose signature contains individual constants and predicate symbols including identity. Let V ar be an infinite set of variables. Terms are defined as usual. The logical symbols are ⊥, →, ∀, and, for n ≥ 0, |t : tx11 . . . txnn |, where x1 , . . . , xn are pairwise distinct variables and t, t1 , . . . , tn are terms; when n = 0, we write |t : ?|. |t : x1 . . . xn | stands for |t : xx11 . . . xxnn |. We will also use x and t for n-tuples of variables and terms, respectively. Definition 1.1. The notions of formula, A, and of its free variables, f v(A), are defined simul- taneously as follows: • If t1 , . . . , tn are terms and P is an n-ary predicate, then P t1 , . . . , tn is a(n atomic) formula whose free variables are all the variables among t1 , . . . , tn ; • ⊥ is a formula with no free variables; • If B and C are formulas, then (B → C) is a formula and f v(B → C) = f v(B) ∪ f v(C); • If B is a formula and x a variable, then ∀xB is a formula and f v(∀xB) = f v(B) − {x}; • If B is a formula whose free variables are among x1 , . . . , xn , then |t : sx11 . . . sxnn |B is a formula, where t, s1 , . . . , sn are terms. The free variables of |t : sx11 . . . sxnn |B are all (and only) the variables occurring in t, s1 , . . . , sn . We use ≡ for syntactical identity. For the sake of simplicity, it will always be assumed that the bound variables occurring in a formula are different from the free ones. This can be achieved by renaming bound variables. Formulas that differ only in the name of the bound variables are taken to be identical. Definition 1.2. The expression s[t/x] stands for t if s ≡ x, else it is s. The notion of substitution of a term t for a variable x in a formula A, A[t/x], is defined thus: (P s1 , . . . , sn )[t/x] =df P s1 [t/x], . . . , sn [t/x] ⊥[t/x], =df ⊥ (B → C)[t/x] =df B[t/x]  → C[t/x]   ∀yB if y ≡ x,  ∀z((B[z/y])[t/x]) if y 6≡ x and y ≡ t, (∀yB)[t/x] =df   where z is new for A and z 6≡ t,  ∀y(B[t/x]) if y 6≡ x and y 6≡ t s [t/x] s [t/x] (|s : sx11 . . . sxnn |B)[t/x] =df |s[t/x] : x11 . . . xnn |B . 2 22 Sequent Calculi for IEL Corsi, Orlandelli Two comments on the notion of substitution. Having identified formulas that differ only in the name of bound variables, we are able to circumvent problems related to ‘captured’ variables by first renaming the bound variables and then by performing the problematic substitution. Second, in epistemic formulas the substitution is carried out inside the epistemic operator and not inside the formula that follows it as it is usually done. This is one of the reasons why the lower tuple of an indexed epistemic operator contains all the free variables of the formula that follows it. In this way we gain a better control of substitutions in epistemic contexts, see [1, 2]. We will also make extensive use of simultaneous substitutions of the terms t1 , . . . , tm for the free variables x1 , . . . , xm , A[t1 , . . . , tm /x1 , . . . , xm ]. This notion can be defined in terms of sequences of simple substitutions as follows: A[s1 , . . . sn , t/x1 , . . . xn , y] ≡ (A[s1 , . . . , sn /x1 , . . . , xn ])[t/y], where y 6≡ xi and y 6≡ si . Semantics. Given the epistemic formula |t : sx |P x considered in (1), its truth conditions are as follows: where a and b are the denotations of t and s, respectively, in a world w, the formula above is true in w if in every world that is compatible with a’s knowledge every object that is a counterpart of b w.r.t. a’s knowledge satisfies the open formula P x; in other words, if every way that b may be that is compatible with a’s knowledge satisfies P x. In order to render such semantical conditions formally, we need to introduce a few notions. Let W be a non-empty set of possible worlds, an epistemic transition model is, intuitively speaking, a family of extensional double-domain models {hUw , Dw , Iw i : w ∈ W} whose elements are related in two different ways: (i) by a compatibility relation between elements of the domain of some model and the other models: a ≺ v means that the world v is compatible with a’s knowledge. (ii) By a counterpart relation between elements of the domains of (not necessarily) a different models, modulo an agent: b  c means that according to the knowledge of agent a, if c ∈ Uv and a ≺ v, c represents in v the object that is b in w. Definition 1.3 (e-model). An e-model is a tuple M = hW, U, D, ≺, , Ii where W is a non-empty set of worlds. U = {Uw : w ∈ W} is a family of pairwise disjoint non-empty sets indexed by members of W: the outer domains. D = {Dw : Dw ⊆ Uw } is a family of inner domains indexed by members of W. ≺⊆ U ×W is the compatibility relation between agents and worlds: a ≺ w means that the world w is compatible with a’s knowl- edge. a = {: a ∈ U} is a family of counterpart relations indexed by agents: a = {a × Uw × Uv : a ∈ Uw and a ≺ v} a intuitively b  c means that c is a counterpart of b accord- ing to a’s knowledge. I is a function associating to every w ∈ W a first-order inter- pretation Iw defined over Uw , in particular: Iw (c) ∈ Uw ; Iw (P n ) ⊆ (Uw )n ; and Iw (=) = {ha, ai : a ∈ Uw }. We say that the e-model M = hW, U, D, ≺, , Ii is based on the e-frame F=hW, U, D, ≺, i. Assignments are defined world by world: a w-assignment σ is a mapping from the set V ar of variables to Uw . Given a w-assignment σ and a ∈ Uw , we use σ x.a for the w-assignment that maps x to a and behaves like σ on all other variables. When no ambiguity arises, we use σ(t) 3 23 Sequent Calculi for IEL Corsi, Orlandelli to denote not only the object assigned by the w-assignment σ to the variable t, but also the object assigned by Iw to the constant t. Definition 1.4. Satisfaction of a formula A at w under σ in M, σ |=M w A, is so defined: σ 6|=M w ⊥ σ |=Mw P t1 , . . . , tn ⇐⇒ hσ(t1 ), . . . , σ(tn )i ∈ Iw (P ) σ |=Mw B →C ⇐⇒ σ 6|=M w B or σ |=w C M σ |=Mw ∀xB ⇐⇒ for all a ∈ Dw , σ x.a |=M w B σ |=M s1 sn w |t : x1 . . . xn |B ⇐⇒ for all v s.t. σ(t) ≺ v and for all v-assignment τ s.t. σ(t) σ(si )  τ (xi ), 1 ≤ i ≤ n, we have that τ |=M v B The notions of truth in a world, |=M w A, truth in a model, |= M A, and validity in a frame, F |= A, are defined in the standard way. Relevant classes of e-frames. Some results of correspondence between classes of e-frames and epistemic formulas are listed here, see [1, Sect. 5] for their proofs. Proposition 1.5. Name Formula is valid on e-frames such that De |t : sx |A → ¬|t : sx |¬A serial (a) ∀a ∈ Uw ∃v ∈ W (a ≺ v) a (b) ∀a, b ∈ Uw ∃c ∈ Uv (b  c) Te |t : sx |A → A reflexive (a) ∀a ∈ Uw (a ≺ w) a (b) ∀a, b ∈ Uw (b  b) a 4e |t : sx |A → |t : sx ty | |y : x|A transitive (a) ∀a ∈ Uw ∀b ∈ Uv (a  b&b ≺ u ⊃ a ≺ u) a a d a (b) ∀a, b ∈ Uw ∀c, d ∈ Uv ∀e ∈ Uu (a  d&b  c&c  e ⊃ b  e) a Be A → |t : sx ty | ¬|y : x|¬A symmetric (a) ∀a ∈ Uw ∀b ∈ Uv (a  b ⊃ b ≺ w) a a d (b) ∀a, b ∈ Uw ∀c, d ∈ Uv (a  d&b  c& ⊃ c  b) CBFe |t : sx |∀yA → ∀y|t : sx y|A D-preservative ∀a ∈ Uw ∀b ∈ Dw ∀c ∈ Uv a (b  c ⊃ c ∈ Dv ) BFe ∀y|t : sx y|A → |t : sx |∀yA D-surjective ∀a ∈ Uw ∀b ∈ Dv a (a ≺ v ⊃ ∃c ∈ Dw (c  b)) GFe ∃y|t : sx y|A → |t : sx |∃yA D-total ∀a ∈ Uw ∀b ∈ Dw a (a ≺ v ⊃ ∃c ∈ Dv (b  c)) SHRTe |t : sx y|A → |t : sx |A U-total ∀a, b ∈ Uw a (a ≺ v ⊃ ∃c ∈ Uv (b  c)) N Ie t1 = t2 → |s : tx1 ty2 |x = y U-functional ∀a, b ∈ Uw ∀c, d ∈ Uv a a (b  c&b  d ⊃ c = d) N De t1 6= t2 → |s : tx1 ty2 |x 6= y U-injective ∀a, b, c ∈ Uw ∀d ∈ Uv a a (b  d&c  d ⊃ b = c) We will use C X,... to denote the class of all e-frames satisfying the condition(s) corresponding to the schema Xe of Prop 1.5. We talk of a single domain e-frame if ∀w ∈ W, Dw = Uw . 4 24 Sequent Calculi for IEL Corsi, Orlandelli Definition 1.6. Let c be any individual constant, we say that a 1. c is rigid iff for all a ∈ Uw , a ≺ v implies Iw (c)  Iv (c) ; a 2. c is stable iff for all a ∈ Uw for all b ∈ Uv ( if a ≺ v and Iw (c)  b then b = Iv (c) ). Proposition 1.7. Let c be any individual constant, it holds that 1. If c is rigid in M, then |=M |t : cx |A → |t : ?|(A[c/x]) ; 2. If c is stable in M, then |=M |t : ?|(A[c/x]) → |t : cx |A . We talk of rigid/stable e-model if all individual constants are rigid/stable. As we can see from the next proposition, term-modal logics are a particular case of indexed epistemic ones: Proposition 1.8. For every term-modal model hW, D, −→, I, i, see [3], there is a pointwise equivalent rigid and stable e-model M which is based on a single-domain e-frame that is D-total, D-injective and D-functional, and vice versa. 2 Labelled Sequent Calculi In this section we introduce labelled sequent calculi in order to characterize the indexed epis- temic logics defined by the properties of Props. 1.5 and 1.7. These calculi are given by rules meant to internalize the semantics into the syntax in the style of [4, 7]. In order to do it the language L is modified as follows: • a countable new set of variables w, v, u . . . called world labels is added, • for each term t of L and each world label w, a labelled term tw is added, • for each wff A of L and each world label w, a labelled formula Aw is added, • a new set of atomic formulas, called ancillary formulas, is added to the language: existence formulas tw ∈ D(w) tw is an element of the inner domain of w: tw ∈ Dw ; compatibility formulas tw (v) world v is compatible with tw ’s knowledge: tw ≺ v; w w v counterpart formulas s (t , r ) according to the agent sw , rv is a counterpart of tw : sw tw  rv Notice that ancillary formulas are not labelled formulas even if they contain labelled terms. Labelled formulas are formulas of L decorated with some label. Given a labelled formula Aw and a term t, we want to pin down those occurrences of t in w A , if any, which are, so to speak, in the scope of the world label w. To this end we introduce the notion of w-ground occurrence. Definition 2.1. Given a labelled formula Aw , a w-ground occurrence of a term t in Aw is defined by induction on Aw . • t is a w-ground occurrence in (P n t1 . . . tn )w iff t ≡ ti for some i, 1 ≤ i ≤ n, • t is a w-ground occurrence in (B → C)w iff t is a w-ground occurrence in B w or t is a w-ground occurrence in C w , • t is a w-ground occurrence in (∀xB)w iff t ≡ x or t is a w-ground occurrence in B w , • t is a w-ground occurrence in |s : sx11 . . . sxnn |B iff t ≡ s or t ≡ si , for some i, 1 ≤ i ≤ n. 5 25 Sequent Calculi for IEL Corsi, Orlandelli Any occurrence of a term t in Aw which is a w-ground occurrence is replaced by tw . If xw is free in Aw , the w-ground occurrences of xw are exactly those occurrences eligible for being substituted. Let us denote by Lext the language so modified. The definition of substitution 1.2 applies (with minor changes due to the labels) to labelled and ancillary formulas and to labelled terms. Whenever convenient, we allow ourselves to write (A[t/x])w instead of (Aw )[tw /xw ]. By E[w/v] we denote the labelled or ancillary formula obtained by replacing each occurrence of the world label v in E with an occurrence of w. Finally, we use sw (tw , rv ) to abbreviate the multiset {sw (tw v w w v v i , ri ) : ti ∈ t and ri ∈ r }. Sequents are expressions of the form Ω, Γ =⇒ ∆ where Ω is a multiset of ancillary formulas, and Γ, ∆ are multisets of labelled formulas. We said that the rules of the calculus are meant to internalize the semantic clauses. In order to see how this is done, let us look at a very simple example. σ(t) σ |=M s w |t : x |P x ⇐⇒ for all v s.t. σ(t) ≺ v and for all v-assignment τ s.t. σ(s)  τ (x), it holds that τ |=M v Px Reading from right to left, we get the following right introduction rule: tw (v), tw (sw , xv ), Ω, Γ =⇒ ∆, (P xv )v w R2 Ω, Γ =⇒ ∆, (|tw : sx |P x)w (2) where v is an eigenvariable, i.e. it doesn’t occur free in the conclusion. This entails that xv is an eigenvariable too. Reading from left to right, we get the following left introduction rule: w tw (v), tw (sw , rv ), (P xv )v [rv /xv ], (|tw : sx |P x)w , Ω, Γ =⇒ ∆ w L2 tw (v), tw (sw , rv ), (|tw : xs |P x)w , Ω, Γ =⇒ ∆ (3) where the principal formulas are repeated into the premiss to make the rule invertible. The rules of labelled calculus GE.K for the minimal indexed epistemic logic, i.e. for the formulas valid on the class of all e-frames, are given in Table 1. Identity is treated by means of mathematical rules so that the structural rules are admissible, see e.g. [7, Chap. 6]. Note that identity formulas are labelled and that the rule of replacement, Repl, is not a world- independent one as it would be for standard quantified modal systems: since terms need not be rigid designators, identities are world-bound. Thus the fact that t and s denote the same object in w doesn’t imply anything about their denotation in other worlds. Thanks to the non-logical rules in Table 2, we can define a calculus for each class of e-frames considered in Props. 1.5 and 1.7: it is enough to add, for each and every semantic condition (Condition), holding in that class of e-frames, the appropriate rule (Cond). See the cut-free proof of GFe (with rule Dtot) given in Table 3. Roughly, we call mathematical (geometrical ) a non-logical rule if it involves no (some) variable condition, see [7, Chaps. 6 and 8] for a precise definition. We will use GE.? to talk of any labelled calculus considered in this paper. Two observations are in order. First, contrary to what normally happens with non-logical rules, we don’t have to close them under contraction in order to prove the hp-admissibility of contraction, see the proof of Theorem 3.6 for the details. Second, the rules Rig and Stab, which capture respectively the conditions of rigidity and stability, don’t follow exactly the general structure of mathematical rules since they are given with respect to an arbitrary individual 6 26 Sequent Calculi for IEL Corsi, Orlandelli Table 1: The sequent calculus GE.K. • Initial sequents Ω, P w , Γ =⇒ ∆, P w (P w is an atomic labelled formula) • Propositional rules Ω, Γ =⇒ ∆, Aw Ω, B w , Γ =⇒ ∆ Ω, Aw , Γ =⇒ ∆, B w w L⊥ L→ R→ Ω, ⊥ , Γ =⇒ ∆ Ω, (A → B)w , Γ =⇒ ∆ Ω, Γ =⇒ ∆, (A → B)w • Quantifier rules (in the rule R∀ , y w is not free in the conclusion). tw ∈ D(w), Ω, (A[t/x])w , (∀xA)w , Γ =⇒ ∆ y w ∈ D(w), Ω, Γ =⇒ ∆, (A[y/x])w L∀ R∀ tw ∈ D(w), Ω, (∀xA)w , Γ =⇒ ∆ Ω, Γ =⇒ ∆, (∀xA)w • Modal rules (in rule R2 , v is not free in the conclusion). tw (v), tw (sw , rv ), Ω, (A[r/x])v , (|s : sx |A)w , Γ =⇒ ∆ tw (v), tw (sw , xv ), Ω, Γ =⇒ ∆, Av L2 R2 tw (v), tw (sw , rv ), Ω, (|t : sx |A)w , Γ =⇒ ∆ Ω, Γ =⇒ ∆, (|t : sx |A)w • Identity rules (E is an atomic labelled formula or an ancillary one.) Ω, (t = t)w , Γ =⇒ ∆ Ω, E[sw /xw ], E[tw /xw ], (t = s)w , Γ =⇒ ∆ Self id Repl Ω, Γ =⇒ ∆ Ω, E[tw /xw ], (t = s)w , Γ =⇒ ∆ constant c, and not with respect to an arbitrary term t as would be the case with mathematical rules. This reflects the fact that these are not conditions on e-frames, but conditions on e-models governing the behaviour of closed terms. This difference does not impair the admissibility of the structural rules of inferences. To characterize the indexed epistemic logics based on single domain e-frames we have introduced the rule Singdom (see Table 2). 3 Structural Properties In this section we show that the calculi GE.? have the same good structural properties of G3c: all rules are hp-invertible, the rules of weakening and contraction are hp-admissible, and cut is admissible. A few notions are needed in order to prove the results above. In the rules in Tables 1 and 2 (i) the multisets Ω, Γ and ∆ are called contexts, (ii) the other formulas occurring in the conclusion are called principal, and (iii) the formulas of the premisses not occurring in the conclusion are called active. As measures for inductive proofs we use the notions of height of a formula and of height of a derivation. The height of a formula E, h(E), is the length of the longest branch of its construction tree. The height of a derivation D, h(D), is the length of its longest branch. We write GE.? `n Ω, Γ =⇒ ∆ if the sequent Ω, Γ =⇒ ∆ is derivable in GE.? with a derivation of height at most n. Definition 3.1. A rule of inference is (height-preserving) admissible in GE.? if, whenever its premisses are derivable (with height n), also its conclusion is derivable (with at most height n). We assume that the free and bound variables occurring in formulas of a sequent are disjoint. Given that formulas that differ only by a renaming of bound variables are considered identical, we don’t have to prove a lemma of α-conversion, see [6, Lemma 4.1.1]. We also assume, without loss of generality, that the bound variables occurring in a derivation are such that we never have to rename them when applying a substitution. 7 27 Sequent Calculi for IEL Corsi, Orlandelli Table 2: Non-logical rules expressing semantic conditions • Rules for De , Te , 4e , Be In the rule Sera (Serb ) v (xv resp.) is not free in the conclusion. tw (v), Ω, Γ =⇒ ∆ tw (u), tw (tw , sv ), sv (u), Ω, Γ =⇒ ∆ Sera T ransa Ω, Γ =⇒ ∆ tw (tw , sv ), sv (u), Ω, Γ =⇒ ∆ tw (sw , xv ), Ω, Γ =⇒ ∆ tw (r1w , r3u ), tw (tw , sv ), tw (r1w , r2v ), sv (r2v , r3u ), Ω, Γ =⇒ ∆ Serb T ransb Ω, Γ =⇒ ∆ tw (tw , sv ), tw (r1w , r2v ), sv (r2v , r3u ), Ω, Γ =⇒ ∆ tw (w), Ω, Γ =⇒ ∆ sv (w), tw (tw , sv ), Ω, Γ =⇒ ∆ Refa Syma Ω, Γ =⇒ ∆ tw (tw , sv ), Ω, Γ =⇒ ∆ tw (sw , sw ), Ω, Γ =⇒ ∆ sv (r2v , r1w ), tw (tw , sv ), tw (r1w , r2v ), Ω, Γ =⇒ ∆ Refb Symb Ω, Γ =⇒ ∆ tw (tw , sv ), tw (r1w , r2v ), Ω, Γ =⇒ ∆ • Rules for N Ie , N De , CBFe , BFe , SHRTe , GFe In the rule Dsurj (Dtot and Utot) xw (xv resp.) is not free in the conclusion. tw (sw , r1v ), tw (sw , r2v ), Ω, (r1 = r2 )v , Γ =⇒ ∆ rv ∈ D(v), tw (sw , rv ), sw 1 ∈ D(w), Ω, Γ =⇒ ∆ Uf unc Dpres tw (sw , r1v ), tw (sw , r2v ), Ω, Γ =⇒ ∆ tw (sw , rv ), sw ∈ D(w), Ω, Γ =⇒ ∆ tw (r1w , sv ), tw (r2w , sv ), Ω, (r1 = r2 )w , Γ =⇒ ∆ xw ∈ D(w), tw (xw , sv ), tw (v), sv ∈ D(v), Ω, Γ =⇒ ∆ Uinj Dsurj tw (r1w , sv ), tw (r2w , sv ), Ω, Γ =⇒ ∆ tw (v), sv ∈ D(v), Ω, Γ =⇒ ∆ tw (sw , xv ), tw (v), Ω, Γ =⇒ ∆ xv ∈ D(v), tw (sw , xv ), tw (v), sv ∈ D(v), Ω, Γ =⇒ ∆ Utot Dtot tw (v), Ω, Γ =⇒ ∆ tw (v), sw ∈ D(w), Ω, Γ =⇒ ∆ • Rules for rigidity, stability, and single domain e-frames, In the rules Rig and Stab cw and cv are labelled individual constants. tw (cw , cv ), tw (v), Ω, Γ =⇒ ∆ tw (v), tw (cw , sv ), Ω, (c = s)v , Γ =⇒ ∆ Rig Stab tw (v), Ω, Γ =⇒ ∆ tw (v), tw (cw , sv ), Ω, Γ =⇒ ∆ tw ∈ D(w), Ω, Γ =⇒ ∆ Singdom Ω, Γ =⇒ ∆ Table 3: Example: a cut free proof of GFe (using rule Dtot) z v ∈ D(v), tw (y w , z v ), tw (v), y w ∈ D(w), (P x[z/x])v , (|t : yx |P x)w =⇒ (∃xP x)v , (P x[z/x])v R∃ z v ∈ D(v), tw (y w , z v ), tw (v), y w ∈ D(w), (P x[z/x])v , (|t : yx |P x)w =⇒ (∃xP x)v L 2 z v ∈ D(v), tw (y w , z v ), tw (v), y w ∈ D(w), (|t : yx |P x)w =⇒ (∃xP x)v Dtot tw (v), y w ∈ D(w), (|t : yx |P x)w =⇒ (∃xP x)v x[y/x] R2 y w ∈ D(w), (|t : x |P x)w =⇒ (|t : ?|∃xP x)w L∃ (∃x|t : x|P x)w =⇒ (|t : ?|∃xP x)w R → =⇒ (∃x|t : x|P x → |t : ?|∃xP x)w 8 28 Sequent Calculi for IEL Corsi, Orlandelli Lemma 3.2. 1. The rule of substitution of labelled terms is hp-admissible in GE.?: GE.? `n Ω, Γ =⇒ ∆ implies GE.? `n Ω[tw /xw ], Γ[tw /xw ] =⇒ ∆[tw /xw ] 2. The rule of substitution of world labels is hp-admissible in GE.?: GE.? `n Ω, Γ =⇒ ∆ implies GE.? `n Ω[w/v], Γ[w/v] =⇒ ∆[w/v] Proof. (3.2.1) The proof is by induction on the height of the derivation D of Ω, Γ =⇒ ∆. If h(D) = 1, then Ω, Γ =⇒ ∆ is an initial sequent or an instance of L⊥ and also the result of the substitution is an initial sequent or an instance of L⊥ . If h(D) > 1 we distinguish various cases according to the last rule R applied in them. Let us consider just the following two. If R ≡ L2 , we apply the inductive hypothesis (IH) to its premiss and then L2 to obtain a derivation D[tw /xw ] of Ω[tw /xw ], Γ[tw /xw ] =⇒ ∆[tw /xw ] with same derivation height of D. If R ≡ R2 we proceed analogously, but we apply IH twice: the first time to replace the eigenvariables of R with some variables occurring neither in D nor in tw , and the second time to apply the substitution [tw /xw ]. (3.2.2) We proceed as above by induction on h(D). We show the interesting case of R∀ with eigenvariable y v . We transform D: y v ∈ D(v), Ω, Γ =⇒ ∆, (A[y/x])v 3.2.1 (y ∈ D(v))[z v /y v ], Ω, Γ =⇒ ∆, (A[y/x])v [z v /y v ] v IH y v ∈ D(v), Ω, Γ =⇒ ∆, (A[y/x])v z w ∈ D(w), Ω[w/v], Γ[w/v] =⇒ ∆[w/v], (A[z/x])w R∀ R ∀ Ω, Γ =⇒ ∆, (∀xA)v into Ω[w/v], Γ[w/v] =⇒ ∆[w/v], (∀xA)w where both z v and z w do not occur in D. The steps by Lemma 3.2.1 and by IH are hp-admissible, and therefore D[w/v] has the same height of D. Lemma 3.3. All sequents Ω, Aw , Γ =⇒ ∆, Aw , with Aw arbitrary labelled formula, are deriv- able in GE.?. Proof. By an easy induction on h(Aw ). Weakening and contraction. In the following E stands for an arbitrary labelled or ancillary formula and Aw for an arbitrary labelled formula. Theorem 3.4. The left and right rules of weakening are hp-admissible in GE.?: Ω, Γ =⇒ ∆ Ω, Γ =⇒ ∆ L-W R-W Ω, E, Γ =⇒ ∆ Ω, Γ =⇒ ∆, Aw Proof. If E (Aw ) contains world labels used in the proof D of the premiss as eigenvariables, then by Lemma 3.2 we replace those eigenvariables by new variables occurring neither in D nor in E (Aw ). Then the proof proceeds in the standard way by induction on the height of the derivation of the premiss. Lemma 3.5. All rules of GE.? are hp-invertible. Proof. The proof is by induction on the height of the derivation D of the conclusion of the rule R we are considering. Here is a paradigmatic case. Suppose that a proof of `n Ω, Γ =⇒ ∆, (|t : s w x |A) is given and that the last rule applied in that proof is Sera . So we have: (1) `n−1 tw (v), Ω, Γ =⇒ ∆, (|t : sx |A)w , and then by Sera (2) `n Ω, Γ =⇒ ∆, (|t : sx |A)w . 9 29 Sequent Calculi for IEL Corsi, Orlandelli Our aim is to show that (3) `n tw (v), tw (sw , xv ), Ω, Γ =⇒ ∆, Av , where v is the eigenvariable of the instance of Sera we are considering. By applying Lemma 3.2 to (1) (w.r.t. to some u not occurring in D) we get (4) `n−1 tw (u), Ω, Γ =⇒ ∆, (|t : sx |A)w , then by IH to (4) (5) `n−1 tw (u), tw (v), tw (sw , xv ), Ω, Γ =⇒ ∆, Av , and by Sera we conclude (3) `n tw (v), tw (sw , xv ), Ω, Γ =⇒ ∆, Av . Theorem 3.6. The left and right rules of contraction are hp-admissible in GE.?: Ω, E, E, Γ =⇒ ∆ Ω, Γ =⇒ ∆, Aw , Aw L-C R-C Ω, E, Γ =⇒ ∆ Ω, Γ =⇒ ∆, Aw Proof. The proofs are by simultaneous induction on the height of the derivation D of the premiss for left and right contraction. The base case is straightforward. For the inductive cases, we have two subcases for each possible last rule R in D, depending on whether one or no instance of the formula we are contracting is principal in R. If no instance is principal, two instances occur in the premiss(es) and we can apply IH to it and then the rule R. Else, one instance of the contraction formula is principal in R and we have three subcases. (i) If R is a rule with repetition of the principal formulas in the premiss (i.e. either L∀ or L2 or a non-logical rule), we can simply apply IH to the premiss and then the rule. Observe that the non-logical rules we are considering are such that we don’t have to close them under contraction: for T ransb and Symb we have only to apply IH twice, and for Repl, Uf unc and Usurj any contracted instance can be obtained by using IH and then rule Self id. Thus, if the last step in D is by rule Uf unc with E ≡ tw (sw , rv ), we transform Ω, tw (sw , rv ), tw (sw , rv ), (r = r)v , Γ =⇒ ∆ Ω, tw (sw , rv ), tw (sw , rv ), (r = r)v , Γ =⇒ ∆ Uf unc IH Ω, tw (sw , rv ), tw (sw , rv ), Γ =⇒ ∆ Ω, tw (sw , rv ), (r = r)v , Γ =⇒ ∆ L-C Self id Ω, tw (sw , rv ), Γ =⇒ ∆ into Ω, tw (sw , rv ), Γ =⇒ ∆ which has the same derivation height of D. All other non-logical rules cannot have instances with a duplicated principal formula. (ii) If R is a rule where all active formulas are proper subformulas of the principal one (i.e. any propositional rule), we proceed as for G3c. (iii) If R is a rule where active formulas are (a) proper subformulas of the principal one and (b) ancillary formulas (i.e. one of R∀ and R2 ), we start by using the hp-invertibility – Lemma 3.5 – of that rule, then we apply IH as many times as needed and finally the rule R; see [4, Theorem 4.12] for the details. Admissiblity of cut. Theorem 3.7. The rule of cut is admissible in GE.?: Ω, Γ =⇒ ∆, Aw Ω0 , Aw , Π =⇒ Σ 0 Cut Ω, Ω , Γ, Π =⇒ ∆, Σ Proof. The proof is by induction on the height of the cut formula with a subinduction on the cut-height, i.e. the sum of the heights of the derivations of the two premisses. The cases of (i) initial sequents, (ii) cut formula not principal in at least one of the two premisses, and (iii) cut formula principal in both premisses but not of shape (|t : sx |B)w are treated as for G3Kq? , see [7, Theorem 12.9], and are therefore omitted. 10 30 Sequent Calculi for IEL Corsi, Orlandelli If the cut formula is (|t : sx |B)w and it is principal in both premisses, we have a derivation of the form .. .. . D1 . D2 Ω, tw (u), tw (sw , xu ), Γ =⇒ ∆, B u Ω0 , tw (v), tw (sw , rv ), (B[r/x])v , (|t : sx |B)w , Π =⇒ Σ R2 L2 Ω, Γ =⇒ ∆, (|t : sx |B)w Ω0 , tw (v), tw (sw , rv ), (|t : sx |B)w , Π =⇒ Σ Cut Ω, Ω0 , tw (v), tw (sw , rv ), Γ, Π =⇒ ∆, Σ which can be transformed into a derivation of the same conclusion having two cuts that are admissible by IH: first we construct the derivation D3 which has a cut on (|t : sx |B)w of lesser cut-height, .. . D1 .. Ω, tw (u), tw (sw , xu ), Γ =⇒ ∆, B u . D2 R2 Ω, Γ =⇒ ∆, (|t : sx |B)w Ω0 , tw (v), tw (sw , rv ), (B[r/x])v , (|t : sx |B)w , Π =⇒ Σ Cut Ω, Ω0 , tw (v), tw (sw , rv ), (B[r/x])v , Γ, Π =⇒ ∆, Σ Second, we make use of the hp-admissibility of substitutions, Lemma 3.2, to apply the following substitutions to the derivation D1 : first [ru /xu ] and then [v/u]. Observe that it is essential to apply the substitutions in this order since the xu s, but not the xv s, satisfy the variable condition and therefore don’t occur in Ω, Γ, ∆, tw , sw . Now we can apply a cut, which has a cut formula of lesser height and therefore is admissible by IH, to (D1 [ru /xu ])[v/u] and D3 as follows .. .. . (D1 [ru /xu ])[v/u] . D3 0 Ω, t (v), t (sw , rv ), Γ =⇒ ∆, (B[r/x])v w w w v Ω, Ω , t (v), t (s , r ), (B[r/x])v , Γ, Π =⇒ ∆, Σ w w Cut Ω, tw (v), tw (sw , rv ), Ω, Ω0 , tw (v), tw (sw , rv ), Γ, Γ, Π =⇒ ∆, ∆, Σ L-C and R-C, some Ω, Ω0 , tw (v), tw (sw , rv ), Γ, Π =⇒ ∆, Σ The only case where the cut formula can be principal in a non-logical rule is when the cut formula is atomic and we are dealing with a rule for identity. Thus the presence of non-logical rules from Table 2 has no role w.r.t. the admissibility of Cut. We are now going to show that the rules Self id and Repl are enough to capture the logic of identity and, by using the admissibility of cut, that the rule that generalizes Repl to arbitrary Lext -formulas is admissible. Lemma 3.8. 1. GE.? ` =⇒ (t = t)w 2. GE.? ` (r1 = r2 )w , (A[r1 /y])w =⇒ (A[r2 /y])w 3. The following rule, where E is an arbitrary Lext -formula, is admissible in GE.? Ω, E[sw /xw ], E[tw /xw ], (t = s)w , Γ =⇒ ∆ ReplA Ω, E[tw /xw ], (t = s)w , Γ =⇒ ∆ Proof. 3.8.1. The sequent =⇒ (t = t)w is derivable by applying Self id to the initial sequent (t = t)w =⇒ (t = t)w . 3.8.2. By induction on h(Aw ). The only interesting case is Aw ≡ (|t : sx |B)w where, instead of IH, we have to use Lemma 3.3. This happens because formulas with an indexed epistemic operator as principal behave like atomic formulas with respect to substitutions. 3.8.3. If E ≡ Aw with Aw not atomic, we proceed as follows: 11 31 Sequent Calculi for IEL Corsi, Orlandelli 3.8.2 (A[t/x])w , (t = s)w =⇒ (A[s/x])w Ω, (A[s/x])w , (A[t/x])w , (t = s)w , Γ =⇒ ∆ Cut Ω, (A[t/x])w , (A[t/x])w , (t = s)w , (t = s)w , Γ =⇒ ∆ L-C, 2 times Ω, (A[t/x])w , (t = s)w , Γ =⇒ ∆ 4 Soundness and Completeness Soundness. The proof of soundness is structured as in [5, 7]; we proceed, in brief, by defining what it means for a sequent to be valid on a class of e-frames, and then we show that initial sequents are valid on any e-frames and that each rule of GE.? preserves validity over the appropriate class of e-frames C ? . Definition 4.1. Let W ? be the set of all world labels occurring in a sequent S, M = hW, U, D, ≺, , Ii a t-model, f be a mapping from W ? to W, and f ? be a function asso- ciating to each f (w) some f (w)-assignment σ that we agree to indicate with σf (w) . We say that: hf, f ? , Mi satisfies Aw (∈ S) iff σf (w) |=M f (w) A; hf, f ? , Mi satisfies tw (v) (∈ S) iff σf (w) (t) ≺ f (v); σf (w) (r) hf, f ? , Mi satisfies rw (tw , sv ) (∈ S) iff σf (w) (t)  σf (v) (s); hf, f ? , Mi satisfies tw ∈ D(w) (∈ S) iff σf (w) (t) ∈ Dw . Definition 4.2 (C ? -validity). A sequent Ω, Γ =⇒ ∆ is said to be C ? -valid iff every triple hf, f ? , Mi where M is (rigid and/or stable and) based on a e-frame in C ? is such that: if hf, f ? , Mi satisfies all formulas in Ω, Γ, then it satisfies some formula in ∆. Theorem 4.3 (Soundness). If GE.? ` Ω, Γ =⇒ ∆, then Ω, Γ =⇒ ∆ is C ? -valid (on rigid and/or stable models if the corresponding rules are in GE.?). Proof. The proof is by induction on the height of the derivation D of the sequent Ω, Γ =⇒ ∆. The base case holds trivially since either some (P t1 . . . tn )w occurs both in Γ and in ∆, or ⊥w occurs in Γ. For the inductive step, we distinguish cases according to the last rule applied in D. We omit the cases of the propositional rules and of the rules for ∀, see [7, Theorem 12.13]. If the last step of D is tw (v), tw (sw , rv ), Ω, (A[r/x])v , (|t : sx |A)w , Γ =⇒ ∆ L2 tw (v), tw (sw , rv ), Ω, (|t : sx |A)w , Γ =⇒ ∆ we know by IH that any triple hf, f ? , Mi satisfying all the formulas in the antecedent of the premiss satisfies also some formula in ∆. The antecedent of the conclusion differs from the antecedent of the premiss insofar as the formula (A[r/x])v is missing. Nevertheless, any triple hf, f ? , Mi satisfying tw (v), tw (sw , rv ), (|t : sx |A)w satisfies also (A[r/x])v . If the last step is tw (v), tw (sw , xv ), Ω, Γ =⇒ ∆, Av R2 Ω, Γ =⇒ ∆, (|t : sx |A)w 12 32 Sequent Calculi for IEL Corsi, Orlandelli where sw and xv are tuples of length n, we know by IH that the premiss is C ? -valid. Let hf, f ? , Mi be a generic triple that is defined w.r.t. the language of the conclusion and such that it satisfies all formulas in Ω, Γ. Either there are some u ∈ W such that σf (w) (tw ) ≺ u and some σf (w) (tw ) o1 , . . . , on ∈ Uu such that, for all sw w w i ∈ s , σf (w) (si )  oi , or not. If not, it can be seen that hf, f , Mi trivially satisfies (|t : x |A) . Otherwise, we extend f and f ? to f 0 and (f 0 )? ? s w such that: f 0 (v) = u and (f 0 )? (u) = σu for some σu such that: σu (xvi ) = oi for all xi ∈ xv (this extension is feasible thanks to the variable condition of R2 ). The triple hf 0 , (f 0 )? , Mi satisfies all the formulas in the antecedent of the premiss and, therefore, it satisfies also some formula in ∆ or it satisfies Av . In the former case we have that the non-extended triple hf, f ? , Mi satisfies some formula in ∆ and in the latter that it satisfies (|t : sx |A)w . If the last step is by some mathematical rule, it can at once be seen that the theorem holds since M is (rigid and/or stable and) based on a e-frame in C ? and = is interpreted as real identity. Suppose that the last step is by a geometrical rule, say xw ∈ D(w), tw (xw , sv ), tw (v), sv ∈ D(v), Ω, Γ =⇒ ∆ Dsurj, xw fresh tw (v), sv ∈ D(v), Ω, Γ =⇒ ∆ Take any triple hf, f ? , Mi such that (i) it is defined w.r.t. the language of the conclusion, (ii) it satisfies all formulas in tw (v), sv ∈ D(v), Ω, Γ, and (iii) M is based on a D-surjective e-frame. Thanks to (i), (ii) and (iii), we can extend f and f ? to obtain a triple hf 0 , (f 0 )? , Mi satisfying all formulas in the antecedent of the premiss. By IH this triple satisfies also some formula in ∆. We conclude that also hf, f ? , Mi satisfies some formula in ∆ because xw doesn’t occur in the conclusion. Completeness. We follow the pattern of [7, Theorem 12.14] for G3.Kq? : we give a con- structive proof of (weak) completeness by defining a root-first proof search procedure. The procedure is such that if it terminates, the sequent is derivable and therefore valid; otherwise the tree generated by the proof search has at least one infinite branch. Such an infinite branch contains all the information needed to construct a countermodel for Ω, Γ =⇒ ∆ based on a e-frame in C ? . In order to set up the procedure, it is expedient to add for each w an infinite set of new individual constants cw , and to consider sequents Ω, Γ =⇒ ∆ containing only closed formulas. Definition 4.4 (?-reduction tree). Given a sequent Ω, Γ =⇒ ∆ containing only closed formulas and a calculus GE.?, we define the following procedure for constructing a ?-reduction tree T : Stage 0. We write Ω, Γ =⇒ ∆ as root of T . Stage n+1 Two cases need to be distinguished. Case (i). Each topmost sequent of the n-th stage of T is an initial sequent or an instance of L⊥ . The construction ends. Case (ii). Else we continue the construction by applying the following 8 + k + 1 substages (k is the number of non-logical rules of GE.?) to all the leaves of the tree generated at the previous (sub)stage which are not initial sequents or instances of L⊥ . Substage 1. We reduce all formulas of the form (A → B)w occurring in the antecedent as follows: if the leaf is Ω, (A1 → B1 )w1 , . . . , (An → Bn )wn , Γ =⇒ ∆ we write over it the new 2n topmost sequents: Ω, (Bi1 )wi1 , . . . , (Bik )wik , Γ =⇒ ∆, (Aik+1 )wik+1 , . . . , (Ain )win 13 33 Sequent Calculi for IEL Corsi, Orlandelli where {i1 , . . . , ik } ⊆ {1, . . . , n} and {ik+1 , . . . , in } = {1, . . . , n} − {i1 , . . . , ik }. Substage 2. We reduce all formulas (A → B)w occurring in the succedent of the leaf by applying, root-first, all possible instances of R→ . Substage 3. We apply, root-first, all possible instances of L∀ : for any pair of Lext -formulas (∀xA)w and tw ∈ D(w) occurring in the antecedent of the leaf, we add to the new topmost sequent the formula (A[t/x])w . Substage 4. For each formula (∀xA)w occurring in the succedent, we apply, root-first, rule R∀ by using a fresh constant cw . Substage 5. We apply, root-first, all possible instances of L2 : for any set of Lext -formulas tw (v), tw (sw , rv ), (|t : sx |A)w occurring in the antecedent of the leaf, we add to the new topmost sequent the formula (A[r/x])v . Substage 6. For each formula (|t : sx |A)w occurring in the succedent, we apply, root-first, rule R2 by using a fresh world label v. Substage 7. We apply, root-first, rule Self id for every labelled constant occurring in the leaf. Substage 8. We apply, root-first, all possible instances of rule Repl. substage 8+j. We apply, root-first, all possible instances of the j-th non-logical rule R of GE.?. If R is a mathematical rule, we apply it w.r.t. all constants occurring in the topmost sequent for which we can apply it. If R is a geometrical rule, we apply it w.r.t. some new labelled constant. Substage 8+k+1. If at no previous substage we have introduced some new topmost sequent, we write a copy of the topmost sequent on top of itself. Definition 4.5. Given an infinite branch B of a ?-reduction tree, • LB (RB ) denotes the set of all formulas occurring in the antecedents (succedents) of B. • if tw and sw are constants occurring in formulas of sequents of B, tw ≈ sw =df (t = s)w ∈ LB Given the ?-reduction procedure and Lemma 3.8, ≈ is an equivalence relation. By [tw ] we denote the equivalence class of tw modulo ≈. Definition 4.6. Let B be an infinite branch of a ?-reduction tree. We define the model MB = hW B , U B , DB , ≺B , B , I B i as: • W B is the set of world labels occurring in LB ∪ RB ; • U B is the family of all sets Uw where w ∈ W B and Uw is the set of all equivalence classes [cw ], where cw is a labelled constant occurring in LB ∪ RB ; • DB is the family of the sets Dw = {[cw ] : cw ∈ D(w) occurs in LB }; • ≺B is such that [tw ] ≺B v iff tw (v) occurs in LB ; [tw ] • B is such that, for all w ∈ W B and all [tw ] ∈ Uw , [sw ]  [rv ] iff tw (sw , rv ) occurs in LB ; • I B maps each w ∈ W B to an interpretation Iw such that (i) Iw (cw ) = [cw ] for every cw occurring in LB ∪ RB ; (ii) Iw (P n ) = {h[tw w n w B 1 ], . . . , [tn ]i : (P t1 , . . . , tn ) occurs in L }. Theorem 4.7 (Completeness). Any sequent Ω, Γ =⇒ ∆ not containing free variables is such that either it is derivable in GE.? or there is some M, which is (rigid/stable and) based on a member of C ? , that satisfies all unlabelled version of the formulas in Γ and no one in ∆. 14 34 Sequent Calculi for IEL Corsi, Orlandelli Proof. We build a ?-reduction tree T of Ω, Γ =⇒ ∆. If T is a finite tree, then Ω, Γ =⇒ ∆ is derivable and the theorem is proved. Otherwise the proof search fails and, by König’s Lemma, T has an infinite branch B out of which we can construct a model MB as in Defn. 4.6. We know that B B if Aw occurs in LB (RB ), then |=Mw A ( 6|=M w A) (4) This claim, which can be proved by an easy induction on h(Aw ), is enough to conclude that B M satisfies all (unlabelled) members of Γ and no member of ∆. We prove just one case of (4), if Aw ≡ (|t : sx |B)w occurs in RB , the ?-reduction is such that that formula has been reduced at some stage. Thus the antecedent of some sequent of B (and LB ) contains tw (v) and tw (sw , cv ) B and its succedent (and RB ) contains (B[c/x])v . By IH, this last fact implies that 6|=M v B[c/x], B [tw ] and therefore 6|=M i ]  [ci ] for all si ∈ s and ci ∈ c . |t : sx |B, since [tw ] ≺B v and [sw v w w v v w B ? To show that M is (rigid/stable and) based on a e-frame in C , just notice that the ‘if’- clause of some instance of any semantic Condition, which holds in C ? , can be satisfied in MB only if the corresponding ancillary formulas occur in some node of B. Thus, at substage 8 + j of some stage of the construction of the ?-reduction tree, the formulas corresponding to the ‘then’-clause of Condition have been added to the antecedent (by rule Cond), and therefore they occur in LB . Given the way we have constructed MB , this means that the ’then’-clause of the given instance of Condition holds in MB , and by generalization we conclude that MB is (rigid/stable and) based on a member of C ? . Concluding remarks. In this paper we have introduced a labelled sequent calculus for every IEL considered in [1, 2]. These calculi have good structural properties insofar as weakening and contraction are hp-admissible and cut is admissible. In this way we have answered the question of finding a cut-free calculus for logics with GFe , [1, p.1182]. Then we have shown that each calculus GE.? is sound and complete w.r.t. the corresponding class of e-frames C ? . In particular the proof of completeness is based on a procedure that gives a proof in GE.? of every C ? -valid sequent and a countermodel (based on a e-frame in C ? ) of every sequent which is not C ? -valid. Given Prop. 1.8, we have also implicitly introduced a labelled calculus for every term-modal logic considered in [3], as well as for the TML based on symmetric structures, which weren’t considered in [3]. The completeness of the calculi gives us also a semantic proof that cut is admissible therein, proof which backs up the constructive proof given in Theorem 3.7. References [1] Giovanna Corsi and Eugenio Orlandelli. Free quantified epistemic logics. Studia Logica, 101(6):1159– 1183, 2013. [2] Giovanna Corsi and Gabriele Tassi. A new approach to epistemic logic. In Erik Weber, Dietlinde Wouters, and Joke Meheus, editors, Logic, Reasoning, and Rationality, volume 5 of Logic, Argu- mentation & Reasoning, pages 27–44. Springer Netherlands, 2014. [3] Melvin Fitting, Lars Thalmann, and Andrei Voronkov. Term-modal logics. Studia Logica, 69(1):133– 169, 2001. [4] Sara Negri. Proof analysis in modal logic. J. Philosophical Logic, 34(5-6):507–544, 2005. [5] Sara Negri. Kripke completeness revisited. In Giuseppe Primiero and Sahid Rahman, editors, Acts of Knowledge: History, Philosophy and Logic, pages 233–266. College University Press, 2009. [6] Sara Negri and Jan von Plato. Structural Proof Theory. Cambridge University Press, 2001. [7] Sara Negri and Jan von Plato. Proof Analysis - A Contribution to Hilbert’s Last Problem. Cambridge University Press, 2011. 15 35