Hao Wu Hans van Ditmarsch Jinsheng Chen

Abstract. Public announcement logic (PAL) is an extension of epistemic logic (EL) with some reduction axioms.In this paper,we propose a cut free labelled sequent calculus for PAL,which is an extension of that for EL with sequent rules adapted from the reduction axioms.This calculus admits cut and allows terminating proof search.

1 Introduction

The modern modal approach to the logic of knowledge and belief was exten sively developed by Hintikka([10])to interpret epistemic notions utilizing possible world semantics.The standard multi agent epistemic logic EL is usually identified with the poly modal modal logic S5 for a group of agents.Public announcement logic(PAL),introduced by Plaza([17]),is an extension of EL that studies logical dynam ics of epistemic information after the action of public announcement.More general actions are studied in action model logic(see e.g.[4,5,7]).

PAL is an extension of EL with announcement operators of the form[φ].As EL,formulas in PAL are interpreted in Kripke models in which all relations are reflexive,transitive and symmetric.In particular,formulas of the form[φ]ψare interpreted in the restrictions of Kripke models induced by the announcementφ.The Hilbert style axiomatization of PAL is obtained by adding to that of EL the so calledreduction axiomsfor announcement operators,which can be used to eliminate announcement operators in a PAL formula.

Generally speaking,it is difficult to prove whether proof search using a Hilbert style axiomatization is decidable.In view of these,many proof systems for PAL are proposed in the literature,e.g.,tableau systems([3]),labelled sequent calculi([2,16]).

In this paper,we propose another labelled sequent calculus for PAL.This cal culus is based on a labelled sequent calculus for EL proposed by Hakli and Negri([9])and rules for announcement operators designed according to the reduction ax ioms.This calculus admits structural rules (including cut) and allows terminating proof search.Unlike [2,16],which are based on another semantics for PAL,our calculus is based on the original semantics and takes into account the conditions of reflexivity,transitivity and symmetry in EL.

The rest of the paper is structured as follows:Section 2 presents some basic notions and concepts.Section 3 presents our labelled sequent calculusGPALfor PAL.Section 4 shows thatGPALadmits some structural rules,including cut.Section 5 shows thatGPALallows terminating proof search.Section 6 comparesGPALwith related works,concludes the paper and discusses future work.

2 Preliminaries

2.1 EL and PAL

Let Prop be a denumerable set of variables and Ag a finite set of agents.Lan guageLELfor epistemic logic is defined inductively as follows:

Moreover,languageLPALfor public announcement logic is defined inductively as follows:

wherep ∈Prop anda ∈Ag.We useφ ?ψas an abbreviation for(φ →ψ)∧(ψ →φ).LPALis an extension ofLELwith announcement formulas.

Anepistemic frame Fis a tuple(W,{～a}a∈Ag),whereWis a set of states and～a?W ×Wis a reflexive,transitive and symmetric relation for eacha ∈Ag.

Anepistemic model Mis a tuple (W,{～a}a∈Ag,V) where (W,{～a}a∈Ag) is an epistemic frame andVis a function from Prop toP(W).

LetM=(W,{～a}a∈Ag,V)be an epistemic model andw ∈W.The notion ofφbeingtrueatwinM(notation:M,w?φ)is defined inductively as follows:

A formulaφisglobally truein an epistemic model (notation:M?φ) ifM,w?φfor allw ∈W.A formulaφisvalidin an epistemic frameFifF,V?φfor all valuationsV.

Epistemic logic EL is the set ofLELformulas that are valid on the class of all epistemic frames.Public announcement logic PAL is the set ofLPALformulas that are valid on the class of all epistemic frames.

EL is axiomatized by(Tau),(K),(4),(T),(5),(MP)and(GKa).PAL is axiom atized by the axiomatization for EL plusreduction axioms(R1)–(R6):

Remark 1.The standard language for PAL does not contain→.To simplify our writing,we add→to our language.Because of its existence,(R4) is added to the axiomatization.

2.2 Labelled sequent calculus

A labelled sequent calculus for a logic with Kripke semantics is based on the internalization of Kripke semantics.

LetF=(W,{～a}a∈Ag) be an epistemic frame.Arelational atomis of the formx ～a y,wherex,y ∈Wanda ∈Ag.Alabelled formulais of the formx：φ,wherex ∈Wandφis anLELformula.We useσ,δwith or without subscript to denote relational atoms or labelled formulas.

Amultisetis a ‘set with multiplicity’,or put the other way round,a sequence modulo the ordering.Alabelled sequentis of the form Γ??where Γ,?are finite multisets of relational atoms and labelled formulas.Asequent ruleis of the form

wherem ≥0.Γ1??1,...,Γm ??mare calledpremisesof this rule and Γ??is called the conclusion.Ifm=0,we simply write Γ??and call it aninitial sequent.The formula with the connective in a rule is theprincipalformula of that rule,and its components in the premisses are theactiveformulas.Alabelled sequent calculusis a set of sequent rules.A derivation in a labelled sequent calculusGis defined as usual.Thederivation height hof a sequent is defined as the length of longest branch in the derivation of the sequent.We useG ?Γ??to denote that Γ??is derivable inGandG ?hΓ??to denote that Γ??is derivable inGwith a derivation of height which is at mosth.

A sequent rule(R)isadmissibleinGifG ?Γi ??ifor 1≤i ≤mimpliesG ?Γ??.It isheight preserving admissibleifG ?hΓi ??ifor 1≤i ≤mimpliesG ?hΓ??.

LetM=(W,{～a}a∈Ag,V)be an epistemic model.Theinterpretation τMof relational atoms and labelled formulas are defined as follows:

A labelled sequentσ1,...,σm ?δ1,...,δnisvalidif

is true,whereM=(W,{～a}a∈Ag,V) is an epistemic model,andx1,...,xkare variables occurring inσ1,...,σm ?δ1,...,δnranging overW.

A sequent ruleRisvalidif the validity of all the premises implies the validity of the conclusion.

Given a labelled sequent calculusGand a logic Λ,we sayGis alabelled sequent calculus forΛ if for allφ,G ??φif and only ifφ ∈Λ.

2.3 Labelled sequent calculus for EL

Definition 1.Labelled sequent calculusGELfor EL consists of the following initial sequents and rules1It is mentioned without proof in[9]that this is a labelled sequent calculus for EL.This calculus is a multi agent version of the labelled sequent calculus for S5 proposed in[14].:

(1)Initial sequents:

(2)Propositional rules:

(3)Modal rules:

whereydoes not occur in the conclusion of(?Ka).

(4)Relational rules:

Proposition 1.For any LELformula φ,GEL?x：φ,Γ??,x：φ.

Proof.It can be proved by induction onφ.□

By proofs similar to those in[14],we have Theorems 2 and 3.

Theorem 2.Structural rules(w ?),(?w),(c ?),(?c),(cR ?)and(?cR)are height preserving admissible in GEL.The cut rule(Cut)is admissible in GEL.

Theorem 3.GELallows terminating proof search.

Example 1.A derivation for axiom(5)inGELis as follows:

3 Labelled Sequent Calculus for PAL

In this section,we introduce a labelled sequent calculus for PAL.The Hilbert style axiomatization for PAL is the extension of that for EL with reduction axioms.Can we obtain a labelled sequent calculus for PAL by adding some rules adapted from reduction axioms to the labelled sequent calculusGELfor EL? The answer is yes and this is what we do.

Take reduction axiom (R1)[φ]p ?(φ →p) as an example.The equivalence symbol in the axiom means that[φ]pandφ →pare equivalent in PAL.Therefore,the most direct sequent rules for(R1)are

The rule on the left is sound because of [φ]p →(φ →p) and the rule on the right is sound because of (φ →p)→[φ]p.These rules can be written in a more neat way if we seeφ →p,Γ??as the conclusion of an application of (→?) and Γ??,φ →pas the conclusion of an application of(?→).Applying the reverse of(→?)and(?→)to their premises,we have the rules for(R1)that will be added toGEL:

In a similar way,we can have sequent rules for other reduction axioms.Therefore,we have:

Definition 2.Labelled sequent calculusGPALfor PAL isGELplus the following sequent rules:

We call these sequent rules thereduction rules.

There are six pairs of reduction rules inGPAL,each pair dealing with a kind of announcement formulas.Each left rule introduces a formula on the left of?,and each right rule introduces one on the right of?.Another desirable property for sequent rules is that the complexity of each premise should be less than that of the conclusion.If we define the complexity of a sequent to be the the sum of relational atoms and labelled formulas occurring in it,then the definition of formula complexity that counts the number of connectives will make (R5) and (R6) fail to satisfy the complexity increasing property.The following definition for formula complexity can solve this problem2This is Definition 7.21 in[7].:

Definition 3.Letφbe anLPALformula,Thecomplexity c(φ) ofφis defined as follows:

Then we have the following lemma3This is Lemma 7.22 in[7].:

Lemma 1.For all LPALformulas φ,ψ and χ:

Lemma 2.For any LPALformula φ,GPAL?x：φ,Γ??,x：φ.

Proof.We prove this by induction on the structure ofφwith a subinduction onψof the inductive case whereφequals [φ]ψ.All inductive case not involving an nouncement are the same as in the proof of Proposition 1.Whenφinvolves a public announcement operator,there are 6 subcases.We show two representative cases.

Whenφ=[?]Kaψ,the derivation is as follows:

Whenφ=[?][χ]ψ,the derivation is as follows:

Other cases can be proved analogously.□

Example 2.Now we show that (R5)[φ]Kaψ ?(φ →Ka[φ]ψ) is derivable inGPAL.A derivation for[φ]Kaψ →(φ →Ka[φ]ψ)inGPALis as follows:

and then

A derivation for(φ →Ka[φ]ψ)→[φ]KaψinGPALis as follows:

Example 3.[p ∧?Kap]?Kapis not derivable inGPAL.

whereD0is:

4 Admissibility of Some Structural Rules

In light of the reduction axioms,we can define a translation fromLPALformulas toLELformulas.4This is Definition 7.20 in[7].

Definition 4.The translationt：LPAL→LELis defined as follows:

Now we extend the translationtto relational atoms and labelledLPALformulas:for any relational atomx ～a y,lett(x ～a y)=x ～a y? for any labelledLPALformulax：φ,t(x：φ)=x：t(φ).Moreover,for any set Γ of relational atoms and labelled formulas:t(Γ)={t(σ)|σ ∈Γ}.

Lemma 3.For any LPALsequentΓ??,the following hold:

Proof.We prove these claims simultaneously by induction on the height of deriva tionhofGPAL?x：t(φ),t(Γ)?t(?)(orGPAL?t(Γ)?t(?),x：t(φ)).

Ifh=1,thenx：t(φ),t(Γ)?t(?)(ort(Γ)?t(?),x：t(φ))is an initial sequent.Ifx：t(φ) is principal,thent(φ)=pfor some proposition letterp.It follows thatφ=p.Therefore,x：φ,t(Γ)?t(?)(ort(Γ)?t(?),x：φ)is also an initial sequent.Ifx：t(φ)is not principal,it is immediate thatx：φ,t(Γ)?t(?)(ort(Γ)?t(?),x：φ)is an initial sequent.

Ifh>1,the induction hypothesis is formulated as:(1′)for alli

In what follows we only give the proof for claim(1′).The proof for the other is similar.

Assume thatGPAL?h x：t(φ),t(Γ)?t(?).Then there exists a derivationDforx：t(φ),t(Γ)?t(?)inGPAL.Let the last rule applied inDbeR.Ifx：t(φ)is not principal in the application ofR,the desired result can be obtained by applying the induction hypothesis to the premise(s)ofRand then applyingR.

Ifx：t(φ)is principal in the application ofR,we prove by an sub induction on the complexityc(φ)ofφ.Sincex：t(φ)is principal andh>1,φis not a proposition letter.We have ten sub cases.We divide them into two groups depending on whetherφstarts with an announcement operator or not.

Ifφdoes not start with an announcement operator,the desired result can be ob tained by applying the induction hypothesis to the premise(s)ofRand then applyingR.There are four sub cases:φis of the form?ψ,ψ1∧ψ2,ψ1→ψ2orKaψ.We illustrate this by the cases?ψandKaψ.

(1) Ifφ=?ψ,thenRis (? ?).Note thatt(φ)=t(?ψ)=?t(ψ).Let the derivationDend with

By the induction hypothesis,we haveGPAL?t(Γ)?t(?),x：ψ.Then by(??)we haveGPAL?x：?ψ,t(Γ)?t(?).

(2) Ifφ=Kaψ,thenRis(Ka ?).Note thatt(φ)=t(Kaψ)=Kat(ψ).Let the derivationDend with

First apply the main induction hypothesis tox：Kat(ψ)and we haveGPAL?y：t(ψ),x：Kaψ,x ～a y,t(Γ)?t(?).Then apply the sub induction hypothesis toy：t(ψ)and we haveGPAL?y：ψ,x：Kaψ,x ～a y,t(Γ)?t(?).Finally by(Ka ?)we haveGPAL?x：Kaψ,x ～a y,t(Γ)?t(?).

Ifφstarts with an announcement operator,then there are six sub cases:φis[?]p,[?]?ψ,[?](ψ1∧ψ2),[?](ψ1→ψ2),[?]Kaψor[?][ψ]χ.

Ifφis[?]p,[?]?ψ,[?](ψ1→ψ2)or[?]Kaψ,thent(φ)ist(?)→p,t(?)→t(?[?]ψ),t([?]ψ1)→t([?]ψ2),ort(?)→t(Ka[?]ψ),respectively.Sincex：t(φ)is principal,Rmust be(→?).We substitute the application of(→?)with an appli cation of (R1?),(R2?),(R4?) and (R5?),respectively.We illustrate the proof by the case whereφis[?]?ψand the case whereφis[?]Kaψ.

(1) Ifφis[?]?ψ,then the derivationDends with

Apply the induction hypothesis to the premises and we haveGPAL?t(Γ)?t(?),x：?andGPAL?x：?[?]ψ,t(Γ)?t(?).Then by(R2?)we haveGPAL?x：[?]?ψ,t(Γ)?t(?).

(2) Ifφis[?]Kaψ,then the derivationDends with

Apply the induction hypothesis to the premises and we haveGPAL?t(Γ)?t(?),x：?andGPAL?x：Ka[?]ψ,t(Γ)?t(?).Then by(R5?)we haveGPAL?x：[?]Kaψ,t(Γ)?t(?).

Ifφis[?](ψ1∧ψ2),thent(φ)ist([?]ψ1)∧t([?]ψ2).Sincex：t(φ)is principal,Rmust be (∧?).We substitute the application of (∧?) with an application of(R3?).Let the derivationDend with

Apply the sub induction hypothesis to the premise twice and we haveGPAL?x：[?]ψ1,x：[?]ψ2,t(Γ)?t(?).Then by (R3?) we haveGPAL?x：[?](ψ1∧ψ2),t(Γ)?t(?).

This completes the proof.□

The following theorem is a bridge betweenGPALandGEL,enabling us to prove properties ofGPALthroughGEL.

Theorem 4.For any LPALsequentΓ??,

Proof.(1)Assume thatGEL?t(Γ)?t(?).SinceGPALis an extension ofGEL,GPAL?t(Γ)?t(?).Sincet(Γ)?t(?) is finite,applying Lemma 3 a finite number of times,we haveGPAL?Γ??.

(2)The proof is by induction onh.

Ifh=1,then Γ??is an initial sequent inGPAL.By definition,it is also an initial sequent inGEL.

Ifh >1,we consider the last ruleRapplied in the derivation.IfRis not a reduction rule,the claim can be proved by first applying the induction hypothesis to the premise(s)and then applyingR.

IfRis a reduction rule for (R1),(R2),(R4) or (R5),we apply the induction hypothesis to the premise(s),and then apply(→?)or(?→).We illustrate this by a few cases.

IfRis(R1?),let the derivation end with:

By the induction hypothesis,we haveGEL?h?1t(?！?? t(?),x：t(φ) andGEL?h?1x：t(p),t(?！??t(?).We proceed as follows:

Sincet(x：[φ]p)=x：t(φ)→t(p),we have

IfRis(?R2),let the derivation end with:

By the induction hypothesis,we haveGEL?h?1x：t(φ),t(Γ)? t(?′),x：t(?[φ]ψ).We proceed as follows:

Sincet(x：[φ]?ψ)=x：t(φ)→t(?[φ]ψ),we have

IfRis(R5?),let the derivation end with:

By the induction hypothesis,we haveGEL?h?1t(?！?? t(?),x：t(φ) andGEL?h?1x：t(Ka[φ]ψ),t(?！??t(?).We proceed as follows:

Sincet(x：[φ]Kaψ)=x：t(φ)→t(Ka[φ]ψ),we have

IfRis a reduction rule for(R3),we apply the induction hypothesis to the premise(s),and then apply an inference rule for∧.We illustrate this by the case whereRis(R3?).

IfRis(R3?),let the derivation end with:

By induction hypothesis,we haveGEL?h?1x：t([φ]ψ1),x：t([φ]ψ2),t(?！??t(?).We proceed as follows:

Sincet(x：[φ](ψ1∧ψ2))=x：t([φ]ψ1)∧t([φ]ψ2),we have

IfRis a reduction rule for(R6),then we simply apply the induction hypothesis to the premise.

This completes the proof.□

Remark 2.Since PAL is more succinct than EL(see[8,11]),one might expect that a derivation of a sequent Γ??inGPALis strictly shorter(with respect to derivation height)than a derivation oft(Γ)?t(?)inGEL.This is not the case forGPALandGELas shown in Theorem 4.This is because a derivation for Γ??inGPALis obtained by executing the translation functiont(encoded by the reduction rules)in a derivation fort(Γ)?t(?)inGEL,which increases the length of the derivation.

Corollary 1.The following structural rules are admissible in GPAL:

Proof.It follows directly from Theorem 2 and Theorem 4.Take (Cut) as an ex ample.Assume thatGPAL?Γ??,x：φandx：φ,Γ′ ??′.By Theorem 4,GEL?t(Γ)?t(?),x：t(φ)andGEL?x：t(φ),t(Γ′)?t(?′).Then by admis sibility of cut inGEL(Theorem 2),GEL?t(Γ),t(?！??t(?),t(?′).By Theorem 4 again,GPAL?Γ,?！???,?′.□

Theorem 5(Soundness and Completeness).For any LPALformula φ,φ ∈PALiff GPAL??φ.

Proof.For the left to right direction,it suffices to show that each axiom in the Hilbert style axiomatization for PAL is derivable inGPALand that(MP)and(GKa)are admissible inGPAL.SinceGPALis an extension ofGEL,derivability of axioms in EL.Admissibility of(MP)follows from admissibility of cut inGPAL(Corollary 1).Admissibility of(GKa)inGPALfollows from admissibility of(GKa)inGELand Theorem 4.For the reduction axioms,since each reduction axiom has a correspond ing pair of sequent rules inGPAL,their derivations can be obtained by direct root first search.One derivation of(R5)is given in Example 2.

For the right to left direction,it suffices to show that each sequent rule inGPALis valid.This is routine.We omit the proof here.□

5 Decidability

In this section we show thatGPALallows terminating proof search.This result can be proved indirectly by Theorems 3 and 4.In this section we present a direct proof.

Readers familiar with the proof for terminating proof search inGELmay notice that the proof for terminating proof search inGPALis essentially the same as that inGELbecauseGPALis an extension ofGELwith some reduction rules.For this reason,we sketch the proof in this section and refer to[14]for a detailed description.

To show thatGPALallows terminating proof search,first we extend the notion ofsubformulasforLPALformulas,because active formulas are not subformulas of the principal formula in the usual sense in the reduction rules ofGPAL.

Definition 5.Letφbe anLPALformula.Formulaψis called asemi subformulaofφif one of the following conditions hold:

(1)ψis a subformula ofφ?

(2)φ=[?]?χandψ=?[?]χ,where?∈{?,Ka}?

(3)φ=[?](χ1?χ2)andψ=[?]χ1orψ=[?]χ2,where?∈{∧,→}?

(4)φ=[?][χ]ξandψ=[? ∧[?]χ]ξ.

The set of semi subformulas ofφis denoted bySSub(φ).We say thatψis aproper semi subformulaofφifψis a semi subformula ofφandψφ.

By Definition 3,the complexity of a proper semi subformula ofφis strictly smaller than that ofφ.

Definition 6.A derivation inGPALsatisfies theweak subformula propertyif all expressions in the derivation are either semi subformulas of formulasφin labelled formulasx：φin the endsequent of the derivation,or relational atoms of the formx ～a y.

It is easy to verify that each derivation inGPALsatisfies the weak subformula property.

The potential sources of non terminating proof search inGPALare as follows:

(1) (Transa),(Syma)(read root first)can be applied infinitely on the same principal formulas.

(2) (Refa)(read root first)can be applied infinitely to introduce new relational atoms.

(3) (Ka ?)(read root first)can be applied infinitely on the same principal formulas.

(4) By(Transa)and its iteration with(?Ka)that brings in new accessible worlds,we can build chains of accessible worlds on which(Ka ?)can be applied infinitely.

To show that the space of root first proof search is finite,it is useful to look atminimal derivations,that is,derivations where shortenings are not possible.

For(1),since no rules,read root first,can change a relational atom,any applica tion of(Transa)or(Syma)on the same principal formulas will make the derivation fail to be minimal.Therefore,this case should be excluded when searching for mini mal derivation.

For(2),we need the following lemma:

Lemma 4.All variables in relational atoms of the form x ～a x removed by(Refa)in a minimal derivation of a sequentΓ??in GPALare variables inΓor?.

Proof.It can be proved by tracing the relational atomx ～a xup in the derivation.For a detailed proof,see Lemma 6.2 of[14].□

For(3),we need to show the following lemma:

Lemma 5.Rule(Ka ?)permutes down with respect to(?Ka)in case the principal relational atom of(Ka ?)is not active in(?Ka).Moreover,rule(Ka ?)permutes down with respect to all other rules.

Then we can prove the following proposition:

Proposition 6.(Ka ?)and(?Ka)cannot be applied more than once on the same pair of principal formulas on any branch in any derivation in GPAL.

For (4) we need first some definitions.Positive partandnegative partof a sequent Γ??are defined as the positive part and negative part in the formula∧?！?respectively.An occurrence of a subformula in a formula is a positive part if it is in the scope of an even number of negation signs? it is a negative part if it is in the scope of an odd number of negation signs(to apply this definition,every occurrence of implicationφ →ψin subformula should be rewritten as?φ∨ψ).Then we are ready to prove the following proposition:

Proposition 7.In a minimal derivation of a sequent in GPAL,for each formula x：Kaφ in its positive part there are at most n(Ka)applications of(?Ka)iterated on a chain of accessible worlds x ～a x1,x1～a x2,...with principal formula xi：Kaφ,where n(Ka)denotes the number of Ka in the negative part ofΓ??.

6 Conclusion,Comparison and Future Research

In this paper we proposed a labelled sequent calculus for PAL.It is based on a proof system for EL,namely poly modal S5,extended with sequent rules to deal with announcement operators that directly mirror the PAL reduction rules.We also deter mined that the obtained system allows terminating proof search,and compared our system with the calculus for EL on matters such a height preservation of derivations.

Various proposals for sequent calculi for PAL have been made in[2,3,13,16].The labelled sequent calculi in[2,16]for PAL are based on a reformulation of the semantics for PAL.The notion of a model restriction to a (single) formula is gen eralized in these works to that of a model restriction to a list of formulas.Denote byαorβfinite lists(φ1,...,φn)of formulas,and by?the empty list.For any listα=(φ1,...,φn) of formulas,defineMαrecursively as follows:Mα：=M(ifα=?),and.

Then an equivalent semantics for PAL is defined as follows:

With this semantics,Balbiani([2])and Nomura et al.([16])5Nomura et al.([15])extended the method developed in[16]to action modal logic.developed different labelled sequent calculi for PAL,simultaneously repairing some perceived deficien cies in the previously published in Maffezioli and Negri([13]).The calculus in[2]admits cut and allows terminating proof search,and the calculus in[16]also admits cut.Note that these calculi,unlike ours,are for PAL based on the normal modal logic K,whereas we took PAL as an extension of S5(like[9,13]).We therefore also in clude the usual inference rules for S5(i.e.,(Refa),(Transa)and(Syma))into our calculus.Further,our calculus uses sequent rules based on PAL reduction axioms to deal with the announcement operators.

The method we proposed can be directly applied to action model logic([7])since this logic is also an extension of EL with some reduction axioms,of which PAL is a special case.

There are many extensions of other logics with public announcement that also in volve reduction axioms for such announcements,such as intuitionistic PAL([12]),bi lattice PAL([18]),?ukasiewicz PAL([6]),and variations/extensions of action model logic like bilattice logic of epistemic actions and knowledge([1]).We can try to de velop calculi for these logics with the steps similar to those for PAL.