公开宣告逻辑的一个加标矢列演算.pdf

Studies in Logic,Vol.16,No.3(2023):89107PII:16743202(2023)03008919A Labelled Sequent Calculus for PublicAnnouncement LogicHao WuHans van DitmarschJinsheng ChenAbstract.Public announcement logic(PAL)is an extension of epistemic logic(EL)withsome reduction axioms.In this paper,we propose a cutfree labelled sequent calculus for PAL,which isan extension of that forEL with sequentrules adapted fromthe reductionaxioms.Thiscalculus admits cut and allows terminating proof search.1IntroductionThe modern modal approach to the logic of knowledge and belief was extensively developed by Hintikka(10)to interpret epistemic notions utilizing possibleworld semantics.The standard multiagent epistemic logic EL is usually identifiedwiththepolymodalmodallogicS5foragroupofagents.Publicannouncementlogic(PAL),introduced by Plaza(17),is an extension of EL that studies logical dynamics of epistemic information after the action of public announcement.More generalactions are studied in action model logic(see e.g.4,5,7).PALisanextensionofELwithannouncementoperatorsoftheform.AsEL,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 inthe restrictions of Kripke models induced by the announcement.The Hilbertstyleaxiomatization of PAL is obtained by adding to that of EL the so called reductionaxioms for announcement operators,which can be used to eliminate announcementoperators in a PALformula.Generally speaking,it is difficult to prove whether proof search using a Hilbertstyle axiomatization is decidable.In view of these,many proof systems for PALare proposed in the literature,e.g.,tableau systems(3),labelled sequent calculi(2,16).Received 20220718Revision Received 20221104Hao WuInstitute of Logic and Cognition,Sun Yatsen UniversityDepartment of Philosophy,Sun Yatsen UHans van DitmarschCNRS,University of Toulouse,IRIThans.vanditmarschloria.frJinsheng ChenDepartment of Philosophy(Zhuhai),Sun Yatsen U90Studies in Logic,Vol.16,No.3(2023)In this paper,we propose another labelled sequent calculus for PAL.This calculus 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 axioms.This calculus admits structural rules(including cut)and allows terminatingproof search.Unlike 2,16,which are based on another semantics for PAL,ourcalculus is based on the original semantics and takes into account the conditions ofreflexivity,transitivity and symmetry in EL.The rest of the paper is structured as follows:Section 2 presents some basicnotions and concepts.Section 3 presents our labelled sequent calculus GPALforPAL.Section4showsthatGPALadmitssomestructuralrules,includingcut.Section5 shows that GPALallows terminating proof search.Section 6 compares GPALwithrelated works,concludes the paper and discusses future work.2Preliminaries2.1EL and PALLet Prop be a denumerable set of variables and Ag a finite set of agents.Language LELfor epistemic logic is defined inductively as follows:L :=p|KaMoreover,language LPALfor public announcement logic is defined inductively asfollows:L :=p|Ka|where p Prop and a Ag.We use as an abbreviation for()().LPALis an extension of LELwith announcement formulas.An epistemic frame F is a tuple(W,aaAg),where W is a set of states anda W W is a reflexive,transitive and symmetric relation for each a Ag.An epistemic model M is a tuple(W,aaAg,V)where(W,aaAg)isan epistemic frame and V is a function from Prop to P(W).Let M=(W,aaAg,V)be an epistemic model and w W.The notion of being true at w in M(notation:M,w )is defined inductively as follows:M,w piffw V(p)M,w iffM,w M,w iffM,w and M,w M,w iffM,w or M,w M,w Kaifffor all v W,w av implies M,v M,w iffM,w implies M,w where M=(W,aaAg,V)is the model restricted to with W=w W|M,w ,a=a(W W)and V=V(p)W.Hao Wu,Hans van Ditmarsch,Jinsheng Chen/A Labelled Sequent Calculus for Public Announcement Logic91A formula is globally true in an epistemic model(notation:M )ifM,w for all w W.A formula is valid in an epistemic frame F if F,V for all valuations V.Epistemic logic EL is the set of LELformulas that are valid on the class of allepistemic frames.Public announcement logic PAL is the set of LPALformulas thatare valid on the class of all epistemic frames.EL is axiomatized by(Tau),(K),(4),(T),(5),(MP)and(GKa).PAL is axiomatized by the axiomatization for EL plus reduction axioms(R1)(R6):(Tau)Classical propositional tautologies.(K)Ka()(Ka Ka)(4)Ka KaKa(T)Ka (5)Ka KaKa(MP)From and infer.(GKa)From infer Ka.(R1)p (p)(R2)()(R3)()()(R4)()()(R5)Ka (Ka)(R6)Remark 1.The standard language for PAL does not contain.To simplify ourwriting,we add to our language.Because of its existence,(R4)is added to theaxiomatization.2.2Labelled sequent calculusA labelled sequent calculus for a logic with Kripke semantics is based on theinternalization of Kripke semantics.Let F=(W,aaAg)be an epistemic frame.A relational atom is of theform x ay,where x,y W and a Ag.A labelled formula is of the form x:,where x W and is an LELformula.We use,with or without subscript todenote relational atoms or labelled formulas.A multiset is a set with multiplicity,or put the other way round,a sequencemodulo the ordering.A labelled sequent is of the form where,are finitemultisets of relational atoms and labelled formulas.A sequent rule is of the form(R)1 1.m m where m 0.1 1,.,m mare called premises of this rule and is called the conclusion.If m=0,we simply write and call it an initialsequent.The formula with the connective in a rule is the principal formula of thatrule,and its components in the premisses are the active formulas.A labelled sequentcalculus is a set of sequent rules.A derivation in a labelled sequent calculus G isdefined as usual.The derivation height h of a sequent is defined as the length of92Studies in Logic,Vol.16,No.3(2023)longest branch in the derivation of the sequent.We use G to denote that is derivable in G and G h to denote that is derivable in Gwith a derivation of height which is at most h.A sequent rule(R)is admissible in G if G i ifor 1 i m impliesG .It is heightpreserving admissible if G hi ifor 1 i mimplies G h .Let M=(W,aaAg,V)be an epistemic model.The interpretation Mofrelational atoms and labelled formulas are defined as follows:M(x ay)=x ay;M(x:)=M,x .A labelled sequent 1,.,m 1,.,nis valid ifMx1xkM(1)M(m)M(1)M(n)is true,where M=(W,aaAg,V)is an epistemic model,and x1,.,xkarevariables occurring in 1,.,m 1,.,nranging over W.A sequent rule R is valid if the validity of all the premises implies the validityof the conclusion.GivenalabelledsequentcalculusGandalogic,wesayGisalabelledsequentcalculus for if for all,G if and only if .2.3Labelled sequent calculus for ELDefinition1.LabelledsequentcalculusGELforELconsistsofthefollowinginitialsequents and rules1:(1)Initial sequents:x:p,x:px ay,x ay(2)Propositional rules:(),x:x:,()x:,x:()x:1,x:2,x:1 2,(),x:1 ,x:2 ,x:1 2(),x:x:,x:,()x:,x:,x:1It is mentioned without proof in 9 that this is a labelled sequent calculus for EL.This calculus isa multiagent version of the labelled sequent calculus for S5 proposed in 14.Hao Wu,Hans van Ditmarsch,Jinsheng Chen/A Labelled Sequent Calculus for Public Announcement Logic93(3)Modal rules:(Ka)y:,x:Ka,x ay,x:Ka,x ay,(Ka)x ay,y:,x:Kawhere y does not occur in the conclusion of(Ka).(4)Relational rules:(Refa)x ax,(Transa)x az,x ay,y az,x ay,y az,(Syma)y ax,x ay,x ay,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 heightpreserving admissible in GEL.The cut rule(Cut)is admissible in GEL.(w)x:,(w),x:(c)x:,x:,x:,(c),x:,x:,x:(cR)x ay,x ay,x ay,(cR),x ay,x ay ,x ay(Cut),x:x:,Theorem 3.GELallows terminating proof search.Example 1.A derivation for axiom(5)in GELis as follows:z:,y:Ka,y az,x az,y ax,x ay z:(Ka)y:Ka,y az,x az,y ax,x ay z:(Trana)y:Ka,x az,y ax,x ay z:(Syma)y:Ka,x az,x ay z:()x az,x ay y:Ka,z:(Ka)x ay y:Ka,x:Ka(Ka)x:KaKa,x:Ka()x:Ka x:KaKa()x:Ka KaKa94Studies in Logic,Vol.16,No.3(2023)3Labelled Sequent Calculus for PALIn this section,we introduce a labelled sequent calculus for PAL.The Hilbertstyle 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 adaptedfrom reduction axioms to the labelled sequent calculus GELfor EL?The answer isyes and this is what we do.Take reduction axiom(R1)p (p)as an example.The equivalencesymbol in the axiom means that p and p are equivalent in PAL.Therefore,the most direct sequent rules for(R1)arex:p,x:p,and ,x:p ,x:pThe rule on the left is sound because of p (p)and the rule on the rightis sound because of(p)p.These rules can be written in a more neatway if we see p,as the conclusion of an application of()and ,p as the conclusion of an application of().Applying the reverseof()and()to their premises,we have the rules for(R1)that will be addedto GEL:,x:x:p,x:p,andx:,p ,x:pIn a similar way,we can have sequent rules for other reduction axioms.Therefore,we have:Definition 2.Labelled sequent calculus GPALfor PAL is GELplus the followingsequent rules:(R1),x:x:p,x:p,(R1)x:,x:p ,x:p(R2),x:x:,x:,(R2)x:,x:,x:(R3)x:1,x:2,x:(1 2),(R3),x:1 ,x:2 ,x:(1 2)Hao Wu,Hans van Ditmarsch,Jinsheng Chen/A Labelled Sequent Calculus for Public Announcement Logic95(R4),x:1x:2,x:(1 2),(R4)x:1,x:2 ,(1 2)(R5),x:x:Ka,x:Ka,(R5)x:,x:Ka ,x:Ka(R6)x:,x:,(R6),x:,x:We call these sequent rules the reduction rules.There are six pairs of reduction rules in GPAL,each pair dealing with a kindof 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 forsequent rules is that the complexity of each premise should be less than that of theconclusion.If we define the complexity of a sequent to be the the sum of relationalatoms and labelled formulas occurring in it,then the definition of formula complexitythat counts the number of connectives will make(R5)and(R6)fail to satisfy thecomplexity increasing property.The following definition for formula complexity cansolve this problem2:Definition 3.Let be an LPALformula,The complexity c()of is defined asfollows:c(p)=1c()=1+maxc(),c()c()=1+c()c(Ka)=1+c()c()=1+maxc(),c()c()=(4+c()c().Then we have the following lemma3:Lemma 1.For all LPALformulas,and:(1)c(p)c(p)(2)c()c()(3)c()c()(4)c(Ka)c(Ka)(5)c()c().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 an2This is Definition 7.21 in 7.3This is Lemma 7.22 in 7.96Studies in Logic,Vol.16,No.3(2023)nouncement are the same as in the proof of Proposition 1.When involves a publicannouncement operator,there are 6 subcases.We show two representative cases.When =Ka,the derivation is as follows:x:,x:Ka,x:x:Ka,x:,x:Ka(R5)x:,x:Ka,x:Ka(R5)x:Ka,x:KaWhen =,the derivation is as follows:x:,x:(R6)x:,x:(R6)x:,x:Other cases can be proved analogously.Example 2.Now we show that(R5)Ka (Ka)is derivable inGPAL.A derivation for Ka (Ka)in GPALis as follows:y:,x:Ka,x ay,x:y:(Ka)x:Ka,x ay,x:y:and thenx ay,x:y:,x:x:Ka,x ay,x:y:(R5)x ay,x:Ka,x:y:(Ka)x:Ka,x:x:Ka()x:Ka x:Ka()x:Ka (Ka)A derivation for(Ka)Ka in GPALis as follows:x:x:Ka,x:x:Ka,x:x:Ka()x:,x:Ka x:Ka(R5)x:Ka x:Ka()x:(Ka)Ka)Example 3.p KapKap is not derivable in GPAL.D0 x ay,x:Kap Kapp,x:p y:p(Ka)x:Kap Kapp,x:p x:Kapx:p x:p Kap,x:Kapx:p KapKap,x:p x:Kap()x:p KapKap,x:p,x:Kap(,)x:p Kap x:p KapKap x:p KapKapHao Wu,Hans van Ditmarsch,Jinsheng Chen/A Labelled Sequent Calculus for Public Announcement Logic97where D0is:x ay,x:p y:p,y:py:Kap,x ay,x:p y:px ay,x:p y:p,y:Kapx ay,x:p y:p,y:p Kapy:p,x ay,x:p y:py:p Kapp,x ay,x:p y:px ay,x:Kap Kapp,x:p y:p4Admissibility of Some Structural RulesInlightofthereductionaxioms,wecandefineatranslationfromLPALformulasto LELformulas.4Definition 4.The translation t:LPAL LELis defined as follows:t(p)=pt()=t()t()=t()t()t()=t()t()t(Ka)=Kat()t(p)=t(p)t()=t()t()=t()t()=t()t(Ka)=t(Ka)t()=t()NowweextendthetranslationttorelationalatomsandlabelledLPALformulas:for any relational atom x ay,let t(x ay)=x ay for any labelled LPALformula x:,t(x:)=x:t().Moreover,for any set of relational atoms andlabelled formulas:t()=t()|.Lemma 3.For any LPALsequent ,the following hold:(1)if GPAL x:t(),t()t(),then GPAL x:,t()t()(2)if GPAL t()t(),x:t(),then GPAL t()t(),x:.Proof.We prove these claims simultaneously by induction on the height of derivation h of GPAL x:t(),t()t()(or GPAL t()t(),x:t().If h=1,then x:t(),t()t()(or t()t(),x:t()is an initialsequent.If x:t()is principal,then t()=p for some proposition letter p.Itfollows that =p.Therefore,x:,t()t()(or t()t(),x:)is alsoan initial sequent.If x:t()is not principal,it is immediate that x:,t()t()(or t()t(),x:)is an initial sequent.If h 1,the induction hypothesis is formulated as:(1)for all i h,if GPALix:t(),t()t(),4This is Definition 7.20 in 7.98Studies in Logic,Vol.16,No.3(2023)then GPALix:,t()t()(2)for all i 1,isnotapropositionletter.We have ten subcases.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 obtained by applying the induction hypothesis to the premise(s)of R and then applyingR.There are four subcases:is of the form,1 2,1 2or Ka.Weillustrate this by the cases and Ka.(1)If =,then R is().Note that t()=t()=t().Let thederivation D end witht()t(),x:t()()x:t(),t()t()By the induction hypothesis,we have GPAL t()t(),x:.Then by()we have GPAL x:,t()t().(2)If =Ka,then R is(Ka).Note that t()=t(Ka)=Kat().Let thederivation D end withy:t(),x:Kat(),x ay,t()t()(Ka)x:Kat(),x ay,t()t()First apply the main induction hypothesis to x:Kat()and we have GPALy:t(),x:Ka,x ay,t()t().Then apply the subinductionhypothesis to y:t()and we have GPAL y:,x:Ka,x ay,t()t().Finally by(Ka)we have GPAL x:Ka,x ay,t()t().Ifstartswithanannouncementoperator,thentherearesixsubcases:isp,(1 2),(1 2),Ka or.If is p,(1 2)or Ka,then t()is t()p,t()t(),t(1)t(2),or t()t(Ka),respectively.Since x:t()is principal,R must be().We substitute the application of()with an application of(R1),(R2),(R4)and(R5),respectively.We illustrate theproof by the case where is and the case where is Ka.Hao Wu,Hans van Ditmarsch,Jinsheng Chen/A Labelled Sequent Calculus for Public Announcement Logic99(1)If is,then the derivation D ends witht()t(),x:t()x:t(),t()t()()x:t()t(),t()t()Apply the induction hypothesis to the premises and we have GPAL t()t(),x:and GPAL x:,t()t().Then by(R2)we haveGPAL x:,t()t().(2)If is Ka,then the derivation D ends witht()t(),x:t()x:t(Ka),t()t()()x:t()t(Ka),t()t()Apply the induction hypothesis to the premises and we have GPAL t()t(),x:and GPAL x:Ka,t()t().Then by(R5)we haveGPAL x:Ka,t()t().If is(12),then t()is t(1)t(2).Since x:t()is principal,R must be().We substitute the appl