Some Truths Are Best Left Unsaid
Philippe Balbiani 1
University of Toulouse and CNRS

Hans van Ditmarsch 2
University of Sevilla

Andreas Herzig 3
University of Toulouse and CNRS

Tiago de Lima 4
University of Artois

Abstract
We study the formal properties of extensions of the basic public announcement logic
by standard modal axioms such as D, T, 2, 4, and 5. We show that some of themfail to be conservative extensions of the underlying modal logic. This leads us topropose new truth conditions for announcements that better suit these extensions.
The corresponding reduction axioms postulate the suitability of the updated modelto the underlying logic. We show that if the fact can be expressed that the frame ofan updated model is in the class of frames of the underlying modal logic, then the
public announcement extension is axiomatisable. This is the case for, for example,
K, KT, S4, and S4.3. We also show that such a formula does not exist for several
logics whose frame condition involves existential quantification. This is the case for,for example, S4.2.
Keywords: public announcement logic, dynamic epistemic logic, reduction axioms.

1 Address:
Institut de recherche en informatique de Toulouse, CNRS — Universitéde Toulouse, 118 route de Narbonne, 31062 Toulouse Cedex 9, FRANCE;
Philippe.Balbiani@irit.fr.
2 Address: Department of Logic, University of Sevilla, Calle Camilo José Cela s/n, 41018
Sevilla, SPAIN; hvd@us.es.
3 Address:
Institut de recherche en informatique de Toulouse, CNRS — Universitéde Toulouse, 118 route de Narbonne, 31062 Toulouse Cedex 9, FRANCE;
Andreas.Herzig@irit.fr.
4 Address: CRIL, Université d’Artois, Rue Jean Souvraz, SP 18, 62307 Lens Cedex,
FRANCE; delima@cril.fr.

Balbiani, van Ditmarsch, Herzig and de Lima

1

37

Introduction

In public announcement logics, one can write formulas like hϕ!iψ standing for“the announcement of ϕ can be made and, after that, ψ holds”. Such logics
have been extensively studied over the last years, starting with Plaza’s paper[13] (reprinted in [14]); see [16] for an overview. In the literature, the term
“Public Announcement Logic” is often used in the singular. But there is morethan one such logic because the underlying modal logic of knowledge or belief
may vary. In the literature, it is mainly the basic modal logic K and the modal
logic S5 that are investigated, or rather their multimodal versions. The reasonsthat are given for these choices are that K is an appropriate basis for a logic ofbelief, while S5 is the logic of knowledge.
One may argue against S5 as a logic of knowledge. It is typically taken for
granted in artificial intelligence and game theory that it is S5; however, thischoice has been criticised in the philosophical literature, most prominently so
by Lenzen [11,12]. The latter argues for S4.2 and S4.3 as the appropriate logics
of knowledge. Let us remark that we only consider knowledge of a perfectreasoner, i.e. we leave the omniscience problem aside.
The base modal logic K is not a suitable logic of belief: philosophers insisted
that such a logic should contain the D axiom since the seminal work of Hintikka[7]; Hintikka took KD, while later authors rather took KD45 [11,12].
These considerations motivate a more systematic study of extensions ofmodal logics by public announcements. It turns out that many of these extensions are problematic. Semantically speaking, the problem is that the updateof a model by an announcement may no longer be in the intended class ofmodels: typically existential properties such as seriality may be lost after an
update. Axiomatically speaking, as soon as we take it for granted that the
public announcement operator is a normal modal operator, i.e. it obeys the Kaxiom and the necessitation rule, then the extensions of different modal logics
may collapse.
In order to illustrate this let us show that the public announcement extension of KD coincides with the public announcement extension of KT if theannouncement operator is normal. First, from the KD theorem ¬2i ⊥ we caninfer[¬ϕ!]¬2i ⊥by the necessitation rule for announcements. Second, we have2i ϕ → [¬ϕ!]2i ⊥by the usual reduction axioms for public announcements [¬ϕ!]2i ⊥ ↔ (¬ϕ →2i [¬ϕ!]⊥) and [¬ϕ!]⊥ ↔ ϕ. From the above two and the fact that [¬ϕ!] isnormal it follows that 2i ϕ → [¬ϕ!]⊥ is a theorem. The application of the
reduction axioms uses the inference ruleϕ ↔ ϕ0[ψ!]ϕ ↔ [ψ!]ϕ038

Some Truths Are Best Left Unsaid

which is derivable for normal modal operators. As [¬ϕ!]⊥ reduces to ϕ we
obtain that 2i ϕ → ϕ is a theorem. Another way of formulating this result
is the following: if we extend KD by Plaza’s reduction axioms (plus rules of
replacement of equivalents for announcements) then one can prove the T axiom.
Given the above negative result we propose a new truth condition for publicannouncements that has not been studied before. It differs from the standard
interpretation where the update is conditioned by the truth of the announcement: it requires moreover that the updated model is a legal frame of theunderlying logic. We denote that interpretation by the superscript ‘C’ where C
is a class of frames validating the underlying logic. We investigate the axiomatisability of the resulting public announcement logics. We give axiomatisations
for all those of our logics where the fact that a frame is a C frame can becharacterised in the language (more precisely, in its extension by the universal
modal operator). On the negative side, the C-semantics still does not allow
to axiomatise a public announcement extension of S4.2; the reason is that it
cannot be characterised in the language of S4.2 that a frame is a legal frameof the underlying logic L.
The paper is organised as follows: In Section 2 we recall the standard
presentation of public announcement logics: a semantics in terms of updates
that are conditioned by the truth of the announcement and an axiomatics
in terms of reduction axioms. In Section 3 we present our version of publicannouncement logics in terms of an enhanced truth condition. In Section 4 wecharacterise the validities of different classes of frames axiomatically by meansof reduction axioms. In Section 5 we present several examples of classes offrames that still cannot be axiomatised. In Section 6 we discuss various othersemantical options allowing to define variants of public announcement logics.
In Section 7 we discuss some related work and in Section 8 we conclude.

2

Public announcement logics: standard version

Let P be a countable set of propositional letters and let J be a finite set of agent
names. The public announcement language LPAL is defined by the following
BNF:
ϕ ::= p | ⊥ | ¬ϕ | (ϕ ∨ ϕ) | 3i ϕ | hϕ!iϕwhere p ranges over P and i ranges over J. The length of ϕ, i.e. the number ofoccurrences of symbols in ϕ, will be denoted l(ϕ).
The epistemic language LEL is the fragment of LPAL without announcement
operators hϕ!i. As usual, > abbreviates ¬⊥, 2i ϕ abbreviates ¬3i ¬ϕ, and[ϕ!]ψ abbreviates ¬hϕ!i¬ψ. We adopt the standard rules for omission of theparentheses.
2.1 Models and their updates
A Kripke frame is a tuple hW, Ri such that:•

W is a nonempty set of possible worlds;

Balbiani, van Ditmarsch, Herzig and de Lima•

39

R : J → ℘(W ×W ) associates to every agent i ∈ J a binary relation Ri on W .

The class of all Kripke frames is denoted by Call .
A Kripke model is a tuple M = hW, R, V i such that hW, Ri is a Kripke frame
and V : P → ℘(W ) associates an interpretation V (p) ⊆ W to each p ∈ P. For
every x ∈ W , the pair (M, x) is a pointed model. For convenience, we define
Ri (x) = {x0 | (x, x0 ) ∈ Ri }. In an epistemic or doxastic interpretation, theelements of Ri (x) are the worlds agent i considers possible at x: the worldsthat are compatible with i’s knowledge or respectively i’s belief.
Let M = hW, R, V i be a Kripke model and let U be some subset of W . The
world update (alias relativisation) of M by U is defined as M ◦U = hW 0 , R0 , V 0 i,
with:
W0 = URi0 = Ri ∩ (U × U ), for every i ∈ J0
V (p) = V (p) ∩ U, for every p ∈ P
If U is empty then hW 0 , R0 i is not a Kripke frame. We shall see that thestandard truth condition avoids this by conditioning the update, preventing
thus the semantics from being ill-defined.
If U is non-empty then hW 0 , R0 i is a Kripke frame. Things are less straightforward if we want to preserve membership in some subclass C of the class of
all Kripke frames: it may for example happen that existential properties suchas seriality, density, or confluence of the relations Ri are not always preserved.
This will be the raison d’être of our enhanced semantics.
2.2 Standard truth conditions and validity
We recall the interpretation of LPAL formulas in a given model M = hW, R, V i:||p||M = V (p), for p ∈ P||¬ϕ||M = W \ ||ϕ||M||ϕ ∨ ψ||M = ||ϕ||M ∪ ||ψ||M||3i ϕ||M = Ri−1 (||ϕ||M )= {x ∈ W | Ri (x) ∩ ||ϕ||M 6= ∅}||hϕ!iψ||M = ||ϕ||M ∩ ||ψ||M ◦||ϕ||M
If we write M, x ϕ instead of x ∈ ||ϕ||M , then we can restate the last condition
in a form that is perhaps more customary:
M, x

hϕ!iψ

iff

M, x

ϕ and M ◦ ||ϕ||M , xψAn LPAL formula ϕ is globally true in the Kripke model M = hW, R, V i if
and only if ||ϕ||M = W . (This is sometimes noted Mϕ.) We say that ϕis valid in the Kripke frame hW, Ri if and only if ϕ is globally true in every
Kripke model over hW, Ri.
We are interested in several particular classes of Kripke frames: Call is theclass of all Kripke frames; Cserial is the class of frames where each accessibility

40Some Truths Are Best Left Unsaid

relation is serial; Crefl is the class of frames where each accessibility relation isreflexive; Cconfl is the class of frames where each accessibility relation is confluent; Crefl,trans,eucl is the class of frames where each accessibility relation is anequivalence relation (reflexive, transitive and Euclidean); and so on.
Given a class of frames C, let Λ(C) be the set of LPAL formulas that are valid
in every frame of C. An example of a formula that is valid in the class of all
Kripke frames Call is [p!]2i p, for atomic p. In contrast, the schema [ϕ!]2i ϕ is
not valid in every Kripke frame. Another schema that is valid in every Kripke
frame is 2i ϕ → [¬ϕ!]2i ⊥. It plays an important role in this paper: rememberthat we have already used it in the introduction when proving the T axiom.
Let us immediately say that the definition of Λ(C) is problematic. Consider
a Kripke model M = hW, R, V i such that R is serial (i.e., hW, Ri ∈ Cserial ) andsuch that M, x
ϕ ∧ 2i ¬ϕ, and suppose we want to check whether M, x
hϕ!i2i ⊥. This involves checking whether M ◦||ϕ||M , x 2i ⊥; which is the case,and therefore M, x hϕ!i2i ⊥. This means that it may happen that after anannouncement, agent i gets crazy and starts to believe everything. Formallyspeaking, while ¬2i ⊥ is valid in serial frames, its necessitation [ϕ!]¬2i ⊥ isnot: necessitation by announcements does not preserve validity! This is clearly
undesirable. The key observation is that in M ◦ ||ϕ||M we have Ri0 (x) = ∅: theaccessibility relation Ri0 is not serial any more.
The above discussion was about the preservation of seriality, but the sameproblem arises for example for confluence. More generally, it arises for classesof frames that are defined by an existential condition.
2.3 Axiomatisation of K-PAL
Let K-PAL be the least set of formulas in our language LPAL that contains all
instances of axiom schemas of the basic modal logic K for every 3i and of the
reduction axiom schemas
hψ!ip ↔ ψ ∧ p, for p ∈ P
hψ!i⊥ ↔ ⊥hψ!i¬ϕ ↔ ψ ∧ ¬hψ!iϕhψ!i(ϕ1 ∨ ϕ2 ) ↔ hψ!iϕ1 ∨ hψ!iϕ2
hψ!i3i ϕ ↔ ψ ∧ 3i hψ!iϕRedh!i,P
Redh!i,⊥
Redh!i,¬
Redh!i,∨
Redh!i,3i

and that is closed with respect to the inference rules of Modus Ponens, necessitation by announcements, and the two rules of equivalents for hψ!i:ϕ ↔ ϕ0hψ!iϕ ↔ hψ!iϕ0ψ ↔ ψ0hψ!iϕ ↔ hψ 0 !iϕRErh!iRElh!iCompleteness of K-PAL w.r.t. Call follows from Wang’s result that the axiom
schemas of K for every 3i plus the above reduction axioms plus the K axiom andthe necessitation rule for announcements make up a complete axiomatisation

Balbiani, van Ditmarsch, Herzig and de Lima

41

of K-PAL [17, Corollary 1]: indeed, the K axiom and the necessitation rule forannouncements may equivalently be replaced by Redh!i,⊥ , Redh!i,∨ , and RElh!i(cf. [4, Theorem 4.3]).
As customary in dynamic epistemic logics, our axiomatic system allows fora proof procedure in terms of reduction axioms. As there is no axiom schema
for two consecutive announcements, reduction has to be performed ‘bottomup’ (or ‘inside-out’ as Wang calls it [17]), starting by some innermost dynamic
operator. The sound performance of such ‘deep replacements’ requires therule of replacement of proved equivalents RRE; and indeed, our two rules of
equivalents for announcements RErh!i and RElh!i enable the derivation of the ruleχ ↔ χ0(ϕ)pχ ↔ (ϕ)pχ0

RRE

where (ϕ)pχ denotes the result of replacing all occurrences of p in ϕ by χ.
Proposition 2.1 The rule RRE is derivable from the axiom schemas of K for
3i by Modus Ponens, necessitation by announcements, RErh!i , and RElh!i .
Proof. This follows from the fact that rules of equivalents can be derived forevery (Boolean and modal) operator; remember that for the dynamic operatorshψ!i we directly have the two rules RErh!i and RElh!i ). For a proof see e.g. [4]. 2
Here is an example of proof by means of reduction axioms:
hp!ih¬q!ir ↔ hp!i(¬q ∧ r)
↔ hp!i¬q ∧ hp!ir↔ p ∧ ¬hp!iq ∧ hp!ir↔ p ∧ ¬(p ∧ q) ∧ p ∧ r↔ p ∧ ¬q ∧ r

Redh!i,P
Redh!i,∧
Redh!i,¬
Redh!i,P (twice)In the second step, Redh!i,∧ stands for the equivalence hψ!i(ϕ1 ∧ ϕ2 ) ↔ hψ!iϕ1 ∧hψ!iϕ2 that can be proved from Redh!i,∨ and Redh!i,¬ .
Observe that RRE is used in each of the steps. Observe also that we have tostart by reducing the innermost dynamic operator h¬q!i by means of the Redh!i,¬rule —which requires the application of RErh!i — because our axiomatisation
does not provide for a reduction axiom for the case of two consecutive dynamic
operators.
2.4

Alternative axiomatisation

The axiomatisations in the literature typically lack RErh!i and RElh!i . They
instead have the following axiom schema for the composition of announcements:hψ1 !ihψ2 !iϕ ↔ hhψ1 !iψ2 !iϕRedh!i,h.!i42Some Truths Are Best Left Unsaid(see e.g. [13] or [16, Proposition 4.22]). To illustrate the difference we give a
proof of the above example formula via Redh!i,h.!i .
hp!ih¬q!ir ↔ hhp!i¬q!ir↔ hp!i¬q ∧ r↔ p ∧ ¬hp!iq ∧ r↔ p ∧ ¬(p ∧ q) ∧ r↔ p ∧ ¬q ∧ r

Redh!i,h.!i
Redh!i,P
Redh!i,¬
Redh!i,PThis is an ‘outside-in’ reduction, as opposed to reductions without Redh!i,h.!i
which have to proceed ‘inside-out’ and require our above rule of replacementof proved equivalents RRE [17].
RRE is stated in Proposition 4.46 in [16], and its proof (Exercise 4.48) saysthat it follows from the fact that the necessitation rule for announcements is
an admissible inference rule (cf. also Exercise 4.52 there). We note in passingthat Wang proved that neither RRE nor RErh!i can be derived from the axiom
schemas of K plus the above reduction axioms alone, i.e., without RErh!i , RElh!i ,or Redh!i,h.!i [17].
Remark 2.2 It follows from the completeness theorem (and from the fact that
RRE preserves validity) that RRE is admissible, i.e., it preserves theoremhood:for every formula instance χ ↔ χ0 and every formula instance ϕ, if there isa proof of χ ↔ χ0 then there is a proof of (ϕ)pχ ↔ (ϕ)pχ0 . However, thisdoes not mean that RRE is derivable, i.e., that there is a derivation of theinference rule RRE itself. This situation can be compared to the completenesstheorem for K-PAL which only says that every valid formula is provable, butdoes not guarantee that there are proofs of all valid formula schemas. These
two versions of completeness —w.r.t. schemas and w.r.t. instances— coincide
for logics where the rule of uniform substitution preserves validity, but K-PAL
does not have that property. We note in passing that it is only recently that acomplete axiomatisation of the schematic validities of K-PAL was given [8].
2.5When things get wrong: public announcement extensions ofKD, KD45, S4.2, etc.
We have just seen how K-PAL completely axiomatises the set of formulas thatare valid in the class of all Kripke frames. Let KT-PAL denote the least set of
formulas in our language that contains K-PAL and all instances of the T axiom.
Then KT-PAL completely axiomatises the set of formulas Λ(Crefl ), i.e., the setof formulas that are valid in the class of all reflexive Kripke frames. In thesame way, S5-PAL —the extension of K-PAL by the axiom schemas T, 4, and5— axiomatises Λ(Crefl,trans,eucl ).
More generally, one might naively expect that if the validities of a class offrames C in the non-dynamic language LEL can be axiomatised by some set ofschemas and rules AX C , then the validities of C in LPAL can be axiomatisedby the set of schemas and rules for K-PAL plus AX C . The following argumentshows what happens when we do this for the logic KD.

Balbiani, van Ditmarsch, Herzig and de Lima43

By Redh!i,¬ , Redh!i,3i , and Redh!i,P , one can derive p ∧ ¬3i p → hp!i¬3i >.
We have seen in Section 2.3 that the rule of necessitation for announcements isderivable in our axiomatics of K-PAL and therefore also in the —hypothetical—
axiomatisation of KD-PAL. Thus, in KD, by the axiom 3i > and the necessitation by announcement, one can derive [p!]3i >. From p ∧ ¬3i p → hp!i¬3i >and [p!]3i >, one can obviously derive 2i p → p.
This makes that ϕ is a theorem of the latter system if and only if ϕ is atheorem of KT-PAL, which is clearly undesirable.
It seems that in the case of serial frames the only way to ‘save’ the standard truth condition is to abandon the rule of necessitation by announcements.
While this is technically possible, the price to pay is that in many cases, theextension of an underlying modal logic by public announcements cannot be
a conservative extension of that underlying logic. We think that this should
better be avoided.

3

A new semantics

The preceding observation has motivated us to design a new semantics for the
logics of public announcements.
Our results typically require a master modality, such as the universal modality. We therefore add the latter to our language: we define the language LPAL,∀
by the following BNF:
ϕ ::= p | ⊥ | ¬ϕ | (ϕ ∨ ϕ) | 3i ϕ | hϕ!iϕ | ∀ϕ
The formula ∃ϕ abbreviates ¬∀¬ϕ. The language LEL,∀ is the fragment of
LPAL,∀ without dynamic operators.
The universal modality ∀ is interpreted as follows:(
W if ||ϕ||M = W||∀ϕ||M =∅else
3.1 A parametrised truth condition
Let C be a given class of Kripke frames. Let M be some model over someframe of C. In order to distinguish our semantics from the standard semantics
we write ||ϕ||CM instead of ||ϕ||M .
The truth conditions for all but the dynamic operator take the same form
as before. For the latter we define:(∅
if the frame of M ◦ ||ϕ||CM is not in CC||hϕ!iψ||M =||ϕ||CM ∩ ||ψ||CM ◦||ϕ||CotherwiseM

If we write M, x C ϕ instead of x ∈ ||ϕ||CM , then we can restate this condition
in a form that is perhaps more customary:
M, x

C

hϕ!iψ

iff

the frame of M ◦ ||ϕ||CM is in C,
M, xC

ϕ and M ◦ ||ϕ||CM , x

C

ψ

44

Some Truths Are Best Left Unsaid

Remark that the above truth condition for the dynamic operator makes it anormal modal operator, i.e. the dynamic operator obeys the K axiom and thenecessitation rule.
Obviously, given a class C of Kripke frames, what interests us is the set
Λ(C)C of LPAL formulas that are valid in every Kripke frame of the class C
under our C conditioned interpretation. Traditionally, if a class C 0 of frames
is included in a class C 00 , then every formula valid in C 00 is also valid in C 0 . In
our new semantics, seeing that the truth conditions are conditioned by classesof frames, validity with respect to C 00 and validity with respect to C 0 are notequivalent notions. For some classes C 0 and C 00 , it might appear that C 0 ⊆ C 0000
0and Λ(C 00 )C 6⊆ Λ(C 0 )C . To see an example, let C 0 be the set of all strict totalorders with at least 3 points and C 00 be the set of all strict total orders with at00
0least 2 points. Obviously, C 0 ⊆ C 00 . In order to show that Λ(C 00 )C 6⊆ Λ(C 0 )C ,let us consider the formula ϕ = p ∧ [p!]⊥ → 2¬p. We claim the following:
00(i) ϕ ∈ Λ(C 00 )C ;0(ii) ϕ 6∈ Λ(C 0 )C .
To demonstrate (i), let M = hW, R, V i be some model based on a linear orderhW, Ri in C 00 . Hence, W contains at least 2 points. Let x ∈ W be such that
00
M, x C p ∧ [p!]⊥. Thus, x ∈ V (p) but V (p) does not contain at least 2
00
points. Therefore, V (p) = {x} and M, x C 2¬p. To demonstrate (ii), let
M = hW, R, V i be a model based on the linear order {0, 1, 2} in C 0 such that00
V (p) = {0, 1}. Obviously, M, 0 C p ∧ [p!]⊥ and M, 0 6 C 2¬p.
In sections 4 and 5 we will explore this C conditioned interpretation. We
focus on axiomatisability in terms of reduction axioms. In that perspective, thecrucial point is whether we are able to characterise the condition “the frameof M ◦ ||ϕ||CM belongs to class C” in the logical language. For the cases where
this is possible, our characterisations require in general a ‘master modality’such as the common knowledge operator or the universal modality [1] (i.e.,they require the language LEL,∀ ); the only exception is the class Ctr1 where J is asingleton and where the frames have transitive accessibility relations: no mastermodality is needed in that case. An example of such a frame class
Vcharacterisingcondition, relative to a given announced formula ψ, is ∀(ψ → i∈J 3i ψ). Not
surprisingly, this is the characterising formula for the class of serial frames.
Before we formally introduce that, we have to further prepare the theoreticalground.

Balbiani, van Ditmarsch, Herzig and de Lima

3.2

45

Reduction axioms

We define the announcement degree of a LPAL,∀ formula ϕ as follows:d(p) = 0d(⊥) = 0d(¬ϕ) = d(ϕ)
d(ϕ ∨ ψ) = max(d(ϕ), d(ψ))
d(3i ϕ) = d(ϕ)
d(hϕ!iψ) = max(d(ϕ), d(ψ)) + 1d(∀ϕ) = d(ϕ)

For example, the announcement degree of both hp!i3i h¬q!i3j r andhhp!i¬q!i(3j r ∨ hp!i>) is 2.
Consider some class of Kripke frames C. Suppose the fact that the frame of
the updated model M ◦ ||ϕ||CM belongs to C can be characterised by an LPAL,∀
formula f(ϕ) whose announcement degree is at most that of ϕ. We then obtainthe following reduction axioms:

hψ!ip ↔ ψ ∧ f(ψ) ∧ p

for p ∈ P

RedCh!i,Phψ!i⊥ ↔ ⊥RedCh!i,⊥hψ!i¬ϕ ↔ ψ ∧ f(ψ) ∧ ¬hψ!iϕ

RedCh!i,¬hψ!i(ϕ1 ∨ ϕ2 ) ↔ hψ!iϕ1 ∨ hψ!iϕ2

RedCh!i,∨hψ!i3i ϕ ↔ ψ ∧ f(ψ) ∧ 3i hψ!iϕ

RedCh!i,3ihψ!i∃ϕ ↔ ψ ∧ f(ψ) ∧ ∃hψ!iϕ

RedCh!i,∃Observe that the announcement degree of formulas does not increase fromthe left to the right due to our hypothesis that the announcement degree off(ϕ) is at most that of ϕ; this would be violated e.g. if f(ϕ) was hϕ!i>.
Let us associate to every formula ψ in LPAL,∀ , its measure m(ψ) =(d(ψ), l(ψ)) in N0 × N0 , N0 denoting the set of all the non-negative integers, and d(ψ) and l(ψ) respectively denoting the announcement degree andthe length of ψ. Let  be the well-founded ordering on N0 × N0 defined by(m1 , n1 )  (m2 , n2 ) iff either m1 < m2 , or m1 = m2 and n1 < n2 .
The above reduction axioms suggest us to consider a function τ : LPAL,∀ −→46

Some Truths Are Best Left Unsaid

LEL,∀ defined by the following equations:τ (p) = pτ (⊥) = ⊥τ (¬ϕ) = ¬τ (ϕ)τ (ϕ ∨ ψ) = τ (ϕ) ∨ τ (ψ)τ (3i ϕ) = 3i τ (ϕ)τ (hψ!ip) = τ (ψ) ∧ τ (f (ψ)) ∧ p
τ (hψ!i⊥) = ⊥τ (hψ!i¬ϕ) = τ (ψ) ∧ τ (f (ψ)) ∧ ¬τ (hψ!iϕ)τ (hψ!i(ϕ1 ∨ ϕ2 )) = τ (hψ!iϕ1 ) ∨ τ (hψ!iϕ2 )τ (hψ!i3i ϕ) = τ (ψ) ∧ τ (f (ψ)) ∧ 3i τ (hψ!iϕ)τ (hψ!i∃ϕ) = τ (ψ) ∧ τ (f (ψ)) ∧ ∃τ (hψ!iϕ)τ (∃ϕ) = ∃τ (ϕ)
These equations really define a function by -induction from LPAL,∀ to
LEL,∀ , seeing that if τ (ψ) occurs on the right side of the equation defining τ (ϕ)
then m(ψ)  m(ϕ).
In other respect, remark that for every ψ in LPAL,∀ , the formulaψ ↔ τ (ψ)
is valid in C. It follows that when applying τ , we can eliminate step by step
every occurrence of a dynamic operator. Therefore we can prove completenessof the axiomatisation obtained by replacing the standard reduction axioms
by the above ones in the very same way as the completeness of the standard
axiomatisation for K-PAL. Moreover, the validity problem of LPAL,∀ formulasin the class C is reducible to the validity problem of LEL,∀ formulas in C.
So it remains to find out for which classes C such a function exists. This is
the same as looking for a function f : LPAL,∀ −→ LPAL,∀ such that for every ψ in
LPAL,∀ , the formulahψ!i> ↔ ψ ∧ f(ψ)
is valid in C and the announcement degree of f(ψ) is at most that of ψ (thelatter ensuring that reduction terminates). We do so in the next two sections.

4

Positive results

For which classes of frames C can we express that the frame of the updated
model belongs to C by means of a formula f(ψ) of the language LPAL,∀ ? Clearly,
when C is the class of all Kripke frames Call then f(ψ) = >. The same isthe case when C is a class of frames that is defined by universal first-orderconditions 5 , such as reflexivity, transitivity, symmetry, Euclideanity, linearity,
5 A first-order formula is universal if it is of the form ∀x . . . ∀x ϕ where ϕ is quantifier-freen1
and where the variables of ϕ are among x1 , . . . , xn .

Balbiani, van Ditmarsch, Herzig and de Lima

47

or combinations thereof: these conditions are preserved under any update. Thisaccounts for the public announcement extensions of modal logics such as KT,
K4, KT4 = S4, KB, KTB, KB4, KT45 = S5 and S4.3.
Things are less straightforward for frames defined by seriality and combinations of seriality with other conditions such as transitivity and Euclideanity.
In this section we exhibit formulas f(.) for some of these cases, thus accounting
in particular for the public announcement logics KD-PAL and KD45-PAL.
4.1 Universal frame conditions
Let Φ be a universal first-order sentence over {R, =}. Let CΦ be the class offrames satisfying Φ. Thenhψ!i> ↔ ψ
is valid in CΦ . Therefore, we can set fΦ (ψ) = >.
This covers in particular the case where C is the class of frames for S4.3,
i.e., the class of reflexive, transitive and linear frames.
4.2 Seriality
The equivalencehψ!i> ↔ ψ ∧ ∀(ψ →

^

3i ψ)

i∈J

is validVin the class of all serial frames Cserial . We can therefore set f(ψ) =∀(ψ → i∈J 3i ψ).
We observe that there is no LEL formula ϕ such that hp!i> ↔ ϕ is valid inserial frames. Suppose such a formula exists. Let n be its modal degree. Consider the frame hN0 , Ri where N0 is the set of all the non-negative integers andhx, yi ∈ R iff y = x + 1. This is clearly a serial frame. We define two valuations
V and V 0 on that frame by stipulating V (p) = N0 , V 0 (p) = {0, · · · , n}, andV (q) = ∅ for every q 6= p. We have hN0 , R, V i, 0 Cserial ϕ iff hN0 , R, V 0 i, 0 Cserial
ϕ because n is the modal degree of ϕ. However, hN0 , R, V i, 0 Cserial hp!i>while hN0 , R, V 0 i, 0 6 Cserial hp!i>; the latter is the case because the frame of the
updated model M ◦ ||p||CMserial is not serial. We therefore have a contradiction.
4.3 Seriality and transitivity
As the reader can check, the equivalenceVhψ!i> ↔ ψ ∧ ∀(ψ → i∈J 3i ψ)
is also valid in the class of all serial and transitive frames Cserial,trans . We cansimplify that equivalence when the set of agents J is a singleton, say {i}.
gConsider the class Cserial,transof frames for KD4 that are point-generated, i.e.
the class of serial and transitive frames hW, Ri with a world x ∈ W such that
W = {x} ∪ Ri (x). Thenhψ!i> ↔ ψ ∧ 3i ψ ∧ 2i (ψ → 3i ψ)gis valid in Cserial,trans. We may therefore set f(ψ) = 3i ψ ∧ 2i (ψ → 3i ψ).

48

Some Truths Are Best Left Unsaid

Example 4.1 Let us check that for the logic KD4-PAL the formula(p ∧ ¬3i p) → hp!i¬3i >is not valid. For Cserial,trans we have the condition f(p) = ∀(p →the reduction axioms of Section 3.2 we obtain:^
hp!i¬3i > ↔ p ∧ ∀ p →3i p ∧ ¬hp!i3i >Vi∈J 3i p).

By

RedCh!i,¬

i∈J





↔ p ∧ ∀ p →^3i p ∧i∈J¬(p ∧ ∀ p →^RedCh!i,3i

3i p ∧ 3i hp!i>)i∈J↔ p ∧ ∀ p →

^3i p ∧ ¬3i hp!i>(propos. simplif.)

i∈J




↔ p ∧ ∀ p →^3i p ∧

i∈J







¬3i p ∧ ∀ p →^RedCh!i,>3i p

i∈Jwhere the reduction axiom used in the last step can be obtained from RedCh!i,¬
and RedCh!i,⊥ . The LPAL,∀ formula(p ∧ ¬3i p) → p ∧ ∀(p →


^
i∈J

3i p) ∧ ¬3i (p ∧ ∀(p →^3i p))

i∈J

is not valid in serial and transitive frames. (It is actually even invalid in Call .)Therefore(p ∧ ¬3i p) → hp!i¬3i >is not valid either. This contrasts with the hypothetical proof system that wehave discussed in Section 2.5.
4.4 Seriality, transitivity, and Euclideanity: single agent caseLet us suppose that the set of agents J is the singleton {i}. Consider thegclass Cserial,trans,euclof frames for KD45 that are point-generated, i.e. the class ofserial, transitive and Euclidean frames hW, Ri with a world x ∈ W such that
W = {x} ∪ Ri (x).

Balbiani, van Ditmarsch, Herzig and de Lima

49

Just as for serial frames the equivalence V
hψ!i> ↔ ψ ∧ ∀(ψ → i∈J 3i ψ)gis valid in Cserial,trans,eucl. However, we can do better because there is only one
agent: the schemahψ!i> ↔ ψ ∧ 3i ψgis valid in Cserial,trans,eucl, i.e., f(ψ) = 3i ψ.
We observe that the restriction to point-generated frames cannot be avoided
if we want a characterisation by a LEL formula: there is no LEL formula ϕ suchthat
hp!i> ↔ ϕis valid in the class of serial, transitive and Euclidean frames. Indeed, suppose
such a formula ϕ exists. Consider the frame hW, Ri where W = {0, 1, 2} andR = {h0, 0i, h1, 2i, h2, 2i}. That frame is serial, transitive and Euclidean. Let
V1 (p) = {0, 1} and let V2 (p) = {0}. However, we have hW, R, V1 i, 0 6 Cserial,trans,eucl
hp!i>, while hW, R, V2 i, 0 Cserial,trans,eucl hp!i>. Then we have hW, R, V1 i, 0 6 ϕ
and hW, R, V2 i, 0 ϕ. Since ϕ is without ∀ this leads us to a contradiction.

5

Negative results

We now show that there is no such formula as f(ψ) for the class of confluent
frames, for the class of reflexive, transitive and confluent frames —i.e., for thebasic logic S4.2—, and for the class of dense frames.
5.1 Confluence
Let Cconfl be the class of all confluent frames. Is there a LEL,∀ formula ϕ suchthat hp!i> ↔ ϕ is valid in Cconfl ?
Suppose such a formula exists.
Let W = {x, y, z} and let Ri be the reflexive and transitive closure of therelation {hx, yi, hy, zi}, for every i. The frame hW, Ri is in Cconfl . Let V be avaluation on hW, Ri such that V (p) = {x, y}. The model M = hW, R, V i andits update by ||p||M are depicted (without the reflexive edges) in Figure 1.
x : {p}/ y : {p}%x : {p}/ y : {p}z:∅Fig. 1. M and its update by ||p||CM (reflexive edges omitted)

Now let W 0 = {x, y, y 0 , z} and let Ri0 be the reflexive and transitive closureof the relation {hx, yi, hy, zi, hx, y 0 i, hy 0 , zi}, for every i. The frame hW 0 , R0 i is
in Cconfl , too. Let V 0 be a valuation on hW 0 , R0 i such that V 0 (p) = {x, y, y 0 }.
The model M 0 = hW 0 , R0 , V 0 i and its update by ||p||M 0 are depicted (without
the reflexive edges) in Figure 2.
The models M and M 0 are bisimilar 6 , and we therefore have M, x ϕ iff
6

The definition of bisimilarity has to take the universal modality into account. So M =50Some Truths Are Best Left Unsaid

x : {p}/ y : {p}x : {p}y 0 : {p}% /z : ∅

y 0 : {p}/ y : {p}Fig. 2. M 0 and its update by ||p||CM 0 (reflexive edges omitted)

M 0 , x ϕ for every LEL,∀ formula ϕ. However, we have M, x Cconfl hp!i>, while
M 0 , x 6 Cconfl hp!i>; the former is the case because the frame of the updated
model M ◦ ||p||CM is confluent, and the latter is the case because the frame of
the updated model M 0 ◦ ||p||CM is not. We therefore have a contradiction.
5.2 Reflexivity, transitivity, and confluence
Let Crefl,trans,confl be the class of all reflexive, transitive, and confluent frames.
There is no LEL,∀ formula ϕ such that hp!i> ↔ ϕ is valid in that class. Indeed,suppose such a formula exists. We take over the two above counterexample
models for confluence. Observe that both frames are in Crefl,trans,confl . Again,
M and M 0 are bisimilar, and therefore M, x
ϕ iff M 0 , x
ϕ for every ϕ.
However, M, x Crefl,trans,confl hp!i>, while M 0 , x 6 Crefl,trans,confl hp!i>. We therefore
have a contradiction.
5.3 Density
Let Cdense be the class of all dense frames. There is no LEL,∀ formula ϕ suchthat hp!i> ↔ ϕ is valid in Cdense . Indeed, suppose such a formula exists. Let
hW, Ri be the frame defined by W = {α, ω, 1, 2, 3, 4, 5} andRi = {hα, ωi} ∪{hα, yi | 1 ≤ y ≤ 5} ∪{hx, ωi | 1 ≤ x ≤ 5} ∪{hx, yi | 1 ≤ x, y ≤ 5, x 6= y}for every i ∈ J. The reader may check that hW, Ri is indeed dense. Let
V1 (p) = {α, ω, 1, 5} and let V2 (p) = {α, ω, 1, 3, 5}. The models M1 = hW, R, V1 i
and M2 = hW, R, V2 i are bisimilar, and therefore M1 , α ϕ iff M2 , α ϕ forevery LEL,∀ formula ϕ. However, M1 , α 6 Cdense hp!i>, while M2 , α Cdense hp!i>.
We therefore have a contradiction.
hW, R, V i and M 0 = hW 0 , R0 , V 0 i are bisimilar if there is a relation Z ⊆ W × W such that:(i) if (x, x0 ) ∈ Z then x ∈ V (p) iff x0 ∈ V 0 (p), for every p ∈ P(ii) if (x, x0 ) ∈ Z and (x, y) ∈ Ri then there is y 0 ∈ W 0 such that (x0 , y 0 ) ∈ Ri0 and (x, y) ∈ Z(iii) if (x, x0 ) ∈ Z and (x0 , y 0 ) ∈ Ri0 then there is y ∈ W such that (x, y) ∈ Ri and (x, y) ∈ Z(iv) for every x ∈ W there is x0 ∈ W 0 such that (x, x0 ) ∈ Z(v) for every x0 ∈ W 0 there is x ∈ W such that (x, x0 ) ∈ Z
The last two conditions say that both Z and its converse Z −1 are serial.

Balbiani, van Ditmarsch, Herzig and de Lima

651

Discussion: semantic alternatives

We now explore some alternative semantics for public announcements that one
can find in the literature: first, a proposal to update models in a different way,
and second, a different formulation of the truth condition for public announcements.
6.1 Relation updates
Beyond the standard way of updating a Kripke model by eliminating worlds ofSection 2, there are proposals in the literature where instead of worlds it is edges
that are eliminated [5,6]. Let M = hW, R, V i be a model, and let U be somer
subset of W . The relation update of M by U is defined as M ◦ U = hW, R0 , V i,with:
Ri0 = Ri ∩ (W × U )Let Λ(C)r be the set of LPAL formulas valid in C under relation update(under our truth condition for announcements of Section 2.2 requiring truth of
the announcement).
We argue that if one wants the underlying modal logic to be a customary logic of knowledge or belief, then this way of extending a modal logic byannouncements is not very interesting, for two reasons. First, as far as thelanguage LPAL is concerned we have Λ(C) = Λ(C)r (because the generated subrmodels of M ◦ U and M ◦ U are equal); the logics differ only when the universal
modal operator comes into play. Second, while membership in the class of allmodels Call is preserved under relation update, membership in a particular classof models is preserved in fewer cases: not only do existential first-order conditions such as seriality, density and confluence fail, but also universal conditions
such as reflexivity and symmetry.
6.2 An unconditioned truth condition
Remember that the standard formulation of the truth condition requires announcements to be truthful. This means that the agents acquire knowledge. In
the literature one can find not only another definition of model update, but also
another formulation of the truth condition for public announcements. To thecontrary, in Gerbrandy’s formulation announcements may be false [5,6]. The
latter formulation is therefore often claimed to be more appropriate for agentsacquiring beliefs, see e.g. [9]. We call this the unconditioned truthconditionand highlight it by “u”:
M, x

u

hϕ!iψ

iff M ◦ ||ϕ||uM , xψThen we have two options, according to whether we use world update or
relation update. Call Λ(C)u and Λ(C)ru the resulting logics of the class offrames C. For example, Kooi’s basic public announcement logic is Λ(Call )ru [9].
Observe that none of the logics Λ(C)u makes sense. Indeed, consider thecase where a model M is updated by a formula that is false at every point of52

Some Truths Are Best Left Unsaid

M ; then the set of possible worlds of the updated model is empty, and therefore
the update of the model is not a legal Kripke model: the unconditioned interpretation is ill-defined. Let us finally notice that when we ‘repair’ the logics
Λ(C)u by replacing the unconditioned truth condition by our enhanced version
then we obtain Λ(C)C .

7

Related work

Yanjing Wang has recently investigated axiomatisations of public announcement logics [17]. He focusses on public announcement extensions of the basic
modal logic K and subtleties with different versions of the axiomatization. In
particular, he highlights the role of the rule of replacement of equivalents RErh!i .
His work certainly provide a stimulating background to our own. Updates that
preserve KD45 have been investigated in [15,2,10]. Guillaume Aucher [2] defines
a language fragment that makes you go mad (‘crazy formulas’). The formula
characterising the cases where this can be avoided is the same as ours in Section
4. David Steiner [15] proposes that the agent does not incorporate the new information if he already believes to the contrary. In that case, nothing happens.
Otherwise, access to states where the information is not believed is eliminated,just as for believed public announcements. This solution to model unbelievable
information is similarly proposed in the elegant [10], where it is called ‘cautious
update’ — a suitable term. The difference between these approaches and ours
is that the agent simply keeps his old beliefs in case the new information isunbelievable (i.e., if there is no accessible state where the announced formula
is true). In our KD45 preserving updates the update cannot be executed if it
is unbelievable.

8

Conclusion

In this paper we had a closer look at the axiomatization and the semantics
of various public announcement logics. We highlighted problems that arise for
epistemic or doxastic logics with existential frame conditions such as seriality or
confluence and proposed an enhanced truth condition avoiding these problems
in some cases. Our new truth condition amounts to the original condition if
the basic logic is K or S5. We have studied the limitations of our solution; inparticular the case of confluence remains without a satisfactory solution, andwith it the extension of the logic of knowledge S4.2 by public announcements.
Our results required to extend the language by a master modality. We
opted for the universal modality; however, the common knowledge modality
would do, too.
Everything said here transfers to other kinds of updates such as assignments.
More precisely, in dynamic epistemic logics with assignments, we can model
announcements that stay within a certain frame class in the same way, but
for the dynamics involving assignments there are no additional complications:an assignment is a total function that can always be executed, and that neverchanges the frame properties of the transformed model. It would be interesting
to study whether (and how) it transfers to dynamic epistemic logics with event

Balbiani, van Ditmarsch, Herzig and de Lima

53

models and product update [3]. In [3], Baltag and Moss showed that reflexivity,transitivity and Euclideanity are preserved under standard product updates.
In [2], Aucher provided a characterisation of the condition f(ψ) under which
product update preserves seriality.
Here is a proposal for a way to overcome the expressive limitations that wehave highlighted in Section 5. The idea is to enrich the language by a modal
constant δC whose interpretation is that it is true exactly when the frame it isevaluated in is part of the class C. Let us call that language LPAL,δC . Its truth
condition is:
hW, R, V i, x

δC iff hW, Ri ∈ C

Let us define a translation from LPAL to LPAL,δC whose main clauses are:pt = p(hψ!iϕ)t = hψ t !i(δC ∧ ϕt )and homomorphic for the other cases. We then have that for every frame
hW, Ri, every valuation V over that frame, and every world x ∈ W ,hW, R, V i, x C ϕ iff hW, R, V i, x
ϕt . It remains however to axiomatise
the C validities in the augmented language.

Acknowledgements
Thanks are due to the three AiML reviewers for their thorough commentson the submitted version. We wish to express our special appreciation forthe second AiML reviewer, who went far beyond his duties in giving us very
precise and detailed comments that helped to improve the paper and make it
more readable. Hans van Ditmarsch also wants to thank the IMSc (Instituteof Mathematical Sciences), Chennai, India, where he is affiliated as a research
associate.

References[1] Carlos Areces and Balder ten Cate. Hybrid logics. In Patrick Blackburn, Johan van
Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3. Elsevier
Science, 2006.
[2] Guillaume Aucher.
Consistency preservation and crazy formulas in BMS.
In
S. Hölldobler, C. Lutz, and H. Wansing, editors, Logics in Artificial Intelligence, 11th
European Conference, JELIA 2008. Proceedings, pages 21–33. Springer, 2008. LNCS
5293.
[3] Alexandru Baltag and Lawrence Moss. Logics for epistemic programs. Synthese,
139(2):165–224, 2004.
[4] Brian Chellas. Modal logic: An introduction. Cambridge University Press, 1980.
[5] Jelle Gerbrandy. Bisimulations on Planet Kripke. PhD thesis, ILLC, University of
Amsterdam, 1999.
[6] Jelle Gerbrandy and Willem Groeneveld. Reasoning about information change. J. of
Logic, Language and Information, 6(2), 1997.
[7] Jaakko Hintikka. Knowledge and Belief. Cornell University Press, 1962.

54

Some Truths Are Best Left Unsaid[8] Wesley H. Holliday, Tomohiro Hoshi, and Thomas F. Icard III. Schematic validity
in dynamic epistemic logic: decidability. In Proceedings of the Third international
conference on Logic, rationality, and interaction, LORI’11, pages 87–96, Berlin,
Heidelberg, 2011. Springer-Verlag.
[9] Barteld Kooi. Expressivity and completeness for public update logic via reduction
axioms. Journal of Applied Non-Classical Logics, 17(2):231–253, 2007.
[10] Barteld Kooi and Bryan Renne. Arrow update logic. Review of Symbolic Logic, 4:536–
559, 2011.
[11] Wolfgang Lenzen. Recent work in epistemic logic. North Holland Publishing Company,
Amsterdam, 1978.
[12] Wolfgang Lenzen. On the semantics and pragmatics of epistemic attitudes. In Armin
Laux and Heinrich Wansing, editors, Knowledge and belief in philosophy and AI, pages
181–197. Akademie Verlag, Berlin, 1995.
[13] Jan Plaza. Logics of public communications. In M. L. Emrich, M. Hadzikadic, M. S.
Pfeifer, and Z. W. Ras, editors, Proceedings of the Fourth International Symposium on
Methodologies for Intelligent Systems (ISMIS), pages 201–216, 1989.
[14] Jan Plaza. Logics of public communications. Synthese, 158(2):165–179, 2007.
[15] D. Steiner. A system for consistency preserving belief change. In Proceedings of the
ESSLLI Workshop on Rationality and Knowledge, pages 133–144, 2006.
[16] Hans van Ditmarsch, Wiebe van der Hoek, and Barteld Kooi. Dynamic Epistemic Logic,
volume 337 of Synthese Library. Springer, 2007.
[17] Yanjing Wang. On axiomatizations of PAL. In Proc. LORI’11, pages 314–327, 2011.