Dynamic consequence and public announcement

Dynamic consequence and public announcement Andr´es Cord´on Franco∗ , Hans van Ditmarsch† , Angel Nepomuceno‡ August 2, 2013 Abstract In [25] van Benthem proposes a dynamic consequence relation defined as ψ1, . . . , ψn|=dϕiff |=pa [ψ1]...[ψn]ϕ, where the latter denotes consequence in public announcement logic, a dynamic epistemic logic. In this paper we investigate the structural properties of a conditional dynamic consequence relation |=d Γextending van Benthem’s proposal. It takes into account a set of background conditions Γ, inspired by [18] wherein Makinson calls this reasoning ‘modulo’ a set Γ. In the presence of common knowledge, conditional dynamic consequence is definable from (unconditional) dynamic consequence. An open question is whether dynamic consequence is compact. We further investigate a dynamic consequence relation for soft instead of hard announcements. Surprisingly, it shares many properties with (hard) dynamic consequence. Dynamic consequence relations provide a novel perspective on reasoning about protocols in multi-agent systems. 1 Introduction and preliminaries In dynamic semantics or update semantics, dynamic consequence relations are an obligatory phenomenon and are well-studied [29, 23, 15, 17]. Sometime in the late 1980s, dynamic epistemic logic [28] parted ways with dynamic semantics and put all the dynamics in modal dynamic operators instead. These modal operators are interpreted employing a standard Kripke semantics. The consequence relation associated with this semantics has nothing dynamic. In [25], van Benthem proposes a way that goes back from dynamic epistemic logic to dynamic consequence. He defines a dynamic consequence relation as: ψ1, . . . , ψn|=dϕ ∗Department of Computer Science and Artificial Intelligence, Universidad de Sevilla, Av. Reina Mercedes s/n, 41012 Seville, Spain. Email: [email protected] †LORIA, CNRS – Universit´e de Lorraine, BP 239, 54506 Vandoeuvre-l`es-Nancy, France. Email: [email protected] ‡Department of Philosophy and Logic and Philosophy of Science, Universidad de Sevilla, Av. Camilo Jos´e Cela s/n, 41018 Seville, Spain. Email: [email protected] 1 iff |=pa [ψ1]...[ψn]ϕ, where the latter denotes consequence in public announcement logic, a dynamic epistemic logic. In public announcement logic, [ψ]ϕstands for ‘after (truthful public) announcement of ψ,ϕ(is true)’. Example 1 After public announcement of factual information p(‘It rains in Seville’), the agent knows that p(‘Fernando knows that it rains in Seville’). This is formalized as [p]Kp. Seen as consequence, we then have that p|=dKp. This new form of dynamic consequence is not trivial. For (another) example, observe that p∧ ¬Kp 6|=dp∧ ¬Kp: if I inform you that (pis true and you do not know that p), then you know pas a result. (‘Fernando calls Graham, who lives in Australia, and tells him: “You don’t know that it is raining in Seville!”.’ With the usual conversational implicature, this is an announcement of p∧¬Kp. Then, of course, Graham knows p, so p∧ ¬Kp is now false.) We propose a dynamic consequence relation |=d Γ, called conditional dynamic consequence, that extends van Benthem’s proposal. It is an extension of |=dbecause it also takes a third parameter into account in the consequence relation, namely a set of background conditions Γ. This is a set of formulas commonly known by the agents. The reason to propose such an extension is that the study of the consequences of sequences of announcements is often in the context of a given system satisfying a number of initial properties. Now there is nothing per se that prevents that such properties are made known to all agents by yet another sequence of dynamic phenomena—initializing the system, one might say, from some sort of perspective of common ignorance; but in fact such initial configurations are often a given. Also, in such initial configurations agents have different perspectives. Such different perspectives cannot have been the consequence of making public announcements in a state of commonly known ignorance, but need more complex dynamics, such as private announcements. A more elegant starting point therefore seems the assumption of that third parameter. This assumption also matches the general observation on multi-S5 systems that the structure of the model is commonly known to all agents, and that for many such systems (for example, those with finite models) this structure can be captured by a set of commonly known formulas. This is the background theory, the set of background conditions. We then investigate the structural properties of conditional dynamic consequence. Like van Benthem’s dynamic consequence, the structural rules permutation, contraction, reflexivity, cut and monotonicity fail. Van Benthem’s dynamic consequence satisfies cautious monotonicity, left cut, and left monotonicity (these structural rules will later be defined). Conditional dynamic consequence satisfies cautious monotonicity and left cut, but does not satisfy left monotonicity. We further investigate how the presence of common knowledge in the logical language influences the results, and give tentative results on what the consequences are of allowing infinite sets of premises, in relation to a suitable notion of compactness. We also present a version of the dynamic consequence relation for so-called soft public announcements, for which the results are (surprisingly) similar to those for (standard, or ‘hard’) public announcements. 2 1.1 Public announcement logic Dynamic epistemic logics [28] combine modal operators for knowledge or belief, typically for a set of agents, with dynamic modal operators for change of knowledge or belief. Public announcement logic [19, 8] is one such dynamic epistemic logic, namely where the dynamics consists of public truthful announcements (unlike, e.g., private announcements to subgroups). We present the version of the logic with common knowledge operators. The language of public announcement logic [19] is defined over a finite set of agents A and a countable set of primitive propositions (or propositional variables)P. Let a∈Aand p∈P: Lpa C3ϕ::= p| ¬ϕ|ϕ∧ϕ|Kaϕ|[ϕ]ϕ|Cϕ Other propositional connectives and the constants >(‘true’) and ⊥(‘false’) are defined by the usual abbreviations. For arbitrary formulas we write ϕ,ψ, ... Formula Kaϕstands for ‘agent aknows ϕ’, Cϕ for ‘the agents commonly know ϕ’ and [ϕ]ψfor ‘after public announcement of ϕ,ψ’. Sets of formulas are represented by Γ,Γ0, . . . or ∆, . . . and sequences of formulas by Σ, . . . (for Sequence). We use various sublanguages in our presentation. Without the inductive construct for common knowledge, we get the language Lpa, without public announcement as well we get the language of (multi-agent) epistemic logic Lel, and Lel Cis the language with common knowledge but without public announcement. The language Lpl of propositional logic, the booleans, does not have any modalities. The basis for our presentation of dynamic consequence will be Lel. The reason for this restriction is that we try to obtain our results for a minimal setting, and generalize the results from there. With common knowledge we get different results. AKripke structure or epistemic model over Aand Pis a tuple M= (S, {∼a}a∈A, V ) where Sis a (non-empty) set or domain of states, for each agent a∈A,∼a⊆S×Sis an epistemic accessibility or indistinguishability relation that is assumed to be an equivalence relation, and valuation V:P→ P(S) assigns primitive propositions to the set of states in which they are true. For ‘state sis in the domain of model M’ we write s∈M. A pointed Kripke structure is a pair (M, s) where s∈M(we often omit the two parentheses in constructs wherein (M, s) occurs). To interpret common knowledge we further need the reflexive transitive closure of the union of the accessibility relations of the agents, namely ∼A::= (Sa∈A)∗. This is also an equivalence relation. We write KaΓ for {Kaϕ|ϕ∈Γ} and similarly for CΓ. The interpretation of the crucial constructs in a pointed Kripke structure is defined as follows—in this definition, the symbol |=pa is more properly a forcing and not a logical consequence symbol, but the convention in epistemic logic is to allow this overload of notation, as the two coincide in the notion of validity. M, s |=pa piff p∈V(p) M, s |=pa ϕ∧ψiff M, s |=pa ϕand M, s |=pa ψ M, s |=pa ¬ϕiff M, s 6|=pa ϕ 3 M, s |=pa Kaϕiff for every tsuch that s∼at,M, t |=pa ϕ M, s |=pa Cϕ iff for every tsuch that s∼At,M, t |=pa ϕ M, s |=pa [ϕ]ψiff M, s |=pa ϕimplies that M|ϕ, s |=pa ψ where M|ϕ= (S0,{∼0 a}a∈A, V 0) such that S0={s0∈S:M, s0|=pa ϕ};∼0 a=∼a∩(S0×S0); V0(p) = V(p)∩S0. We write M, s |=pa Γ for (for all ϕ∈Γ, M, s |=pa ϕ). We further define that ‘ϕis valid on M’, notation M|=pa ϕ, as ‘for all s∈M, M, s |=pa ϕ’, and ‘ϕis valid’ (or pa-valid), notation |=pa ϕ, as ‘for all M(in the class of models for agents in Aand primitive propositions in P), ϕis valid on M’. Logical consequence |=pa is defined as: Γ |=pa ϕiff for all models Mand states s∈M, if M, s |=pa ψ for all ψ∈Γ, then M, s |=pa ϕ. We write ∆ |=pa Γ for: ∆ |=pa ψfor all ψ∈Γ. 1.2 Structural properties of consequence relations Assume a logical language L. A consequence relation is a binary relation |= between a sequence Σ of formulas in L, the premises, and a formula in L, the conclusion. An example is the just introduced |=pa; where the premises constitute a set, not a sequence. Consequence relations may satisfy certain structural rules, the standard rules are: •ϕ|=ϕreflexivity •Σ, ϕ, ϕ |=ψimplies Σ, ϕ |=ψcontraction •Σ, ϕ, ϕ0,Σ0|=ψimplies Σ, ϕ0, ϕ, Σ0|=ψpermutation •Σ|=ψand Σ0, ψ, Σ00 |=ϕimply Σ0,Σ,Σ00 |=ϕcut •Σ|=ψimplies Σ, ϕ |=ψmonotonicity For relational studies of logical consequence, see [22, 11]. For an overview of various logics satisfying fewer or different structural rules, see e.g. [20]. The modified structural rules considered by van Benthem in [25] for dynamic consequence are as follows. •Σ|=ψand Σ, ψ, Σ0|=ϕimply Σ,Σ0|=ϕleft cut •Σ|=ψimplies ϕ, Σ|=ψleft monotonicity •Σ|=ψand Σ,Σ0|=ϕimply Σ, ψ, Σ0|=ϕcautious monotonicity We are now sufficiently prepared to present van Benthem’s dynamic consequence relation and our conditional dynamic consequence relation. 4 2 Conditional dynamic consequence Using the standard Kripke semantics of public announcement logic one can define a dynamic consequence relation where the premises stand for consecutive announcements, and the conclusion stands for a postcondition of these announcements. Given a set of agents Aand a set of atoms P, let Σ = ψ1, . . . , ψnbe a (finite!) sequence of Lel formulas, and ϕ∈ Lel. We write [Σ]ϕfor [ψ1]. . . [ψn]ϕ(we note that [Σ]ϕ∈ Lpa), and we write M|Σ for (. . . (M|ψ1)|. . . )|ψn. Definition 2 (Dynamic consequence [25]) Σ|=dϕiff |=pa [Σ]ϕ. If Σ |=dϕwe say that ϕis a dynamic consequence of Σ, or Σ dynamically entails ϕ. In other words, Σ dynamically entails ϕiff for every model Mand state s∈M, it holds that M, s |=pa [ψ1]...[ψn]ϕ; where the latter means that on condition that ψ1is true in (M, s), and ψ2is true in (M|ψ1, s), and so on, then we have that M|Σ, s |=pa ϕ. We emphasize that, as this should be the case for every state sin Msatisfying the announcement sequence, ϕ is therefore not merely true in some state of M|Σ but a model validity on M|Σ.1 A main result in [25] is that |=dsatisfies the structural rules of left monotonicity, left cut, and cautious monotonicity, that were introduced in the previous section2; and that these three rules even represent that consequence relation, where ‘represent’ is interpreted in a technical sense lifting the discussion to abstract transition models, see [25, pp.193-194] for details. We now extend this consequence relation. Let Γ be a set of Lel formulas, called the set of background conditions of the consequence relation. (Γ may be infinite.)3 Definition 3 (Conditional dynamic consequence) Σ|=d Γϕiff for all M,M|=pa Γimplies M|=pa [Σ]ϕ. We say that Σ dynamically entails ϕconditional to background Γ. Obviously, |=dis the special case of |=d Γfor Γ = {>}. If Γ is a singleton set {ϕ}we write |=d ϕinstead of |=d {ϕ}.4 1Van Benthem does not really define dynamic consequence as Σ |=dϕiff |=pa [Σ]ϕ, but as Σ |=dϕiff |=pa [Σ]Cϕ. In the language Lpa Cof public announcement logic with common knowledge this amounts to the same. In that logic, |=pa [ψ]ϕis equivalent to |=pa [ψ]Cϕ, for all ϕand ψ. (If [ψ]ϕis valid, then in any given model, ϕis valid on its ψ-restriction. But in that case Cϕ is also valid on the ψ-restriction. Therefore [ψ]Cϕ is valid on that model. As the model was arbitrary, [ψ]Cϕ is valid. The other direction is even simpler.) And therefore we also have this for sequences of announcements. 2This does not depend on the presence of common knowledge in van Benthem’s setting. See Section 3. 3Our inspiration was the so-called pivotal-assumption consequence in [18]. Makinson proposes logical consequence modulo an assumption set K. This assumption set Kin [18] plays the role of our Γ. Otherwise, his setting is different. E.g., Makinson’s has classical structural properties, and the pivotal assumptions / background conditions Γ can be added to the premises, unlike in our proposal. 4In a prior version [10] of this work we distinguished conditional dynamic consequence (there called global dynamic consequence) from local dynamic consequence, defined as Σ|=ld Γϕiff Γ |=pa [Σ]ϕ. 5 Example 4 Consider a pack of cards dealt over different players, such that every player only knows his own card. An epistemic model encoding this uncertainty of the players about the card deal can be described by a set of formulas [27]. This set consists of the available facts, the available (positive) knowledge, and the available ignorance. The facts are, that one of all possible deals of cards is actually the case. Each player knows his own hand of cards. And each player considers all deals of cards possible wherein she holds her own cards (this entails that each player is ignorant of the ownership of all other cards than her own). For three players and three cards, with therefore nine propositions cafor ‘player aholds card c’, a valuation (‘the facts’) describes a card deal (like 0a∧1b∧2c∧¬1a∧¬2a∧. . . —four more negated variables), knowledge is encoded by propositions like 0a→Ka0a(if player a holds card 0, she knows that), and ignorance by propositions like ¬Ka2b(player adoes not know that player bholds card 2). Let this theory describing a card deal model be called T. Typical sequences of announcements that one wishes to check for their consequences in this setting, are protocols wherein the two players a, b can achieve knowledge of the card deal by means of public announcements without the third player cgetting to know the card deal. These protocols Σshould satisfy information requirements ϕ(containing components such as 2b→Ka2b, ‘if bholds card 2, aknows it’) and safety requirements ψ(containing components such as 2b→ ¬Kc2b, ‘.. . but cdoes not’). The question is then whether Σ|=d Tϕ∧ψ. Example 5 We have that p|=d p∧¬Kp ¬p, whereas p∧¬Kp, p 6|=d¬p. The first holds because p∧ ¬Kp cannot be a model validity (in S5). Example 5 shows that background conditions cannot, instead, be simply announced first. Section 2.4 will discuss when they can and when they cannot. 2.1 The failure of classical structural rules The so-called classical structural rules reflexivity, contraction, permutation, monotonicity, and cut all fail for conditional dynamic consequence. In [25] it is shown that they fail for Although on first sight the more obvious definition, it does not to capture the intuition that the formulas in Γ are background conditions. For example, we then have that ¬K¬p|=ld pp. It is true that ‘on condition that pis true, after announcement of ¬K¬p,pis then always true’, because propositional variables do not change their value in public announcement logic. But we cannot then say that ‘pis background knowledge for the agent’. If that were so, we would expect pto be known by the agent, no matter what the subsequent announcement is. But of course, ¬K¬p6|=ld pKp. (The example does not need a premise: we also have that |=ld ppbut 6|=ld pKp.) That we cannot strengthen the consequent seems a strong argument against this local dynamic consequence. Local dynamic consequence satisfies even fewer structural rules than conditional dynamic consequence. 6 the dynamic consequence relation |=dwithout background, which is the borderline case for Γ = {>} of |=d Γ. It is instructive to show counterexamples. •Reflexivity fails. As known, the formula [p∧ ¬Kap]¬(p∧ ¬Kap) is valid, so p∧ ¬Kap6|=dp∧ ¬Kap •Contraction fails. We again make use of the Moore-sentence p∧ ¬Kapto show that. –p∧ ¬Kap, p ∧ ¬Kap|=d⊥, because p∧ ¬Kapcannot be truthfully announced more than once. –p∧ ¬Kap6|=d⊥. •Permutation fails. –p, ¬Kap|=d⊥, because after announcing p, this is known, so ¬Kapcannot be truthfully announced after that. –¬Kap, p 6|=d⊥, because after announcing your ignorance of a fact, this fact remains unknown; so it can then be very well announced truthfully. •Monotonicity fails. A counterexample is as follows. ¬Kap|=d¬Kap, however, ¬Kap, p 6|=d¬Kap, since 6|=pa [¬Kap][p]¬Kap. •Cut fails. Take (see the definition of cut) Σ = ¬p,ψ=Ka¬p, Σ0=¬Ka¬p, Σ00 =∅, and ϕ=⊥. Then it holds that –¬p|=dKa¬p, and –¬Ka¬p, Ka¬p|=d⊥; but –¬Ka¬p, ¬p6|=d⊥. 7 2.2 Structural rules for conditional dynamic consequence In view of the failure of classical structural rules, it is natural to ask ourselves if conditional dynamic consequence satisfies any variant of these rules. The prime candidates are the modified structural rules ‘left monotonicity’, ‘left cut’, and ‘cautious monotonicity’, that are satisfied by unconditional dynamic consequence. The first one is not satisfied but the other two are. We prove the results for conditional but also for unconditional dynamic consequence, as [25] does not give proofs. This we will address first. But we can also consider rules for changing the background conditions Γ of our consequence relation |=d Γ, or consider special background conditions. That will be addressed subsequently. We need a simple lemma, used in the theorem that follows it. Lemma 6 If M|=pa [Σ]ϕ, then for all χ,M|=pa [Σ][ϕ]χ↔[Σ]χ. Proof The assumption M|=pa [Σ]ϕentails that ϕis a model validity on M|Σ. Therefore, announcing it in model M|Σ has no informative effect: it is the trivial model restriction.  Theorem 7 Conditional dynamic consequence satisfies cautious monotonicity and left cut but not left monotonicity. Proof •Cautious monotonicity In order to show that Σ, ϕ, Σ0|=d Γψwe assume that Σ |=d Γϕand that Σ,Σ0|=d Γψ. Let model Mbe such that M|= Γ. From M|= Γ and assumption Σ |=d Γϕfollows M|=pa [Σ]ϕ. From M|= Γ and assumption Σ,Σ0|=d Γψfollows M|=pa [Σ][Σ0]ψ. From M|=pa [Σ]ϕ,M|=pa [Σ][Σ0]ψand Lemma 6, by taking χ= [Σ0]ψ, follows M|=pa [Σ][ϕ][Σ0]ψ. •Left cut It suffices to observe that on assumption of M|=pa [Σ]ϕ, from M|=pa [Σ][ϕ][Σ0]ψ also follows M|=pa [Σ][Σ0]ψ(Lemma 6 is an equivalence). •(Failure of) Left monotonicity Consider Γ = {¬Kap}, Σ = >,ψ=pand ϕ=¬Kap. Then, we have that > |=d ¬Kap¬Kap, however p, > 6|=d ¬Kap¬Kap.  Theorem 8 ([25]) Dynamic consequence satisfies cautious monotonicity, left cut and left monotonicity. Proof The proof for cautious monotonicity and left cut is the case Γ = {>} of Theorem 7. We prove left monotonicity: Σ |=dψimplies ϕ, Σ|=dψ. But this is obvious, as it is an instantiation of necessitation for the announcement operator. The principle of necessitation is: |=pa σimplies |=pa [ϕ]σ. Therefore, |=pa [Σ]ψimplies |=pa [ϕ][Σ]ψ. 8 2.3 Structural rules for the background conditions So far we have studied structural rules involving Σ and ϕ, where Γ is held as a fixed parameter. But we can also consider structural rules where the background conditions are a variable. A formula ϕis preserved if, whenever M, s |=pa ϕ, then for all M0⊆Msuch that M0 contains s, we have that M0, s |=pa ϕ. Proposition 9 Assume that Γ|=pa ϕ. Then: 1. Σ|=d Γϕmay not hold; 2. Σ|=d Γϕwhenever the formulas in Γare preserved; 3. Σ|=d Γϕwhenever the formulas in Γare boolean. Proof 1. Let Γ = {¬Kap}, and Σ = p. Assuming that M|=pa ¬Kap, then as long as there is ap-state in M, we have M6|=pa [p]¬Kap. Therefore p6|=d ¬Kap¬Kap. 2. If formulas are preserved under submodels, then the successive announcements of Σ preserve the truth of all formulas in Γ: Σ |=d ΓΓ. From that and Γ |=pa ϕwe get Σ|=d Γϕ. 3. If formulas of Γ are boolean, then they do not change their truth value by successive updates. In other words, they are preserved. So again, any of their |=pa-consequences remains the case.  Proposition 10 Let Γ,∆⊆ Lel. •Let ∆|=pa Γ. Then Σ|=d Γϕimplies Σ|=d ∆ϕ. •Let Γ⊆∆. Then Σ|=d Γϕimplies Σ|=d ∆ϕ. background monotonicity Proof We prove the first. Suppose Σ |=d Γϕ. Let a model Mbe such that M|=pa ∆. From that and ∆ |=pa Γ follows M|=pa Γ, so M|=pa [Σ]ϕ. Therefore Σ |=d ∆ϕ. The second item is a special case of the first item.  One can also consider structural rules that involve variation in the premises and the background conditions simultaneously. Proposition 11 The following structural rules hold for conditional dynamic consequence. •Let Γ|=pa ψ. Then ψ, Σ|=d Γϕimplies Σ|=d Γϕ. cautious contraction • |=d Σϕiff Σ|=d Σϕ. 9 single event only. Intriguing results on this are presented by Sadzik in [21].7Here again, the observation that for some given model Mof information there is an infinite informative sequence ψ1, ψ2, . . . of announcements, as Sadzik does, is one thing. Whereas the question whether, given a formula ϕ, there is an infinite informative sequence ψ1, ψ2, . . . of announcements such that for some model Mthe formula ϕnever becomes a validity, is another thing: it is a weaker statement.8 Before we proceed, let us contrast our problem with the known compactness results for these logics. For the consequence relation |=pa the results are that the logic of public announcements with common knowledge is not compact, and that the logic of public announcements without common knowledge is compact [8]. These results expand the results that epistemic logic without common knowledge is compact and epistemic logic with common knowledge is not compact (summarized in [12]). This is the standard setbased notion of compactness: If Γ |=pa ψthen there is a finite subset ∆ ⊆Γ such that ∆|=pa ψ. A typical example is the set {p, Kap, Kbp, KaKbp, ..., ¬Cp}(any finite stack of two alternating modalities). This set is unsatisfiable but any finite subset is satisfiable. To use the compactness result for epistemic logic, we need to define a relevant unsatisfiable infinite set. Now consider this. Suppose in order to derive a contradiction that dynamic consequence is not compact. Assume that Σ |=dϕbut that Σn6|=dϕfor all n. In other words, for all n∈N, we have that 6|=pa [Σn]ϕ, and therefore: For all n∈N,hΣni¬ϕis satisfiable. (i) Somehow, we would like to arrive from here at The set {hΣni¬ϕ|n∈N}is satisfiable. (ii) But (i) does not imply (ii). Statement (i) says that for all n∈Nwe can find a model Mnand a state sn∈Mnsuch that: Mn, sn|=pa hΣni¬ψ. Whereas (ii) says that there is a (single) model Mand a state s∈Msuch that for all n∈N:M, s |=pa hΣni¬ψ. This pointed model (M, s) does it for the whole set. And even it we get there, and we have an (M, s) satisfying (ii), we cannot know if ψis true or false there: ψmight easily be false after every announced Σnbut still true after Σ.9 We only were able to get (ii) from (i) for conclusions of dynamic consequence of a specific form, not for any formula. We now list these relevant results and the conjecture. Proposition 23 If ϕ∈ Lel with ¬ϕpreserved, then Σ|=dϕimplies that there is n∈N such that the following formula is pa–valid: [Σ1]ϕ∨[Σ2]ϕ∨. . . ∨[Σn]ϕ 7Probably the most publishable but not formally published result in dynamic epistemic logic. 8In [21, Section 4] it is proved that for a given formula ϕ, events with boolean preconditions, when infinitely repeated, have at some stage no longer informative consequences. The examples given involve non-public events (events that are not public announcements). This result suggests that, in principle, we have a compactness result of the form: If ψ, ψ, . . . |=dϕand ψis boolean, then there is an nsuch that ψ,ψ,...,ψ |=dϕ(where ψis announced ntimes). But if ψis boolean, then for any M,M|ψ|=ψ, so we would have already had ψ|=dϕstraightaway. 9See footnote 6. 16 Proof Towards a contradiction, assume that for each n∈Nthe formula [Σ1]ϕ∨[Σ2]ϕ∨. . . ∨[Σn]ϕ is not pa–valid. Then, for each n∈Nthe formula ¬([Σ1]ϕ∨[Σ2]ϕ∨. . . ∨[Σn]ϕ) is pa–satisfiable. That is, for each n∈Nthe formula (?)hΣ1i¬ϕ∧ hΣ2i¬ϕ∧. . . ∧ hΣni¬ϕ is pa–satisfiable. Now consider the set S={hΣni¬ϕ|n∈N}. Let S0⊂Sbe any finite subset. The set S0will have a maximal element hΣmi¬ϕ. By (?) let Mand s∈Mbe such that M, s |=pa hΣ1i¬ϕ∧ hΣ2i¬ϕ∧. . . ∧ hΣmi¬ϕ. Therefore M, s satisfies the entire set S00 ={hΣni¬ϕ|n≤m}. As S0⊆S00,S0is also satisfiable (by (M, s)). So, any finite subset of Sis satisfiable. From the compactness of public announcement logic without common knowledge it follows that Sis satisfiable as well. Thus, there exist Nand t∈Nsatisfying that for all n∈N: 1. N, t |=pa hΣni>, and 2. N, t |=pa hΣni¬ϕ. From the first item follows that t∈N|Σ. From the second item follows that N|Σ, t |=pa ¬ϕ. For that, observe that N|Σ1, t |=pa ¬ϕand ¬ϕis preserved. But this contradicts Σ |=dϕ.  Proposition 23 gives us almost but not quite what we want. Although we can get a nsuch that |=pa [Σ1]ϕ∨[Σ2]ϕ∨. . .∨[Σn]ϕ, for compactness (given the restrictions on ϕ) we would have liked Σn|=dϕ, i.e., |=pa [Σn]ϕ. We cannot get that from the former disjunction, unless even more restrictions are satisfied: Corollary 24 If ϕis boolean, then Σ|=dϕimplies that there is an nsuch that Σn|=dϕ. Proof The result follows from Proposition 23 together with the following facts. 1. All booleans and their negations are positive formulas (see Section 2.4), and therefore preserved. 2. If ϕis preserved, the following formula is pa–valid ([Σ1]ϕ∨[Σ2]ϕ∨. . . ∨[Σn]ϕ)→[Σn]ϕ To see this, let Mand s∈Mbe such that M, s |=pa [Σ1]ϕ∨[Σ2]ϕ∨. . . ∨[Σn]ϕ. Then there is i≤nsuch that M, s |=pa [Σi]ϕ. Now as ϕis preserved, we also have that M, s |=pa [Σn]ϕ.  Conjecture 25 Dynamic consequence is compact. 17 5 Dynamic consequence for soft public announcements An alternative to the ‘hard’ public announcements that we have been dealing with so far are the so-called ‘soft’ public announcements. In a soft public announcement of ϕ, the agents are willing to incorporate ϕ, but only tentatively so. When they are later informed of something that would be in contradiction with (the informative consequences of) ϕ, their beliefs will not become inconsistent, but they will change again in some consistency preserving way. A typical example is to compare the hard public announcement with the soft public announcement of a primitive proposition p. Just a hard public announcement of pwill make the agent (or agents) know p, a soft public announcement of pwill make the agent believe p. After a hard public announcement of pthe agent cannot incorporate hard public announcement of ¬p: that is in contradiction with his (infallible) knowledge of p. But after a soft public announcement of pthe agent can very well incorporate soft public announcement of ¬p. After that, he will no longer believe p, but believe ¬p. Hard public announcement is a form of belief expansion, and soft public announcement is a form of belief revision. The dynamic epistemic logic way to implement belief revision as soft public announcement is presented in [24]. For this we need to enrich the epistemic models with plausibility relations that tell us, given two states that an agent considers possible, which of these is more plausible than the other. An agent believes a proposition ϕiff ϕis true in the most plausible states. A way to implement this (following van Benthem’s presentation) is to have, apart from an equivalence relation ∼afor every agent a, also a plausibility relation <afor every agent a(that is a well-preorder, i.e., a well-founded, reflexive, and transitive relation), such that we can define ≺a::= <a∩ ∼a(≤ais the reflexive closure of <a, and ais the reflexive closure of ≺a). This then defines the plausibility order per equivalence class. The well-preorder requirement is to ensure that there are most plausible states in every class (most plausible is <a-minimal), so that belief is always consistent. Such models (S, ∼, <, V ) are often called plausibility epistemic models. The simplest language to be considered under this setting is Lbpa 3ϕ::= p| ¬ϕ|ϕ∧ϕ|Baϕ|[[ϕ]]ϕ where Baϕstands for ‘agent abelieves ϕ’and [[ϕ]]ψstands for ‘after soft public announcement of ϕagent abelieves that ψ’. The language without soft public announcement operators is Lbl (the language of doxastic logic). There are various extensions of the language Lbpa: with knowledge, with conditional belief—essential for a complete axiomatization—, with group epistemic operators or group epistemic operators, ... We need not consider these extensions here. The semantics of the two novel modalities is now defined as follows. M, s |=bpa Baϕiff for every tsuch that s∼atand t≤aufor all u∼as,M, t |=bpa ϕ M, s |=bpa [[ϕ]]ψiff Mϕ, s |=bpa ψ 18 where Mϕis as Mexcept that the plausibility relation <0is defined as t <0 at0iff t <at0,and M, t |=bpa ϕand M, t0|=bpa ϕ, or M, t |=bpa ϕand M, t06|=bpa ϕ, or t <at0,and M, t 6|=bpa ϕand M, t06|=bpa ϕ. The idea behind this operation is that after soft public announcement of ϕ, all ϕ-states are considered more plausible than all ¬ϕ-states, and that the existing plausibility relation among the ϕ-states and also among the ¬ϕ-states is otherwise preserved. Example 26 Consider a controller room with a light and a fan, the state of the light is represented by a proposition p(light on/off) and the state of the fan by a proposition q. A model representing the uncertainty of the controller contains all four valuations pq,p¬q, ¬pq and ¬p¬q. The controller’s beliefs are as follows: pq <a¬pq <ap¬q=a¬p¬q; in other words: he considers it most plausible that the light and fan are both functional, slightly less so that at least the fan is working (but the light off), and even less so that the fan is not working (where he is indifferent about the state of the light). The controller believes that the light and fan are both functional: Bap∧Baq. To ascertain the state of affairs, he can make a tentative observation namely that the light is off. It is tentative, because it is a bit hard to see, as there is daylight outside the controller room. As a result of that, all ¬pstates now become more plausible than all pstates, but the order within the ¬pstates and the order within the pstates is preserved. Therefore, the new plausibility relation is: ¬pq <a¬p¬q <apq <ap¬q. The controller now believes that the light is off but the fan still on: Ba¬p∧Baq. Before the soft public announcement (i.e., tentative observation) of ¬p, he believed that p, but now, afterwards, he believes that ¬p. So, referring to the initial state of affairs, we have that Bap∧[[¬p]]Ba¬pis true there. In [25], van Benthem also proposes dynamic consequence for soft public announcement, namely as Σ |=ϕiff |=bpa [[Σ]]Bϕ (after soft public announcement of Σ, ϕis always believed) and as Σ |=ϕiff |=bpa [Σ]Bϕ (after hard public announcement of Σ, ϕis always believed); where in the second case we further need to extend the language Lbpa with a clause for hard public announcement and a corresponding clause in the semantics. A peculiarity of the former is that even for atomic propositions belief does not persist, as we now have p|=p but p, ¬p6|=p. This made him predict (but not investigate) different structural properties of such dynamic consequence relations. We followed a different route than van Benthem. Although |=pa ϕis equivalent to |=pa Kϕ, clearly |=bpa ϕis not equivalent to |=bpa Bϕ. If one instead requires model validity of ϕ, not Bϕ, the obvious definition is as follows. We give this straightaway in unconditional and conditional version, and for multiple agents. 19 Definition 27 (Soft dynamic consequence) Let ϕ∈ Lbl and Σ⊆ Lbl. Σ|=bd ϕiff |=bpa [[Σ]]ϕ soft (unconditional) dynamic consequence Σ|=bd Γϕiff for all M:M|=bpa Γimplies M|=bpa [[Σ]]ϕ soft conditional dynamic consequence The conditional version is now of more interest than before, as the conditions are knowledge conditions (commonly known background conditions) whereas the premises of the dynamic consequence relation are soft public announcements. Soft public announcements affect beliefs but not (factual) knowledge. Surprisingly, for soft dynamic consequence we obtain the same results as for (hard) dynamic consequence. In the first place, the classical substructural rules also fail for soft dynamic consequence. This may be not too surprising. But we considered it surprising that they fail on the same counterexamples as for hard dynamic consequence—we merely need to replace knowledge by belief. •Reflexivity fails: [[p∧ ¬Bap]]¬(p∧ ¬Bap) is valid, so p∧ ¬Bap6|=bd p∧ ¬Bap. •Contraction fails: p∧ ¬Bap, p ∧ ¬Bap|=bd ⊥, but p∧ ¬Bap6|=bd ⊥. •Permutation fails: p, ¬Bap|=bd ⊥, but ¬Bap, p 6|=bd ⊥. •Monotonicity fails: ¬Bap|=bd ¬Bap, however,¬Bap, p 6|=bd ¬Bap. •Cut fails. We now have that ¬p|=bd Ba¬p, and that ¬Ba¬p, Ba¬p|=bd ⊥; but ¬Ba¬p, ¬p6|=bd ⊥. Secondly, and more surprisingly so, soft dynamic consequence satisfies (at least) the same structural properties as hard dynamic consequence and conditional soft dynamic consequence satisfies (at least) the same structural properties as conditional (hard) dynamic consequence. As before (see Lemma 6), a helpful lemma is: Lemma 28 If M|=bpa [[Σ]]ϕ, then for all χ,M|=bpa [[Σ]][[ϕ]]χ↔[[Σ]]χ. Proof This is now true because soft public announcement of a model validity (also) has no informative consequence. Of the three cases of the computation of the new plausibility relation, only the first applies: on the part of the model that satisfies the soft public announcement formula, the plausibility relation remains the same. That is, for a formula that already is a model validity: it remains the same on the entire model.  Theorem 29 Soft dynamic consequence satisfies cautious monotonicity, left cut and left monotonicity. 20 Proof The structural rules cautious monotonicity and left monotonicity are the special case of Γ = {>} of the proof for conditional soft dynamic consequence, next. We prove left monotonicity: Σ |=bd ψimplies ϕ, Σ|=bd ψ. Just as in the proof of Theorem 8, this is an instantiation of necessitation, which also holds for the soft public announcement operator. (Necessitation is: |=bpa σimplies |=bpa [[ϕ]]σ. Then, take σ= [[Σ]]ψ.)  Theorem 30 Conditional soft dynamic consequence satisfies cautious monotonicity and left cut but not left monotonicity. Proof •Cautious monotonicity Assume that Σ |=bd Γϕ(i), that Σ,Σ0|=bd Γψ(ii), and that, for some model M, M|=bpa Γ. From the last and assumption (i) follows M|=bpa [[Σ]]ϕ. From M|=bpa Γ and assumption (ii) follows M|=bpa [[Σ]][[Σ0]]ψ. From M|=bpa [[Σ]]ϕ,M|=bpa [[Σ]][[Σ0]]ψ and Lemma 28, by taking χ= [[Σ0]]ψ, follows M|=bpa [[Σ]][[ϕ]][[Σ0]]ψ. •Left cut Assume M|=bpa [[Σ]]ϕ. From M|=bpa [[Σ]][[ϕ]][[Σ0]]ψalso follows M|= [[Σ]][[Σ0]]ψ, as Lemma 28 is an equivalence. •(Failure of) Left monotonicity The same counterexample as in Theorem 7 holds (replacing Kby B). Consider Γ = {¬Bap}, Σ = >,ψ=pand ϕ=¬Bap. Then, we have that > |=bd ¬Bap¬Bap, however p, > 6|=bd ¬Bap¬Bap.  We did not investigate if these three rules represent this (unconditional) soft dynamic consequence relation in the technical sense of lifting the discussion to abstract transition models, just as in [25] for (hard) dynamic consequence. We can merely observe that we did not find structural rules, except those explicitly formulated in terms of Kor Boperators, that are satisfied by hard dynamic consequence but not by soft dynamic consequence. (And we can observe that the proofs of the following theorems are all similar: Theorem 7 and 8, Theorem 18, and Theorem 29 and 30.) In the setting of soft dynamic consequence there is little point in investigating background conditions as announcements. These are now very different phenomena. Background conditions are hard constraints, corresponding, if one wishes, to hard public announcements. Whereas soft dynamic consequence is relative to soft public announcements, a clearly different form of belief revision. We see this as an advantage. In conditional soft dynamic consequence the hard information part is in the background conditions, whereas the soft information part is in the premises. As in many information processing scenarios we have a clear distinction between hard and soft information. Conditional soft dynamic consequence can therefore be seen as an implementation of that role distinction. 21 6 Conclusions, related work, and future work Given formulas in multi-agent epistemic logic, we investigated the structural properties of a conditional dynamic consequence relation Σ |=d Γϕ, that stands for ‘on all models that satisfy the set of background conditions Γ, after announcing the sequence Σ, the formula ϕalways holds’. This consequence relation does not satisfy the so-called classical structural rules reflexivity, contraction, permutation, monotonicity, and cut; it satisfies cautious monotonicity and left cut. In the presence of common knowledge, conditional dynamic consequence is definable from (unconditional) dynamic consequence. We leave for further research whether dynamic consequence is compact, although we prove a ‘disjunctive’ form of compactness for the formulas such that their negation is preserved under submodel restrictions. Our results for (hard) conditional dynamic consequence also hold for soft dynamic consequence. As soft announcement corresponds to radical upgrade in the belief revision community, further research might reveal how conditional dynamic consequence behaves on other update policies, such as conservative upgrade. Our hope is that dynamic consequence relations provide a novel and productive perspective on reasoning about protocols in multi-agent systems. A tableau calculus for dynamic consequence seems an interesting challenge, where, possibly, the reported calculi for public announcement logic such as [7] may provide inspiration. Recalling the dynamic consequence pattern Σ |=d Γϕ, we focussed on Σ |=d Γ? : what could be obtained given conditions Γ and a sequence of announcements Σ. But one could equally think of this as ? |=d Γϕ: given background conditions and a desirable goal, which sequence of announcements will always realize that goal? We can either see this as a problem of abduction, as in [1], in a philosophical logical setting. But one can equally well see this as a classical AI planning problem, but in a dynamic epistemic logic, as in [9, 4]. In works such as [3, 4] Aucher and collaborators investigate a consequence relation γ, ψd|=ϕwhere γis a formula in a logical language (e.g. Lel) that is true in a pointed Kripke structure, ψdis a formula in another type of logical language, for actions (the upper index dis ours, not Aucher’s; it is to emphasize its dynamic role), and ϕis a formula true in the Kripke structure resulting from executing an action satisfying ψdin the Kripke model satisfying γ. For actions that are public announcements we can almost, but not quite, think of ψdas the announced formula. This two-typed consequence relation (γ, ϕ of ‘static’ type, and ψdof ‘dynamic’ type) has therefore aspects of dynamic consequence. In the cited works sequent calculi are proposed for this consequence relation. In [6] the approach is generalized to a consequence relation of form γ1, ψd 1, . . . , γn, ψd n|=ϕ, i.e., where pairs of static/dynamic premises γi, ψd iformalize the successive execution of a sequence of actions satisfying action formulas ψd i, each preceded by a static requirement γi. In the forthcoming [5] van Benthem’s dynamic consequence ψ1, . . . , ψn|=dϕis then embedded in this framework, as some such γ1, ψd 1, . . . , γn, ψd n|=ϕ. It does not simply replace the announced ψiby action formulas ψd i, for example the embedding also employs common knowledge operators (infinitary modalities), but the relation is close enough to use suggestive corresponding notation. In future research we wish interpret our results in Aucher’s 22 framework. Acknowledgements In an early stage where ideas for dynamic consequence floated around, Hans van Ditmarsch acknowledges various discussions with Ramanujam at NIAS Wassenaar in 2007 and with Ramanujam and S.P. Suresh at IMSc in Chennai from 2008 onward. We thank Johan van Benthem for his input. We further thank various participants of the ever evolving LPIS seminar in Seville, from 2009 onward: Laura Leonides, Cristina Bar´es, David Fern´andez, Emililio Gom´ez-Caminero, Ignacio Hern´andez, Joost Joosten, and Fernando Soler. A previous version of this work appeared in workshop proceedings [10]. Subsequently, we thank Guillaume Aucher, Barteld Kooi, Olivier Roy, and Sonja Smets for further input, at M4M Osuna, in Munich, and in Groningen. Hans van Ditmarsch is also affiliated to IMSc (Institute of Mathematical Sciences), Chennai, as research associate. This work was mainly carried out while Hans van Ditmarsch worked in Seville, supported by project P08-HUM- 04159. We acknowledge support from European Research Council grant EPS 313360. We thank the reviewers of the Review of Symbolic Logic for their comments. References [1] A. Aliseda. Abductive Reasoning. Logical Investigations into Discovery and Explanation. Synthese Library, volume 220. Springer, 2006. [2] H. Andr´eka, I. N´emeti, and J. van Benthem. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27(3):217–274, 1998. [3] G. Aucher. DEL-sequents for progression. Journal of Applied Non-Classical Logics, 21(3-4):289–321, 2011. [4] G. Aucher. DEL-sequents for regression and epistemic planning. Journal of Applied Non-Classical Logics, 22(4):337–367, 2012. [5] G. Aucher. Dynamic epistemic logic as a substructural logic. Manuscript to appear in a forthcoming book volume honouring Johan van Benthem, 2013. [6] G. Aucher, B. Maubert, and F. Schwarzentruber. Generalized DEL-sequents. In Proc. of 13th JELIA, LNCS 7519, pages 54–66, 2012. [7] P. Balbiani, H. van Ditmarsch, A. Herzig, and T. de Lima. Tableaux for public announcement logics. Journal of Logic and Computation, 20(1):55–76, 2010. [8] A. Baltag, L.S. Moss, and S. Solecki. The logic of public announcements, common knowledge, and private suspicions. In Proc. of 7th TARK, pages 43–56, 1998. 23 [9] T. Bolander and M.B. Andersen. Epistemic planning for single and multi-agent systems. Journal of Applied Non-classical Logics, 21(1):9–34, 2011. [10] A. Cord´on-Franco, H. van Ditmarsch, D. Fern´andez-Duque, E. Gomez-Caminero, and A. Nepomuceno-Fern´andez. Two mischievous dynamic consequence relations. In Proceedings of the 2nd ILCLI, pages 197–208. University of the Basque Country Press, 2010. [11] J. Etchemendy. The Concept of Logical Consequence. Harvard University Press, 1990. [12] R. Fagin, J.Y. Halpern, Y. Moses, and M.Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge MA, 1995. [13] F.B. Fitch. A logical analysis of some value concepts. The Journal of Symbolic Logic, 28(2):135–142, 1963. [14] J.D. Gerbrandy. Bisimulations on Planet Kripke. PhD thesis, University of Amsterdam, 1999. ILLC Dissertation Series DS-1999-01. [15] W. Groeneveld. Logical investigations into dynamic semantics. PhD thesis, University of Amsterdam, 1995. ILLC Dissertation Series DS-1995-18. [16] W. Holliday and T. Icard. Moorean phenomena in epistemic logic. In L. Beklemishev, V. Goranko, and V. Shehtman, editors, Advances in Modal Logic 8, pages 178–199. College Publications, 2010. [17] M. Kracht. Dynamic semantics. In F. Hamm and T.E. Zimmermann, editors, Semantics, pages 217–241, Hamburg, 2002. Buske Verlag. [18] D. Makinson. Bridges between classical and nonmonotonic logic. Logic Journal of the IGPL, 11:69–96, 2003. [19] J.A. Plaza. Logics of public communications. In Proc. of the 4th ISMIS, pages 201–216. Oak Ridge National Laboratory, 1989. [20] G. Restall. An Introduction to Substructural Logics. Routledge, 2000. [21] T. Sadzik. Exploring the iterated update universe. ILLC, Amsterdam. Technical report PP-2006-18, 2006. [22] A. Tarski. On the concept of logical consequence. Oxford University Press, 1936. Reprinted in A. Tarski, Logic, Semantics, Metamathematics, 2nd ed. [23] J. van Benthem. Exploring logical dynamics. CSLI Publications, 1996. [24] J. van Benthem. Dynamic logic of belief revision. Journal of Applied Non-Classical Logics, 17(2):129–155, 2007. 24 [25] J. van Benthem. Logical dynamics meets logical pluralism? Australasian Journal of Logic, 6:182–209, 2008. [26] H. van Ditmarsch and B. Kooi. The secret of my success. Synthese, 151:201–232, 2006. [27] H. van Ditmarsch, W. van der Hoek, and B. Kooi. Descriptions of game states. In G. Mints and R. Muskens, editors, Logic, Games, and Constructive Sets, pages 43–58, Stanford, 2003. CSLI Publications. CSLI Lecture Notes No. 161. [28] H. van Ditmarsch, W. van der Hoek, and B. Kooi. Dynamic Epistemic Logic, volume 337 of Synthese Library. Springer, 2007. [29] F. Veltman. Defaults in update semantics. Journal of Philosophical Logic, 25:221–261, 1996. 25