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.
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 [
In [
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.
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
∀z((B[z/y])[t/x])
∀y(B[t/x])
|s[t/x] : sx11[t/x] . . . sxnn[t/x]|B .
if y ≡ x,
if y 6≡ x and y ≡ t,
where z is new for A and z 6≡ t,
if y 6≡ x and y 6≡ t
(|s : sx11 . . . sxnn |B)[t/x]
=df
=df
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 [
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, Iwi : 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 U = {Uw : w ∈ W} D = {Dw : Dw ⊆ Uw} ≺ ⊆ U × W
a = {
: a ∈ U } I is is is is is is a non-empty set of worlds. a family of pairwise disjoint non-empty sets indexed by members of W: the outer domains. a family of inner domains indexed by members of W. the compatibility relation between agents and worlds: a ≺ w means that the world w is compatible with a’s knowledge. 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 according to a’s knowledge. a function associating to every w ∈ W a first-order interpretation 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) 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, σ |=wM A, is so defined: σ 6|=wM ⊥ σ |=wM P t1, . . . , tn σ |=wM B → C σ |=wM ∀xB σ |=wM |t : sx11 . . . sxnn |B ⇐⇒ ⇐⇒ ⇐⇒ ⇐⇒ σ(si) hσ(t1), . . . , σ(tn)i ∈ Iw(P ) σ 6|=wM B or σ |=wM C for all a ∈ Dw, σx.a |=wM B for all v s.t. σ(t) ≺ v and for all v-assignment τ s.t.
σ(t)
τ (xi), 1 ≤ i ≤ n, we have that τ |=vM B
The notions of truth in a world, |=wM 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.
Name Formula is valid on
e-frames such that |t : sx|A → ¬|t : sx|¬A |t : sx|A → A |t : sx|A → |t : sx ty| |y : x|A serial reflexive transitive (a) (b) (a) (b) (a) A → |t : sx ty| ¬|y : x|¬A
symmetric (a) (b) ∀a, b ∈ Uw∀c, d ∈ Uv∀e ∈ Uu (a d&b
c&c (b) ∀a, b ∈ Uw∀c, d ∈ Uv (a ∀a ∈ Uw∃v ∈ W (a ≺ v)
a ∀a, b ∈ Uw∃c ∈ Uv (b ∀a ∈ Uw (a ≺ w)
a ∀a, b ∈ Uw (b b) ∀a ∈ Uw∀b ∈ Uv (a a
c) ∀a ∈ Uw∀b ∈ Uv (a a a a a d&b b&b ≺ u ⊃ a ≺ u) d a
e ⊃ b b ⊃ b ≺ w) a c& ⊃ c d e) b)
De 4e CBFe BFe GFe N Ie N De SHRTe |t : sx y|A → |t : sx|A |t : sx|∀yA → ∀y|t : sx y|A ∀y|t : sx y|A → |t : sx|∀yA ∃y|t : sx y|A → |t : sx|∃yA t1 = t2 → |s : tx1 ty2 |x = y t1 6= t2 → |s : tx1 ty2 |x 6= y
D-preservative D-surjective D-total U -total U -functional U -injective (a ≺ v ⊃ ∃c ∈ Uv (b ∀a, b ∈ Uw∀c, d ∈ Uv
a a (b c&b d ⊃ c = d) ∀a, b, c ∈ Uw∀d ∈ Uv
a a (b d&c d ⊃ b = c) a a a b)) c)) c)) We will use CX,... 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. Definition 1.6. Let c be any individual constant, we say that
a
Iv(c) ;
b then b = Iv(c) ). a Proposition 1.7. Let c be any individual constant, it holds that
|=M |t : cx|A → |t : ?|(A[c/x]) ;
|=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 [
2
In this section we introduce labelled sequent calculi in order to characterize the indexed
epistemic 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 [
Given a labelled formula Aw and a term t, we want to pin down those occurrences of t in Aw, 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 nt1 . . . 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 Bw or t is a w-ground occurrence in Cw, • t is a w-ground occurrence in (∀xB)w iff t ≡ x or t is a w-ground occurrence in Bw, • t is a w-ground occurrence in |s : sx11 . . . sxnn |B iff t ≡ s or t ≡ si, for some i, 1 ≤ i ≤ n.
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(tiw, riv) : tiw ∈ tw and riv ∈ rv}.
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. σ |=wM |t : sx|P x ⇐⇒ for all v s.t. σ(t) ≺ v and for all v-assignment τ s.t. σ(s)
it holds that τ |=vM P x Reading from right to left, we get the following right introduction rule: tw(v), tw(sw, xv), Ω, Γ =⇒ Δ, (P xv)v Ω, Γ =⇒ Δ, (|tw : sxw |P x)w
R2 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: tw(v), tw(sw, rv), (P xv)v[rv/xv], (|tw : sxw |P x)w, Ω, Γ =⇒ Δ tw(v), tw(sw, rv), (|tw : sxw |P x)w, Ω, Γ =⇒ Δ L2 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 worldindependent 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
(P w is an atomic labelled formula) • Initial sequents
Ω, P w, Γ =⇒ Δ, P w •
Ω, ⊥w, Γ =⇒ Δ
L⊥ Ω, Γ =⇒ Δ, Aw Ω, Bw, Γ =⇒ Δ Ω, (A → B)w, Γ =⇒ Δ
L→
Ω, Aw, Γ =⇒ Δ, Bw Ω, Γ =⇒ Δ, (A → B)w R→ • Quantifier rules (in the rule R∀, yw is not free in the conclusion). tw ∈ D(w), Ω, (A[t/x])w, (∀xA)w, Γ =⇒ Δ tw ∈ D(w), Ω, (∀xA)w, Γ =⇒ Δ
L∀ yw ∈ D(w), Ω, Γ =⇒ Δ, (A[y/x])w Ω, Γ =⇒ Δ, (∀xA)w
R∀ • 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, Γ =⇒ Δ • Identity rules (E is an atomic labelled formula or an ancillary one.) Ω, (t = t)w, Γ =⇒ Δ Ω, Γ =⇒ Δ
Self id 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
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. • Rules for De,Te,4e,Be In the rule Sera (Serb) v (xv resp.) is not free in the conclusion.
tw(v),Ω,Γ =⇒ Δ Sera
Ω,Γ =⇒ Δ tw(sw,xv),Ω,Γ =⇒ Δ Serb
Ω,Γ =⇒ Δ tw(w),Ω,Γ =⇒ Δ Refa
Ω,Γ =⇒ Δ tw(sw,sw),Ω,Γ =⇒ Δ Refb Ω,Γ =⇒ Δ tw(u),tw(tw,sv),sv(u),Ω,Γ =⇒ Δ tw(tw,sv),sv(u),Ω,Γ =⇒ Δ
Transa tw(r1w,r3u),tw(tw,sv),tw(r1w,r2v),sv(r2v,r3u),Ω,Γ =⇒ Δ tw(tw,sv),tw(r1w,r2v),sv(r2v,r3u),Ω,Γ =⇒ Δ
Transb sv(w),tw(tw,sv),Ω,Γ =⇒ Δ Syma
tw(tw,sv),Ω,Γ =⇒ Δ sv(r2v,r1w),tw(tw,sv),tw(r1w,r2v),Ω,Γ =⇒ Δ Symb
tw(tw,sv),tw(r1w,r2v),Ω,Γ =⇒ Δ • Rules for NIe,NDe,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,Γ =⇒ Δ Ufunc tw(sw,r1v),tw(sw,r2v),Ω,Γ =⇒ Δ rv ∈ D(v),tw(sw,rv),s1w ∈ D(w),Ω,Γ =⇒ Δ Dpres tw(sw,rv),sw ∈ D(w),Ω,Γ =⇒ Δ tw(r1w,sv),tw(r2w,sv),Ω,(r1 = r2)w,Γ =⇒ Δ Uinj xw ∈ D(w),tw(xw,sv),tw(v),sv ∈ D(v),Ω,Γ =⇒ Δ Dsurj tw(r1w,sv),tw(r2w,sv),Ω,Γ =⇒ Δ tw(v),sv ∈ D(v),Ω,Γ =⇒ Δ tw(sw,xv),tw(v),Ω,Γ =⇒ Δ Utot tw(v),Ω,Γ =⇒ Δ xv ∈ D(v),tw(sw,xv),tw(v),sv ∈ D(v),Ω,Γ =⇒ Δ Dtot 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),Ω,Γ =⇒ Δ Rig
tw(v),Ω,Γ =⇒ Δ tw ∈ D(w),Ω,Γ =⇒ Δ
Singdom Ω,Γ =⇒ Δ tw(v),tw(cw,sv),Ω,(c = s)v,Γ =⇒ Δ tw(v),tw(cw,sv),Ω,Γ =⇒ Δ
Stab zv ∈ Dz(vv∈),Dtw((vy)w,,twzv(y),wt,wz(vv)),,tyww(v∈),Dyw(w∈),D(P(wx[)z,/(Px]x)v[z,/(|xt]):vyx,|(P|tx:)wyx|P=⇒x)w(∃=x⇒Px()∃vx,P(Pxx)v[z/Lx2])v R∃ zv ∈ D(v),tw(yw,zv),tw(v),yw ∈ D(w),(|t : yx|Px)w =⇒ (∃xPx)v Dtot tw(v),yw ∈ D(w),(|t : yx|Px)w =⇒ (∃xPx)v yw ∈ D(w),(|t : xx[y/x]|Px)w =⇒ (|t : ?|∃xPx)w R2
L∃ (∃x|t : x|Px)w =⇒ (|t : ?|∃xPx)w =⇒ (∃x|t : x|Px → |t : ?|∃xPx)w R→ 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] 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]. with(3e.i2g.e2n)variWabelepyrvo.ceWede atsraanbsofovrembyDi:nduction on h(D). We show the interesting case of R∀ yv ∈ D(v), Ω, Γ =⇒ Δ, (A[y/x])v (yv ∈ D(v))[zv/yv], Ω, Γ =⇒ Δ, (A[y/x])v[zv/yv] 3.2.1 zw ∈ D(w), Ω[w/v], Γ[w/v] =⇒ Δ[w/v], (A[z/x])w IH
R∀ Ω[w/v], Γ[w/v] =⇒ Δ[w/v], (∀xA)w yv ∈ D(v), Ω, Γ =⇒ Δ, (A[y/x])v Ω, Γ =⇒ Δ, (∀xA)v
R
∀ into where both zv and zw 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 derivable 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.?: Ω, Γ =⇒ Δ Ω, E, Γ =⇒ Δ L-W
Ω, Γ =⇒ Δ Ω, Γ =⇒ Δ, Aw R-W 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 : sx|A)w 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. 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.
(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, Γ =⇒ Δ Ω, E, Γ =⇒ Δ
L-C Ω, Γ =⇒ Δ, Aw, Aw Ω, Γ =⇒ Δ, Aw
R-C 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, U f unc and U surj any contracted instance can be obtained by using IH and then rule Self id. Thus, if the last step in D is by rule U f unc with E ≡ tw(sw, rv), we transform Ω, tw(sw, rv), tw(sw, rv), (r = r)v, Γ =⇒ Δ Ω, tw(sw, rv), tw(sw, rv), Γ =⇒ Δ Ω, tw(sw, rv), Γ =⇒ Δ L-C
U f unc into Ω, tw(sw, rv), tw(sw, rv), (r = r)v, Γ =⇒ Δ Ω, tw(sw, rv), (r = r)v, Γ =⇒ Δ Ω, tw(sw, rv), Γ =⇒ Δ
IH Self id 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.
Theorem 3.7. The rule of cut is admissible in GE.?: Ω, Γ =⇒ Δ, Aw Ω, Ω0, Γ, Π =⇒ Δ, Σ Ω0, Aw, Π =⇒ Σ
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. R2
R2
If the cut formula is (|t : sx|B)w and it is principal in both premisses, we have a derivation of the form .
. Ω, tw(u), tw(sw.,Dxu1), Γ =⇒ Δ, Bu Ω, Γ =⇒ Δ, (|t : sx|B)w . .
. D2 Ω0, tw(v), tw(sw, rv), (B[r/x])v, (|t : sx|B)w, Π =⇒ Σ Ω0, tw(v), tw(sw, rv), (|t : sx|B)w, Π =⇒ Σ
Cut
L2 Ω, Ω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, .
. Ω, tw(u), tw(sw.,Dxu1), Γ =⇒ Δ, Bu Ω, Γ =⇒ Δ, (|t : sx|B)w Ω, Ω0, tw(v), tw(sw, rv), (B[r/x])v, Γ, Π =⇒ Δ, Σ . .
. D2 Ω0, tw(v), tw(sw, rv), (B[r/x])v, (|t : sx|B)w, Π =⇒ Σ Cut 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 xus, but not the xvs, 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] Ω, tw(v), tw(sw, rv), Γ =⇒ Δ, (B[r/x])v . .
. D3 Ω, Ω0, tw(v), tw(sw, rv), (B[r/x])v, Γ, Π =⇒ Δ, Σ Ω, tw(v), tw(sw, rv), Ω, Ω0, tw(v), tw(sw, rv), Γ, Γ, Π =⇒ Δ, Δ, Σ Ω, Ω0, tw(v), tw(sw, rv), Γ, Π =⇒ Δ, Σ
Cut L-C and R-C, some 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, Γ =⇒ Δ Ω, E[tw/xw], (t = s)w, Γ =⇒ Δ
ReplA 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: (A[t/x])w, (t = s)w =⇒ (A[s/x])w 3.8.2
Ω, (A[s/x])w, (A[t/x])w, (t = s)w, Γ =⇒ Δ Ω, (A[t/x])w, (A[t/x])w, (t = s)w, (t = s)w, Γ =⇒ Δ Ω, (A[t/x])w, (t = s)w, Γ =⇒ Δ
L-C, 2 times 4
Soundness. The proof of soundness is structured as in [
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 associating 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) hf, f ?, Mi satisfies
tw(v) (∈ S) hf, f ?, Mi satisfies
rw(tw, sv) (∈ S) hf, f ?, Mi satisfies tw ∈ D(w) (∈ S) σf(w) |=fM(w) A; σf(w)(t) ≺ f (v);
σf(w)(r) σf(w)(t) σf(w)(t) ∈ Dw.
σf(v)(s); 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].
tw(v), tw(sw, rv), Ω, (A[r/x])v, (|t : sx|A)w, Γ =⇒ Δ tw(v), tw(sw, rv), Ω, (|t : sx|A)w, Γ =⇒ Δ
L2 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 Ω, Γ =⇒ Δ, (|t : sx|A)w
R2 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 siw ∈ sw, σf(w)(siw) oi, or not. If not, it can be seen that hf, f ?, Mi trivially satisfies (|t : sx|A)w. Otherwise, we extend f and f ? to f 0 and (f 0)? such that: f 0(v) = u and (f 0)?(u) = σu for some σu such that: σu(xiv) = 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), Ω, Γ =⇒ Δ tw(v), sv ∈ D(v), Ω, Γ =⇒ Δ
Dsurj, xw fresh 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 constructive 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
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 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.
• 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 ≈.
MB = hWB, U B, DB, ≺B, B, IBi as: We define the model • WB is the set of world labels occurring in LB ∪ RB; • U B is the family of all sets Uw where w ∈ WB 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; •
B is such that, for all w ∈ WB and all [tw] ∈ Uw, [sw] [tw] [rv] iff tw(sw, rv) occurs in LB; • IB maps each w ∈ WB to an interpretation Iw such that (i) Iw(cw) = [cw] for every cw occurring in LB ∪ RB; (ii) Iw(P n) = {h[t1w], . . . , [tnw]i : (P nt1, . . . , tn)w occurs in LB}. 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 Δ. 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¨onig’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 if Aw occurs in LB (RB), then |=wMB A ( 6|=wMB A) (4)
This claim, which can be proved by an easy induction on h(Aw), is enough to conclude that MB 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) and its succedent (and RB) contains (B[c/x])v. By IH, this last fact implies that 6|=vMB B[c/x], and therefore 6|=wMB |t : sx|B, since [tw] ≺B v and [siw] [tw] [civ] for all siw ∈ sw and civ ∈ cv.
To show that MB 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 [