The Logic of Public Announcements, Common Knowledge and Private Suspicions

A. Baltag, L.S. Moss, S. Solecki

Software Engineering (SEN)

SEN-R9922 November 30, 1999

Report SEN-R9922ISSN 1386-369XCWI

P.O. Box 94079

1090 GB AmsterdamThe Netherlands

CWI is the National Research Institute for Mathematicsand Computer Science. CWI is part of the StichtingMathematisch Centrum (SMC), the Dutch foundationfor promotion of mathematics and computer scienceand their applications.

SMC is sponsored by the Netherlands Organization forScientific Research (NWO). CWI is a member ofERCIM, the European Research Consortium forInformatics and Mathematics.

Copyright © Stichting Mathematisch CentrumP.O. Box 94079, 1090 GB Amsterdam (NL)Kruislaan 413, 1098 SJ Amsterdam (NL)

Telephone +31 20 592 9333Telefax +31 20 592 4199

TheLogicofPublicAnnouncements,CommonKnowledge,andPrivateSuspicions

AlexandruBaltag

CWI

P.O.Box94079,1090GBAmsterdam,TheNetherlands

Email:abaltag@cwi.nl

LawrenceS.MossandSlawomirSolecki

MathematicsDepartment,IndianaUniversity

Bloomington,IN47401,USA

Emails:lsm@indiana.eduandssolecki@indiana.edu

ABSTRACT

Thispaperpresentsalogicalsysteminwhichvariousgroup-levelepistemicactionsareincorporatedintotheobjectlanguage.Thatis,weconsiderthestandardmodelingofknowledgeamongasetofagentsbymulti-modalKripkestructures.Onemightwanttoconsideractionsthattakeplace,suchasannouncementstogroupsprivately,announcementswithsuspiciousoutsiders,etc.Inoursystem,suchactionscorrespondtoadditionalmodalitiesintheobjectlanguage.Thatis,wedonotaddmachineryontopofmodels(asinFaginetal[4]),butwereifyaspectsofthemachineryinthelogicallanguage.

SpecialcasesofourlogichavebeenconsideredinPlaza[13],Gerbrandy[5,6],andGerbrandyandGroene-veld[7].ThelattergroupofpapersintroducealanguageinwhichonecanfaithfullyrepresentallofthereasoninginexamplessuchastheMuddyChildrenscenario.Inthatpaperwefindoperatorsforupdatingworldsviaannouncementstogroupsofagentswhoareisolatedfromallothers.Weadvancethisbyconsideringmanymoreactions,andbyusingamoregeneralsemantics.

Ourlogiccontainstheinfinitaryoperatorsusedinthestandardmodelingofcommonknowledge.Wepresentasoundandcompletelogicalsystemforthelogic,andwestudyitsexpressivepower.

1991MathematicsSubjectClassification:03B45,68T27,68T301991ACMComputingClassificationSystem:F.4.1,I.2.4,I.2.11

KeywordsandPhrases:epistemicactions,epistemiclogic,knowledgeupdate,publicannouncements

Note:WethankJelleGerbrandyandRohitParikhforusefulconversationsonthiswork.Anearlierversionofthispaperwaspresentedatthe1998ConferenceonTheoreticalAspectsofRationalityandKnowledge.

2

TableofContents

1

Introduction:ExampleScenariosandTheirRepresentations.....................1.1Models.........................................................1.2EpistemicActions.................................................1.3TheIssues.......................................................1.4FurtherContentsofThisPaper......................................2ALogicalLanguagewithEpistemicActions..................................

2.1Syntax.........................................................2.2Semantics.......................................................2.3MoreonActions..................................................3ALogicforL([α])......................................................4ALogicforL([α],2∗)...................................................5CompletenessforL([α],2∗)...............................................

5.1SomeSyntacticResults............................................5.2Completeness....................................................5.3TwoExtensions..................................................6ResultsonExpressivePower..............................................

6.1AnnouncementsaddExpressivePowertoModalLogicwith2∗.............6.2PrivateAnnouncementsAddExpressivePower..........................7ConclusionsandHistoricalRemarks........................................8Appendix:thelexicographicpathorder.....................................References.................................................................35810111111111315171919212424262728293132

References

1.Introduction:ExampleScenariosandTheirRepresentations

3

1.Introduction:ExampleScenariosandTheirRepresentations

Weintroducetheissuesinthispaperbypresentingafewepistemicscenarios.TheseareallbasedontheMuddyChildrenscenario,well-knownfromtheliteratureonknowledge.Theintentionistoexposetheproblemsthatwewishtoaddress.Theseproblemsarefirstofalltogetmodelswhicharefaithfultoourintuitions,andthentobuildandstudylogicalsystemswhichcapturesomeofwhatisgoingoninthescenarios.

Thecastofcharactersconsistsofthreechildren:A,B,andC.Sothatwecanusepronounsfortheminthesequel,weassumethatAismale,andBandCarefemale.Furthermore,AandBaredirty,andCisclean.Eachofthechildrencanseeallandonlytheothers.Itisknowntoall(say,asaresultofashoutfromoneoftheparents)thatatleastonechildisdirty.Furthermore,eachchildmusttrytofigureouthisorherstateonlybystating“IknowwhetherI’mdirtyornot”or“Idon’tknowwhetherI’mdirtyornot.”Theymusttellthetruth,andtheyareperfectreasonersinthesensethattheyknowallofthesemanticconsequencesoftheirknowledge.Theopeningsituationandtheserulesareallassumedtobecommonknowledge.

Scenario1.Afterreflection,AandBannouncetoeveryonethatatthatpointtheydonotknowwhethertheyaredirtyornot.(ThereasonwearehavingAandBmakethisannouncementratherthanallthreechildrenisthatitfitsinbetterwithourscenariostofollow.)Letαdenotethisannouncement.

AsintheclassicalMuddyChildren,thereareintuitionsaboutknowledgebeforeandafterα.Herearesomeofthoseintuitions.Beforeα,nobodyshouldknowthatheorsheisdirty.However,AshouldthinkthatitispossiblethatBknows.(ForifAwereclean,Bwouldinferthatshemustthedirtyone.)Afterα,AandBshouldeachknowthattheyaredirty,andhencetheyknowwhethertheyaredirtyornot.Ontheotherhand,Cshouldnotknowwhethersheisdirtyornot.

Scenario1.5.Thisscenariobeginsafterα.Atthispoint,AandBannouncetoallthreethattheydoknowwhetherornottheyaredirty.We’llcallthiseventα′.Ourintuitionisthatafterα′,Cshouldknowthatsheisnotdirty.Moreover,AandBshouldknowthatCknowsthis.Actually,thedirty-or-notstatesofallthechildrenshouldbecommonknowledgetoallthree.

Scenario2.Asanalternativetothefirstscenario,let’sassumethatCfallsasleepforaminute.Duringthistime,AandBgottogetherandtoldeachotherthattheydidn’tknowwhethertheyweredirtyornot.Letβdenotethisevent.Afterβ,Cwakesup.PartofwhatwemeanbyβisthatCdoesnotevenconsideritpossiblethatβoccurred,andthatit’scommonknowledgetoAandBthatthisisthecase.Thenourintuitionsarethatafterβ,Cshould“know”(actually:believe)thatAdoesnotknowwhetherheisdirty(andsimilarlyforB);andthisfactaboutCiscommonknowledgeforallthreechildren.Ofcourse,itshouldalsobecommonknowledgetoAandBthattheyaredirty.Scenario2.5.FollowingScenario2,weagainhaveα′:AandBannouncethattheydoknowwhethertheyaredirtyornot.Ourintuitionsarenotentirelyclearatthispoint.SurelyCshouldsuspectsomekindofcheatingormiscalculationonthepartoftheothers.However,wewillnothavemuchtosayabouttheworkingsofthiskindofreal-worldsensibility.Ourgoalwillbemoreinthedirectionofmodelingdifferentalternatives.

Scenario3.NowwevaryScenario2.CmerelyfeignedsleepandthoughtsheheardbothAandBwhispering.Ccannotbesureofthis,however,andalsoentertainsthepossibilitythatnothingwascommunicated.(Inreality,AandBdidcommunicate.)AandBfortheirpart,stillbelievethatCwassleeping.Wecallthiseventγ.

4

OnemightatfirstglancethinkthatAandB’s“knowledge”ofC’sepistemicstateisunchangedbyγ.Afterall,thecommunicationwasnotaboutC.However,weworkwithasemanticnotionofknowledge,andafterγ,AandBknowthattheyaredirty,hencethenknowthatCknowsthattheyaredirty.AandBdidnotknowthisattheoutset.

Soweneedtorevisetheinitialintuition.WhatiscorrectisthatifCknowssomefactϕbeforeγ,thenafterγ,AandBknow(orrather,believe)thatCknowsϕ.Thisisbecauseafterγ,AandBnotonlyknowtheclean-or-dirtystateofeveryone,they(therefore)alsoknowexactlywhichpossibilitieseveryoneisawareof,whichtheydiscardasimpossible,etc.SoeachofthemcanreconstructC’sentireepistemicstate.Theybelievethattheirreconstructioniscurrent,butofcourse,whattheyreconstructisC’soriginalone,beforeγ.

Conversely,ifafterγ,AandB“know”thatCknowsϕ,thenbeforeγ,Creallydidknowϕ.Thatis,thereconstructionisaccurate.Forexample,afterγ,AbelievesthatCshouldnotconsideritpossiblethatAknowsthatheisdirty.However,CthinksitispossiblethatAknowsheisdirty.Thereisastrongerstatementthatistrue:Cknowsϕbeforeγiffafterγ,itiscommonknowledgetoAandBthateachofthemknowsthatCknowsϕ.Intuitively,thisholdbecauseeachofAandBknowsthatbothofthemareabletocarryoutthereconstructionofC’sstate.

Ourfinalintuitionisthatafterγ,CshouldknowthatifAweretosubsequentlyannouncethatheknowsthatheisdirty,thenCwouldknowthatBknowsthatsheisdirty.

Scenario3.5.Again,continueScenario3byα′.Atthispoint,Cshouldknowthathersuspicionswereconfirmed,andhencethatsheisnotdirty.Fortheirpart,AandBshouldthinkthatCisconfusedbyα′:theyshouldthinkthatCisasshewasfollowingScenario2.5.

Scenario4.AandBareononesideofthetableandCisontheother,dozing.CwakesupatwhatlookstoherlikethemiddleofajointconfessionbyAandB.Thetwosidesstareeachotherdown.Infact,AandBhavealreadycommunicated.Wecallthisactionδ.SoCsuspectsthatδiswhathappened,butcan’ttellifitwasδornothing.Fortheirpart,AandBseethatCsuspectsbutdoesnotknowthatδhappened.

Thebasicintuitionisthatafterδ,itshouldbecommonknowledgetoallthreethatCsuspectsthatthecommunicationhappened.EvenifCthinksthatAandBdidnotcommunicate,Cshouldnotthinkthatsheissureofthis.

Onerelatedintuitionisthatafterδ,itshouldbecommonknowledgethatCsuspectsthatAknowsthatheisdirty.Asithappens,thisintuitioniswrong.Hereisadetailedanalysis:Cthinksitpossiblethateveryoneisdirtyattheoutset,andifthiswerethecasethentheannouncementofB’signorancewouldnothelpAtolearnthatheisdirty;fromA’spointofview,hestillcouldbecleanandBwouldnotknowthatsheisdirty.C’sviewonthisdoesnotchangeasaresultofδ,soafterwards,CstillthinksthatitcouldbethecasethatAsays,“It’spossiblethatBandCarethedirtyoneandIamclean,HenceCwouldseemycleanfaceandnotsuspectthatIknowthatIamdirty.”SoitcertainlyshouldnotbecommonknowledgethatCsuspectsthatAknowsheisdirty.

NoticealsothatCwouldsayafterδ:“Ithinkitispossiblethatnoannouncementoccurred,andyetAthinksitpossiblethatBistheonlydirtyone.Inthatcase,whatAwouldthinkthatIsuspectthatAtoldBthatheknowsthatheisnotdirty.Ofcourse,thisisnotwhatIactuallysuspect.”ThepointisthatC’sreasoningaboutAandB’sreasoningaboutherinvolvessuspicionofadifferentannouncementthanweatfirstconsidered.

Scenario4.5.Onceagain,wecontinuewithα′.OurintuitionisthatthisistantamounttoanadmissionofprivatecommunicationbyAandB.Ifwedisregardthisandonlylookathigherorderknowledgeconcerningwhoisandisnotdirty,weexpectthattheepistemicstateafterα′isthesameforallthreechildrenasitisattheendofScenario1.5.

1.Introduction:ExampleScenariosandTheirRepresentations

5

1.1Models

Nowthatwehavedetailedafewscenariosandourintuitionsaboutthem,itistimetoconstructsomeKripkemodelsasrepresentationsforthem.

TheModelsUandV.Webeginwitharepresentationofthesituationbeforeα.WetaketheKripkemodelUwhoseworldsareu1,...,u7andwhosestructureisgiveninthetableontheleftbelow:

World

A

••••

C

u1,u5u2,u6u3,u7u4

u1,u5u2,u6u3,u7

B→

u1

u2,u3u2,u3u4,u5u4,u5u6,u7u6,u7

WorldA

•••

C

v1,v5v3,v7v1,v5v6v3,v7

B→

v1v3v5v6,v7v6,v7

Forexample,inworldu3,Aisclean,butBandCaredirty.Also,theworldswhichAthinksarepossibleareu3andu7.Thatis,AseesthatBandCaredirty,soAinfers√thattheworldiseitheru3oru7.Therestofthestructureisexplainedsimilarly,exceptforthemarknexttou6.Thisspecifiesu6astheactualworldinthemodel,theonewhichcorrespondstoourdescriptionofthemodelbeforeα.NotethatUincorporatessomeoftheconventionsstatedinScenario1.Forexample,ineachworld,eachchildhasacompleteandcorrectassessmentofwhichworldsarepossibleforallthreereasoners.

Eachofourintuitionsaboutknowledgebeforeαturnsintoastatementinthemodallogicofknowledge.ThislogichasatomicsentencesDA,DB,andDCstandingfor“Aisdirty”,etc.;ithasknowledgeoperators2A,2B,and2Calongwiththeusualbooleanconnectives.WearegoingtousethestandardKripkesemanticsformulti-modallogicthroughoutthispaper.Sogivenamodel-worldpair,say󰀤A,a󰀥,andsomeagent,sayD,we’llwrite

󰀤K,k󰀥|=2Dϕiff

D

linK,wehave󰀤K,l󰀥|=ϕ.wheneverk→

Thebooleanconnectiveswillbeinterpretedclassically.Wecanthencheckthefollowing:

󰀤U,u6󰀥|=¬2ADA∧¬2A¬DA∧¬2BDB∧¬2B¬DB∧¬2CDC∧¬2C¬DC

󰀤U,u6󰀥|=3A2BDB

ThemodelafterαistheKripkemodelV,shownontherightabove.ThewaywegotVfromUwastodiscardtheworldsu2andu4ofU,sinceinUateachofthoseworlds,eitherAorBwouldknowiftheyweredirty.Wealsochangedtheu’stov’stoavoidconfusion,andtostressthefactthatwegetanewmodel.Turningbacktoourintuitions,wecanseethatthefollowingholds:

󰀤V,v6󰀥|=2ADA∧2BDB∧¬(2CDC∨2¬DC)

TheModelW.Scenario1.5elaboratesScenario1bytheeventα′.SowediscardtheworldswherethisisfalseinV,andweobtainaone-worldmodelW:

World

A

•

C

w6

B→

w6

(Wehaverenamedv6tow6.)Thismodelreflectsourintuitionthatatthispoint,Cshouldknowthatsheisnotdirty.

6

TheModelX.ThiscorrespondstoScenario2.WestartwithUandseetheeffectoftheprivateannouncementβ.TheresultingmodelXis:

World

A

C

x1,x5x3,x7x1,x5x6

x3,x7

B→

•••

u1

u2,u3u4,u5u6,u7u6,u7

Noticethattheworldsu1,...,u7arealsoworldsinX.WedidnotputanyinformationinthechartaboveforthoseworldssinceitshouldbeexactlythesameasinUabove.Thereasonforhavingthese“oldworlds”inXisthatsinceCwasasleep,theworldsthatCconsiderspossibleafterβshouldbejusttheonesthatwerepossiblebeforeβ.Wecancheckthat

󰀤X,x6󰀥|=¬2C(2ADA∨2A¬DA).

Letϕbethesentenceabove.Thenalso,󰀤X,x6󰀥|=2∗{A,B,C}ϕ.Thisisourformalstatementthatitiscommonknowledgeinthegroupofthreechildrenthatϕholds.ThesemanticsofthisisthatforallsequencesD1,...,Dm∈{A,B,C}∗,󰀤X,x6󰀥|=2D1···2Dmϕ.NotethatwehavenowayofsayinginthemodallanguagethatCsuspectsthatanannouncementhappened;thebestwecandois(roughly)tosaythatCthinksthatsomesentenceψispossibleinthesensethatψholdsinsomepossibleworld.Ofcourse,wehavenowaytosaythatAandBknowthatCwasasleep,either.

C

x6.Inotherwords,therealworldwouldnotbeNoteaswellthatinX,wedonothavex6→

possibleforC.Thisissomeindicationthatsomethingstrangeisgoingoninthismodel.Further,weconsiderthemodelofwhathappensafterAandB’sannouncement.Theninthismodel,noworldswouldbeaccessibleforCfromtheactualworld.Theseanomaliesshouldjustifyourinterestinthemorecomplicatedscenariosandmodelsinvolvingsuspicionsofannouncements.

TheModelobtainedbyannouncingα′inX.Thiswouldbetheone-worldmodelbelow:

World

A

•

C

x∗6

B

→

WehavenotonlydeletedtheworldswhereeitherAorBdoesnotknowthattheyaredirtyinX,butwealsodiscardedallworldsnotreachablefromthenewversionx∗6ofx6.TheanomalyhereisthatCthinksnoworldsarepossible.

TheModelY.WeconsiderγfromScenario3,inwhichCthoughtshemighthaveheardAandB,whileAandBthinkthatCisunawareofγ.WegetthemodelYdisplayedinFigure1below.Yhas24worlds,andsowewon’tjustifyallofthemindividually.WewillgiveamoreprincipledconstructionofYfromWandγ,oncewehavesettleonamathematicalmodelofγ.Fornow,theideasarethattheyworldsarethosewheretheannouncementhappened,andthey′worldsarethoseinwhichitdidnot.Notethatsomeoftheyworldsaremissing,sincethetruthfulannouncementbyAandBpresupposesthattheydon’tknowwhethertheyaredirtyinUatthecorrespondingworld.Thex’sandu’sarefromabove,andtheyinherittheaccessibilityrelationswhichwehaveseen.Nowourmainintuitionhereisthat󰀤U,u6󰀥|=2Cϕiff󰀤Y,y6󰀥|=2+{A,B}2Cϕ.(Thesentence+

2{A,B}χmeansthatAknowsϕ,AknowsBknowsχ,etc.Itdiffersfrom2∗{A,B}χinthatitdoesnot

C

u6,u7andnootherworlds.Andtheonlyworldsentailthatχistrue.)Toseethis,notethatu6→

1.Introduction:ExampleScenariosandTheirRepresentations

7

B→

WorldAC

•••••••

x1,x5x3,x7x1,x5x6

x3,x7u1,u5u2,u6u3,u7u4

u1,u5u2,u6u3,u7

′y1,y1

′′y3,y2,y3

′′y5,y4,y5

′′

y6,y7,y6,y7

′′

y6,y7,y6,y7

′y1,y1

′′y3,y2,y3

′′y3,y2,y3

′

y5,y4,y5

′′y5,y4,y5

′′

y6,y7,y6,y7

′′

y6,y7,y6,y7

Figure1:ThemodelY

ABC

reachablefromy6usingoneormore→or→transitionsfollowedbya→transitionareagainu6andu7.

Anotherintuitionisthatin󰀤Y,y6󰀥,CshouldthinkthatitispossiblethatAknowsthatheisdirty.

C

Thisisjustifiedsincey6→x6,and󰀤Y,x6󰀥∼=󰀤X,x6󰀥(thatis,thesubmodelsofXandYgeneratedbyx6areisomorphic),and󰀤X,x6󰀥|=2ADA.

Ourfinalintuitionisthatin󰀤Y,y6󰀥,CshouldknowthatifAweretosubsequentlyannouncethatheknowsthatheisdirty,thenCwouldknowthatBknowsthatsheisdirty.Tocheckthis,weneed

′

tomodifyYbydeletingtheworldswhereAdoesnotknowthatheisdirty.Theseincludey7,y6and′

y7.Intheupdatedmodel,theonlyworldaccessibleforCfrom(thenewversionof)y6isy6itself,andaty6inthenewstructure,Bcorrectlyknowssheisdirty.

TheModelobtainedbyannouncingα′inY.Aswhenα′isannouncedinX,weonlykeepthe

′′

worldsofYworldswherebothAorBdoknowtheyaredirty.Sowedropy7,y6,andy7.

World

A

•

•

C

x#6x#6

B

→

∗y6

Wealsoonlykeeptheworldsaccessiblefromy6(thischangeisharmless).Cknowssheisnotdirty.Technically,AandB“know”this,butthisisforthenonsensicalreasonthatthey“know”thatCknowseverything.

8

TheModelZ.CorrespondingtoScenario4,wegetthemodelZshownbelow.

w

A

••••

C

z1,z5z2z3,z7z4z1,z5z6z3,z7

B→

w

′z1,z1

′′

z2,z3,z2,z3

′′

z2,z3,z2,z3

′′

z4,z5,z4,z5

′′

z4,z5,z4,z5

′′

z6,z7,z6,z7

′′

z6,z7,z6,z7

A

•

•••

C

′′z1,z5′′z2,z6′′z3,z7′′z4,z6′′z1,z5′′z2,z6′′z3,z7

B

→

′z1,z1

′′

z2,z3,z2,z3

′′

z2,z3,z2,z3

′′

z4,z5,z4,z5

′′

z4,z5,z4,z5

′′

z6,z7,z6,z7

′′

z6,z7,z6,z7

RecallourlastpointinScenario4,thatweneedtoconsiderafewpossibleannouncementsforCto

suspect.Thisisreflectedinthefactthatthezworldsareofthreetypes.Inz2,Bannouncedthatsheknowswhethersheisdirty,andAannouncedthathedoesn’t.Similarremarksapplytoz4.Inallotherzworlds,bothannouncedthattheydonotknow.Theworldsaccessiblefromeachoftheseisbasedontherelevantannouncement.Forexample,inz2,neitherAnorBthinksanyotherworld

A

z6.Butinz6,Bcouldnotannouncethatsheknowssheisispossible.(Onemightthinkthatz2→

dirty.Soiftheworldwerez2andtherelevantannouncementmade,thenAwouldnotthinkz6ispossible.)Thez′worldsarethoseinwhichnoannouncementactuallyhappened.

OurkeyintuitionwasthatitiscommonknowledgethatCsuspectsthatδhappened.ThiswillnotcorrespondtoanythingintheformallanguageL([α],2∗)introducedlaterinthispaper.(However,itwillberepresentableinanauxiliarylanguageaboutactions;seeExample2.3.)Informally,the

′C

intuitionisvalidforZbecauseforeveryzi(orzi)thereissomezj(unprimed)suchthatzi→zj

′C

(orzi→zj).Inaddition,inthisparticularmodelthereisasentenceinourformallanguagewhichhappenstoholdonlyattheworldswhereanannouncementoccurred.Hereisone:

χ

≡

2ADA∨2A¬DA∨3∗{A,B}3C2ADA

So󰀤Z,z6󰀥|=2∗{A,B,C}3Cχ.

AC

z3,and3A2ADAfailsinz7→TheexplanationofthemistakenintuitioninScenario4isthatz6→

′′

z2,z3,z2,andz3..Overall,󰀤Z,z6󰀥|=¬2C2A3A2ADA.

ThepointthatC’ssuspicionvariescorrespondstothefactthat3C3A3C2A¬DAholdsat󰀤Z,z6󰀥.

′A′CC

Indeedz6→z6→z2→z2,and󰀤Z,z2󰀥|=2A¬DA.

AfewmoreinvolvedstatementsaretrueinZ.Forexample,2{A,B,C}∗(2ADA→3C2ADA).ItiscommonknowledgetoallthreethatifAknowsheisdirty,thenCthinksitpossiblethatAknowsthis.

TheModelobtainedbyannouncingα′inZ.ThismodelisWfromabove.(Actually,itisbisimilartoW;seeSection2.2.)ThiscorrespondstotheintuitionthatScenarios2.5and4.5leadtothesamemodel.

1.2EpistemicActions

WewillformalizealanguageinSection2alongwiththenotionsof(epistemic)actionstructureandactions.Beforewedothat,itmakessensetopresenttheideainformallybasedontheexampleswhichwehavealreadydealtwith.

αandα′:announcementstoeveryone.WefirstconsiderαofScenario1.Letψbegivenby

ψ

:=

¬(2ADA∨2A¬DA)∧¬(2BDB∨2B¬DB)

(1.1)

1.Introduction:ExampleScenariosandTheirRepresentations

9

SoψsaysthatneitherAnorBknowwhetherornottheyaredirty.Thisisthepreconditionoftheannouncement,butitisnotthestructure.Thestructureofthisannouncementisquitesimple(somuchsothatthereaderwillneedtoreadfurthertogetanideaforwhatwemeanbystructure).Itis

D

kforallD∈{A,B,C}.thefollowingKripkestructureK:wetakeonepoint,callitk,andwesetk→

Wecall󰀤K,k󰀥anactionstructure.AlongwithK,wealsohaveaprecondition;thiswillbeψfrom(1.1).Todealwithactionstructureswithmorethanonepoint,thepreconditionwillbeafunctionprefromworldstosentences.Inthiscase,thefunctionpreisjust{󰀤k,ψ󰀥}.Thetuple󰀤K,k,pre󰀥willbeanexampleofwhatwecallanaction.Thisparticularactionisourmodeloftheannouncementα.Henceforthweusethesymbolαtoreferambiguouslytothepretheoreticnotionoftheannouncementeventandtoourmathematicalmodelofit.

Anotherexampleofanannouncementtoeveryoneisα′.Herewejustchangeψfrom(1.1)tothesentenceψ′whichsaysthatbothAandBknowwhetherornottheyaredirty.Yetanotherexampleisthenullannouncement.Thismodelstheannouncementofatautologytruetoeveryone.We’llwritethisasτ.

β:asecureannouncementtoasetofagents.Next,supposewehaveanannouncementmadetosomepossiblypropersubsetB⊆AinthemannerofScenario2.Sothereissomedisputeastowhathappened:theagentsinBthinkthattherewasanannouncement,whilethoseoutofBaresurethatnothinghappened.WeformalizethiswithaKripkestructureoftwopoints,landt.

DDD

tforallD.ThepointisthatlhereisthetforD∈/B,andt→lforallD∈B,l→Wesetl→

actualannouncement,andtheagentsinBknowthatthisistheannouncement.TheagentsnotinBthinkthattisforsuretheonlypossibleaction,andtinthismodelwillbehavejustlikethenullannouncement.Thepreconditionfunctionwillbecalledpreinallofourexamples.Herepreisgivenbypre(l)=ψandpre(t)=true,whereψisfrom(1.1).Theactionoverallis󰀤L,l,pre󰀥,whereL={l,t}.Wecallthisactionβ.

γ:anannouncementwithasuspiciousoutsider.structurehasfourpoints,asfollows:

World

A→

ThisisbasedonScenario3.Theassociated

C→

ltltψtrueψtrue

Theideaisthatmisthe(private)announcementthatCsuspects,andnisotherannouncementthatCthinksispossible(wherenothingwascommunicatedbyAandB).Thenifmhappened,AandBweresurethatwhathappenedwasl;similarly,ifnhappened,AandBwouldthinkthattwaswhathappened.Wecallthisactionγ;technicallyitis󰀤{m,n,l,t},m,pre󰀥.Wegetadifferentaction,sayγ′ifweusethesamemodelasabovebutchangethedesignated(“real”)worldfrommton.δ:anannouncementwithcommonknowledgeofsuspicion.CorrespondingtoScenario4,wehavethefollowingmodel.InitψAdenotesthesentencesayingthatAknowswhetherheisdirtybutBdoesnot,ψBthesentencesayingthatBknowswhethersheisdirtybutAdoesnot,andψ∅thesentencestatingthatneitherknows.

World

A→

opqrs

C→

ψψAψBψ∅true

10

Wecallthisactionδ.Therearefivepossibleactionshere,dependingonwhetheritwasψ,ψA,ψB,ψ∅ornothingwhichwasannounced.Ineachcase,AandBaresureofwhathappened.Evenifnothingactuallyhappened(s),Cwouldsuspectoneoftheotherfourpossibilities.Inthose,Cstillconsidersitpossiblethatnothinghappened.

Stilltocome.Thereaderisperhapswonderingwhattheactualconnectionisbetweenthe(formal)actionsjustintroducedandtheconcretemodelsoftheprevioussection.Theconnectionisthatthereisawayoftakingamodelandanactionandproducinganothermodel.WhenappliedtothespecificmodelUandtheactionsofthissection,wegetthemodelsV,...,Z.WedelaythisconnectionuntilSection2.2below,sinceitishightimethatweintroduceourlanguageofepistemicactionsanditssemantics.Thepointisthatthereisaprincipledreasonbehindthemodels.

Thequestionalsoarisesastowhetherthereareanyprinciplesbehindtheparticularactionswhichweputdowninthissection.Asithappens,thereismorewhichcanbesaidonthismatter.WepostponethatdiscussionuntilSection2.3,afterwehaveformallydefinedthesyntaxandsemanticsofourlogicallanguages.

1.3TheIssues

Themainissueweaddressinthispaperistoformallyrepresentepistemicupdates,i.e.,changesintheinformationstatesofagentsinadistributedsystem.Wethinkofthesechangesasbeinginducedbyspecificinformation-updatingactions,whichcanbeofvarioustypes:(1)information-gatheringandprocessing(e.g.,realizingthepossibilityofotheragents’hiddenactions,andmoregenerally,learningofanykindofnewpossibilityviaexperiment,computation,orintrospection);(2)information-exchangeandcommunication(learningbysending/receivingmessages,publicannouncements,secretinterceptionofmessages,etc.);(3)information-hiding(lyingorotherformsofdeceivingactions,suchascommunicationoversecretchannels,sendingencryptedmessages,holdingsecretsuspicions);(4)information-lossandmisinformation(beingliedto,startingtohavegratuitoussuspicions,non-introspectivelearning,wrongcomputationsorfaultyobservations,paranoia);(5)andmoregenerallysequentialorsynchronouscombinationsofalloftheabove.

Specialcasesofourlogic,dealingonlywithpublicorsemi-publicannouncementstomutuallyisolatedgroups,havebeenconsideredinPlaza[13],Gerbrandy[5,6],andGerbrandyandGroeneveld[7].ThesedealwithactionssuchasαandβinourIntroduction.Ourexamplesγandδgobeyondwhatispossibleinthesettingofthesepapers.Butouroverallsettingismuchmoreliberalsetting,sinceitallowsforalltheabove-mentionedtypesofactions.Wefeelitwouldbeinterestingtostudyfurtherexampleswithaneyetowardsapplications,butweleavethistootherpapers.

Inourformalsystem,wecaptureonlytheepistemicaspectoftheserealactions,disregardingother(intentional)aspects.Inparticular,forsimplicityreasons,weonlydealwith“‘purelyepistemic”actions;i.e.,theonesthatdonotchangethefactsoftheworld,butaffectonlytheagents’beliefsabouttheworld.However,thisisnotanessentiallimitation,asourformalsettingcanbeeasilyadaptedtoexpressfact-changingactions(seetheendofSection2.3andalsoSection5.3).

Onthesemanticalside,themainoriginaltechnicalcontributionofourpaperliesinourdecisiontorepresentnotonlytheepistemicstates,butalsotheepistemicactions,byKripkestructures.Whileforstates,thesestructuresrepresentintheusualwaytheuncertaintyofeachagentconcerningthecurrentstateofthesystem,wesimilarlyuseaction-structurestorepresenttheuncertaintyofeachagentconcerningthecurrentactiontakingplace.Theintuitionisthatwearedealingwithpotentially”half-opaque/half-transparent”actions,aboutwhichtheagentsmaybeincompletelyinformed,orevencompletelymisinformed.Besidesthestructure,actionshavepreconditions,definingtheirdomainofapplicability:noteveryactionispossibleineverystate.Wemodeltheupdateofastatebyanactionasapartialupdateoperation,givenbyarestrictedproductofthetwostructures:theuncertaintiespresentinthegivenstateandthegivenactionaremultiplied,whilethe“impossible”combinationsofstatesandactionsareeliminated(bytestingtheactions’preconditionsonthestate).Theunderlyingintuitionisthattheagent’suncertaintiesconcerningthestateandtheonesconcerningtheactionare

2.ALogicalLanguagewithEpistemicActions

11

mutuallyindependent,exceptfortheconsistencyoftheactionwiththestate.

Onthesyntacticalside,weuseamixtureofdynamicandepistemiclogic,withdynamicmodalitiesassociatedtoeachaction-structure,andwithcommon-knowledgemodalitiesforvariousgroupsofagents(inadditiontotheusualindividual-knowledgeoperators).Wegiveacompleteanddecidableaxiomatizationforthislogic,andweprovevariousexpressivityresults.Fromaproof-theoreticalpointofview,themainoriginalityofoursystemisthepresenceofourActionRule,aninferencerulecapturingwhatmightbecalledanotionof“epistemic(co)recursion”.WeunderstandthisruleandourKnowledge-ActionAxiom(ageneralizationofRamsey’saxiomtohalf-opaqueactions)asexpressingfundamentalformalfeaturesoftheinteractionbetweenactionandknowledgeinmulti-agentsystems,featuresthatwethinkhavenotbeenformallyexpressedbefore.

1.4FurtherContentsofThisPaper

Section2givesourbasiclogicL([α])ofepistemicactionsandknowledge.Theideaistodefinethelogictogetherwiththeactionstructureswhichwehavejustlookedatinformally.SoinL([α])wefinallywillpresentthepromisedformalversionsoftheannouncementsofSection1.2.InSection3wepresentasoundandcompleteaxiomatizationofL([α]).WeaddthecommonknowledgeoperatorstogetL([α],2∗)inSection4.CompletenessforthislogicisprovedinSection5.TworesultsontheexpressivepowerarepresentedinSection6.AnAppendixcontainssometechnicalresultswhich,whileneededforourwork,seemtointerrupttheflowofthepaper.

2.ALogicalLanguagewithEpistemicActions2.1Syntax

WebeginwithasetAtSenofatomicsentences,andwedefinetwosetssimultaneously:thelanguageL([α]),andasetofactions(overL([α])).

L([α])isthesmallestcollectionwhichincludesAtSenandwhichisclosedunder¬,∧,2AforA∈A,and[α]ϕ,whereαisanactionoverL([α]),andϕ∈L([α]).

Anactionstructure(overL([α]))isapair󰀤K,pre󰀥,whereKisafiniteKripkeframeoverthesetAofagents,andpreisamappre:K→L.WewillusuallywriteKfortheactionstructure󰀤K,pre󰀥.Anaction(overL([α]))isatupleα=󰀤K,k,pre󰀥,where󰀤K,pre󰀥isanactionstructure

D

overL([α]),andk∈K.Eachactionαthusisafinitesetwithrelations→forD∈A,togetherwithapreconditionfunctionandaspecifiedactualworld.

TheactionsthemselvesconstituteaKripkeframeActionsinthenaturalway,bysetting

Whenα=󰀤K,k,pre󰀥,wesetpre(α)=pre(k).Thatis,pre(α)isthepreconditionassociatedtothedistinguishedworldoftheaction.Forthisreason,weoftenwritepre(α)insteadofpre(k).Examples2.1AllofthesentencesmentionedinSection1.1aresentencesofL([α]),exceptfortheonesthatuse2∗{A,B,C}.Thisconstructgivesusamoreexpressivelanguage,asweshallsee.Thestructuresα,τ,β,γ,γ′,δ,andδ′describedinformallyinSection1.2arebonafideactions.As

D

αexamplesoftheaccessibilityrelationontheclassofactions,wehavethefollowingfacts:α→

DBCCABCABAB

andτ→τforallD∈{A,B,C};β→β;β→β;β→τ;γ−→β;γ,γ′→γ,γ′;γ′−→τ;δ−→δ,′AB′′C′δ−→δ,andδ,δ→δ,δ.

Manyothertypesofexamplesarepossible.Wecanrepresentmisleadingepistemicactions,e.g.lying,ormoregenerallyactingsuchthatsomepeopledonotsuspectthatyouractionispossible.Wecanalsorepresentgratuitoussuspicion(“paranoia”):maybeno“real”actionhastakenplace,exceptthatsomepeoplestartsuspectingsomeaction(e.g.,someprivatecommunication)hastakenplace.2.2Semantics

Aswiththesyntax,wedefinetwothingssimultaneously:thesemanticrelation󰀤W,w󰀥|=ϕ,andapartialoperation(󰀤W,w󰀥,α)→󰀤W,w󰀥α.Beforethis,weneedanotherdefinition.GivenamodelWandanactionstructureK,wedefinethemodelWKasfollows:

D

󰀤L,l,pre′󰀥iff󰀤K,k,pre󰀥→

D

linK.K=L,pre=pre′,andk→

(2.1)

12

1.TheworldsofWKarethepairs(w,k)∈W×Ksuchthat󰀤W,w󰀥|=pre(k).2.Forsuchpairs,

A

(w′,k′)(w,k)→

AA

k′.w′andk→iffw→

(2.2)

3.WeinterprettheatomicsentencesbysettingvWK((w,k))=vW(w).Thatis,pistrueat(w,k)

inWKiffpistrueatwinW.Givenanactionα=󰀤K,k󰀥andamodel-worldpair󰀤W,w󰀥,wesaythat󰀤W,w󰀥αisdefinediff󰀤W,w󰀥|=pre(k),andinthatcaseweset󰀤W,w󰀥α=󰀤W,w󰀥󰀎K,k󰀏=󰀤WK,(w,k)󰀥.Onecannowcheckthatthefollowingholdsforthesedefinitions.

A

󰀤W,w󰀥α→󰀤W,x󰀥β

iff

AA

󰀤W,w󰀥αand󰀤W,x󰀥βaredefined,w→xinW,andα→β.

Thesemanticsisgivenbyextendingtheusualclausesformodallogicbyoneforactions:

󰀤W,w󰀥|=[α]ϕ

iff󰀤W,w󰀥αisdefinedimplies󰀤W,w󰀥α|=ϕ.

󰀤W,w󰀥αisdefinedand󰀤W,w󰀥α|=ϕ.

Asiscustomary,weabbreviate¬[α]¬ϕby󰀤α󰀥ϕ.Thenwehave

󰀤W,w󰀥|=󰀤α󰀥ϕ

iff

Wealsoabbreviatethebooleanconnectivesclassically,andwelettruedenotesometautologysuchas

p∨¬p.

ThelargerlanguageL([α],2∗)WealsoconsideralargerlanguageL([α],2∗).Thisisdefinedbyaddingoperators2∗BforallsubsetsB⊆A.(Whenwedothis,ofcoursewegetmoreactionsaswell.)Thesemanticsworksbytaking2∗Bϕtoabbreviatetheinfinitaryconjunction

󰀃

2A1···2Anϕ.

󰀎A1,...,An󰀏∈B∗

HereB∗isthesetofallsequencesfromB.Thisincludestheemptysequence,so2∗Bϕlogicallyimpliesϕ.

BisimulationGiventwomodels,sayKandL,overthesamesetofAofagents,abisimulationbetweenKandLisarelationR⊆K×LsuchthatifkRlandA∈A,then:1.Forallatomicp,󰀤K,k󰀥|=piff󰀤L,l󰀥|=p.

AA

l′suchthatk′Rl′.k′thereissomel→2.Forallk→

AA

3.Foralll→l′thereissomek→k′suchthatk′Rl′.

Giventwomodel-worldpairs󰀤K,k󰀥and󰀤L,l󰀥,wewrite󰀤K,k󰀥≡󰀤L,l󰀥iffthereissomebisimulationRsuchthatkRl.Itisastandardfactthatif󰀤K,k󰀥≡󰀤L,l󰀥,thenthetwopairsagreeonallsentencesofstandardmodallogic.Inoursetting,wealsocanspeakaboutactionsbeingbisimilar:wechangecondition(1)abovetorefertosaythatpre(k)=pre(l).Itiseasynowtochecktwothingssimultaneously:(1)bisimilarpairsagreeonallsentencesofL([α]);and(2)if󰀤K,k󰀥≡󰀤L,l󰀥andα≡β,then󰀤K,k󰀥α≡󰀤L,l󰀥β.Furthermore,theseresultsextendtoL([α],2∗).

Examples2.2WelookbackatSection1.1forsomeexamples.Weuse∼=todenotetherelationofisomorphismonmodel-worldpairs.Itisnothardtocheckthefollowing:󰀤U,u6󰀥α∼=󰀤V,v6󰀥,

δ∼γ∼β∼󰀤U,u6󰀥=󰀤X,x6󰀥,󰀤U,u6󰀥=󰀤Y,y6󰀥,and󰀤U,u6󰀥=󰀤Z,z6󰀥.Forexample,theisomorphismwhich

2.ALogicalLanguagewithEpistemicActions

13

′

showsthat󰀤U,u6󰀥δ∼=󰀤Z,z6󰀥is(ui,o)→zifori=2,4,(u2,q)→z2,(u4,p)→z4,and(ui,r)→ziforalli.

Letα′betheactionofannouncingtoallagentsthatbothAandBdoknowwhethertheyare

′′

dirty.Then󰀤V,v6󰀥α∼=󰀤X,x6󰀥.Moreover,󰀤Z,v6󰀥α≡󰀤X,x6󰀥.Notethatinthiscaseweonlyhavebisimilarity.However,weknowthatourlanguageswillnotdiscriminatebetweenbisimilarpairs,sowecanregardthemasthesame.ThismodelsourintuitionthattheepistemicstatesattheendofScenarios1.5and4.5shouldbethesame.

Finally,allofthesemanticfactsaboutthevariousmodelsinSection1.1nowturnintoprecisestate-ments.Forexample,󰀤U,u6󰀥|=[α]3A2BDB.Also,󰀤U,u6󰀥|=[α][α′]2∗A,B,C2CDC.Thisformalizesourintuitionthatifwestartwith󰀤U,u6󰀥,firstannouncethateachofAandBdonotknowtheirstate,thensecondannouncethattheyeachdoknowit,thenatthatpointitwillbecommonknowledgetoallthreethatCknowssheisdirty.

2.3MoreonActions

Inthissection,wehaveafewremarksonactions.ThepointhereistoclarifytherelationbetweenthescenariosofSection1andtheintuitionsconcerningthem,andthecorrespondingactionsofSection1.2.Firstandforemost,herearethetheconceptualpointsinvolvedinourformalization.Theideaisthatepistemicactionspresentalotofuncertainty.Indeed,whatmightbethoughtofasasingleaction(orevent)isnaturallyinterpretedbyagentsindifferentways.Thevariousagentsmightbeunclearonwhatexactlyhappened,andagaintheymightwellhavedifferentinterpretationsonwhatishappening.OurformalizationreflectsthisbymakingepistemicactionsintoKripkemodels.Soouruseofpossible-worldsmodelingofactionsisonaparwithotherusesofthesemodels,anditinheritsallofthefeaturesandbugsofthoseapproaches.

Next,wewanttospelloutinwordswhatourproposalamountsto.ThebasicproblemistodecidehowtorepresentwhathappenstoaKripkemodelWafteranannouncementα.(Ofcourse,wearemodelingαbyanactioninourformalsense.)OursolutionbeginsbyconsideringcopiesofW,oneforeachactiontokenkofαinwhichpre(α)holds.WecanthinkoftaggingtheworldsofWwiththeworldsofα,andthenwemustgiveanaccountoftheaccessibilityrelationbetweenthem.Theintuitionisthattheagents’relationstoalternativeworldsshouldbeindependentfromtheirrelationstootherpossibilitiesforα.SotheaccessibilityrelationsofKandWshouldbecombinedindependently.Thisisexpressedformallyin(2.2).

ˆhasasatomicsentencesallsentencesϕofL([α],2∗).IthasallbooleanTheauxiliarylanguageL

connectives,standardmodaloperators2AforA∈A,andalsogroupknowledgeoperators2∗BforB⊆A.

ˆonactionsusingthestandardclausesfortheconnectivesandmodaloperators,andWeinterpretL

byinterpretingtheatomicsentencesasfollows󰀤K,k󰀥|=piffpre(k)=p.

Examples2.3Theideahereisthattheauxiliarylanguageformalizestalkaboutwhatthedifferentagentsthinkishappeninginourannouncements.WereferbacktotheactionsofSection1.2.Forexample,α|=2∗{A,B,C}ψ.Intuitively,inα,itiscommonknowledgethatψwasannounced.Anotherexample:that

δ|=2∗{A,B,C}3C(ψ∨ψA∨ψB).

Thatis,inδ,itiscommonknowledgethatCthinksitispossiblethatsomenon-trivialannouncement

happened.Recallthatthiswasoneofourbasicintuitionsaboutδ,onewhichisnotingeneralstatableinourmainlanguageL([α],2∗).

ˆ.ThenχcharacterizesDefinitionLet󰀤K,k󰀥beamodel-worldpair,andletϕbeasentenceofL

󰀤K,k󰀥iffforall󰀤L,l󰀥,󰀤L,l󰀥|=χiff󰀤L,l󰀥≡󰀤K,k󰀥.

14

ˆProposition2.4Let󰀤K,k󰀥beamodel-worldpairwithKfinite.ThenthereisasentenceχofL

whichcharacterizes󰀤K,k󰀥.

ProofByreplacing󰀤K,k󰀥byitsquotientunderthelargestauto-bisimulation,wemayassumethatifl=m,then󰀤K,l󰀥≡󰀤K,m󰀥.Itiswell-knownthattherelationofelementaryequivalenceinmodallogicisabisimulationonmodelsinwhicheachworldhasfinitelymanyarrowscominginandout.ItfollowsfromthisandtheoverallfinitenessofKthatwecanfindsentencesϕlforl∈Kwiththepropertythatforalllandm,󰀤K,m󰀥|=ϕliffm=l.Letψbethefollowingsentence

󰀂󰀃󰀁󰀃󰀅

ψ≡3Aϕl′ϕl′∧ϕl→2A

AAl∈K,A∈Al→l′l→l′Goingbacktoouroriginal󰀤K,k󰀥,letχbeϕk∧2∗Aψ.Itiseasytocheckthateach󰀤K,l󰀥satisfiesψ;

∗

henceeachsatisfies2Aψ.Therefore󰀤K,k󰀥|=χ.Weclaimthatχcharacterizes󰀤K,k󰀥.Toseethis,supposethat󰀤J,j󰀥|=χ.ConsidertherelationR⊆K×Jgivenby

k′Rj′

iff󰀤J,j′󰀥|=ϕk′∧2∗Aψ.

ItissufficienttoseethatRisabisimulation.We’llverifyhalfofthis:supposethatk′Rj′and

AAj′→j′′.Byusingψ,weseethatthereissomek′′suchthatk′→k′′andj′′|=ϕk′′.Andalso,since

∗′′

|=2∗=2∗⊣Aψ→2A2Aψ,weseethat󰀤J,j󰀥|Aψ.Thiscompletestheproof.

Theconnectionofthisresultandourdiscussionofactionsisthatitisoftendifficulttogofromaninformaldescriptionofananepistemicactiontoaformalonealongourlines.(Forexample,ourformulationofδwasthelastofseveralversions.)Presumably,onewaytogetaformalactioninoursenseistothinkcarefullyaboutwhichpropertiestheactionshouldhave,expressthemintheauxiliarylanguage,andthenwriteacharacterizingsentencesuchasψintheproofofProposition2.4.Thenonecanconstructthefinitemodelbystandardmethods.Althoughthiswouldbeatediousprocess,itseemsworthwhiletoknowthatitisavailable.

Ourformalizationofactionsreflectssomechoiceswhichonemightwishtomodify.Oneofthesechoicesistotaketherangeofthefunctionpretobesomelanguage.Anotheroptionwouldbetohavetherangetobethepowersetofthatlanguage.ThiswouldmakeactionsintoKripkemodelsoverthewholesetofsentences.(Andsowhatwehavedoneislikeconsideringmodallogicwiththerestrictionthatatanyworldsatisfiesexactlyoneatomicsentence.)Takingthisotheroptionthusbringsactionsandmodelscloser.ThisideaispursuedinBaltag[1],acontinuationofthisworkwhichdevelopsa“calculusofepistemicactions.”Thisreplacesthe“semantic”actionsofthispaperwithactionexpressions.Theseexpressionshavenicerpropertiesthantheauxiliarylanguageofthispaper,butitwouldtakeustoofarafieldtodiscussthisfurther.

Onadifferentmatter,itmakessensetorestrictattentionfromthefullcollectionofactionsaswe

A

havedefinedittothesmallercollectionofS5actions,whereeachaccessibility→isanequivalencerelation.Thiscorrespondstothestandardmoveofrestrictingattentiontomodelswiththisproperty,andthereasonsfordoingthisaresimilar.Intuitively,anS5actionisoneinwhicheveryagentisintrospective(withrespecttotheirownsuspicionsaboutactions).Moreover,theintrospectionisaccurate,andthisfactiscommonknowledge.

Afinalmodificationwhichisquitenaturalistoallowactionswhichchangetheworld.Onewoulddothisbyaddingtoournotionofactionasententialupdateu.ThiswouldbeafunctiondefinedonAtSenandwrittenintermsofupdateequationssuchasu(p):=p∧q;u(q)=false,etc.Weareconfidentthatourlogicalsystemscanbemodifiedtoreflectthischange,andwediscussthisatcertainpointsbelow.Wedecidednottomakethischangemostlyinordertokeepthebasicnotionsassimpleaspossible.

Withrespecttobothofthechangesmentionedinthelasttwoparagraphs,itisnothardtomodifyourlogicalworktogetcompletenessresultsforthenewsystems.WediscussallofthisinSection5.3.

3.ALogicforL([α])

15

BasicAxioms

Allsententialvalidities([α]-normality)(2A-normality)∗(2∗C-normality)ActionAxioms

(AtomicPermanence)(PartialFunctionality)(Action-Knowledge)∗MixAxiom

∗CompositionAxiomModalRules(ModusPonens)([α]-necessitation)(2A-necessitation)∗(2∗C-necessitation)∗ActionRule

⊢[α](ϕ→ψ)→([α]ϕ→[α]ψ)

⊢2A(ϕ→ψ)→(2Aϕ→2Aψ)

∗∗

⊢2∗C(ϕ→ψ)→(2Cϕ→2Cψ)

⊢[α]p↔(pre(α)→p)⊢[α]¬χ↔(pre(α)→¬[󰀆α]χ)

A

β})⊢[α]2Aϕ↔(pre(α)→{2A[β]ϕ:α→

󰀆

{2A2∗Cϕ:A∈C}

⊢2∗Cϕ→ϕ∧

⊢[α][β]ϕ↔[α◦β]ϕFrom

FromFromFrom

⊢ϕand⊢ϕ→ψ,infer⊢ψ⊢ψ,infer⊢[α]ψ⊢ϕ,infer⊢2Aϕ⊢ϕ,infer⊢2∗Cϕ

Letψbeasentence,andletCbeasetofagents.Lettherebesentencesχβforallβsuchthat

α→∗Cβ(includingαitself),andsuchthat1.⊢χβ→[β]ψ.

A

γ,then⊢(χβ∧pre(β))→2Aχγ.2.IfA∈Candβ→

Fromtheseassumptions,infer⊢χα→[α]2∗Cψ.

Figure2:ThelogicalsystemforL([α],2∗).ForL([α]),wedropthe∗axiomsandrules.3.ALogicforL([α])

InFigure2belowwepresentalogicforL([α],2∗)whichweshallstudylater.Inthissection,weshallrestrictthelogictothesimplerlanguageL([α]).Wedosopartlytobreakupthestudyofasystemwithmanyaxiomsandrules,andpartlytoemphasizethesignificanceofaddingtheinfinitaryoperators2∗BtoL([α]).Tocarryouttherestriction,weforgettheaxiomsandrulesofinferenceinFigure2whicharemarkedbya∗.Inparticularα◦βwillbedefinedlater(Section4).

Therulesofthesystemareallquitestandardfrommodallogic.TheActionAxiomsaretheinterestingnewones.IntheAtomicPermanenceaxiom,pisanatomicsentence.Theaxiomthensaysthatannouncementsdonotchangethebrutefactofwhetherornotpholds.Thisaxiomreflectsthefactthatouractionsdonotchangeanykindoflocalstate.(WediscussanextensionofoursysteminSection5.3wherethisaxiomisnotsound.)ThePartialFunctionalityAxiomcorrespondstothefactthattheoperation󰀤W,w󰀥→󰀤W,w󰀥αisapartialfunction.ThekeyaxiomofthesystemistheAction-KnowledgeAxiom,givingacriterionforknowledgeafteranannouncement.Wewillchecksoundnessofthisaxiomleavingcheckingsoundnessofotherunstarredaxiomsandrulestothereader.

16

Proposition3.1TheAction-KnowledgeAxiom

[α]2Aϕ↔(pre(α)→

issound.

ProofWeremindthereaderthattherelevantdefinitionsandnotationarefoundinSection2.2.Letαbetheaction󰀤K,k󰀥.Fixapair󰀤W,w󰀥.If󰀤W,w󰀥|=¬pre(α),thenbothsidesofourbiconditionalhold.Wethereforeassumethat󰀤W,w󰀥|=pre(α)intherestofthisproof.Assumethat󰀤W,w󰀥α|=2Aϕ.

AA

k′.Letβ.Thisβisoftheform󰀤K,k′󰀥forsomek′suchthatk→Takesomeβsuchthatα→

Aw→w′.Wehavetwocases:󰀤W,w′󰀥|=pre(k′),and󰀤W,w′󰀥|=¬pre(k′).Inthelattercase,󰀤W,w′󰀥|=[β]ϕtrivially.We’llshowthisintheformercase,soassume󰀤W,w′󰀥|=pre(k′).Then

A

(w′,k′).Nowourassumptionthat󰀤W,w󰀥α|=2Aϕ(w′,k′)isaworldofWK,andindeed(w,k)→

impliesthat󰀤WK,(w′,k′)󰀥|=ϕ.Thismeansthat󰀤W,w′󰀥β|=ϕ.Hence󰀤W,w′󰀥|=[β]ϕ.Sinceβand󰀆

w′werearbitrary,󰀤W,w󰀥|=β2A[β]ϕ.Theotherdirectionissimilar.⊣TherestofthissectionisdevotedtothecompletenessresultforL([α]).Thereadernotinterestedinthismayomittherestofthissection,butatsomepointslaterwewillreferbacktothetermrewritingsystemRwhichweshalldescribeshortly.OurcompletenessproofisbasedonatranslationofL([α])toordinarymodallogicL.AndthistranslationisbasedonatermrewritingsystemtobecalledR.TherewritingrulesofRare:

[α]p[α]¬ψ[α](ψ∧χ)[α]2Aψ

;;;;

pre(α)→ppre(α)→¬[α]ψ[α]ψ∧[α]χ󰀆

A

β}pre(α)→{2A[β]ψ:α→

󰀃

A

β}){2A[β]ϕ:α→

Asinallrewritesystems,weapplytherulesofRatarbitrarysubsentencesofagivensentence.(For

example,considerwhathappenswithsomethinglike[α][β]ϕ.Wemightrewrite[β]ϕusingsomerule,saytoψ.Thenwemightrewrite[α]ψtosomethinglike[γ]ψ,etc.)Lemma3.2Thereisarelation2.Forallrulesϕ;ψofR,ψ<ϕ.

3.Asentenceϕ∈L([α])isanormalformiffitisamodalsentence(thatis,ϕcannotberewritteniffnoactionsoccurinϕ).Thistakessomework,andbecausethedetailsarelessimportantthanthefactsthemselves,wehaveplacedtheentirematterinanAppendixtothispaper.(TheAppendixalsodiscussesanextensionoftherewritesystemRtoasystemR∗forthelargerlanguageL([α],2∗),soifyoureaditatthispointyouwillneedtokeepthisinmind.)

Inthenextresult,weletLbeordinarymodallogicoverAtSen(whereofcoursetherearenoactions).

Proposition3.3Thereisatranslationt:L([α])→Lsuchthatforallϕ∈L([α]),ϕissemanticallyequivalenttoϕt.Proof

EverysentenceϕofL([α])mayberewrittentoanormalform.ByLemma3.2,thenormal

4.ALogicforL([α],2∗)17

formsofϕisasentenceinL.Wethereforesetϕttobeanynormalformofϕ,saytheoneobtainedbycarryingoutleftmostreductions.Thesemanticequivalencefollowsfromthefactthattherewriterulesthemselvesaresound,andfromthefactthatsemanticequivalenceispreservedbysubstitutions.

⊣Lemma3.4(Substitution)Letϕbeanysentence,andlet⊢χ↔χ′.Supposethatϕ[p/χ]comesfromϕbyreplacingpbyχatsomepoint,andϕ[p/χ′]comessimilarly.Then⊢ϕ[p/χ]↔ϕ[p/χ′].Proof

Byinductiononϕ.Thekeypointisthatwehavenecessitationrulesforeach[α].

⊣

Theorem3.5ThislogicalsystemforL([α])isstronglycomplete:Σ⊢ϕiffΣ|=ϕ.

ProofThesoundnesshalfbeingeasy,weonlyneedtoshowthatifΣ|=ϕ,thenΣ⊢ϕ.First,Σt|=ϕt.Sinceoursystemextendsthestandardcompleteproofsystemofmodallogic,Σt⊢ϕt.NowforeachχofL([α]),⊢χ↔χt.(ThisisaneasyinductiononStrongcompletenessresultsofthiskindmayalsobefoundinPlaza[13]andinGerbrandyandGroeneveld[7].WediscusssomeofthehistoryofthesubjectinSection7.

4.ALogicforL([α],2∗)

Atthispoint,weturntothecompletenessresultforL([α],2∗).Itiseasytocheckthatthereisnohopeofgettingastrongcompletenessresult(whereonehasarbitrarysetsofhypotheses).Thebestonecanhopeforisweakcompleteness:⊢ϕifandonlyif|=ϕ.Also,incontrasttoourtranslationsresultsforL([α]),thelargerlanguageL([α],2∗)cannotbetranslatedintoLoreventoL(2∗)(modallogicwithextramodalities2∗B).WeprovethisinTheorem6.2below.Socompletenessresultsfor

∗

L([α],2)cannotsimplybebasedontranslation.

OurlogicalsystemislistedinFigure2above.Wediscussedthefragmentofthesystemwhichdoes

∗

nothavethe∗axiomsandrulesinSection3.The2∗C-normalityAxiomand2C-necessitationRulearestandard,asistheMixAxiom.Weleavecheckingtheirsoundnesstothereader.ThekeyfeaturesofthesystemarethustheCompositionAxiomandtheActionRule.WebeginwiththeActionRule,restatedbelow:

TheActionRuleLetψbeasentence,andletCbeasetofagents.Lettherebesentencesχβforallβsuchthatα→∗Cβ(includingαitself),andsuchthat1.⊢χβ→[β]ψ.

A

2.IfA∈Candβ→γ,then⊢(χβ∧pre(β))→2Aχγ.

Fromtheseassumptions,infer⊢χα→[α]2∗Cψ.

RemarkWeuse→∗Casanabbreviationforthereflexiveandtransitiveclosureoftherelation󰀄∗A

A∈C→.Recallthatthereareonlyfinitelymanyβsuchthatα→Cβ,sinceeachisdeterminedbyaworldofthesamefiniteKripkeframethatdeterminesα.SoeventhoughtheActionRulemightlooklikeittakesinfinitelymanypremises,itreallyonlytakesfinitelymany.

Anotherpoint:ifonesodesires,theActionRulecouldbereplacedbya(morecomplicated)axiomschemewhichwewillnotstatehere.

Lemma4.1󰀤W,w󰀥|=󰀤α󰀥3∗CϕiffthereisasequenceofworldsfromW

w=w0

→A1

w1

→A2

···

→Ak−1

wk−1

→Ak

wk

18

wherek≥0,andalsoasequenceofactionsofthesamelengthk,

α=α0

suchthatAi∈Cand󰀤W,wi󰀥|=pre(αi)forall0≤i≤k,and󰀤W,wk󰀥|=󰀤αk󰀥ϕ.RemarkThecasek=0justsaysthat󰀤W,w󰀥|=󰀤α󰀥3∗=󰀤α󰀥ϕ.Cϕisimpliedby󰀤W,w󰀥|

Proof󰀤W,w󰀥|=󰀤α󰀥3∗=pre(α)and󰀤Wα,(w,α)󰀥|=3∗=pre(α)andCϕiff󰀤W,w󰀥|Cϕ;iff󰀤W,w󰀥|

α

thereisasequenceinW,

(w,α)=v0

wherek≥0suchthatAi∈Cand󰀤Wα,vk󰀥|=ϕ.NowsupposesuchsequencesexistinWα.ThenwegetasequenceofworldswiinWandactionsαisuchthatvi=(wi,αi)and󰀤W,wi󰀥|=pre(αi).Theconditionthat󰀤Wα,vk󰀥|=ϕtranslatesto󰀤W,wk󰀥|=󰀤αk󰀥ϕ.Conversely,ifwehaveasequenceinWwiththeseproperties,wegetoneinWαbytakingvi=(wi,αi).⊣Proposition4.2TheActionRuleissound.

ProofAssumethat󰀤W,w󰀥|=χαbutalso󰀤W,w󰀥|=󰀤α󰀥3∗C¬ψ.AccordingtoLemma4.1,thereisalabeledsequenceofworldsfromW

w=w0α=α0

wherek≥0andeachAi∈C,andalsoasequenceofactionsoflengthk,withthesamelabels,suchthat󰀤W,wi󰀥|=pre(αi)forall0Nowwearguethecasek>0.Weshowbyinductionon1≤i≤kthat󰀤W,wi󰀥|=χαi∧[αi]ψ.Inparticular,󰀤W,wk󰀥|=[αk]ψ.Thisisacontradiction.⊣WeclosewithadiscussionoftheCompositionRule,beginningwithageneraldefinition.

DefinitionLetα=󰀤K,k󰀥andβ=󰀤L,l󰀥beactions.Thentheactioncompositionα◦βistheactiondefinedasfollows.ConsidertheproductsetK×L.WeturnthisintoaKripkeframeusingtherestrictionoftheproductarrows.Wegetanactionstructurebysetting

pre((k′,l′))

Finally,wesetα◦β=󰀤K×L,(k,l)󰀥.

=

pre(k′)∧[󰀤K,k′󰀥]pre(l′).

→A1

α1

→A2

···

→Ak−1

αk−1

→Ak

αk

→A1

w1

→A2

···

→Ak−1

wk−1

→Ak

wk

→A1

v1

→A2

···

→Ak−1

vk−1

→Ak

vk

→A1

α1

→A2

···

→Ak−1

αk−1

→Ak

αk

Proposition4.3Concerningthecompositionoperation:1.(Wα)β∼=Wα◦βviatherestrictionof((w,k′),l′)→(w,(k′,l′))to(Wα)β.2.TheCompositionAxiomissound:[α][β]ϕ↔[α◦β]ϕ.3.α◦(β◦γ)∼=(α◦β)◦γ.

4.α◦τ∼=α∼=τ◦α,wherethenullactionτisfromSection1.2.

ProofLetα=󰀤K,k󰀥andβ=󰀤L,l󰀥.For(1),notethattheworldsof(Wα)βareoftheform((w,k′),l′),where(w,k′)∈Wαand󰀤Wα,(w,k′)󰀥|=pre(l′).Forsuch((w,k′),l′),󰀤W,w󰀥|=pre(k′)and󰀤W,w󰀥|=[󰀤K,k′󰀥]pre(l′).Thatis,(w,(k′,l′))∈Wα◦β.Theconverseissimilar,andtherestoftheisomorphismpropertiesareeasy.

Part(2)followsfrom(1).Weusetheobviousisomorphism((k,l),m)→(k,(l,m))inpart(3).WeusetheCompositionand[α]-necessitationaxiomstoshowthatthisisomorphismpreservestheprefunctionuptologicalequivalence.Part(4)iseasy,usingthefactthat|=[τ]ϕ↔ϕ.⊣

5.CompletenessforL([α],2∗)19

ExtendingtherewritingsystemRtoL([α],2∗).WeconsiderL([α],2∗).TherewritingsystemRextendsnaturallytothislargerlanguage,takingnewsymbolsfortheoperators2∗B.WealsoaddarulecorrespondingtotheCompositionAxiom:[α][β]ϕ;[α◦β]ϕ.WecallthisrewritingsystemR∗.Lemma4.4Thereisarelation2.Forallrulesϕ;ψofR∗,ψ<ϕ.

3.Ifψisapropersubsentenceofϕ,thenψ<ϕ.

4.Asentenceϕ∈L([α],2∗)isanormalformiffitisbuiltfromatomicsentencesusing¬,∧,2A,

∗

and2∗B,orifitisoftheform[α]2Bψ,whereαisanactioninnormalform,andψtooisinnormalform.

∗

β,pre(β)isanormalformsentence.5.Anactionαisanormalformifwheneverα→∗

6.Ifα→β,then[α]2∗Cψ>[β]ψ.

7.nf(ϕ)≤ϕ.

Onceagain,thedetailsareintheAppendix.

InSection3,wesawatranslationtfromL([α])toLcanbeextendedtoatranslationfromL([α],2∗)totheinfinitarylanguageL∞,wherewehavecountableconjunctionsanddisjunctions.ThisextensionisdefinedusingPart(4)ofLemma4.4.Theadditionalclausesinthedefinitionoftare

󰀆tt

(2∗ϕ)=B󰀎A1,...,An󰀏∈B∗(2A1···2Anϕ)󰀆tt([α]2∗=Bψ)󰀎A1,...,An󰀏∈B∗([α]2A1···2Anψ)Inthisway,weseethatL([α],2∗)mayberegardedasafragmentofinfinitarymodallogic.

RemarkItispossibletodroptheCompositionAxiominfavorofamoreinvolvedversionofthe

ActionRule.ThepointistheCompositionAxiomsimplifiesthenormalformsoftheL([α],2∗):WithouttheCompositionAxiom,thenormalformsofsentencesofL([α],2∗)wouldbeoftheform[α1][α2]···[αr]ψ,whereeachαiisanormalformactionandψisanormalformsentence.TheCompositionAxiominsuresthatthenormalformsareoftheform[α]ψ.SoifweweretodroptheCompositionAxiom,wewouldneedaformulationoftheActionRulewhichinvolvedsequencesofactions.Itisnotterriblydifficulttoformulatesucharule,andcompletenesscanbeobtainedbyanelaborationoftheworkwhichweshalldo.Wedidnotpresentthiswork,mostlybecauseaddingtheCompositionAxiomleadstoshorterproofs.

ThiscompletesthediscussionoftheaxiomsandrulesofourlogicalsystemforL([α],2∗).5.CompletenessforL([α],2∗)

Inthissection,weprovethecompletenessofthelogicalsystemforL([α],2∗).Section5.1hassometechnicalresultswhichculminateintheSubstitutionLemma5.3.ThisisusedinsomeofourworkonnormalformsintheAppendix,andthatworkfiguresinthecompletenesstheoremofSection5.2.5.1SomeSyntacticResults

Lemma5.1ForallA∈Candallβsuchthatα→Aβ,1.⊢[α]2∗Cψ→[α]ψ.

∗2.⊢[α]2∗Cψ∧pre(α)→2A[β]2Cψ.

ProofPart(1)followseasilyfromtheMixAxiomandmodalreasoning.Forpart(2),westartwitha

20

∗∗∗

consequenceoftheMixAxiom:⊢2∗Cψ→2A2Cψ.Thenbymodalreasoning,⊢[α]2Cψ→[α]2A2Cψ.

∗

BytheAction-KnowledgeAxiom,,wehave⊢[α]2∗⊣Cψ∧pre(α)→2A[β]2Cψ.

DefinitionLetαandα′beactions.Wewrite⊢α↔α′ifαandα′arebasedonthesameKripkeframeWandthesameworldw,andifforallv∈W,⊢pre(v)↔pre′(v),wherepreistheannouncementfunctionforα,andpre′forα′.Wenotethefollowingbisimulation-likeproperties:1.If⊢α↔α′,thenalso⊢pre(α)↔pre(α′).

′′∗

2.Wheneverβ′issuchthatα′→∗Cβ,thenthereissomeβsuchthat⊢β↔βandα→Cβ.

Thesefolloweasilyfromthewaywedefinedpreonactionsintermsoffunctionsonframes.Lemma5.2If⊢α↔α′,thenforallψ,⊢[α]ψ↔[α′]ψ.

ProofByinductiononψ.Forψatomic,ourresultiseasy.Theinductionstepsfor¬and∧aretrivial.Thestepfor2Aisnothard,andsoweomitit.Assumingtheresultforψgivestheresultfor[χ]ψ,usingtheCompositionAxiomandtheinductionhypothesis.Thisleavesthestepforsentencesof

∗′∗

theform2∗Bψ,assumingtheresultforψ.WeusetheActionRuletoshowthat⊢[α]2Cψ→[α]2Cψ.

′

Foreachβ′,weletχβ′be[β]2∗Cψ,whereβissuchthat⊢β↔β.Weneedtoshowthatforallrelevantβ′andγ′,

′

a.⊢[β]2∗Cψ→[β]ψ;and

′∗Ab.Ifβ′→γ′,then⊢[β]2∗Cψ∧pre(β)→2A[γ]2Cψ.

For(a),weknowfromLemma5.1,part(1)that⊢[β]2∗Cψ→[β]ψ.Byinductionhypothesisonψ,⊢[β]ψ↔[β′]ψ.Andthisimplies(a).For(b),Lemma5.1,part(2)tellsusthatundertheassumptions,

∗

⊢[β]2∗Cψ∧pre(β)→2A[γ]2Cψ.Asweknow,⊢pre(β)↔pre(β′).Thisimplies(b).

Thiscompletestheinductiononψ.

⊣

Lemma5.3(Substitution)LettbeasentenceoractionofL([α],2∗),andlet⊢χ↔χ′.Supposethatt[p/χ]comesfromtbyreplacingpbyχatsomepoint,andt[p/χ′]comessimilarly.Then⊢t[p/χ]↔t[p/χ′].Proof

Byinductionont,usingLemma5.2.

⊣

Lemma5.4Foreverysentenceϕ∈L([α],2∗)thereissomenormalformnf(ϕ)≤ϕsuchthat⊢ϕ↔nf(ϕ).

ProofGivenϕ,thereisafinitesequenceϕ0;···;ϕn=ϕ′suchthatϕ0=ϕ,andϕnisinnormalform.Thisisaconsequenceofthefactthat5.CompletenessforL([α],2∗)21

5.2Completeness

TheproofofcompletenessanddecidabilityisbasedonthefiltrationargumentforcompletenessofPDLduetoKozenandParikh[10].Weshowthateveryconsistentϕhasafinitemodel,andthatthesizeofthemodelisrecursiveinϕ.WeshallneedtousesomeresultsconcerningtherewritingsystemR∗fromSection4.

DefinitionLets(ϕ)bethesetofsubsentencesofϕ,includingϕitself.Thisincludesallsentencesoccurringinactionswhichoccurinϕandtheirsubsentences.Forfutureuse,wenotethat

󰀄∗∗

s([α]2∗ϕ)={[α]2ϕ,2ϕ}∪s(ϕ)∪{s(pre(β)):α→∗(5.1)CCCCβ}

Wedefineafunctionf:L([α],2∗)→P(L([α],2∗))byrecursiononthewellfoundedrelationf(p)f(¬ϕ)f(ϕ∧ψ)f(2Aϕ)f(2∗Bϕ)f([α]2∗Cϕ)

=

=====

∪∪∪∪

{p}

f(ϕ)∪{¬ϕ}

f(ϕ)∪f(ψ)∪{ϕ∧ψ}f(ϕ)∪{2Aϕ}

∗

f(ϕ)∪{2∗Bϕ}∪{2A2Bϕ:A∈B}

∗

{2A[β]2∗Cϕ:α→Cβ&A∈C}

∗

{[β]2∗Cϕ:α→Cβ&A∈C}󰀄

{f(χ):(∃β)α→∗Cβ&χ∈s(pre(β))}∗f(2Cϕ)󰀄

{f([β]ϕ):α→∗Cβ}

Forϕnotinnormalform,letf(ϕ)=f(nf(ϕ)).(Notethatweneedtodefinefonsentenceswhichare

notnormalforms,becausef([β]ψ)figuresinf([α]2∗Cϕ).Also,thedefinitionmakessensebecausethecallstofontheright-handsidesareall1.f(ϕ)isafinitesetofnormalformsentences.2.nf(ϕ)∈f(ϕ).

3.Ifψ∈f(ϕ),thenf(ψ)⊆f(ϕ).4.Ifψ∈f(ϕ),thens(ψ)⊆f(ϕ).

∗∗∗

5.If[γ]2∗Cχ∈f(ϕ),γ→Cδ,andA∈C,thenf(ϕ)alsocontains2A[δ]2Cχ,[δ]2Cχ,pre(δ),andnf([δ]χ).

ProofAllofthepartsarebyinductiononϕinthewell-order<.Forpart(1),notethatif[α]2∗Cψis

∗

anormalform,theneachsentence2A[β]2Cψandallsubsentencesofthissentencearenormalforms.Forpart(2),notethatwhenϕisanormalform,ϕ∈f(ϕ).

Inpart(3),weonlyneedtoconsiderϕinnormalform.Theresultisimmediatewhenϕisan

∗

atomicsentencep.Theinductionstepsfor¬,∧,and2Aareeasy.For2∗Bϕ,notethatsinceϕ<2Bϕ,ourinductionhypothesisimpliestheresultforϕ;weverifyitfor2∗Bϕ.Theonlyinterestingcaseis

∗

whenψis2A2BϕforsomeA∈B.Andinthiscase

f(ψ)

=

∗

f(2∗Bϕ)∪{2A2Bϕ}

⊆

f(2∗Bϕ).

22

∗

Tocompletepart(3),weconsider[α]2∗Cϕ.Ifthereissomeχ<[α]2Cϕsuchthatψ∈f(χ)andf(χ)⊆f([α]2∗Cϕ),thenweareeasilydonebytheinductionhypothesis.Thiscoversallofthecases

∗∗

exceptforψ=[β]2∗Cϕandψ=2A[β]2Cϕ.Forthefirstofthese,weusethetransitivityof→Cto

∗

checkthatf([β]2∗Cϕ)⊆f([α]2Cϕ).Andnowthesecondcasefollows:

f(2A[β]2∗Cϕ)

=

∗

f([β]2∗Cϕ)∪{2A[β]2Cϕ}

⊆

f([α]2∗Cϕ).

Part(4)issimilartopart(3),usingequation(5.1)atthebeginningofthissubsection.

∗

Forpart(5),assumethat[γ]2∗Cχ∈f(ϕ).Bypart(1),[γ]2Cχisanormalform.Weshowthat

∗∗

2A[δ]2∗Cχ,[δ]2Cχ,pre(δ),andnf([δ]χ)allbelongtof([γ]2Cχ),andthenusepart(3).Thefirsttwoofthesesentencesareimmediatebythedefinitionoff;thethirdonefollowsfrompart(4);andthelastcomesfrompart(2)sincenf([δ]χ)∈f([δ]χ)⊆f([γ]2∗⊣Cχ.Theset∆=∆(ϕ)Fixasentenceϕ.Weset∆=f(ϕ)(i.e.,wedropϕfromthenotation).Thisset∆istheversionforourlogicoftheFischer-Ladnerclosureofϕ.Let∆={ψ1,...,ψn}.GivenamaximalconsistentsetUofL([α],2∗),let

[[U]]

=

+

ψn,

wherethesignsaretakeninaccordancewithmembershipinU.Thatis,ifψi∈U,thenψisaconjunctof[[U]];butifψi∈/U,then¬ψiisaconjunct.

Two(standard)observationsareinorder.Noticethatif[[U]]=[[V]],then[[U]]∧[[V]]isinconsistent.Also,forallψ∈∆,

󰀅

⊢ψ↔{[[W]]:Wismaximalconsistentandψ∈W}.(5.2)

⊢¬ψ↔

󰀅

{[[W]]:Wismaximalconsistentand¬ψ∈W}.

(5.3)

and

(Thereasonisthatψisequivalenttothedisjunctionofallcompleteconjunctionswhichcontainit.However,someofthosecompleteconjunctionsareinconsistentandthesecanbedroppedfromthebigdisjunction.Theothersareconsistentandhencecanbeextendedtomaximalconsistentsets.)DefinitionThefiltrationFisthemodelwhoseworldsaretheequivalenceclasses[U],whereUisamaximalconsistentsetinthelogicforL([α],2∗),andtheequivalencerelationisU≡Viff[[U]]=[[V]](iffU∩∆=V∩∆).Weset󰀤F,[U]󰀥|=piffp∈U∩∆.Furthermore,

A

[V]inF[U]→

iffwhenever2Aψ∈U∩∆,thenalsoψ∈V.(5.4)

Thisconditionisindependentofthechoiceofrepresentatives:weusepart(4)ofLemma5.5tosee

thatif2Aχ∈∆,thenalsoχ∈∆.Agoodpathfrom[V0]for󰀤α󰀥3∗CψisapathinF

[V0]

→A1

[V1]

α1→A2

→A2

suchthatk≥0,eachAi∈C,andsuchthatthereexistactions

α=α0

suchthatpre(αi)∈Viforall0≤i≤k,and󰀤αk󰀥ψ∈Vk.

→A1

···

→Ak−1

···

→Ak−1

[Vk−1]αk−1

→Ak

→Ak

[Vk]αk

TheideabehindagoodpathcomesfromconsideringLemma4.1inF.Ofcourse,thespecialcaseofthatresultwouldrequirethat󰀤F,[Vi]󰀥|=pre(αi)ratherthanpre(αi)∈Vi,andsimilarlyfor󰀤αk󰀥ψandVk.TheexactformulationabovewasmadeinorderthattheTruthLemmawillgothroughforsentencesoftheform󰀤α󰀥3∗Cψ(seethefinalparagraphsoftheproofofLemma5.8).Proof

∗∗Lemma5.6Let[α]2∗Cψ∈∆.Ifthereisagoodpathfrom[V0]for󰀤α󰀥3C¬ψ,then󰀤α󰀥3C¬ψ∈V0.

Byinductiononthelengthkofthepath.Ifk=0,then󰀤α󰀥¬ψ∈V0.If󰀤α󰀥3∗/V0,thenC¬ψ∈

5.CompletenessforL([α],2∗)23

[α]2∗Cψ∈V0.ByLemma5.1,part(1),wehave[α]ψ∈V0.Thisisacontradiction.Assumetheresultfork,andsupposethatthereisagoodpathfrom[V0]for󰀤α󰀥3∗C¬ψoflengthk+1.

∗∗

Thenthereisagoodpathoflengthkfrom[V1]for󰀤α1󰀥3C¬ψ.Also,[α1]2Cψ∈∆,byLemma5.5,part(5).Byinductionhypothesis,󰀤α1󰀥3∗C¬ψ∈V1.

∗∗

If󰀤α󰀥3C¬ψ∈/V0,then[α]2Cψ∈V0.ByLemma5.1,part(2),V0contains[α]2∗Cψ∧pre(α)→

∗∗

2A[α1]2Cψ.SoV0contains2A[α1]2Cψ.Again,thissentencebelongsto∆byLemma5.5,part(5).

A

inF,weseethat[α1]2∗Nowbydefinitionof→⊣Cψ∈V1.Thisisacontradiction.

∗

Lemma5.7If[[V0]]∧󰀤α󰀥3∗Cψisconsistent,thenthereisagoodpathfrom[V0]for󰀤α󰀥3Cψ.

Wewillneedthefollowingstandardclaim,anargumentforwhichcanbefoundinKozenandParikh[10].WewillalsousethisclaimintheproofofLemma5.8.ClaimIf[[U]]∧3A[[V]]isconsistent,then[U]→A[V].

ProofofClaimAssume2Aψ∈U∩∆.Ifψ∈V,then¬ψ∈V,sosinceψ∈∆,⊢[[V]]→¬ψ.Thus,⊢3A[[V]]→3A¬ψ,andso⊢[[U]]∧3A[[V]]→2Aψ∧3A¬ψ,whence[[U]]∧3A[[V]]isinconsistent.Thiscontradictionestablishestheclaim.

ProofForeachβsuchthatα→∗Cβ,letSβbethe(finite)setofall[W]∈Fsuchthatthereisno

∗

goodpathfrom[W]for󰀤β󰀥3Cψ.Weneedtoseethat[V0]∈/Sα;supposetowardacontradictionthat[V0]∈Sα.Let󰀅

χβ={[[W]]:W∈Sβ}.

󰀇

Notethat¬χβislogicallyequivalentto{[[W′]]:[W′]∈FandW′∈/Sβ}.SinceweassumedV0∈Sα,wehave⊢[[V0]]→χα.

Wefirstclaimthatχβ∧󰀤β󰀥ψisinconsistent.Otherwise,therewouldbe[W]∈Sβsuchthatχβ∧󰀤β󰀥ψ∈W.NotethatbythePartialFunctionalityAxiom,⊢󰀤β󰀥ψ→pre(β).Butthentheone-pointpath[W]isagoodpathfrom[W]for󰀤β󰀥3∗/Sβ,andthisisacontradiction.Cψ.Thus[W]∈Soindeed,χβ∧󰀤β󰀥ψisinconsistent.Therefore,⊢χβ→[β]¬ψ.

WenextshowthatforallA∈Candallβsuchthatβ→Aγ,χβ∧pre(β)∧󰀇3A¬χγisinconsistent.Otherwise,therewouldbe[W]∈Sβwithχβ,pre(β),and3A¬χγinit.Then{3A[[W′]]:W′∈Sγ},beingequivalentto3A¬χβ,wouldbelongtoW.Itfollowsthat3A[[W′]]∈WforsomeW′∈Sγ.Bytheclaim,[W]→A[W′].Since[W′]∈/Sγ,thereisagoodpathfrom[W′]for󰀤γ󰀥3∗Cψ.But

∗

sinceβ→AγandWcontainspre(β),wealsohaveagoodpathfrom[W]for󰀤β󰀥3Cψ.Thisagaincontradicts[W]∈Sβ.Asaresult,forallrelevantA,β,andγ,⊢χβ∧pre(β)→2Aχγ.BytheActionRule,⊢χα→[α]2∗[V0]]→χα.So⊢[[V0]]→[α]2∗C¬ψ.Now⊢[C¬ψ.Thiscontradictstheassumptionwithwhichwebeganthisproof.⊣Lemma5.8(TruthLemma)Considerasentenceϕ,andalsotheset∆=f(ϕ).Forallχ∈∆and[U]∈F:χ∈Uiff󰀤F,[U]󰀥|=χ.

ProofWearguebyinductiononthewellfoundedSupposenextthatχ≡2Aψ.Suppose2Aψ∈U;weshow󰀤F,[U]󰀥|=2Aψ.Let[V]besuchthatAA

[U]→[V].Thenbydefinitionof→,ψ∈V.Theinductionhypothesisappliestoψ,sinceψ<2Aψ,andsinceψ∈∆byLemma5.5,part(4).Sobyinductionhypothesis,󰀤F,[V]󰀥|=ψ.Thisgiveshalfofourequivalence.Conversely,supposethat󰀤F,[U]󰀥|=2Aψ.Supposetowardsacontradictionthat3A¬ψ∈U.So[[U]]∧3A¬ψisconsistent.Weuseequation(5.3)󰀇andthefactthat3Adistributesoverdisjunctionstoseethat[[U]]∧3A¬ψislogicallyequivalentto([[U]]∧3A[[V]]),wherethedisjunctionis

24

takenoverallVwhichcontain¬ψ.Since[[U]]∧3A¬ψisconsistent,oneofthedisjuncts[[U]]∧3A[[V]]mustbeconsistent.Theinductionhypothesisagainapplies,andweuseittoseethat󰀤F,[V]󰀥|=¬ψ.

A

BytheclaimintheproofofLemma5.7,[U]→[V].Weconcludethat󰀤F,[U]󰀥|=3A¬ψ,andthisisacontradiction.

Forχoftheform2∗Cψ,weusethestandardargumentforPDL(seeKozenandParikh[10]).ThisisbasedonlemmasthatparallelLemmas5.6and5.7.Theworkissomewhateasierthanwhatwedobelowforsentencesoftheform[α]2∗Cψ,andsoweomitthesedetails.

Weconcludewiththecasewhenχisanormalformsentenceoftheform[α]2∗Cψ∈∆.Assumethat∗∗

[α]2Cψ∈∆.First,supposethat[α]2Cψ∈/U.ThenbyLemma5.7,thereisagoodpathfrom[U]for

∗

󰀤α󰀥3C¬ψ.WewanttoapplyLemma4.1inFtoassertthat󰀤F,[U]󰀥|=󰀤α󰀥3∗C¬ψ.Letkbethelengthofthegoodpath.Fori≤k,pre(αi)∈Ui.Noweachpre(αi)belongsto∆byLemma5.5,part(5),andis<[α]2∗=pre(αi).WealsoneedtocheckthatCψ.Sobyinductionhypothesis,󰀤F,[Ui]󰀥|

󰀤F,[Uk]󰀥|=󰀤αk󰀥¬ψ.Forthis,recallfromLemma5.5,part(5)that∆containsnf([αk]ψ)≤[αk]ψ.ByLemma4.4,nf([αk]ψ)≤[αk]ψ<[α]2∗Cψ.Sincethepathisgood,Ukcontains󰀤αk󰀥¬ψandhence¬[αk]ψ.Italsomustcontainthenormalformofthis,byLemma5.4.Sobyinductionhypothesis,󰀤F,[Uk]󰀥|=nf(¬[αk]ψ).Bysoundness,󰀤F,[Uk]󰀥|=󰀤αk󰀥¬ψ.NowitdoesfollowfromLemma4.1that󰀤F,[U]󰀥|=󰀤α󰀥3∗C¬ψ.

Goingtheotherway,supposethat󰀤F,[U]󰀥|=󰀤α󰀥3∗C¬ψ.ByLemma4.1,wegetapathinFwitnessingthis.Theargumentofthepreviousparagraphshowsthatthispathisagoodpathfrom

∗

[U]for󰀤α󰀥3∗⊣C¬ψ.ByLemma5.6,Ucontains󰀤α󰀥3C¬ψ.Thiscompletestheproof.Theorem5.9(Completeness)Forallϕ,⊢ϕiff|=ϕ.Moreover,thisrelationisdecidable.ProofByLemma5.4,⊢ϕ↔nf(ϕ).Letϕbeconsistent.BytheTruthLemma,nf(ϕ)holdsatsomeworldinthefiltrationF.Sonf(ϕ)hasamodel;thusϕhasone,too.Thisestablishescompleteness.Fordecidability,notethatthesizeofthefiltrationiscomputableinthesizeoftheoriginalϕ.⊣5.3TwoExtensions

WebrieflymentiontwoextensionsoftheCompletenessTheorem5.9.TheseextensionscomefromourdiscussionattheendofSection2.3.

First,considerthecaseofS5actions.WechangeourlogicalsystembyrestrictingtotheseS5actions,andweaddtheS5axiomstoourlogicalsystem.WeinterpretthisnewsystemonS5models.ItiseasytocheckthatapplyinganS5actiontoanS5modelgivesanotherS5model.Further,theS5actionsareclosedundercomposition.Finally,ifαisanS5actionandα→Aβ,thenβalsoisanS5action.Theseeasilyimplythesoundnessofthenewaxioms.Forcompleteness,weneedonlycheckthatifweassumetheS5axioms,thenthefiltrationFfromtheprevioussectionhastheproperty

A

thateach→isanequivalencerelation.Thisisastandardexerciseinmodallogic(see,e.g.,Faginetal[4],Theorem3.3.1).

Oursecondextensionconcernsthemovefromactionsaswehavebeenworkingthemtoactionswhichchangethetruthvaluesofatomicsentences.Ifwemakethismove,thentheaxiomofAtomicPermanenceisnolongersound.However,itiseasytoformulatetherelevantaxioms.Forexample,ifwehaveanactionαwhicheffectsthechangep:=p∧¬q,thenwewouldtakeanaxiom[α]p↔(pre(α)→p∧¬q).Havingmadethesechanges,alloftherestoftheworkwehavedonegoesthrough.Inthisway,wegetacompletenesstheoremforthislogic.

6.ResultsonExpressivePower

Inthissection,wepresenttworesultswhichshowthataddingannouncementstomodallogicwith3∗addsexpressivepowerasdoesaddingprivateannouncementstomodallogicwith3∗andpublicannouncements.ToshowtheseresultsitwillbesufficienttotakethesetAofagentstobe{A,B}andconsideronlylanguagescontainedinalanguagebuilt-upfromtheatomicsentencespandq,using

6.ResultsonExpressivePower

25

∗∗

3A,3B,3∗A,3B,and3AB,andtheactions[ϕ]A,[ϕ]BofannouncingϕtoAorBprivately,and[ϕ]ABtheactionofannouncingϕtoAandBpublicly.LetLallstandforthislanguage.Weuseherethecustomarynotation([ϕ]A,[ϕ]B,[ϕ]AB)forannouncements,but[ϕ]Aissimplytheactionwiththe

A

fromktokandpre(k)=ϕ.Wethinkof[ϕ]Bsimilarly.[ϕ]ABisKripkestructureK={k}with→

AB

theactionwiththeKripkestructureK={k}with→and→goingfromktokandpre(k)=ϕ.Weneedtodefinearank|ϕ|onsentencesfromLall.Let|p|=0forpatomic,|¬ϕ|=|ϕ|,|ϕ∧ψ|=max(|ϕ|,|ψ|),|¬ϕ|=|ϕ|,|3Xϕ|=1+|ϕ|,forX=AorX=B,|3∗Xϕ|=1+|ϕ|forX=A,X=B,orX=AB,and|[ϕ]Xψ|=max(|ϕ|,|ψ|)forX=A,X=B,orX=AB.

Firstwepresentalemmawhichallowsus,incertaincircumstances,todothefollowing:fromtheexistenceofasentenceinalanguageL1whichisnotequivalenttoanysentenceinalanguageL0inferthatthereexistsasentenceinL1notequivalenttoanytheoryinL0.

Lemma6.1LetL0bealanguageincludedinLall,andletψbeasentenceinLall.AssumethatforeachnwehavemodelsFnandGnwithsomeworldsfn∈Fnandgn∈Gnsuchthat󰀤Fn,fn󰀥satisfies¬ψ,󰀤Gn,gn󰀥satisfiesψ,and󰀤Fn,fn󰀥and󰀤Gn,gn󰀥agreeonallsentencesinL0ofrank≤n.Then3AψisnotequivalentwithanytheoryinL0.

󰀈

ProofForasequenceofmodel-worldpairs󰀤Hn,hn󰀥,n∈D⊆ω,weletn∈D(Hn,hn)beamodel-worldpairdefinedasfollows.Lethbeanewworld.TakedisjointcopiesoftheHn’sandaddanA-arrowfromhtoeachhn.AllotherarrowsarewithintheHn’sandstaythesameasinHn.Noatomicsentencesaretrueath.AtomicsentencestrueintheworldsbelongingtothecopyofHnin󰀈

n)arepreciselythosetrueatthecorrespondingworldsofHn.n∈D(Hn,h󰀈

m

n∈ω(Fn,fn)withthenewworlddenotedbyf.DefinealsoF,form∈ω,tobe󰀈LetFbem

whereHm=Gm,hm=gmandforalln=m,Hn=Fnandn∈ω(Hn,hn)withthenewworldf

hn=fn

Nowassumetowardsacontradictionthat3AψisequivalentwithatheoryΦinL0.Clearly3Aψfailsin󰀤F,f󰀥.Thussomesentenceϕ∈Φfailsin󰀤F,f󰀥.Ontheotherhand,each󰀤Fm,fm󰀥satisfies3Aψ,whence󰀤Fm,fm󰀥satisfiesϕ.Letm0=|ϕ|.Thefollowingclaimshowsthatboth󰀤F,f󰀥and󰀤Fm0,fm0󰀥makeϕtrueorbothofthemmakeitfalse,whichleadstoacontradiction.

ClaimLetϕbeasentenceinΦofrank≤m.LetHn,Kn,n∈D,withhn∈Hnand󰀈kn∈Knbemodels󰀈suchthat󰀤Hn,hn󰀥and󰀤Kn,kn󰀥agreeonsentencesinΦofrank≤m.Then󰀤n(Hn,hn),h󰀥and󰀤n(Kn,kn),k󰀥agreeonϕ.

Thisclaimisprovedbyinductiononcomplexityofϕ.Itisclearforatomicsentences.Theinductionstepsforbooleanconnectivesaretrivial.Amomentofthoughtgivestheinductionstepfor3and3∗withvarioussubscripts.Itremainstoconsiderthecasewhenϕ=[ϕ1]Aϕ2.(Thecaseswhenϕ=[ϕ1]Bϕ2andϕ=[ϕ1]ABϕ2aresimilar.)FixHn,Kn,hn∈Hn,kn∈Kn,withn∈D,suchthat󰀤Hn,hn󰀥and󰀤Kn,kn󰀥agreeonsentencesinΦofrank≤m.Notethat,foreachn∈D,󰀤Hn,hn󰀥|=ϕ1

′

ifandonlyif󰀤Kn,kn󰀥|=ϕ1.LetD1bethesetofalln∈Dforwhich󰀤Hn,hn󰀥|=ϕ1.LetHnand′

KnbemodelsobtainedbyupdatingHnandKnby[ϕ1]A.Bythedefinitionofrankandthefactthat

′′

|ϕ1|≤m,wehavethat󰀤Hn,hn󰀥and󰀤Kn,kn󰀥agreeonsentencesfromΦofrank≤m.Therefore,byourinductivehypothesis

󰀉󰀉

′′

󰀤Hn,h󰀥|=ϕ2iff󰀤Kn,k󰀥|=ϕ2.

n∈D1

n∈D1

However,

󰀉󰀉

′

󰀤Hn,h󰀥|=ϕiff󰀤Hn,h󰀥|=ϕ2

n

n∈D1

and

󰀉󰀤Kn,k󰀥|=ϕiff

n

󰀤

n∈D1

󰀉

′

Kn,k󰀥|=ϕ2,

andwearedone.⊣

26

6.1AnnouncementsaddExpressivePowertoModalLogicwith2∗

Intheresultbelow,therewillbeonlyoneagentA,andsoweomittheletterAfromthenotation.

∗

WeletL([],3∗)bemodallogicwithannouncements(tothisA)and3∗=3∗A.WealsoletL(3)betheobvioussublanguage.

Theorem6.2ThereisasentenceofL([],3∗)whichcannotbeexpressedbyanysetofsentencesofL(3∗).

ProofWeshowfirstthat[p]3+q=[p]33∗qcannotbeexpressedbyanysinglesentenceofL(2∗).(Incidentally,thesameholdsfor[p]3∗q.)Fixanaturalnumbern.WedefinestructuresA=AnandB=Bnasfollows.FirstBhas2n+3pointsarrangedcyclicallyas

0→1→···→n→n+1→−n→···→−1→0.

Fortheatomicsentences,wesetptrueatallpointsexceptn+1,andqtrueonlyat0.

narrangedasThestructureAisacopyofBwithnmorepoints

0→

n→0.

TheshapeofAisafigure-8.Inbothstructures,everypointisreachablefromeverypointbythe

transitiveclosureofthe→relation.Atthepoints

6.ResultsonExpressivePower

27

WereturntothemodelsAandBdescribedinthebeginningofthisproof.For0≤i≤n,weletSi⊆A×Bbethefollowingset

Si

=

∪∪

{(0,0),...,(n,n),(n+1,n+1),(−n,−n),...,(−1,−1)}

n−1,−2)...,(1,−n)}{(

{(n−i,n−i)}

Inthecaseofi=n,thenthelastdisjunctisempty.NotethatS0⊃S1⊃···⊃Sn.Also,for

0≤i≤n,everypointofonestructureisrelatedbySitosomepointoftheother.Claim2If0≤i≤nand(a,b)∈Si,then󰀤A,a󰀥∼i󰀤B,b󰀥.

Theproofisbyinductiononi.Ifi=0,thisisduetothefactthatpairsinS0agreeontheatomicformulas.Assumethestatementfori,andthati+1≤n.Let(a,b)∈Si+1.WeonlyneedtoshowthatIIcanrespondtoanyplayandhavetheresultingpairbelongtoSi.SupposefirstthatIplaysa3-move.Supposealsothata=b,sothat(a,a)comesfromthefirstsubsetofSi+1.Inthiscase,weonlyneedtonoticethat(a+1,a+1)∈Siif|a|≤n,(−n,−n)∈Siifa=n+1,and(

a,a)belongsto

thethirdsubsetofSi+1,thena≤n−(i+1)=n−i−1.Soa+1≤n−i,and(

28

Theproofisbyinductiononϕ.Forϕ=p,theresultisclear,asaretheinductionstepsfor¬and∧.For3Aϕ,supposethataj|=3Aϕ.Eithera∞|=ϕ,inwhichcasea∞|=3Aϕ,orelseaj−1|=ϕ.Inthelattercase,byinductionhypothesis,a∞|=ϕ;whencea∞|=3Aϕ.Theconverseissimilar.Thecaseof3Bϕistrivial:aj|=¬3Bϕanda∞|=¬3Bϕ.

∗

For3∗Aϕ,notethatsincewehaveacycle(6.1)containingallpoints,thetruthvalueof3Aϕdoes

∗

notdependonthepoint.Thecasesof3∗Bϕand3ABϕaresimilar.

For[ϕ]ABψ,assumetheresultforϕandψ,andlet|[ϕ]ABψ|Theothercaseiswhenthereissomex∈/H.Ifak∈/Hforsomek≥jorfork=∞,thenalltheseakdonotbelongtoH.Inparticular,neitherajnora∞belong.Andsobothajanda∞satisfy[ϕ]ABψ.Ifb∈/H,thenHisbisimilartoaone-pointmodel.Thisisbecauseeveryai∈Hwould

AB

havesome→-successorinH(e.g.,a∞),andtherewouldbeno→edges.Soweassumeb∈H.Thusai∈/HforsomeiSoinH,ajanda∞agreeonallsentencesinanylanguagewhichisinvariantforbisimulation.NowL([]AB,3∗)hasthisproperty(asdoallthelanguageswhichwestudy:theyaretranslatableintoinfinitarymodallogic).Inparticular,󰀤H,aj󰀥|=ψiff󰀤H,a∞󰀥|=ψ.Thisconcludestheclaim.

WegetTheorem6.3directlyfromtheclaim,theobservationthat󰀤Gn,an󰀥|=χand󰀤Gn,a∞󰀥|=¬χ,andLemma6.1.⊣Wefeelthatourtworesultsonexpressivepowerarejustasampleofwhatcouldbedoneinthisarea.Wedidnotinvestigatethenextnaturalquestions:Doannouncementswithsuspiciousoutsidersextendtheexpressivepowerofmodallogicwithallsecureprivateannouncementsandcommonknowledgeoperators?Andthendoannouncementswithcommonknowledgeofsuspicionaddfurtherexpressivepower?

7.ConclusionsandHistoricalRemarks

Theworkofthispaperbuildsonthelongtraditionofepistemiclogicaswellastechnicalresultsinotherareas.Inrecenttimes,oneveryactivearenaforworkonknowledgeisdistributedsystems,andthemainsourceofworkinrecenttimesonknowledgeindistributedsystemsisthebookReasoningAboutKnowledge[4]byFagin,Halpern,Moses,andVardi.Wedepartfrom[4]byintroducingthenewoperatorsforepistemicactions,andbydoingwithouttemporallogicoperators.Ineffect,ourKripkemodelsaresimpler,sincetheydonotincorporatealloftherunsofasystem;thenewoperatorscanbeviewedasacompensationforthat.Wehavenotmadeadetailedcomparisonofourworkwiththelargebodyofworkonknowledgeondistributedsystems,andsuchacomparisonwouldrequirebothtechnicalandconceptualresults.Onthetechnicalside,wesuspectthatneitherframeworkistranslatableintotheother.Onewaytoshowthiswouldbebyexpressivityresults.Perhapsanotherwaywouldusecomplexityresults.Inthisdirection,wenotethatHalpernandVardi[8]examinesninety-sixlogicsofknowledgeandtime.Thirty-twoofthesecontaincommonknowledgeoperators,andofthese,allbuttwelveoftheseareundecidable.Butoverall,ourlogicsarebasedondifferingconceptualpointsandintendedapplications,andsoweareconfidentthattheydiffer.

Asfarasweknow,thefirstpapertostudytheinteractionofcommunicationandknowledgeinaformalsettingisPlaza’spaper“LogicsofPublicCommunications”[13].Asthetitlesuggests,theepistemicactionsstudiedareannouncementstothewholegroup,asinourαandα′.Perhapsthemainresultofthepaperisacompletenesstheoremforthelogicofpublicannouncementsandknowledge.ThisresultiscloselyrelatedtoaspecialcaseofourTheorem3.5.ThedifferenceisthatPlazarestrictsattentiontothecasewhenalloftheaccessibilityrelationsareequivalencerelations.

8.Appendix:thelexicographicpathorder

29

Incidentally,Plaza’sproofinvolvesatranslationtomulti-modallogic,justasoursdoes.Inadditiontothis,[13]containsanumberofresultsspecialtothelogicofannouncementswhichwehavenotgeneralized,anditalsostudiesanextensionofthelogicwithnon-rigidconstants.

OtherpredecessorstothispaperarethepapersofGerbrandy[5,6]andGerbrandyandGroene-veld[7].Thesestudyepistemicactionssimilartoourβ,whereanannouncementismadetosetofagentsinaprivatewaywithnosuspicions.Theypresentedalogicalsystemwhichincludedthecommonknowledgeoperators.AnimportantresultisthatallofthereasoningintheoriginalMuddyChildrenscenariocanbecarriedoutintheirsystem.Thisshowsthatinordertogetaformaltreat-mentoftheproblem,oneneednotpositmodelswhichmaintainhistories.Theydidnotobtainthecompleteness/decidabilityresultfortheirsystem,butitwouldbetheversionofTheorem5.9restrictedtoactionswhicharecompositionsofprivateannouncements.SoitfollowsfromourworkthatallofthereasoningintheMuddyChildrencanbecarriedoutinadecidablesystem.

Weshouldmentionthatthesystemsstudiedin[5,6,7]differfromoursinthattheyarevariantsofdynamiclogicratherthanpropositionallogic.Thatis,announcementsareparticulartypesofprogramsasopposedtomodalities.Thisisanaturalmove,andalthoughwehavenotfolloweditinthispaper,wehavecarriedoutastudyofexpressivepowerissuesofvariousfragmentsofadynamiclogicwithannouncementoperators.Wehaveshown,forexample,thatthedynamiclogicformulationsaremoreexpressivethanthepurelypropositionalones.Detailsonthiswillappearinaforthcomingpaper.

Incidentally,thesemanticsin[5,6,7]usenon-wellfoundedsets.Inotherwords,theyworkwithmodelsmodulobisimulation.TheadvantagesofmovingfromthesetoarbitraryKripkemodelsarethatthelogiccanbeusedbythosewhodonotknowaboutnon-wellfoundedsets,andalsothatcompletenessresultsareslightlystrongerwithamoregeneralsemantics.Therelevantequivalenceofthetwosemanticsisthesubjectoftheshortnote[11].Thefollowingarethenewcontributionsofthispaper:

1.Weformulatedalogicalsystemwithmodalitiescorrespondingtointuitivegroup-levelepistemicactions.Theseactionsincludenaturalformalizationsofannouncementssuchasγandδ,whichallowvarioustypesofsuspicionbyoutsiders.Ourapparatusalsopermitsustostudyepistemicactionswhichapparentlyhavenotyetbeenconsideredinthislineofwork,suchasactionsinwhichnothingactuallyhappensbutoneagentsuspectsthatasecretcommunicationtookplace.2.Weformulatedalogicalsystemwiththesemodalitiesandwithcommonknowledgeoperatorsforallgroups.BuildingonthecompletenessofPDLandusingabitoftermrewritingtheory,weaxiomatizedthevaliditiesinoursystem.3.Weobtainedsomeresultsonexpressivepower:inthepresenceofcommonknowledgeopera-tors,itisnotpossibletotranslateawaypublicannouncements,andinourframework,privateannouncementsaddexpressivepowertopublicones.8.Appendix:thelexicographicpathorder

Inthisappendix,wegivethedetailsonthelexicographicpathordering(LPO),bothingeneralandinconnectionwithL([α])andL([α],2∗).

Fixsomemany-sortedsignatureΣofterms.InordertodefinetheLPO(LPO1)If(t1,...,tn)<(s1,...,sn)inthelexicographicorderingonn-tuples,andiftjfor1≤j≤n,thenf(t1,...,tn)(LPO3)Ifg30

Hereishowthisisappliedinthispaper.Weshalltaketwosorts:sentencesandactions.Oursignaturecontainstheusualsentence-formingoperatorsp(forp∈AtSen)¬,∧,and2AforallA∈A.Hereeachpis0-ary,¬and2Aareunary,and∧isbinary.Wealsohaveanoperatorapptakingactionsandsentencestosentences.Wethinkofapp(ψ,α)asmerelyavariationon[α]ψ.(Theorderofargumentstoappissignificant.)Wefurtherhaveabinaryoperator◦onactions.(Thisisadeparturefromthetreatmentofthispaper,sinceweused◦asametalinguisticabbreviationinsteadofasaformalsymbol.ItwillbeconvenienttomakethischangebecausethisleadstoasmoothertreatmentoftheCompositionAxiom.)Finally,foreachfiniteKripkeframeKoverL([α])andeach1≤i≤|K|,wehaveasymbolFiKtaking|K|sentencesandreturninganaction.Eachsentenceϕhasaformalversion

α.Thesearedefinedbytherecursionwhichisobviousexceptfortheclauses

ϕ,

α

=

FiK(

pre(kn))

Hereα=󰀤K,ki,pre󰀥withK={k1,...,kn}insomespecifiedorder.However,outsideoftheproof

ofProposition8.2weshallnotexplicitlymentiontheformalversionsatall,sincetheyarehardertoreadthanthestandardnotation.

Wemustalsofirstfixawellfoundedrelation2.f(x1,...,y,...xn)4.5.Consideratermrewritingsystemeveryruleofwhichoftheforml;rwithrHereisaproofofofthewellfoundednessproperty(4),takenfromonBuchholz[2].(Wegeneralizeditslightlyfromtheone-sortedtothemany-sortedsettingandfromtheassumptionthatLetWbethesetoftermstsuchthattheorder8.Appendix:thelexicographicpathorder

31

uiNowthatweknowthateachftakestuplesinWntoelementsofW,itfollowsbyinductionontermsthatalltermsbelongtoW.⊣FormoreontheLPO,itsgeneralizationsandextensions,seethesurveysDershowitz[3]andPlaisted[12].

Proposition8.2ConsidertheLPO∗

β,thenpre(β)<α.1.Ifα→

∗

2.Ifα→β,then[β]ψ<[α]2∗Cψ.

3.pre(α)→p<[α]p.4.pre(α)→¬[α]ψ<[α]¬ψ.

5.[α]ψ∧[α]χ<[α](ψ∧χ).

󰀆A

β}<[α]2Aψ.6.pre(α)→{2A[β]ψ:α→7.[α◦β]ϕ<[α][β]ψ.

Inparticular,forallrulesϕ;ψoftherewritingsystemR∗,ψ<ϕ.

ProofPart(1)holdsbecauseweregardαasatermα=Fiγn),forsomeframeKandi.K(

∗

Sowheneverα→β,eachpre(β)isapropersubtermofα.

α).Nowlexicograph-Hereistheargumentforpart(2):Weneedtoseethatapp(ψ,ically,(ψ,α).Soweonlyneedtoknowthatα).Letα=Fiγn).K(

γ1,...,Nowaccordingtoequation(2.1)inSection2.1,

γi∗

β32

References

1.AlexandruBaltag,Alogicofepistemicactions,ms.CWI,Amsterdam,1999.

2.WilfriedBuchholz,Proof-theoreticanalysisofterminationproofs,AnnalsofPureandApplied

Logic75(1995)57–65.3.NachumDershowitz,Orderingsforterm-rewritingsystems,TheoreticalComputerScience17

(1982)279–301.4.RonaldFagin,JosephY.Halpern,YoramMoses,andMosheY.Vardi,ReasoningAboutKnowl-edge,MITPress,1995.5.JelleGerbrandy,Dynamicepistemiclogic,inLawrenceS.Moss,etal(eds.)Logic,Language,

andInformation,vol.2,CSLIPublications,StanfordUniversity1999.6.JelleGerbrandy,BisimulationsonPlanetKripke,Ph.D.dissertation,UniversityofAmsterdam,

1999.7.JelleGerbrandyandWillemGroeneveld,Reasoningaboutinformationchange,JournalofLogic,

Language,andInformation6(1997)147–169.8.JosephY.HalpernandMosheY.Vardi,Thecomplexityofreasoningaboutknowledgeand

time.I.Lowerbounds.JournalofComputerandSystemSciences38(19),no.1,195–237.9.S.KaminandJ.J.Levy,Twogeneralizationsoftherecursivepathorderings,Unpublishednote,

DepartmentofComputerScience,UniversityofIllinois,UrbanaIL(1980).10.D.KozenandR.Parikh,AnelementaryproofofthecompletenessofPDL,TheoreticalComputer

Science(1981)113–118.11.LawrenceS.Moss,FromhypersetstoKripkemodelsinlogicsofannouncements,inJ.Gerbrandy

etal(eds.)JFAK.EssaysDedicatedtoJohanvanBenthemontheOccasionofhis50thBirthday,Vossiuspers,AmsterdamUniversityPress,1999.12.DavidA.Plaisted,Terminationorderings,inD.Gabbay(etal)eds.,HandbookofLogicin

ArtificialIntelligenceandLogicProgramming,vol.I,273–3.13.JanPlaza,Logicsofpubliccommunications,Proceedings,4thInternationalSymposiumonMethod-ologiesforIntelligentSystems,19.14.FrankVeltman,Defaultsinupdatesemantics,JournalofPhilosophicalLogic25(1996)221–261.