Epistemic Quantified Boolean Logic: Expressiveness and Completeness Results

1 Introduction

The inspiration for the present contribution comes from a series of papers [van Ditmarsch et al., 2009; 2011; 2012] introducing the language of Local Properties in Modal Logic. LPML extends propositional modal logic with operators to express local properties of Kripke frames. Indeed, it is well-known that there is a tight correspondence between modal formulas and properties of Kripke frames as expressed in first-order logic [van Benthem, 1976; Blackburn et al., 2001]. As an example, let θ(a, b, p) be the modal principle Kap → Kbp and let Θ(a, b, x) represent the first-order formula ∀y(Rb(x, y) → Ra(x, y)). Then θ corresponds with Θ in the following sense: θ(a, b, p) holds at a state w in a Kripke frame F iff Θ(a, b, x/w) is true in F, that is, every Rb-accessible world from w is also Ra-accessible. Loosely speaking, given an epistemic interpretation of modal operators, to model a situation in which agent b knows everything that agent a knows, simply add θ to the axiom system, and assume Θ on the class of frames.

However, adding θ as an axiom to a modal logic would automatically enforce the property expressed by Θ to hold in any state of a frame for the logic, i.e., θ becomes globally true. It is impossible in 'standard' modal logic, to express something like: in state w, agent b knows everything that a knows, and agent c knows that, but d does not.

Moreover, truth in a model (as opposed to validity in a frame) of θ is a necessary but not sufficient condition for Θ to hold. That is, if Θ holds in a Kripke frame F, then θ is

Wiebe van der Hoek

Department of Computer Science University of Liverpool, UK wiebe.van-der-hoek@liverpool.ac.uk

true on any pointed model (M, w) built on F. However, the converse does not hold in general: it may be that θ holds in (M,w), without Θ being true. In other words, θ may hold at w because of some specifically well-chosen assignment V that is part ofM.

To address the issues above, LPML considers, for every first-order property Θ of interest, a new modal operator ⊡Θ, whose interpretation is such that the modal formula ⊡Θ(⃗a) holds at state w for some tuple ⃗a of agents iff Θ(⃗a, x/w) is true in F. Formally, this connection is made through models of the form 〈F, I, V 〉, where V is an assignment of propositional atoms, and I is an interpretation relating ⊡Θ(⃗a) to Θ(⃗a, x). Indeed, now structural properties are no longer determined by validities on frames, but by truths in the model.

In this paper we introduce a modal extension of quantified boolean logic to express formulas such as ⊡Θ(⃗a). Specifically, for Θ(a, b, x) = ∀y(Rb(x, y) → Ra(x, y)), the formula ⊡Θ(a, b) is shown to be equivalent to the universal closure ∀p(Kap → Kbp) of θ(a, b, p), which is a formula of epistemic quantified boolean logic (EQBL). Modal quantified boolean logic originates from the seminal work by Fine and Bull in the late 60's [Bull, 1969; Fine, 1970], which established axiomatisability and complexity results for monomodal languages. However, given the high complexity and some non-axiomatisability results of the formalism, modal quantified boolean logic is comparatively much less explored than its non-modal and non-quantified counterparts. Our main aim in this paper is to show that (multi-modal) EQBL provides us with the expressive power to represent and reason about epistemic properties of agents - such as those considered in [van Ditmarsch et al., 2012] - at a reasonable computational cost.

Scheme of the paper. In Section 2 we introduce the syntax and semantics of multi-agent EQBL. Section 3 is devoted to the analysis of the expressive power of EQBL through a comparison with monadic second-order logic (MSO). In particular, we show that EQBL is strictly more expressive than LPML. In Section 4 we provide novel axiomatisations of EQBL on a number of classes of interest; while in Section 5 we establish that the model checking problem for EQBL is no harder than for (non-modal) quantified boolean logic. We conclude in Section 6 by comparing these results with related literature, and by pointing to future research.

2 Syntax and Semantics

The Formal Language We first introduce the syntax of EQBL. In what follows we fix a set AP of atomic propositions and a finite set Ag of indexes for agents.

Definition 1 (EQBL) For p ∈ AP and a ∈ Ag, the formulas in EQBL are defined by the following BNF:

Our language contains epistemic formulas Kaφ, for every agent name a ∈ Ag, that are read as "agent a knows that φ", as well as formulas Cφ that intuitively mean "φ is common knowledge" in the set Ag of agents [Meyer and van der Hoek, 1995]. We consider the standard abbreviations for ∧, ∨, ∃, while ♯ and Q are placeholders for any unary operator ¬, Ka, C and any quantifier ∀, ∃ respectively. Also, Maφ is a shorthand for ¬Ka¬φ. The set fr(φ) of free atomic propositions in a formula φ is recursively defined as follows:

Sentences in EQBL are formulas φ with an empty set of free propositions, i.e., fr(φ) = ∅. The set bnd(φ) of bound propositions in φ is defined as standard as the set of all propositions q appearing in the scope of any quantifier Qq. Hereafter we assume w.l.o.g. that for each formula φ, fr(φ) and bnd(φ) are disjoint.

Definition 2 (Substitution) Given an atom p ∈ fr(φ), an EQBL formula ψ is free for p in φ iff p does not appear in φ within the scope of any quantifier Qq for q free in ψ.

If ψ is free for p ∈ fr(φ), then we inductively define the substitution φ[p/ψ] as follows:

q[p/ψ] = {q for q different from p ψ otherwise (♯φ)[p/ψ] = ♯(φ[p/ψ]) (φ→φ′ )[p/ψ] = (φ[p/ψ]) → (φ′ [p/ψ]) (∀rφ)[p/ψ] = ∀r(φ[p/ψ]), for r different from p

Intuitively, ψ being free for p in φ means that a substitution of p by ψ in φ does not create any new binding. For instance, ¬q is free for p in ∃t(t → p) but not in φ = ∃q(p ↔ q).

Example 1 As an example of the expressive power of EQBL, consider the specification put forward in the introduction: agent b knows everything that a knows, and agent c knows this fact, but d does not. This can be recast in EQBL as the following formula:

In particular, we can reason further about agent d's knowledge. Indeed, agent d might know that a knows something ignored by b, without being able to explicitly point out the content of a's extra knowledge. This can be recast in EQBL by the following de dicto formula:

However, d could actually know some fact, also known by a but ignored by b, as expressed in the de re formula:

We remark intuitively that (2) is strictly stronger than and entails (1). EQBL allows us to distinguish the two readings - de re and de dicto - of individual knowledge. ■

Kripke Frames and Models To interpret formulas in EQBL we consider multi-modal Kripke frames and models, defined as follows.

Definition 3 A Kripke frame is a tuple F = 〈W, D, R〉 where

• W is a set of possible worlds;
• D ⊆ 2W is the domain of propositions;
• R : Ag → 2W×W assigns a binary relation on W to each agent index in Ag.

As standard, for a ∈ Ag, Ra is the accessibility relation between worlds in W. In the rest of the paper we assume that each Ra is an equivalence relation (i.e., symmetric, transitive and reflexive), consistently with the epistemic reading of modal operators [Meyer and van der Hoek, 1995]. We will state explicitly when this is not the case. Also, for each agent index a ∈ Ag and w ∈ W, we define Ra(w) = {w′ | Ra(w,w′ )}. Moreover, differently from standard Kripke frames [Blackburn et al., 2001], we have a set D ⊆ 2W of "admissible" propositions for the interpretation of atoms and quantifiers.

To evaluate EQBL formulas we introduce assignments as functions V : AP → D. Also, for U ∈ D, the assignment V p U assigns U to p and coincides with V on all other atomic propositions. Hence, atoms can only be assigned propositions in D ⊆ 2W . A Kripke model is then a pair M= 〈F, V 〉. In what follows we consider particular classes of Kripke frames and models. Specifically, we say that a frame is full whenever D = 2W ; while it is boolean if D is closed under intersection, union and complementation, i.e., it is a boolean algebra. The interest of these classes of frames, which have already appeared in the literature [Fine, 1970; Mares and Goldblatt, 2006], will become apparent later on. Finally, a model is full (resp. boolean) whenever the underlying frame is.

Definition 4 (Semantics of EQBL) We define whether a Kripke model M = 〈F, V 〉 satisfies an EQBL formula ϕ at world w, or (M,w) |= ϕ, as follows, where R+ denotes the transitive closure of ⋃a∈Ag Ra (clauses for propositional connectives are trivial and thus omitted).

Hence, a quantified formula ∀pψ (resp. ∃pψ) is true at world w iff for every (resp. some) assignment of propositions in D to p, ψ is true. Further, as standard in epistemic logic [Meyer and van der Hoek, 1995], (M,w) |= Cψ iff (M,w′ ) |= ψ for every world w′ reachable from w, i.e., for every w′ s.t. there exists a sequence w0, . . . ,wk of worlds and (i) w0 = w, (ii) wk = w′ , and (iii) for every i < k, Ra(wi, wi+1) for some a ∈ Ag.

We now define various notions of truth and validity. First, we write (F, V,w) |= φ as a shorthand for (〈F, V 〉,w) |= φ. Then, we say that φ is true at w, or (F,w) |= φ, iff (F, V, w) |= φ for every assignment V ; φ is valid in a frame F, or F |= φ, iff (F,w) |= φ for every world w in F; φ is valid in a class K of frames, or K |= φ, iff F |= φ for every F ∈ K. Also, φ is true in a model M, or M |= φ, iff (M,w) |= φ for every world w. Finally, φ is satisfiable iff there exists a model M s.t. (M, w) |= φ for some world w.

Hereafter we consider the class Kall of all Kripke frames, the class Kbool of all boolean frames, and the class Kfull of all full frames. If we let Th(K) = {φ ∈ EQBL | K |= φ}, then clearly Th(Kall) ⊆ Th(Kbool) ⊆ Th(Kfull). We will show that these inclusions are indeed strict.

Further classes of frames could be introduced, for instance the class where every EQBL (resp. modal) formula defines a proposition. However, neither class is directly relevant for the results below and their introduction requires a non-trivial generalisation of Kripke frames [Mares and Goldblatt, 2006]. Thus, such extensions are beyond the scope of the present paper. Also, notice that the Kripke frames in Def. 3 are related to general frames [Blackburn et al., 2001], as both assume some sort of algebraic structure on the set D of proposition. Nonetheless, the use of quantification makes EQBL strictly more expressive than the theory of general frames.

Example 2 We revisit the example of [van Ditmarsch et al., 2012, Section 4.3], and consider a simple card game with three players 1, 2, and 3. The cards are identified by their colour: red (r), white (w), and blue (b). We assume to have 9 propositional atoms {ri,wi, bi | 1 ≤ i ≤ 3}, where for instance w1 denotes that agent 1 holds the white card. Also, all agents know the cards of the game, and that each agent can see his own card, but not that of the other players. The situation after which each player is dealt a card can be modeled by model M in Fig. 1. The state rwb inMdenotes the situation where player 1 holds the red card, 2 holds white and 3 holds blue. In this state, we have for instance that

i.e., if the deal is rwb, then 1 holds the red card, he knows this, but 2 does not know it, and, finally, 1 knows that 2 does not know that 1 holds the red card. In particular, we have

i.e., for every player, there is a fact that the others don't know.

Now let us assume that M is full. Note that we also have

i.e., there exists an assignment for w1 so that all players have the same information: in fact, there exists an assignment to atomic propositions such that all agents know the same (assign W to each propositional atom)! However, the intended interpretation of atomic propositions should not consider such assignments. Any assignment should satisfy

That is, we only consider deals where each player holds a card, and no player holds two. Note that this still allows for 'un-intended' assignments, allowing for example for ∃w1(w1 ∧¬K1w1) to hold. Our assignments should also satisfy the property that every player knows its own card (koc)

Now, (3) can be made stronger by replacing each occurrence of ∃pi(. . . ) by ∃pi(deal ∧ koc ∧ . . . ). Note that each agent is also aware that the others know something that they don't know: which is for instance expressed by the following de dicto property:

Let us know bring some dynamics to our story (for details on Dynamic Epistemic Logic, see [van Ditmarsch et al., 2007]). Suppose player 1 truthfully announces publicly that he does not own the white card. Such an announcement leads to the updated model N of Fig. 1, which is obtained fromM by simply removing all states in which w1 holds. Indeed, we have

That is, 3 knows at least what 1 knows. In fact, 3 knows strictly more than 1, since we have (N, rwb) |= K3b3 ∧ ¬K1b3. Moreover, not only does player 3 know more than player 1, but player 2 knows that as well:

Note how (5) not only expresses that player 2 knows that 3 knows everything that 1 knows, but also that 2 knows de dicto that 3 knows more than 1, while 3 knows de re that this is the case. ■

We now show a preliminary result used in the completeness proof: an EQBL formula φ is valid iff it is valid in the class of frames where the operator C is the universal modality, defined in every such frame F as (F, V,w) |= Cψ iff for all w′ ∈ W, (F, V,w′ ) |= ψ. First of all, we define the submodel generated by a world w as follows.

Definition 5 (Submodel) Given a model M = 〈W,D,R, V 〉 and a world w ∈ W, the submodel generated by w is the model Mw = 〈Ww,Dw,Rw, Vw〉 s.t.

• Ww is the set of worlds reachable from w, i.e., Ww = (⋃a∈Ag Ra)+(w);
• Dw = {Uw ⊆ Ww | Uw = U ∩Ww for some U ∈ D};
• for every a ∈ Ag, Rw,a = Ra ∩W 2w ;
• for every p ∈ AP, Vw(p) = V (p) ∩Ww.

If the frame F = 〈W,D,R〉 belongs to Kall (resp. Kbool, Kfull), then also Fw = 〈Ww,Dw,Rw〉 ∈ Kall (resp. Kbool, Kfull). We can now prove the following lemma on the preservation of EQBL formulas on generated submodels.

Lemma 1 Let M = (F, V ) be a Kripke model and w ∈ W. For every w′ ∈ Ww and φ ∈ EQBL,

Now let Kuniv be the class of universal Kripke frames, that is, every world is reachable from any other world according to (⋃a∈Ag Ra)+.

By Corollary 2 we can assume w.l.o.g. that, as long as we are interested in validity, the common knowledge operator C acts as a universal modality on the set W of possible worlds. This fact will be used later in the completeness proof.

In what follows we analyse the formal properties of EQBL starting with its expressiveness.

3 Expressiveness

In this section we analyse the expressiveness of (multimodal) epistemic quantified boolean logic and define a correspondence between EQBL and monadic second-order logic (MSO), which is a language suitable to describe properties of frames. First of all, given a Kripke frame F = 〈W,D,R〉 on a set AP of atomic propositions, we consider an MSO alphabet containing binary predicate constants RC and Ra for every agent index a ∈ Ag, and a unary predicate variable P for every atom p ∈ AP . We use the same symbols for semantical and syntactical elements, as context will disambiguate. Then, MSO formulas ψ are defined in BNF as follows:

An assignment σ is a function associating a world w ∈ W to every individual variable x and a set U ∈ D to every predicate variable P . For w ∈ W and U ∈ D, the variants σxw and σP U are defined similarly to EQBL.

Definition 6 (Semantics of MSO) We define whether a frame F satisfies an MSO formula ϕ for an assignment σ, or (F, σ) |= ϕ, as follows (clauses for propositional connectives are omitted):

(F, σ) |= P(x) iff σ(x) ∈ σ(P) (F, σ) |= Ra(x, y) iff Ra(σ(x), σ(y)) (F, σ) |= RC(x, y) iff (⋃a∈Ag Ra)+(σ(x), σ(y)) (F, σ) |= ∀xψ iff for all w ∈ W, (F, σxw) |= ψ (F, σ) |= ∀Pψ iff for all U ∈ D, (F, σPU ) |= ψ

We briefly remark that equality (modulo D) is definable in MSO as x = y ::= ∀P(P(x) ↔ P(y)) ∧ ∧i∈Ag∪{C} ∀z(Ri(x, z) ↔ Ri(y, z)). Having introduced the formal machinery, we move on to define the extension to EQBL of the standard translation between modal and firstorder logic. Then, ST is the translation between EQBL and MSO defined as follows:

STx(p) = P(x) STx(¬φ) = ¬STx(φ) STx(φ→φ′ ) = STx(φ) →STx(φ′ ) STx(Kaφ) = ∀y(Ra(x, y) →STy(φ)) STx(Cφ) = ∀y(RC(x, y) →STy(φ)) STx(∀pφ) = ∀P(STx(φ))

Clearly, for every EQBL formula φ, STx(φ) is an MSO formula where x is the only free individual variable. If ψ is a purely propositional modal formula, then STx(ψ) is a firstorder formula, as obtained via the standard translation.

The following results show that structural properties of frames can be expressed locally through EQBL formulas.

Lemma 3 For every model M = 〈F, V 〉, world w, and formula ψ in EQBL, (M,w) |= ψ iff (F, σ) |= STx(ψ), whenever σ(x) = w and σ(Pi) = V (pi).

As a consequence of Lemma 3 there is a one-to-one correspondence between EQBL formulas and their standard translations in MSO in the following sense: a Kripke frame F validates the universal closure ∀⃗ pψ of an EQBL formula ψ iff the MSO property ∀x∀ ⃗ PSTx(ψ) holds in F, where ⃗ P are all the unary predicates appearing in STx(ψ). We observe that this is not the case in propositional modal logic. For instance, for the McKinsey formula KaMap → MaKap there is no first-order principle α such that α holds in all and only frames validating the McKinsey formula.

We now compare the expressiveness of EQBL to the extended modal logic LPML introduced in [van Ditmarsch et al., 2012] to formulate local properties of models. Table 1 corresponds to Table 1 in [van Ditmarsch et al., 2012]. Formulas θ(⃗a, ⃗ p) belong to propositional epistemic logic, while Θ(⃗a, x) are first-order formulas with at most one free variable x. The formulas ⊡(⃗a) appear in [van Ditmarsch et al., 2012] precisely to describe local properties of models. The satisfaction of ⊡-formulas in Kripke models is given as: (F, V,w) |= ⊡(⃗a) iff (F, σ) |= Θ(⃗a, x) for σ(x) = w, that is, property Θ holds of world w. By the following corollary we obtain that, as regards full Kripke models, EQBL is as expressive as LPML.

Corollary 4 For every full model M, world w, and formulas θ(⃗a, ⃗ p) and ⊡(⃗a) in Table 1, (M,w) |= ∀⃗ pθ(⃗a, ⃗ p) iff (M,w) |= ⊡(⃗a).

From Corollary 4 we conclude that EQBL can deal with all the examples of [van Ditmarsch et al., 2012, Table 1] that LPML deals with. Furthermore, LPML provides a completeness proof for a language in which ⊡ and θ⊡ are connected through some specific axiom and inference rule, and moreover θ⊡ is locally good for Θ [van Ditmarsch et al., 2012, Definition 11]. In other words, for first-order properties Θ for which there is no corresponding propositional modal formula θ, LPML cannot express Θ locally. We now show that EQBL

is sometimes able to express such Θ. Consider the following EQBL formula:

It is not difficult to see that (6) holds on frames where states have at least two successors: a first-order property that is not modally definable [Blackburn et al., 2001], and hence something that cannot be expressed in LPML.

Moreover, there are instances of modal properties expressible in EQBL that are not first-order definable, and hence cannot again be dealt with in LPML locally. Consider the following EQBL formula τ = ∀p(Kap → Kbp) ∧ ∀q(KbKaq → Kbq). Then we can prove the following result.

Lemma 5 Let F be a full frame and R+ a the transitive closure of Ra. Then, (F,w) |= τ iff R+ a (w) ⊆ Rb(w).

Since being the transitive closure is not first-order definable (even though it is modally definable), this shows that EQBL is strictly more expressive than the language of [van Ditmarsch et al., 2012], as the latter cannot express τ locally.

To conclude our comparison between EQBL and LPML, we observe that the ⊡ operators act in fact like linguistic black boxes, bringing the metatheory language of first-order logic into the object language of modal logic. On the other hand, EQBL is more transparent, as everything is done in the object language. In addition, for the first-order conditions in [van Ditmarsch et al., 2012] there must always be a suitable modal counterpart. Indeed, the axioms Ax⊡ : ⊡(⃗a) → θ⊡(⃗a, ⃗ p) in [van Ditmarsch et al., 2012] make sense only as long as there is a propositional modal formula θ⊡ locally good for ⊡, and this is not always the case. In what follows we will show that none of the above has to be assumed to axiomatise EQBL.

Finally, we briefly state one more result showing that EQBL is strictly more expressive than propositional modal logic. In the following lemma we consider Kripke frames and models where each Ra is simply a binary relation.

Lemma 6 Let F be a full Kripke frame, F |= ∃p(Kap ∧ ¬p) iff F is irreflexive.

Since irreflexivity is not expressible in standard modal logic [Blackburn et al., 2001], Lemma 6 illustrates the wellknown fact that EQBL is more expressive than modal logic.

4 Completeness

In this section we present axiomatisations for the sets of validities on the classes Kall, Kbool, and Kfull of Kripke frames built on sets Ag of agent indexes and AP of atomic propositions. We first present a logic for Kall, where ✷ is a placeholder for any modal operators C and Ka for a ∈ Ag.

The logic Kall extends the standard multi-modal epistemic logic S5Cn , including common knowledge, with axioms for quantification. It also includes the Barcan formula BF. The logic Kbool extends Kall through axiom

where ψ is any boolean formula. Finally, Kfull extends Kbool through axiom

where ψ is any EQBL formula, as well as axiom At:

Intuitively, the first two conjuncts of axiom At express that the interpretation of p is an atom in D (i.e., a minimal, nonempty element according to order ⊆ on D). Moreover, by the third conjunct, for every a ∈ Ag, the worlds in the interpretation of p are all connected by each Ra, i.e, the interpretation of p is a clique for every Ra. This means that all worlds in the interpretation of p are actually indistinguishable. The notions of proof and theoremhood ⊢ are defined as standard.

Mono-modal versions of Exbool and Exfull (without common knowledge) were considered in [Fine, 1970]. Hereafter, we extend these results to a multi-agent epistemic setting, including common knowledge, and prove generalised completeness in Section 4.1.

We now state the soundness and completeness results for each logic K w.r.t. the corresponding class K of Kripke frames, starting with the former.

Theorem 7 (Soundness) For every l ∈ {all, bool, full}, for every EQBL formula φ, ⊢Kl φ implies Kl |= φ.

As regards completeness, we show that if a formula is consistent, then we can construct a relevant model that satisfies it. For logics Kall and Kbool we need models whose underlying frame is any frame and a boolean algebra respectively. As regards Kfull we need to introduce some more definitions. First of all, a frame F is atomic iff for every w ∈ W there is an atom U ∈ D (i.e., a minimal, non-empty U ∈ D, according to order ⊆) such that w ∈ U. Moreover, the atom U has to be a clique according to every Ra, i.e., for every w,w′ ∈ U, Ra(w,w′ ). Further, F is complete iff the domain D is closed under infinite unions and intersections. Notice that we use 'complete' with two different meanings: (i) semantical completeness of a logic, and (ii) algebraic completeness. The context will disambiguate. We use at and com as subscripts to designate the respective classes of frames. Clearly, every full frame is boolean, atomic and complete. Hence, Th(Kbool,at,com) ⊆ Th(Kfull). The converse follows from the next well-known algebraic result, which is a consequence of Stone's representation theorem.

Theorem 8 ([Givant and Halmos, 2009]) Every complete atomic Boolean algebra is isomorphic to the powerset of some set.

By Theorem 8 we can prove the following lemma.

In [Fine, 1970] Fine remarks that the language of modal quantified boolean logic is not rich enough to express completeness. We prove that this is the case for EQBL as well.

By combining Lemma 9 and 10 we obtain that Th(Kfull) = Th(Kbool,at). Thus, for our purposes it is sufficient to prove completeness of Kfull w.r.t. Kbool,at.

Theorem 11 (Completeness) For every l ∈ {all, bool, full}, for every EQBL formula φ, Kl |= φ implies ⊢Kl φ.

If ⊬Kl φ then we construct a Kripke model M = 〈F, V 〉, the canonical model for φ, that satisfies ¬φ. Moreover, F is shown to belong to the relevant class of Kripke frames. This implies that Kl ̸|= φ. Hereafter we discuss the case for l = full. We omit the subscript l whenever clear by the context.

As regards the logic Kfull we remarked above that it is sufficient to prove completeness w.r.t. Kbool,at. To do so, we observe that axiom At ensures that the canonical model contains an atom Uw for every state w ∈ W, and that all worlds in these atoms are related by each Ra, provided that the accessibility relation RC = {(w′ ,w′′ ) | {ψ | Cψ ∈ w′} ⊆ w′′} is the universal relation on W. To enforce the latter fact, we restrict W to the set of states reachable from state v ⊇ {¬φ}, for a consistent φ, through the relation (⋃a∈Ag Ra)+. By doing so, we guarantee that D is indeed an atomic boolean algebra, that is, F ∈ Kbool,at.

We summarise the soundness and completeness results for our logics w.r.t. the relevant classes of frames.

Theorem 12 (Soundness and Completeness) For every l ∈ {all, bool, full}, the logic Kl is sound and complete w.r.t. the class Kl of Kripke frames.

4.1 Generalised Completeness

One nice feature of EQBL is that we can extend the completeness results in the previous section by considering extra axioms expressing properties of frames. Specifically, let Kl be any of the axiomatisations above, for l ∈ {all, bool, full}. Then, if we extend Kl with the universal closure ∀⃗ pψ of an EQBL formula ψ, the resulting calculus Kl + ∀⃗ pψ is sound and complete w.r.t. the class of frames satisfying the MSO condition ∀x∀ ⃗ PSTx(ψ).

Theorem 13 Let ψ be an EQBL formula, then the logic Kl + ∀⃗ pψ is sound and complete w.r.t. the class of Kl frames satisfying ∀x∀ ⃗ PSTx(ψ).

By the result above we immediately obtain that for every formula θ(⃗a, ⃗ p) in Table 1, Kl + ∀pθ(⃗a, ⃗ p) is sound and complete w.r.t. the class of Kripke frames satisfying ∀x∀ ⃗ PΘ(⃗a, x). More generally, there is a one-to-one correspondence between an EQBL axiom ∀⃗ pθ and the MSO condition ∀x∀ ⃗ PSTx(θ) on the corresponding class of sound and complete frames. Notice that this is not the case in propositional modal logic.

5 Model Checking EQBL

This section hinges on the model checking problem for EQBL, defined as follows.

Definition 8 (Model Checking) Given an EQBL formula φ and a finite model M, determine whether M |= φ.

Then, we are able to prove the following complexity result.

Theorem 14 (Model Checking) The model checking problem for EQBL is PSPACE-complete.

Algorithm 1 Computation of the satisfaction set [[φ]]M

switch (φ): case ⊥: return ∅; case p: return V (p); case ¬ψ: return W \ [[ψ]]M; case ψ ∧ ψ′ : return [[ψ]]M∩ [[ψ′ ]]M; case Kaψ: return {w ∈ W | Ra(w) ⊆ [[ψ]]M}; case Cψ: return {w ∈ W | (⋃a∈Ag Ra)∗ (w) ⊆ [[ψ]]M}; case ∀pψ: return ⋂U∈D {[[ψ]]M′ ) | M′ = 〈F, V p U 〉};

In particular, we can prove that model checking EQBL is in PSPACE by using Algorithm 1 to compute the satisfaction set [[φ]]M = {w ∈ W | (M, w) |= φ}, and then check whether [[φ]]M = W. Algorithm 1 takes polynomial space in the size of the formula and exponential time in the size of the model.

As a result, the model checking problem for EQBL is no more computationally complex than the corresponding problem for quantified boolean logic. Thus, the enhanced expressiveness comes at no extra computational cost, when compared with quantified boolean logic. With respect to propositional epistemic logic, the complexity increases from PTIME. However, this is expected given the expressive power of propositional quantification.

6 Conclusions

We analysed the formal properties of multi-modal EQBL. Specifically, we provided soundness and completeness results for several classes of multi-agent Kripke frames, according to various assumptions on the domain D of propositions. In particular, we showed that there is a one-toone correspondence between an EQBL axiom ∀⃗ pθ and the MSO condition ∀x∀⃗ PSTx(θ) satisfied by the corresponding class of sound and complete frames. None of this is available in propositional modal logic. Further, we discussed the model checking problem for EQBL and showed that computationally it is no harder than the corresponding question for quantified boolean logic. In future work we plan to investigate precisely the expressive power of EQBL by exploring standard model-theoretic techniques, including (bi)simulation and unravelling. Even though some technical results are available [Kaminski and Tiomkin, 1996; ten Cate, 2006], the area is much less developed in comparison to plain propositional modal logic.

Related Work. The main inspiration for the present contribution comes from a series of papers on LPML, an extension of propositional modal logics to express local properties [van Ditmarsch et al., 2009; 2011; 2012]. Differently from these works we do not consider ad hoc languages, instead we adopt the framework of modal quantified boolean logic (MQBL). MQBL has been first considered in the seminal works by Bull and Fine [Bull, 1969; Fine, 1970]. The latter proved completeness and (un)decidability results for various classes of Kripke frames. Here we extended such results by explictly considering the multi-agent, epistemic interpretation of modalities. In particular, differently from [Fine, 1970], the introduction of common knowledge is essential to mimick an universal modality that, together with axiom At, enforces canonical models that are atomic. More recently, MQBL and its formal properties have been considered in the literature on modal logic, even though its conceptual complexity has hindered its development. The logic is also known as second-order propositional modal logic (SOPML) for the relation with second-order logic detailed in Section 3. In [Kaminski and Tiomkin, 1996] the authors proved that the expressive power of SOPML (for modalities weaker than 4.2) is the same as MSO. While [ten Cate, 2006] provides SOPML with analogues of the van Benthem-Rosen theorem and the Goldblatt-Thomason theorem. We remark that both works hinge only on the specific class of full Kripke frames.

Further, there is also a rich literature on combinations of quantification and epistemic logic [Belardinelli and Lomuscio, 2009; 2012; Corsi and Orlandelli, 2013]. However, the works in this area typically consider first-order quantification and knowledge of relational facts; which is not the case in the present setting.

The present contribution is also related to general Kripke frames [Blackburn et al., 2001; Mares and Goldblatt, 2006], as we also assume some algebraic structure on the set D of propositions, notably for the classes of boolean and full frames. However, propositional quantification makes our framework strictly more expressive than general frames. Also, differently from the contributions above, the main motivation for the present paper comes from the application to artificial intelligence, specifically the representation of agent knowledge in multi-agent contexts. In this respect, there has not been any previous work on EQBL to our knowledge.