Knowing That, Knowing What, and Public Communication: Public Announcement Logic with Kv Operators

1 Introduction

As originally proposed in [Von Wright, 1951; Hintikka, 1962], classic epistemic logic (EL) focuses on propositional knowledge of agents, expressed as knowing that p. Such formalism of knowledge turns out to be very successful in the research of AI and theoretical computer science, demonstrated by the widely use of various EL-based multi-agent systems, such as the epistemic temporal approach proposed in [Fagin et al., 1995; Parikh and Ramanujam, 1985] and the dynamic epistemic approach proposed in [Plaza, 1989; Gerbrandy and Groeneveld, 1997; Baltag et al., 1998].

On the other hand, there are other types of knowledge which are relevant to AI, such as procedural knowledge (knowing how to do a), and descriptive knowledge (knowing what is d). Compared to the heated discussion between propositional knowledge and procedural knowledge in epistemology (cf. e.g., [Ryle, 1949; Carr, 1979; Stanley and Williamson, 2001]), the distinction between "knowing that" and "knowing what" received relatively little attention, although some early work in AI, such as [McCarthy, 1979], claimed that "knowing what" is the most useful notion among the three.

∗This work is supported by the NSSF grant 11CZX054 and the key project of National Social Science Foundation of China 12&ZD119. We also would like to thank the anonymous referees for their insightful comments.

At the first glance, "knowing what" may seem to be reducible to "knowing that", for example, instead of saying (1): "He knows [what] Peter's phone number [is]", we can also say (2): "He knows that Peter's phone number is 1234" if we know Peter's phone number. However, if we replace the "phone number" in (1) by "password" which is usually not known to us, then to express the exact meaning of the revised (1) in terms of knowing that, we may need to say the following:

(3): "He knows that Peter's password is 0000 or he knows that Peter's password is 0001 or . . . or he knows that Peter's password is 9999"

Clearly, in every day communication, we prefer the succinctness of sentence (1) compared to (3). Actually the scenario behind (3) is crucial in the setting of information security, where it is very common to assume that each agent has its private key while others have no idea what it is. We would like to express "I know that he knows his password, but I do not know it." However, the literal translation in terms of propositional knowledge (K1K2φ ∧ ¬K1φ) is clearly inconsistent in classic epistemic logic. Such concerns inspired different formalisms of knowledge in epistemic logic related to security verification (cf. e.g., [Ramanujam and Suresh, 2005; Halpern and Pucella, 2003; Dechesne and Wang, 2010]).

Independently from all the above-mentioned works, Plaza proposed a very natural knowing what operator Kv in the seminal work [Plaza, 1989], which is well-known for its contribution to public announcement logic (PAL) and the reductionstyle axiomatization. 1 Intuitively, Kvid expresses exactly that "Agent i knows what d is (or i knows the value of d, in Plaza's original term)." The Kv operator was used in [Plaza, 1989] to handle the "sum-and-product" puzzle, 2 where it is crucial to distinguish the two kinds of knowledge and express i knows that j does not know what d is (formally, Ki¬Kvjd). With the corresponding semantics, formulas like KiKvjd ∧ ¬Kvid are perfectly consistent, in contrast to the inconsistency of KiKjq ∧ ¬Kiq in the standard epistemic logic.

1 PAL was also independently proposed in [Gerbrandy and Groeneveld, 1997; Gerbrandy, 1999].

Plaza gave an axiomatization of ELKv (EL with the new Kv operator) and proposed a few axioms for PALKv (PAL with Kv). However, it is unknown whether these axioms are enough to axiomatize PALKv (cf. [Plaza, 1989] and [van Ditmarsch, 2007]).

In this paper, we will answer this open question and continue Plaza's work on Kv in the context of public announcement logic. Our main technical contributions of this paper are summarized as below:

• The axioms proposed in [Plaza, 1989] do not axiomatize PALKv completely (Section 3);
• We introduce the relativized Kv operator which is a generalization of the original Kv operator (Section 4). We give a highly non-trivial complete axiomatization of the single-agent epistemic logic with this new operator (ELKvr ), based on which a complete axiomatization of single-agent PAL with this operator (PALKvr ) is provided (Section 5);
• PALKv, PALKvr and ELKvr are equally expressive but ELKv is strictly less expressive than them. Therefore it is impossible to reduce PALKv to ELKv, and we can simply use the more flexible PALKvr instead of PALKv without increasing the expressive power (Section 6).

2 Preliminaries

2.1 Public Announcement Logic

Definition 1 (Logical Languages EL(I,P) and PAL(I,P)). Given a set P of proposition letters and a set I of agent names, the language of public announcement logic PAL(I,P) is defined as follows:

where p ∈ P, i ∈ I. The language of epistemic logic (EL(I,P)) is the announcement-free fragment of PAL(I,P).

Kiφ is read "agent i knows that φ". 〈ψ〉φ says that "ψ can be truthfully announced publicly, and after its announcement φ holds." As usual, we define ⊥, φ∨ψ, φ → ψ, ˆKiφ and [ψ]φ as the abbreviations of ¬⊤, ¬(¬φ∧¬ψ), ¬φ∨ψ, ¬Ki¬φ and ¬〈ψ〉¬φ respectively.

In the sequel, we fix I and P thus simply writing PAL and EL for PAL(I,P) and EL(I,P) respectively.

The semantics of PAL is defined on (S5) Kripke structures. An epistemic model for PAL is a triple M = 〈S, {∼i| i ∈ I}, V 〉 where S is a non-empty set of possible worlds, ∼i is an equivalence relation over S, and V is a valuation function assigning a set of worlds V (p) ⊆ S to each p ∈ P. Given an epistemic model M, the semantics is defined as follows:

2 See [van Ditmarsch et al., 2008] for the history of the puzzle and discussions in PAL without the Kv operator.

An announcement 〈ψ〉 is interpreted as a model transformer which deletes the worlds that do not satisfy ψ.

It is shown in [Plaza, 1989] via a reduction to EL that the following axiomatization is sound and complete (cf. also [van Ditmarsch et al., 2007] for details):

where p ∈ P ∪ {⊤}.

Note that in [Plaza, 1989] Plaza did not make it clear whether the RE rule (replacement of equivalences) allows the substitutions of the formulas inside the announcements. Here we suppose so. 3

It can be shown that the following schemata are derivable/ admissible in PAL: 4

DIST! and NEC! will appear in our later discussions. In the sequel, we use EL to denote PAL without the so-called "reduction axioms" (i.e., !ATOM, !NEG, !CON, and !K). It is well-known that EL completely axiomatizes EL.

2.2 Adding the Kv operator

Given I, P and a set D of names, the language PALKv(I, P, D) (PALKv for short) is defined as:

where p ∈ P, i ∈ I, and d ∈ D. As before, we obtain an epistemic language ELKv(I,P,D) (ELKv for short) when we ignore the announcements in PALKv.

3 This makes our incompleteness result stronger.

4 For a thorough discussion on axiomatizations of PAL, see [Wang and Cao, 2013].

To interpret the new Kvid formulas, we need the assignment function VD : D × S → O in the epistemic models, where O is a non-empty set of objects. The semantics of Kvid is as follows:

Kv acts as a mixture of a modality and a predicate. It is not hard to see that Kvi also obeys the positive and negative introspections, namely the following two axioms are valid:

It is claimed (without a proof) in [Plaza, 1989] that adding Kv4 and Kv5 to EL completely axiomatizes ELKv.

Now a natural question is: how can we axiomatize PALKv? [Plaza, 1989] proposed the following extra axioms on top of PAL with Kv4, Kv5:

It is not known whether the above axiom schemata are enough to completely axiomatize PALKv. 5

In fact, the last three axioms above are superfluous. In the sequel, let us denote PAL+Kv4+Kv5+KKv as PALKVp. It is not hard to see that KvKv, !Kv, !nKv can all be derived in PALKVp by using Kv4, Kv5, T, KKv, !K and RE:

Proposition 2. (1) ⊢PALKVp 〈Kvic〉Kvid ↔ (Kvic∧Kvid);

1. ⊢PALKVp 〈φ〉Kvid →Ki(φ→ 〈φ〉Kvid);
2. ⊢PALKVp 〈φ〉¬Kvid →Ki(φ→ 〈φ〉¬Kvid).

Proof. For (1):

• (i) Kvic ↔KiKvic Kv4, T
• (ii) 〈Kvic〉Kvid ↔ 〈KiKvic〉Kvid RE
• (iii) 〈KiKvic〉Kvid ↔KiKvic ∧Kvid KKv
• (iv) 〈Kvic〉Kvid ↔ (Kvic ∧Kvid) MP(ii) (iii)

For (2):

• (i) Kvid →KiKvid Kv4

• (iii) 〈φ〉KiKvid ↔ (φ ∧Ki(φ→ 〈φ〉Kvid)) !K
• (iv) 〈φ〉Kvid →Ki(φ→ 〈φ〉Kvid) MP(ii)(iii)

In the later discussion we will focus on PALKVp.

3 Incompleteness of PALKVp

To prove the incompleteness of PALKVp, we will show that the following valid formula is not derivable in PALKVp:

5 Note that there is no obvious reduction axiom for Kvid and we will show it is impossible to reduce PALKv to ELKv in Section 6.

In order to show this, we design a semantics ⊩ on a class C of special models such that all the axiom schemata and rules of PALKVp are valid w.r.t. ⊩ on C but not θ. Namely we have for all PALKv formulas φ : ⊢PALKVp φ =⇒ C ⊩ φ and C ⊮ θ, thus we have ⊬PALKVp θ.

Inspired by the semantics developed in [Wang and Cao, 2013], we treat the announcement operator 〈φ〉 as a standard modality interpreted on models with φ transitions.

Definition 3. (Extended model) An extended (epistemic) model for PALKv is a tuple 〈S, {∼i| i ∈ I}, { φ→| φ ∈ PALKv}, V, VD〉 where

• 〈S, {∼i| i ∈ I}, V, VD〉 is a standard epistemic model for PALKv.
• For each PALKv formula φ, φ→ is a binary relation over S.

We now define the truth conditions of PALKv formulas on extended models (w.r.t. ⊩) as follows (we only show the clause which differs from ⊨):

Compared with the standard semantics w.r.t. ⊨, the only change is the interpretation of 〈φ〉ψ. It is clear that

Now we try to define a class of extended models where these two semantics get even closer on PALKv formulas.

Definition 5. (Normal extended epistemic model) An extended model M = 〈S, {∼i| i ∈ I}, { φ→| φ ∈ PALKv}, V, VD〉 is called normal if the following properties hold for any s, t ∈ S, any d ∈ D and φ ∈ PALKv:

PFUNC If M, s ⊩ φ then s has a unique φ-successor. If M, s ⊮ φ then s has no φ-successor.

PR If t ∼i t′ and s φ→ t, then there exists an s′ such that s ∼i s′ and s′ φ→ t′ .

Note that PFUNC and U-RE refer to ⊩. Let C be the class of all the normal extended models. We can show that PFUNC guarantees the validity of !NEG and !CON on C. Under the presence of PFUNC, the validities of !ATOM and !K are guaranteed by P-INV and the combination of NM (no miracles) and PR (perfect recall) respectively (cf. [Wang and Cao, 2013] for a similar proof in the standard PAL). Moreover, U-RE helps to make sure that RE is valid, and D-INV is used to show, under the presence of PR and NM, the validity of KKv. Based on these observations (proofs are omitted due to space limitation), we can prove the following:

Lemma 6. PALKVp is sound w.r.t ⊩ on C.

However, the ⊨-valid formulas θ is not ⊩-valid on C.

Proof. For simplicity we assume I = {1}, P = {p, q} and D = {d}. Consider the following model M (we omit the reflexive epistemic links and only show the necessary parts for evaluating the desired formula, with · and ◦ denoting the objects assigned to d):

q

Note that for any φ: M ⊮ (p ∨ q) ↔ K1φ, since K1φ will have a uniform truth value on t, s, s′ while p ∨ q is false only on the leftmost world. Similarly, for any φ: M ⊮ p ↔ K1φ and M ⊮ q ↔ K1φ. Thus although U-RE and D-INV hold in M, the assignments of d at s and s′ can be different from the assignments at the bottom four worlds. It is not hard to see that (a proper completion of) M is a normal extended model and

From Lemmata 6 and 7 we have:

Theorem 8. 〈p〉Kvid ∧ 〈q〉Kvid → 〈p ∨ q〉Kvid is not derivable in PALKVp, thus PALKVp is not complete w.r.t. ⊨ on epistemic models.

4 PAL with the relativized Kv operator

To prevent the counter example in the previous section, we need an axiom to guarantee that the assignments of the names in D will essentially stay the same after any announcements. A similar issue applies to the basic propositions but we can use !ATOM to guarantee the propositional invariance. In contrast, we cannot directly talk about the assignments in PALKv.

In this section, instead of trying to give an axiomatization of PALKv, we will discuss the language PALKvr where Kv is replaced by a more general operator, which can be viewed as a relativized version of Kv. The idea of relativizing a modal operator also appeared in [van Benthem et al., 2006] where the authors gave an axiomatization of PALCr which is PAL extended with a relativised version of the common knowledge operator.

Formally, the language of PALKvr is defined as follows:

where p ∈ P, i ∈ I, d ∈ D.

Kvi(φ, d) says that the agent i would know what d is if he were informed that φ is true. It is different from φ → Kvid, Kiφ → Kvid, and Ki(φ → Kvid). The distinction will become clear after understanding the following semantics w.r.t.

Now the original Kvi operator can be viewed as Kvi(⊤, ·). Therefore PALKvr is indeed an extension of PALKv. As before, we denote the announcement-free part of PALKvr as ELKvr .

We can see there is a similarity between an announcement and a condition in the relativized Kv operator, demonstrated by the following validity:

Note that !Kvr is also in the shape of the reduction axioms which push the announcement to the "inner" part of the formulas. Based on this observation, we can show, as what Plaza showed for PAL and EL, that PALKvr and ELKvr are equally expressive.

Theorem 9. PALKvr is equally expressive as ELKvr .

Proof. Since PALKvr is an extension of ELKvr thus PALKvr is no less expressive than ELKvr . We show that PALKvr is no more expressive than ELKvr by giving the following truth preserving translation t : PALKvr → ELKvr (we only show the non-trivial cases due to space limitation):

By defining a suitable complexity measure of PALKvr formulas as in the case for PAL (cf. [van Ditmarsch et al., 2007]), we can show the translation can eventually eliminate the announcement operators. We can also prove φ ≡ t(φ) for every φ ∈ PALKvr by induction on the structure of φ.

Now, as in the case of PAL, if we have a complete axiomatization of ELKvr , then we can also axiomatize PALKvr by using the reduction axioms:

Theorem 10. If ELKvr is completely axiomatized by S then S plus RE, !ATOM, !CON, !NEG, !K, and !Kvr completely axiomatizes PALKvr .

Note that we need to include the rule RE to facilitate the completeness proof via reductions (cf.[Wang and Cao, 2013] for detailed discussions in the context of PAL). In the next section we will axiomatize ELKvr in the single agent case.

5 Axiomatization of ELKvr1

As the reader may expect, axiomatizing ELKvr is much harder than the case of ELKv due to the condition in the relativized operator. In the rest of this section, we will provide a complete axiomatization of ELKvr for the single agent case (call it ELKvr1 ). Although all the new axioms that we propose also hold in the multi-agent case, there are still some difficulties in the completeness proof related to multiple agents, to which we will come back at the end of the paper.

5.1 SystemELKVr1

Based on single-agent EL, we propose the following extra axiom schemata and name the resulting system ELKVr1 :

DISTKvr is the distribution axiom for the relativised Kv operator (pay attention to the positions of ψ and φ in the consequent). Kvr 4 is a variation of the positive introspection axiom. Kvr⊥ stipulates the precondition of the Kv operator. Maybe the most interesting axiom is Kvr ∨ which will play a very important role in the later completeness proof. Intuitively, it handles the composition of the conditions in the relativized operator: suppose all the possible φ worlds agree on what d is and all the possible ψ worlds also agree on d, then the overlap between φ possibilities and ψ possibilities implies that all the φ ∨ ψ possibilities also agree on what d is.

It is not hard to see that the extra axioms are all valid:

Theorem 11. ELKVr1 is sound with respect to the class of epistemic models with assignments.

In the sequel, for readability, we will sometimes write ⊢ for ⊢ELKVr1 .

Seeing Kvr 4, the reader may miss a version of negative introspection ¬Kv(φ, d) → K¬Kv(φ, d). Actually it can be derived in ELKVr1 :

Proof.

Kvr ∨ can be generalized to arbitrary finite disjunctions due to an easy induction proof based on Kvr ∨.

Proposition 13. For any finite set of ELKvr1 formulas U:

5.2 Completeness of ELKVr1

In this subsection we prove that ELKVr1 is complete w.r.t. the class of epistemic models. As in normal modal logics, we will show that every consistent set of ELKvr1 formulas is satisfiable at some state in a canonical model. In defining the canonical model we need to borrow some ideas from the Henkin construction in first-order logic. The difficulties lie in the definition of the canonical model and the proof of the truth lemma for the new Kv operator, as we will explain later.

Canonical model

The canonical model Mc of ELKVr1 is 〈Sc ,∼c , V c , V c D 〉 where:

• Sc = MCS×{0, 1}, where MCS is the set of ELKVr1 - maximal consistent sets. That is, every maximal consistent set has two copies in Sc . We write φ ∈ s if φ is in the maximal consistent set of s. We write φ ∈ s ∩ t if φ ∈ s and φ ∈ t.
• s ∼c t iff {φ | Kφ ∈ s} ⊆ t.
• V c (p) = {s ∈ Sc | p ∈ s}.
• V c D (d, s) = |(d, s)|R. That is, V c D (d, s) is the equivalence class under the equivalence relation R defined below over {(d, s) | s ∈ Sc , d ∈ D}:

To show the above definition is well-defined, we need some simple propositions. The first is a standard exercise for EL:

Proposition 14. s ∼c t iff {φ | Kφ ∈ s} = {φ | Kφ ∈ t}, thus ∼c is an equivalence relation.

Based on Proposition 14 and Kvr 4, the following is immediate:

Based on the above two propositions and the definition of R, R is clearly reflexive and symmetric. The transitivity can be shown by using the axiom Kvr ∨, and then we have:

Proposition 16. R is an equivalence relation on {(d, s) | s ∈ Sc , d ∈ D}.

Remark 17. The readers may wonder why we used two copies of each maximal consistent set. Consider the following model:

It is not hard to see that both worlds satisfy exactly the same PALKvr formulas. However, we do need these two worlds to differentiate the assignments of the name d. These two copies of each maximal consistent set will play an important role in our proof of the completeness.

Completeness

In order to establish the truth lemma, we need to show that if Kv(φ, d) ̸∈ s then Mc , s ⊨ ¬Kv(φ, d). This is the most difficult part in the completeness proof which requires a few results below.

Given a state s ∈ Sc such that Kv(φ, d) ̸∈ s, let Z = {ψ | Kψ ∈ s} ∪ {φ} and X = {¬χ | Kv(χ, d) ∈ s}. We have the following observations.

Observation 18. 1. For any ¬χ ∈ X, {¬χ} ∪ Z is consistent.

1. Z is consistent and every element in X is also consistent.

Proof. In the sequel, we will write ⊢ as the shorthand for ⊢ELKVr1 .

For (1): Suppose not, then there exist ψ1, . . . , ψm such that ⊢ ψ1 ∧ · · · ∧ ψm ∧ φ → χ, equivalently, ⊢ ψ1 ∧ · · · ∧ ψm →

(φ → χ), and thus ⊢ Kψ1 ∧ · · · ∧ Kψm → K(φ → χ) by DISTK and NECK. Since Kψ1, . . . , Kψm ∈ s, K(φ → χ) ∈ s. Now by DISTKvr and the fact that Kv(χ, d) ∈ s, it follows that Kv(φ, d) ∈ s, contradiction.

For (2): followed immediately from (1) based on the nonemptiness of X due to Kvr⊥.

Recall that we want to show that Kv(φ, d) ̸∈ s implies Mc , s ⊨ ¬Kv(φ, d). To show that Kv(φ, d) does not hold on s, we need to construct two φ worlds which are linked with s but with different assignments for d. In order to do this, according to the definition of R, we have to make sure that these two worlds do not share any ψ such that Kv(ψ, d) ∈ s.

Now since ELKvr1 is denumerable, we can enumerate all formulas in X as ¬χ0, ¬χ1, . . . . Then we start to add these χi one by one to two copies of Z. The procedure is described as follows:

1. Let B0 = Z ∪ {¬χ0} and let C0 = Z.
2. If Bk and Ck are defined then we take ¬χk+1 ∈ X, and try to add it into B or C as follows: if it is consistent with Bk then let Bk+1 = Bk∪{¬χk+1} and let Ck+1 = Ck; otherwise let Bk+1 = Bk and let Ck+1 = Ck ∪ {¬χk+1}.

To construct two worlds out of B and C, we need to show B and C are consistent. From Observation 18, B0 and C0 are consistent. We only need to show that the second step preserves consistency, which amounts to the following lemma:

Lemma 19. Suppose Kv(φ, d) /∈ s. For any k, if Bk and Ck are consistent, then Bk ∪{¬χk+1} is inconsistent implies Ck ∪ {¬χk+1} is consistent.

Proof. Suppose not, then there is a k such that both Bk ∪ {¬χk+1} and Ck ∪ {¬χk+1} are inconsistent. Now let U = Bk\Z, V = Ck\Z, U = {χ | ¬χ ∈ U}, and V = {χ | ¬χ ∈ V }. Note that U, V, U, V are all finite.

We claim: there exist ψ1, . . . , ψl, ψ′1 , . . . , ψ′m, ψ′′ 1 , . . . , ψ′′ n ∈ {ψ | Kψ ∈ s} such that

• (i) ⊢ ψ1 ∧ · · · ∧ψl ∧ φ ∧ ∧ U →χk+1,
• (ii) ⊢ ψ′1 ∧ · · · ∧ψ′m ∧ φ ∧ ∧ V →χk+1,

(i) and (ii) are immediate from the inconsistency of Bk ∪ {¬χk+1} and Ck ∪{¬χk+1}. For (iii), first note that for any χ ∈ V , {¬χ} ∪ Bk is inconsistent due to the construction of Bk. Therefore for each χ ∈ V there exist θ1, . . . , θh ∈ {ψ | Kψ ∈ s} such that:

Now since V is a finite set, we collect all such θ for each χ ∈ V to obtain (iii).

From (i) - (iii), NECK, DISTK and the fact that

• (iv) K((φ ∧ ∧ U) →χk+1) ∈ s,
• (v) K((φ ∧ ∧ V ) →χk+1) ∈ s,
• (vi) K((φ ∧ ∧ U) → ∧ V ) ∈ s.

In the following, we will show that ˆK(χk+1 ∧ ∧ V ) ∈ s. First we claim ˆK(φ ∧ ∧ U) ∈ s. Suppose not, then K¬(φ ∧ ∧ U) ∈ s, thus ¬(φ ∧ ∧ U) ∈ Bk. Due to the construction of Bk we know φ and U are in Bk, thus Bk is inconsistent, contradicting the assumption. Therefore ˆK(φ∧∧ U) ∈ s thus by (iv), (vi) we have ˆK(χk+1 ∧ ∧ V ) ∈ s.

By our assumption, for any χ ∈ V ∪ {χk+1} we have Kv(χ, d) ∈ s. Now based on this fact and ˆK(χk+1 ∧ ∧ V ) ∈ s, we can use Proposition 13, and obtain the following:

Now let us change the from of (v) to the following:

Based on (v′ ), (vii) and DISTKvr , we have Kv(φ, d) ∈ s, contradiction.

Based on Lemma 19, using Lindenbaum-like argument, we have the following:

Lemma 20. There are X0,X1 such that X0 ∩ X1 = ∅, X0 ∪ X1 = X, and both B = Z ∪ X0 and C = Z ∪ X1 are consistent. Therefore B and C can be extended into two maximal consistent sets.

Note that the above lemma does not rule out the possibility that the two maximal consistent sets being the same. We will handle this by using different copies in the canonical model.

Now we will prove the completeness of ELKVr1 , i.e., every valid ELKvr1 formula is ELKVr1 -provable. As usual, we construct the canonical model which can satisfy each consistent set of ELKvr1 formulas.

Lemma 21 (Truth Lemma). For any ELKvr1 formula φ, φ ∈ s iff Mc , s ⊨ φ.

Proof. By induction on φ. We will only show the case of Kv(φ, d) in detail since other cases are standard exercises as in normal modal logic. The direction from Kv(φ, d) ∈ s to Mc , s ⊨ Kv(φ, d) is straightforward based on the induction hypothesis and our definition of R.

Now for the converse, suppose that Kv(φ, d) /∈ s, we need to showMc , s ⊭ Kv(φ, d). Recall that Z = {ψ | Kψ ∈ s} ∪ {φ} and X = {¬χ | Kv(χ, d) ∈ s}. Lemma 20 guarantees that we can find two (possibly identical) maximal consistent sets B′ and C ′ such that Z ∪X0 ⊆ B′ and Z ∪X1 ⊆ C ′ for some X0, X1 satisfying X = X0 ∪ X1.

Now we can construct two different worlds t0 = (B′ , 0) and t1 = (C ′ , 1). It is clear that t0, t1 ∈ Sc . Since Z ⊆ t0∩t1 we have t0 ∼c s ∼c t1, andMc , t0 ⊨ φ andMc , t1 ⊨ φ due to the induction hypothesis. Now we claim ((d, t0), (d, t1)) ̸∈ R. To see this, consider any Kv(χ, d) ∈ s (equivalently, any ¬χ ∈ X), we have either χ ̸∈ B′ or χ ̸∈ C ′ since X0 ∪X1 = X and B′ , C′ are consistent.

Based on the above lemma it is routine to show:

Theorem 22. ELKVr1 is sound and complete.

Based on this theorem and Theorem 10, ELKVr1+!ATOM+!NEG+!CON+!K+!Kvr is sound and complete for PALKvr1 .

6 Expressivity

In this section we compare the expressivity of the various logical languages that we discussed in this paper. The results are summarized in the following (transitive) diagram:

Note that, in contrast to the axiomatization result, in this section all the results also hold in multi-agent cases.

Theorem 9 already shows that ELKvr and PALKvr are equally expressive. In the sequel, to complete the diagram, we first show that ELKv is strictly less expressive than PALKv then prove that ELKvr is equally expressive as PALKv. To compare ELKv and PALKv, we give two models that cannot be distinguished by any ELKv formula but can be distinguished by a PALKv formula. First we need a notion of bisimulation for ELKv models.

Definition 23. Let M1 = 〈S1, {∼1i | i ∈ I}, V1, V 1 D 〉 and M2 = 〈S2, {∼2i | i ∈ I}, V2, V 2 D 〉 be two models. A d-bisimulation between M1 and M2 is a non-empty relation R ⊆ S1 × S2 such that if s1Rs2 then the following requirements hold for all i ∈ I:

Inv:

V1(s1) = V2(s2);

Zig: if s1 ∼1i t1, then there exists t2 ∈ S2 such that s2 ∼2i t2 and t1Rt2;

Zag:

Kv-Zig: if t1 ∼1i s1 ∼1i t′1 , and V 1 D (d, t1) ̸= V 1 D (d, t′1 ) for some d then there exist t2, t′2 ∈ S2 such that t2 ∼2i s2 ∼2i t′2 , and V 2 D (d, t2) ̸= V 2 D (d, t′2 );

if s2 ∼2i t2, then there exists t1 ∈ S1 such that s1 ∼1i t1 and t1Rt2;

Kv-Zag: if t2 ∼2i s2 ∼2i t′2 , and V 2 D (d, t2) ̸= V 2 D (d, t′2 ) for some d then there exist t1, t′1 ∈ S1 such that t1 ∼1i s1 ∼1i t′1 , and V 1 D (d, t1) ̸= V 1 D (d, t′1 ).

We write M1, s1 ↔d M2, s2 iff there is a d-bisimulation betweenM1 andM2 linking s1 and s2.

We can show d-bisimulation preserves ELKv formulas: Theorem 24. If M1, s1 ↔d M2, s2, then M1, s1 ≡ELKv M2, s2.

Proof. Suppose that M1, s1 ↔d M2, s2, we proceed by induction on the structure of ELKv formula φ. Here we only show the non-trivial case for Kvid.

Suppose M1, s1 ⊭ Kvid, then there exists t1, t′1 with t1 ∼1i s1 ∼1i t′1 and V 1 D (t1, d) ̸= V 1 D (t′1 , d). By Kv-Zig, there exist t2, t′2 ∈ S2 such that t2 ∼2i s2 ∼2i t′2 , and V 2 D (d, t2) ̸= V 2 D (d, t′2 ). Therefore M2, s2 ⊭ Kvid.

The other direction can be proved similarly by using KvZag.

Now consider the following two models (using ◦ and · for the objects assigned to d):

It is not hard to see that these two models are d-bisimiliar linking s and s′ . However, we can distinguish s and s′ easily by a PALKv formula [p]Kv1d.

Based on this example and the fact that PALKv is an extension of ELKv, we have the following result:

Theorem 25. PALKv is strictly more expressive than ELKv.

The readers may recall a similar comparison in the context of (relativised) common knowledge between ELC, ELCr , PALC and PALCr in [van Benthem et al., 2006] where PALC is strictly less expressive than PALCr . However, in our case the situation is different.

Theorem 26. ELKvr is no more expressive than PALKv.

Proof. Define a translation function t : ELKvr → PALKv as follows (we only show the non-trivial clause):

It is not hard to show that t can eliminate the Kvi(φ, ·) operators while preserving the truth of formulas.

Now based on Theorem 26, the fact that ELKvr and PALKvr are equally expressive, and the fact that PALKvr is clearly no less expressive than PALKv, the following corollary is immediate:

Corollary 27. PALKvr , PALKv and ELKvr are equally expressive.

7 Conclusion and Future work

In this paper, we proved that the system PALKVp is not complete. On the other hand, ELKVr1 is complete for single agent ELKvr . Based on this and Theorem 10, ELKVr1+!ATOM+!NEG+!CON+!K+!Kvr is complete for PALKvr1 . We conjecture that PALKvr1 is decidable, since a version of filtration technique should work to show a small model property as in normal modal logic. We leave it to a

future occasion.

It is not very clear whether multi-agent ELKvr can be completely axiomatized by the multi-agent version of ELKVr1 . Two main difficulties in the completeness proof are as follows:

1. The definition of R in the canonical model is to be revised: we may need to take the reflexive transitive closure of R to make it an equivalence relation.
2. The definition of ∼ci also needs to be revised.

To see the second point, consider the following model:

It is clear that these two worlds satisfy exactly the same set of PALKvr formulas. However, it is impossible to embed this model in our previously defined canonical model, since these two worlds must be connected by ∼2 if they have the same maximal consistent sets. We leave the multi-agent axiomatization and the applications of the new relativized Kv operator for future work.