Relevant Epistemic Logic with Public Announcements and Common Knowledge

Abstract

Building on our previous work in non-classical dynamic epistemic logic, we add common knowledge operators to a version of public announcement logic based on the relevant logic $\mathsf {R}$. We prove a completeness result with respect to a relational semantics, and we show that an alternative semantics based on information states is dual to the relational one. We add a question-forming inquisitive disjunction operator to the language and prove a completeness result with respect to the information semantics. It is argued that relevant public announcements are particularly suitable for modelling public argumentation.

1 Introduction

Various problematic closure properties of epistemic operators in classical epistemic logic led to the exploration of a number of alternatives to the classical framework; see [9]. One approach to avoiding closure under classical consequence is to represent epistemic states of agents as sets of abstract situations, roughly in the sense of Barwise and Perry [2], instead of representing them as sets of possible worlds. This approach leads naturally to epistemic logics based on paraconsistent and substructural propositional logics; see [3, 10, 19, 21, 22] for example. Combining these logics with an account of information dynamics is a topic of recent interest: [1, 11] explore versions of intuitionistic public announcement logic, [18, 20] study paraconsistent bilattice public announcement logic, and [4] outlines a fuzzy version of public announcement logic. Authors of the present paper explored versions of public announcement logic based on relevant and substructural logics in [14] and [25]. The latter paper focuses on modelling epistemic updates in the standard relational semantics for relevant modal logic and the former paper used a more general information-state semantics. All papers mentioned so far use languages without common knowledge, a concept linked to information dynamics in a number of important ways.

The aim of this paper is to (i) extend the frameworks presented in [14] and [25] with common knowledge and provide a complete axiomatization, and (ii) explore the relationship between these frameworks. In Sect. 2 we add common knowledge to the relational semantics introduced in [25]. We argue that the notion of update embodied in the semantics has a natural link to the notion of public argumentation. In Sect. 3 we prove a completeness result for the relational semantics. Then, in Sect. 4, we introduce an informational semantics following the approach of [14]. The main result here is that informational and relational models are dual, implying that the sound and complete axiomatization of Sect. 3 is sound and complete with respect to information models as well. In Sect. 5 we add questions to our object language in the style of inquisitive semantics [7] and show that the completeness proof of Sect. 3 can be extended to completeness of this enriched language with respect to informational semantics.

2 Relational Semantics

Definition 1

Fix a countable set of propositional variables Pr and a finite set of agent indices G. The language $\mathcal {L}$ contains operators $\mathrm {t}$ (zero-ary), $\wedge , \rightarrow , \otimes , { \texttt {[}} \, { \texttt {]}}$ (binary), $\lnot$ and $B_a, C_A$ for all $a \in G$ and non-empty $A \subseteq G$ (unary). The set of formulas of $\mathcal {L}$, denoted as $Fm_{\mathcal {L}}$, is generated by Pr using the operators of $\mathcal {L}$ in the usual way.

We define $\varphi \leftrightarrow \psi := (\varphi \rightarrow \psi ) \wedge (\psi \rightarrow \varphi )$, $\varphi \vee \psi := \lnot (\lnot \varphi \wedge \lnot \psi )$, $B_A \varphi := \bigwedge _{a \in A} B_a \varphi$, $B^{+}_A \varphi := B_A C_A \varphi$, and $K_a \varphi := C_{\{ a \}} \varphi$. Operators $\mathrm {t}, \lnot , \wedge , \otimes , \rightarrow$ are propositional, all $B_a$ and $C_A$ are epistemic operators and ${ \texttt {[}} \, { \texttt {]}}$ is the dynamic operator. We use r to range over propositional operators, $r_i$ over i-ary propositional operators and $r_{>0}$ over propositional operators of non-zero arity.

We read “$B_a \varphi$” as “Agent a believes that $\varphi$”, although what we mean is, more generally, that a has information that supports (or allows a to conclude that) $\varphi$. $B_A \varphi$ means that all agents in the group $A \subseteq G$ believe that $\varphi$. We read “$C_A \varphi$” as “$\varphi$ is common knowledge in the group of agents A”. $K_a \varphi$ is read “Agent a knows that $\varphi$” and $B^{+}_A \varphi$ as “it is common belief in group A that $\varphi$”. Our choice of primitive epistemic operators may seem a bit odd, but it can be shown that belief, knowledge, common belief and common knowledge interact in expected ways. In particular, $B^{+}_A \varphi$ holds in s iff $B_A \varphi$ holds in s, $B_A B_A \varphi$ holds in s, and so on, which corresponds to the usual semantics of common belief. $K_a$ is an “S4-type” knowledge operator, that is, $K_a \varphi \rightarrow \varphi$ and $K_a \varphi \rightarrow K_a K_a \varphi$ are valid, as we will see below.

The dynamic operator ${ \texttt {[}} \, { \texttt {]}}$ expresses effects of public announcement of a piece of information: we read ${ \texttt {[}} \varphi { \texttt {]}} \psi$ as “$\psi$ is the case after $\varphi$ is publicly announced to all agents”. Our notion of public announcement differs somewhat from the notion embodied in Public Announcement Logic [12, 26]: we do not assume that the announced piece of information is truthful, nor is it implied that the information is accepted by the agents upon the announcement; we also allow the possibility that the announcement may cause some agents to drop some of the previously accepted information.¹

A natural informal interpretation of such a general notion of public announcement is in terms of public argumentation. Imagine a group of agents, engaged in a public discussion. Public announcements can be seen as acts of putting forward arguments for or against claims in the discussion. These arguments do not have to be truthful and they do not have to be persuasive, meaning that the agents do not always accept the arguments. Moreover, arguments can cause agents to reject some of the information they accepted before. All of these features are characteristic aspects of our general rendering of public announcement. We will return to these aspects after introducing the semantics.

We note that our semantics extends the semantic framework of relevant logic introduced by Routley and Meyer in the 1970s. Our axiomatization extends the axiomatization of the relevant logic $\mathsf {R}$, introduced by Anderson and Belnap in the 1960s. We do not have the space to review relevant logic in detail. The reader is referred to [8] or [17], for example.

Definition 2

A relevant epistemic model for G is $\mathfrak {M} = (S, \sqsubseteq , L, R, C, E, V)$ where $(S, \sqsubseteq , L, R, C, V)$ is a Routley–Meyer model for the relevant logic $\mathsf {R}$, i.e.

• $(S, \sqsubseteq )$ is a partially ordered set;

• L is an up-set in $(S, \sqsubseteq )$;

• R is a ternary relation on $(S, \sqsubseteq )$ that is anti-monotonic in the first two coordinates and monotonic in the third coordinate, and satisfies the following frame conditions (we use the standard notation and )

  

• $s \sqsubseteq t$ iff there is $x \in L$ such that Rsxt;

• C is a symmetric binary relation on $(S, \sqsubseteq )$ that is anti-monotonic in both coordinates such that for all s there is a unique maximal element $\bar{s}$ of the set $C(s) = \{ t \mid Cst \}$ and

  

• V is a function from Pr to up-sets in $(S, \sqsubseteq )$;

and E is a function from G to binary relations on $(S,\sqsubseteq )$ that are anti-monotonic in the first coordinate and monotonic in the second coordinate.

Informally, E(a) represents the information about the epistemic state of a provided by situations in the model as follows. For each $s \in S$ there is a body of information, denote it as s(a), such that s provides information that s(a) is the epistemic state of a (s(a) may be empty). E(a)st represents the assumption that s(a) is contained in t. Hence, $E(a)(s) = \{ t \mid E(a)st \}$ can be seen as the representation of s(a).

We define $E(A) := \bigcup _{a \in A} E(a)$ and $E^{*}(A)$ as the reflexive transitive closure of $\left( \mathord {\sqsubseteq } \, \cup \, E(A)\right)$.² $E^{+}(A)$ is the transitive closure of E(A). We will usually write the agent (group) indices in a subscript.

Remark 1

We note that each relevant epistemic model is fully associative:

$$\begin{aligned} Rstuw \iff Rs(tu)w \end{aligned}$$

(7)

The full associativity condition will be required in our completeness proof, in particular in the steps for ${ \texttt {[}} \varphi { \texttt {]}}{ \texttt {[}} \psi { \texttt {]}}\chi$. Without common knowledge in the language, these cases are dealt with implicitly using the monotonicity rule R5; however, in the present context they have to be dealt with explicitly. This means that our present approach is limited to logics based on fully associative frames, for example the $\mathsf {R}$-based logics we focus on here. An extension of our results to weaker logics is an open problem.

Definition 3

The satisfaction relation between pointed models (that is, pairs of the form $(\mathfrak {M}, s)$ where s is in $\mathfrak {M}$) and $\mathcal {L}$-formulas is induced by V of $\mathfrak {M}$ as follows:

• $(\mathfrak {M}, s) \,\,\models \,\, p$ iff $s \in V(p)$;

• $(\mathfrak {M}, s) \,\,\models \,\, \mathrm {t}$ iff $s \in L$;

• $(\mathfrak {M}, s) \,\,\models \,\, \lnot \varphi$ iff $\forall t$, Cst implies ;

• $(\mathfrak {M}, s) \,\,\models \,\, \varphi \wedge \psi$ iff $(\mathfrak {M}, s) \,\,\models \,\, \varphi$ and $(\mathfrak {M}, s) \,\,\models \,\, \psi$;

• $(\mathfrak {M}, s) \,\,\models \,\, \varphi \rightarrow \psi$ iff, $\forall tu$, if Rstu and $(\mathfrak {M}, t) \,\,\models \,\, \varphi$, then $(\mathfrak {M}, u) \,\,\models \,\, \psi$;

• $(\mathfrak {M}, s) \,\,\models \,\, \varphi \otimes \psi$ iff $\exists tu$ such that Rtus and $(\mathfrak {M}, t) \,\,\models \,\, \varphi$ and $(\mathfrak {M}, u) \,\,\models \,\, \psi$;

• $(\mathfrak {M}, s) \,\,\models \,\, B_a \varphi$ iff $\forall t$, $E_ast$ only if $(\mathfrak {M}, t) \,\,\models \,\, \varphi$;

• $(\mathfrak {M}, s) \,\,\models \,\, C_A \varphi$ iff $\forall t$, $E^{*}_A st$ only if $(\mathfrak {M}, t) \,\,\models \,\, \psi$;

• $(\mathfrak {M}, s) \,\,\models \,\, { \texttt {[}} \varphi { \texttt {]}}\psi$ iff $(\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}}, s) \,\,\models \,\, \psi$, where $\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}}$ differs from $\mathfrak {M}$ only in that $E^{{ \texttt {[}} \varphi { \texttt {]}}}_a st$ iff there are u, v such that $E_a su$, Ruvt and $(\mathfrak {M}, v) \,\,\models \,\, \varphi$.

A formula $\varphi$ is valid in $\mathfrak {M}$ iff $(\mathfrak {M}, s) \,\,\models \,\, \varphi$ for all $s \in L$. We define $\mathfrak {M}(\varphi ) := \{ s \mid (\mathfrak {M}, s) \,\,\models \,\, \varphi \}$.

$\mathfrak {M}^{\,{ \texttt {[}} \varphi { \texttt {]}}}$ is the model that results from $\mathfrak {M}$ after the public announcement of $\varphi$. Intuitively, $\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}}$ results from $\mathfrak {M}$ by extending all situations in $\mathfrak {M}$ with the information that $\varphi$ has been publicly announced. This transformation of the model $\mathfrak {M}$ does not affect the “non-epistemic” structure consisting of the underlying Routley–Meyer model, but it does affect the epistemic accessibility relations since, intuitively, s(a) for each s and a is modified by the announcement. Our semantics reflects the idea that this modification can be represented using the ternary relation R. We take R to represent the effects of “merging” situations: Rstu iff the result of “merging” the information in s with the information in t is contained in u. Crucially, “merging” is not necessarily monotonic.³ Merging is lifted to sets of situations X, Y (representing arbitrary pieces of information) using the standard construction

(8)

After the information that $\varphi$ has been announced to a is added to s, the epistemic state s(a) is transformed into a new epistemic state $s(a)^{{ \texttt {[}} \varphi { \texttt {]}}}$. Intuitively, announcing $\varphi$ triggers a “merge” of the epistemic state of the given agent with the information expressed by $\varphi$. Using (8), we obtain

(9)

Hence, $s(a)^{{ \texttt {[}} \varphi { \texttt {]}}}$ is contained in u iff u contains the result of merging s(a) with the information that $\varphi$. This is exactly how $\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}}$ is defined.

Proposition 1

Formulas of the following forms are not valid: 1. ; 2. ; 3. .

We leave the construction of counterexamples to the reader. The fact that is not valid means that announcements are not necessarily truthful: announcing a false formula does not lead to “explosion”. The failure of means that announced information is not necessarily accepted by agents. This feature is related in spirit to well-known unsuccessful updates of classical public announcement logic, but the mechanism underlying the feature is more general than the so-called Moorean phenomena at work in the classical case. The failure of shows that announcements in our setting are non-monotonic: after an announcement of $\psi$, agents may abandon previously held beliefs. As mentioned above, all three aspects are typical features of public argumentation.

Definition 4

For any $\mathfrak {M}$, $\varphi$ and non-empty $A \subseteq G$:

• an A-path in $\mathfrak {M}$ is a finite sequence $\langle s_i \mid i < n\rangle$ of situations in $\mathfrak {M}$, for some $n \ge 0$, such that for all $j < n-1$, either $s_j \sqsubseteq s_{j+1}$ or $E_A s_j s_{j+1}$;

• an $A^{{ \texttt {[}} \varphi { \texttt {]}}}$-path in $\mathfrak {M}$ is a finite sequence $\langle s_i \mid i < n\rangle$ of situations in $\mathfrak {M}$, for some $n \ge 0$, such that for all $j < n-1$, either $s_j \sqsubseteq s_{j+1}$ or $E^{{ \texttt {[}} \varphi { \texttt {]}}}_A s_j s_{j+1}$.

A path (A-path or an $A^{{ \texttt {[}} \varphi { \texttt {]}}}$-path) is a path from s iff it is non empty and its first element is s; it is a path ending in t iff it is non-empty and its last element is t.

Note that $(\mathfrak {M},s) \,\,\models \,\, C_A \varphi$ iff $(\mathfrak {M}, t) \,\,\models \,\, \varphi$ for all t such that there is an A-path in $\mathfrak {M}$ starting with s and ending in t; similarly $(\mathfrak {M},s) \,\,\models \,\, { \texttt {[}} \psi { \texttt {]}}C_A \varphi$ iff $(\mathfrak {M}, t) \,\,\models \,\, { \texttt {[}} \psi { \texttt {]}}\varphi$ for all t such that there is an $A^{{ \texttt {[}} \psi { \texttt {]}}}$-path in $\mathfrak {M}$ starting with s and ending in t.

3 A Relational Completeness Result

In this section we provide a complete axiomatization of the set of formulas valid in all relevant epistemic models. The axiom system $\mathsf {RPAC}$, shown in Fig. 1, is a combination of the proof system for the relevant logic $\mathsf {R}$, axioms and rules specifying that $B_a$ are regular and monotonic modalities, the usual axioms and rules for the common knowledge operator, and the so-called reduction axioms for the update operator.

The completeness proof will combine the method of “partial filtration”, used to prove completeness for versions of Propositional Dynamic Logic based on relevant logics [23, 24], the standard canonical model argument for $\mathsf {R}$, and the completeness argument for Public Announcement Logic using reduction axioms. Our proof follows the usual strategy of proving completeness for Public Announcement Logic with common knowledge, but we use a different notion of filtration (the “filtrated model” is infinite, only epistemic accessibility relations are defined in terms of a finite set of formulas) and our models are more general. We note that, unlike in [23, 24], our proof does not require the presence of “extensional truth constants” $\top , \bot$. (We will specify the reason for this in Remark 2 below).

Fig. 1.

The axiom system $\mathsf {RPAC}$.

Lemma 1

All theorems of $\mathsf {RPAC}$ are valid in all relevant epistemic models.

Proof

We prove only the cases for A7 and R7 explicitly. First, iff there is t such that $E^{{ \texttt {[}} \varphi { \texttt {]}}}_a st$ and iff there are t, u, v such that $E_a su$ and Ruvt and $(\mathfrak {M}, v) \,\,\models \,\, \varphi$ and iff .

Second, to show that R7 preserves validity, assume that $\mathfrak {M}(\chi ) \subseteq \mathfrak {M}(B_a (\varphi \rightarrow \chi ))$ and $\mathfrak {M}(\chi ) \subseteq \mathfrak {M}({ \texttt {[}} \varphi { \texttt {]}}\psi )$. Let $(\mathfrak {M}, s) \,\,\models \,\, \chi$. To prove that $(\mathfrak {M},s ) \,\,\models \,\, { \texttt {[}} \varphi { \texttt {]}}C_A\psi$, we prove that for all $A^{{ \texttt {[}} \varphi { \texttt {]}}}$-paths from s ending in t, $(\mathfrak {M}, t) \,\,\models \,\, { \texttt {[}} \varphi { \texttt {]}}\psi$; using the second assumption of the rule, this can be established by showing that $(\mathfrak {M}, t) \,\,\models \,\, \chi$ for each such t. We show this by induction on the length of $A^{{ \texttt {[}} \varphi { \texttt {]}}}$-paths from s ending in t. The base case $s = t$ follows directly from our assumptions. Now assume that we have a path $(t_1, \ldots , t_{m}, t)$ such that $t_1 = s$ and that $(\mathfrak {M}, t_{m}) \,\,\models \,\, \chi$. If $t_m \sqsubseteq t$, then we are done. If $E^{{ \texttt {[}} \varphi { \texttt {]}}}_A t_m t$, then we reason as follows. $(\mathfrak {M}, t_m) \,\,\models \,\, \chi$ entails that $(\mathfrak {M}, t_m) \,\,\models \,\, B_A (\varphi \rightarrow \chi )$ and $E^{{ \texttt {[}} \varphi { \texttt {]}}}_A t_m t$ entails that there are u, v such that $E_A t_m u$, Ruvt and $(\mathfrak {M}, v) \,\,\models \,\, \varphi$. Hence, $(\mathfrak {M}, t) \,\,\models \,\, \chi$.    $\square$

Definition 5

A set of formulas $\varGamma$ is closed iff $\varphi \in \varGamma$ implies $\psi \in \varGamma$ for all subformulas $\psi$ of $\varphi$, and

• $C_A \varphi \in \varGamma$ only if $\{ B_A C_A \varphi , B_A \varphi \} \subseteq \varGamma$;

• ${ \texttt {[}} \varphi { \texttt {]}} r_{>0} (\psi _1, \ldots , \psi _n) \in \varGamma$ only if $\{ { \texttt {[}} \varphi { \texttt {]}}\psi _i \mid i \le n \} \subseteq \varGamma$;

• ${ \texttt {[}} \varphi { \texttt {]}}B_A \psi \in \varGamma$ only if $B_A (\varphi \rightarrow { \texttt {[}} \varphi { \texttt {]}}\psi ) \in \varGamma$;

• ${ \texttt {[}} \varphi { \texttt {]}}C_A \psi \in \varGamma$ only if ${ \texttt {[}} \varphi { \texttt {]}}B_A C_A \psi \in \varGamma$ and ${ \texttt {[}} \varphi { \texttt {]}}\psi \in \varGamma$;

• ${ \texttt {[}} \varphi { \texttt {]}}{ \texttt {[}} \psi { \texttt {]}}\chi \in \varGamma$ only if ${ \texttt {[}} \varphi \otimes { \texttt {[}} \varphi { \texttt {]}}\psi { \texttt {]}}\chi \in \varGamma$.

A set of formulas is a prime $\mathsf {RPAC}$-theory iff it is closed under forming conjunctions, closed under $\mathsf {RPAC}$-provable implications, and satisfies the property that if $\varphi \vee \psi$ is in the set, then $\varphi$ or $\psi$ is in the set.

Definition 6

Let $\varPhi$ be a finite closed set. The canonical model for $\varPhi$ is a structure $\mathfrak {M}_{\varPhi } = (S, \sqsubseteq , L, R, C, E, V)$ where

• S is the set of all prime $\mathsf {RPAC}$-theories;

• $\sqsubseteq$ is set inclusion;

• $\varGamma \in L$ iff $\varGamma$ contains all theorems of $\mathsf {L}$;

• $R \varGamma \varDelta \varSigma$ iff, for all $\varphi \rightarrow \psi \in \varGamma$, if $\varphi \in \varDelta$, then $\psi \in \varSigma$;

• $C \varGamma \varDelta$ iff, for all $\lnot \varphi \in \varGamma$, $\varphi \not \in \varDelta$;

• $E(a) \varGamma \varDelta$ iff, for all $B_a \varphi \in \varPhi \cap \varGamma$, $\varphi \in \varDelta$;

• $V(p) = \{ \varGamma \mid p \in \varGamma \}$.

We define $F(a) \varGamma \varDelta$ iff, $\varphi \in \varDelta$ for all $B_a \varphi \in \varGamma$. The satisfaction relation is defined just as for epistemic models.

Note that the canonical epistemic accessibility relations E(a) are defined using $B_a \varphi \in \varPhi$, not arbitrary $B_a \varphi$; the latter defines the auxiliary relations F(a). As in epistemic models, $E_A$ denotes the union of E(a) for $a \in A$. $E^{*}(A)$ is the reflexive transitive closure of the union of $\subseteq$ with E(A). Note that $F(a) \subseteq E(a)$ for all a, but the converse inclusion does not hold.

The notation $\vdash _\mathsf {RPAC} \varphi$ means that $\varphi$ is a theorem of $\mathsf {RPAC}$; we will use only $\vdash \varphi$ in this paper. We call a pair of sets of formulas $(\varGamma , \varDelta )$ independent iff there are no finite non-empty $\varGamma ' \subseteq \varGamma$ and $\varDelta ' \subseteq \varDelta$ such that $\vdash \bigwedge \varGamma ' \, \rightarrow \, \bigvee \varDelta '$.

Lemma 2 (Pair Extension)

If $(\varGamma , \varDelta )$ is independent, then there is a prime theory $\varSigma \supseteq \varGamma$ disjoint from $\varDelta$.

Proof

This is a corollary of the well-known fact that each non-overlapping filter-ideal pair in a distributive lattice is extended by a non-overlapping prime filter-ideal pair. This result is usually stated for non-empty filters and ideals. However, if $\varGamma$ is empty, then we can set $\varSigma := \emptyset$ and if $\varGamma$ is non-empty but $\varDelta$ is empty, then we set $\varSigma := Fm$. It is clear that both Fm and $\emptyset$ are prime theories.    $\square$

Lemma 3

For all $\varPhi$, $\mathfrak {M}_{\varPhi }$ is a relevant epistemic model.

Definition 7

For all finite $\varPhi$, we define the following:

• If $\varGamma$ is a prime theory not disjoint from $\varPhi$, then $\underline{\varGamma _{\varPhi }} := \bigwedge \left( \varGamma \cap \varPhi \right)$;

• if X is a non-empty set of prime theories, then $\underline{X_{\varPhi }} := \bigvee _{\varGamma \in X} \underline{\varGamma _{\varPhi }}$.

If $\varPhi$ is clear from the context, then we write just $\underline{\varGamma }$ and $\underline{X}$.

Note that $\underline{X}$ is well-defined even for infinite X since $\varPhi$ is finite. Note also that $\varGamma \in X$ implies $\underline{X} \in \varGamma$ (since if the assumption holds then $\underline{\varGamma } \rightarrow \underline{X}$ is a theorem and obviously $\underline{\varGamma } \in \varGamma$).

Remark 2

Formulas of the form $\underline{\varGamma _\varPhi }$ and $\underline{X_\varPhi }$ will be used in the proof of the Truth Lemma, in the cases for $C_A \varphi$ and ${ \texttt {[}} \varphi { \texttt {]}}C_A \psi$. In that particular context, each $\varGamma$ we will need to “characterize” by $\underline{\varGamma _\varPhi }$ will have a non-empty intersection with $\varPhi$ and each X considered will be non-empty. For this reason, we do not need to account for empty conjunctions and disjunctions and so, unlike in [23, 24], we do not need the presence of the “extensional” truth constants $\top$ and $\bot$ in the language.

Definition 8 (Complexity)

We define the following complexity function $c: Fm \rightarrow \mathbb {N}$:

• 1. $c(p) = 1$ for all $p \in Pr$;

• 2. $c(\mathrm {t}) = 1$;

• 3. $c(f(\varphi _1, \ldots , \varphi _n)) = \left( \sum _{i = 1}^{n} c(\varphi _i) \right) + 1$ for all $f \in \{ \lnot , \wedge , \rightarrow , \otimes , B_a, C_A \}$;

• 4. $c( { \texttt {[}} \varphi { \texttt {]}}\psi ) = ( 4 + c(\varphi ) ) \cdot c(\psi )$.

The closure of $\varGamma$ is the smallest closed superset of $\varGamma$.

It can be shown that the closure of any finite set is finite. Our definition of the complexity function is virtually the same as the definition used in [26], for example.

Lemma 4

For all $\varphi , \psi$ and $\chi$:

• 1. $c (\varphi ) > c(\psi )$ if $\psi$ is a proper subformula of $\varphi$;

• 2. $c ({ \texttt {[}} \varphi { \texttt {]}} r_{>0} (\psi _1, \ldots , \psi _n \psi _n ))> r_{>0} ( { \texttt {[}} \varphi { \texttt {]}}\psi _1, \ldots , { \texttt {[}} \varphi { \texttt {]}}\psi _n)$;

• 3. $c ({ \texttt {[}} \varphi { \texttt {]}} B_a \psi ) > c (\varphi \rightarrow { \texttt {[}} \varphi { \texttt {]}}\psi ) + 1$;

• 4. $c ( { \texttt {[}} \varphi { \texttt {]}}C_A \psi ) > c ({ \texttt {[}} \varphi { \texttt {]}}\psi )$;

• 5. $c ({ \texttt {[}} \varphi { \texttt {]}}{ \texttt {[}} \psi { \texttt {]}}\chi ) > c ({ \texttt {[}} \varphi \otimes { \texttt {[}} \varphi { \texttt {]}}\psi { \texttt {]}} \chi )$.

Lemma 5 (Truth Lemma)

For all $\mathfrak {M}$, all finite closed $\varPhi$, all formulas $\varphi \in \varPhi$ and all prime theories $\varGamma$:

$$\begin{aligned} \varphi \in \varGamma \iff (\mathfrak {M}_{\varPhi }, \varGamma ) \,\,\models \,\, \varphi \, . \end{aligned}$$

(10)

Proof

Induction on $c(\varphi )$. The base case is trivial. The rest of the cases are established as follows. Our induction hypothesis is that (10) holds for all $\varphi$ such that $c(\varphi ) < c(\theta )$ for some fixed $\theta$. We prove that (10) holds for $\theta$. We reason by cases.

The cases where the main connective of $\theta$ is $r_{>0}$ are established as usual in completeness proofs for $\mathsf {R}$ (these cases use the assumption that $\varPhi$ is closed under subformulas), and the case for $\theta = B_a \varphi$ is established as usual in modal logic.

If $\theta = C_A \varphi$, then we reason as follows. To prove the left-to-right implication, we will use the following facts:

• (i) if $C_A \varphi \in \varGamma \cap \varPhi$ and $E_A \varGamma \varDelta$, then $C_A \varphi \in \varDelta$; and

• (ii) if $C_A \varphi \in \varGamma \cap \varPhi$, then each A-path from $\varGamma$ ends with $\varDelta$ such that $C_A \varphi \in \varDelta$.

Fact (i) is established as follows: If $C_A \varphi \in \varPhi$, then $B_A C_A \varphi \in \varPhi$ and so $B_a C_A \varphi \in \varPhi$ for all $a \in A$. If $E_A \varGamma \varDelta$, then $E_a \varGamma \varDelta$ for some $a \in A$. Hence, if $C_A \varphi \in \varGamma$, then $B_a C_A \varphi \in \varGamma$ using A3 and R3. Hence, $C_A \varphi \in \varDelta$ by the definition of $E_a$ and properties of prime theories.

Fact (ii) is established by induction on the length of A-paths from $\varGamma$. The base case of the one-element path is trivial: $C_A \varphi \in \varGamma$ by assumption and $\varphi \in \varGamma$ by A3. Now assume that we have a path $(\varDelta _1, \ldots , \varDelta _m, \varDelta )$ such that $\varDelta _1 = \varGamma$ and that the claim holds for $(\varDelta _1, \ldots , \varDelta _{m})$. Then $C_A \varphi \in \varDelta _{m}$. If $\varDelta _{m} \subseteq \varDelta$, then clearly $C_A \varphi \in \varDelta$ and so $\varphi \in \varDelta$ by A3. If $E_A \varDelta _m \varDelta$, then $C_A \varphi \wedge \varphi \in \varDelta$ by (i).

Now assume that $C_A \varphi \in \varGamma \cap \varPhi$ and $E^{+}_{A} \varGamma \varDelta$. The latter means that there is an A-path from $\varGamma$ ending with $\varDelta$. Hence, $\varphi \in \varDelta$ by (ii). Since $\varDelta$ was arbitrary, we obtain $(\mathfrak {M}, \varGamma ) \,\,\models \,\, C_A \varphi$.

Conversely, let X be the set of $\varDelta$ such that there is an A-path $(\varGamma , \ldots , \varDelta )$. Assume that $(\mathfrak {M}, \varDelta ) \,\,\models \,\, \varphi$ for all $\varDelta \in X$. By the induction hypothesis, $\varphi \in \varDelta$ for all $\varDelta \in X$. Since $\varphi \in \varPhi$, $\underline{\varGamma }$ and indeed $\underline{\varDelta }$ for all $\varDelta \in X$ and $\underline{X}$ are defined. (We know that at least $\varGamma \in X$.) We prove that

• (iii) $\vdash \underline{\varGamma } \rightarrow \underline{X}$;

• (iv) $\vdash \underline{X} \rightarrow \varphi$;

• (v) $\vdash \underline{X} \rightarrow B_A \underline{X}$.

Using R6, (iv) and (v) entail $\vdash \underline{X} \rightarrow C_A \varphi$, which together with (iii) gives $\vdash \underline{\varGamma } \rightarrow C_A \varphi$. Hence, $C_A \varphi \in \varGamma$.

Claims (iii) and (iv) are obvious. Claim (v) is established as follows. If $\not \vdash \underline{X} \rightarrow B_A \underline{X}$, then there are $\varDelta \in X$ and $\varTheta$ such that $\underline{\varDelta } \in \varTheta$ and $B_A \underline{X} \not \in \varTheta$. Using the Pair Extension Lemma, there is $\varSigma$ such that $F_A \varTheta \varSigma$ and $\underline{X} \not \in \varSigma$. But since $\underline{\varDelta } \in \varTheta$, $F_A \varTheta \varSigma$ implies that $E_A \varDelta \varSigma$. ($F_A \varTheta \varSigma$ entails that $E_a \varTheta \varSigma$ for some $a \in A$. Assume that $B_a \chi \in \varDelta \cap \varPhi$. Then $\vdash \underline{\varDelta } \rightarrow B_a \chi$ and so $B_a \chi \in \varTheta$. This means that $\chi \in \varSigma$.) Hence, $\varDelta \in X$ implies $\varSigma \in X$, contradicting $\underline{X} \not \in \varSigma$.

Now we consider the case $\theta = { \texttt {[}} \varphi { \texttt {]}}\psi$. We reason by cases, depending on the form of $\psi$:

Case 1

$\theta = { \texttt {[}} \varphi { \texttt {]}}p$. Then $\theta \in \varGamma$ iff $p \in \varGamma$ (using A4) iff $(\mathfrak {M}, \varGamma ) \,\,\models \,\, p$ (using the induction hypothesis) iff $(\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}}, \varGamma ) \,\,\models \,\, p$ (using the definition of $\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}}$) iff $(\mathfrak {M}, \varGamma ) \,\,\models \,\, { \texttt {[}} \varphi { \texttt {]}}p$ (using the definition of $\models$).

Case 2

$\theta = { \texttt {[}} \varphi { \texttt {]}}r(\psi _1, \ldots , \psi _n)$. All sub-cases of this form are established using the definition of a closed set (closure under subformulas), Lemma 4, and the fact that update with $\varphi$ does not modify the underlying Routley–Meyer model $(S, \sqsubseteq , L, R, C, V)$, just the epistemic accessibility relations $E_a$.

Case 3

$\theta = { \texttt {[}} \varphi { \texttt {]}}B_a \psi$. Then $\theta \in \varGamma$ iff $B_a (\varphi \rightarrow { \texttt {[}} \varphi { \texttt {]}}\psi ) \in \varGamma$ (using A7) iff $(\mathfrak {M}, \varGamma ) \,\,\models \,\, B_a (\varphi \rightarrow { \texttt {[}} \varphi { \texttt {]}}\psi )$ (using the induction hypothesis, relying on the definition of a closed set and item 3 of Lemma 4) iff for all $\varSigma , \varSigma '$ and $\varDelta$, and $(\mathfrak {M}, \varSigma ') \,\,\models \,\, \varphi$ only if $(\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}}, \varDelta ) \,\,\models \,\, \psi$ (definition of $\models$) iff, for all $\varDelta$, $E_A^{{ \texttt {[}} \varphi { \texttt {]}}} \varGamma \varDelta$ only if $(\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}}, \varDelta ) \,\,\models \,\, \psi$ (definition of $E_A^{{ \texttt {[}} \varphi { \texttt {]}}}$) iff $(\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}}, \varGamma ) \,\,\models \,\, B_a \psi$ (definition of $\models$) iff $(\mathfrak {M}, \varGamma ) \,\,\models \,\, { \texttt {[}} \varphi { \texttt {]}}B_a \psi$ (definition of $\models$).

Case 4

$\theta = { \texttt {[}} \varphi { \texttt {]}}C_A \psi$. We will use the following two facts:

• (vi) If ${ \texttt {[}} \varphi { \texttt {]}}C_A \psi \in \varPhi \cap \varGamma$ and $E^{{ \texttt {[}} \varphi { \texttt {]}}}_{A} \varGamma \varDelta$, then ${ \texttt {[}} \varphi { \texttt {]}}C_A \psi \in \varDelta$ and ${ \texttt {[}} \varphi { \texttt {]}}\psi \in \varDelta$; and

• (vii) if ${ \texttt {[}} \varphi { \texttt {]}}C_A \psi \in \varPhi \cap \varGamma$, then each $A^{{ \texttt {[}} \varphi { \texttt {]}}}$-path from $\varGamma$ ends with $\varDelta$ such that ${ \texttt {[}} \varphi { \texttt {]}}C_A\psi \in \varDelta$ and ${ \texttt {[}} \varphi { \texttt {]}}\psi \in \varDelta$.

Fact (vi) is established as follows. If $E_A^{{ \texttt {[}} \varphi { \texttt {]}}} \varGamma \varDelta$, then there is $a \in A$ such that $E_a^{{ \texttt {[}} \varphi { \texttt {]}}} \varGamma \varDelta$, which means that there are $\varSigma _1, \varSigma _2$ such that $E_a \varGamma \varSigma _1$, $R\varSigma _1\varSigma _2\varDelta$ and $(\mathfrak {M}, \varSigma _2) \,\,\models \,\, \varphi$ (note that $E_a^{{ \texttt {[}} \varphi { \texttt {]}}}$ is defined using $\models$). Using the induction hypothesis ($\varphi$ is a subformula of $\theta$), we get $\varphi \in \varSigma _2$. Now ${ \texttt {[}} \varphi { \texttt {]}}C_A \psi \in \varGamma$ entails ${ \texttt {[}} \varphi { \texttt {]}}B_a C_A \psi \in \varGamma$ and ${ \texttt {[}} \varphi { \texttt {]}}B_a \psi \in \varGamma$ (using A3 and R5) and this entails $B_a (\varphi \rightarrow { \texttt {[}} \varphi { \texttt {]}}C_A \psi ) \in \varGamma$ and $B_a (\varphi \rightarrow { \texttt {[}} \varphi { \texttt {]}}\psi ) \in \varGamma$ (using A7). It follows from the definition of a closed set that $\{ B_a (\varphi \rightarrow { \texttt {[}} \varphi { \texttt {]}}C_A \psi ), B_a (\varphi \rightarrow { \texttt {[}} \varphi { \texttt {]}}\psi ) \} \subseteq \varPhi$, and so we can infer that $\varphi \rightarrow { \texttt {[}} \varphi { \texttt {]}}C_A \psi \in \varSigma _1$ and $\varphi \rightarrow { \texttt {[}} \varphi { \texttt {]}}\psi \in \varSigma _1$, which also means that ${ \texttt {[}} \varphi { \texttt {]}}C_A \psi \in \varDelta$ and ${ \texttt {[}} \varphi { \texttt {]}}\psi \in \varDelta$.

Fact (vii) is established by induction on the length of $A^{{ \texttt {[}} \varphi { \texttt {]}}}$-paths from $\varGamma$. The base case of a one-element path is trivial: ${ \texttt {[}} \varphi { \texttt {]}}C_A\psi$ is assumed to be in $\varGamma$ and ${ \texttt {[}} \varphi { \texttt {]}}\psi \in \varGamma$ by A3. Now assume that (vii) holds for all $A^{{ \texttt {[}} \varphi { \texttt {]}}}$-paths of length m, where $2 \le m < n$ and take $(\varDelta _1, \ldots , \varDelta _{n})$, where $\varDelta _1 = \varGamma$. We know that $C_A \varphi \in \varDelta _{n-1}$. If $\varDelta _{n} \subseteq \varDelta _{n-1}$, then we are done. If $E^{{ \texttt {[}} \varphi { \texttt {]}}}_A \varDelta _{n-1}\varDelta _n$, then ${ \texttt {[}} \varphi { \texttt {]}}C_A \varphi \in \varDelta _n$ thanks to (vi).

Now assume that ${ \texttt {[}} \varphi { \texttt {]}}C_A\psi \in \varGamma$ and that $E^{{ \texttt {[}} \varphi { \texttt {]}}}_A \varGamma \varDelta$. The latter means that there is a $A^{{ \texttt {[}} \varphi { \texttt {]}}}$-path $(\varGamma _1, \ldots , \varGamma _n)$ such that $\varGamma _1 = \varGamma$ and $\varGamma _n = \varDelta$. By (vii), ${ \texttt {[}} \varphi { \texttt {]}}\psi \in \varDelta$. By the induction hypothesis, $(\mathfrak {M}, \varDelta ) \,\,\models \,\, { \texttt {[}} \varphi { \texttt {]}}\psi$ (see item 5 of Lemma 4) and so $(\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}}, \varDelta ) \,\,\models \,\, \psi$. Since $\varDelta$ was arbitrary, we obtain $(\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}}, \varGamma ) \,\,\models \,\, C_A \varphi$. This means that $(\mathfrak {M}, \varGamma ) \,\,\models \,\, { \texttt {[}} \varphi { \texttt {]}}C_A \psi$.

Conversely, let X be the set of $\varDelta$ such that there is an $A^{{ \texttt {[}} \varphi { \texttt {]}}}$-path $(\varGamma , \ldots , \varDelta )$. Assume that $(\mathfrak {M}, \varGamma ) \,\,\models \,\, { \texttt {[}} \varphi { \texttt {]}}C_A \psi$, which means that $(\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}}, \varDelta ) \,\,\models \,\, \psi$ for all $\varDelta \in X$. By the induction hypothesis, ${ \texttt {[}} \varphi { \texttt {]}}\psi \in \varDelta$ for all $\varDelta \in X$. Since ${ \texttt {[}} \varphi { \texttt {]}}\psi \in \varPhi$, $\underline{\varGamma }$ and indeed $\underline{\varDelta }$ for all $\varDelta \in X$ and $\underline{X}$ are defined. (We know that at least $\varGamma \in X$.) We prove that

• (viii) $\vdash \underline{\varGamma } \rightarrow \underline{X}$;

• (ix) $\vdash \underline{X} \rightarrow { \texttt {[}} \varphi { \texttt {]}}\psi$;

• (x) $\vdash \underline{X} \rightarrow B_A (\varphi \rightarrow \underline{X})$.

Using R7, (ix) and (x) entail that $\vdash \underline{X} \rightarrow { \texttt {[}} \varphi { \texttt {]}}C_A\psi$, which together with (viii) entails $\vdash \underline{\varGamma } \rightarrow { \texttt {[}} \varphi { \texttt {]}}C_A \psi$. This means that ${ \texttt {[}} \varphi { \texttt {]}}C_A \psi \in \varGamma$.

Claim (viii) follows from $\varGamma \in X$. Claim (ix) follows from the assumption that ${ \texttt {[}} \varphi { \texttt {]}}\psi \in \bigcap X$. Claim (x) is established as follows. If $\not \vdash \underline{X} \rightarrow B_A (\varphi \rightarrow \underline{X})$, then there is $\varDelta \in X$ such that $\not \vdash \underline{\varDelta } \rightarrow B_A (\varphi \rightarrow \underline{X})$. Hence, by the Pair Extension Lemma, there is $\varTheta$ such that $\underline{\varDelta } \in \varTheta$ and $B_A (\varphi \rightarrow \underline{X}) \not \in \varTheta$. The latter means that there is $a \in A$ and $\varSigma$ such that $F_a \varTheta \varSigma$ and $\varphi \rightarrow \underline{X} \not \in \varSigma$. The latter here means that there are $\varPi , \varOmega$ such that $R\varSigma \varPi \varOmega$, $\varphi \in \varPi$ and $\underline{X} \not \in \varOmega$. Using the induction hypothesis, we obtain $(\mathfrak {M}, \varPi ) \,\,\models \,\, \varphi$, and so $E^{{ \texttt {[}} \varphi { \texttt {]}}}_A\varDelta \varOmega$ (since $F_A \varTheta \varSigma$ and $\underline{\varDelta } \in \varTheta$ imply that $E_A \varDelta \varSigma$). Since $\varDelta \in X$, it follows that $\varOmega \in X$, contradicting $\underline{X} \not \in \varOmega$.

Case 5

$\theta = { \texttt {[}} \varphi { \texttt {]}}{ \texttt {[}} \psi { \texttt {]}}\chi$. We will use the following fact:

• (xi) For $a \in G$ and all formulas $\alpha , \beta$: $E_a^{\,{ \texttt {[}} \alpha { \texttt {]}}{ \texttt {[}} \beta { \texttt {]}}} = E_a^{\,{ \texttt {[}} \alpha \otimes { \texttt {[}} \alpha { \texttt {]}}\beta { \texttt {]}}}$.

(xi) needs the assumption of full associativity (7):

Now we reason as follows: $\theta \in \varGamma$ iff ${ \texttt {[}} \varphi \otimes { \texttt {[}} \varphi { \texttt {]}}\psi { \texttt {]}}\chi \in \varGamma$ (using A8) iff $(\mathfrak {M}, \varGamma ) \,\,\models \,\, { \texttt {[}} \varphi \otimes { \texttt {[}} \varphi { \texttt {]}}\psi { \texttt {]}}\chi$ (induction hypothesis, relying on item 6 of Lemma 4 and the definition of a closed set) iff $(\mathfrak {M}^{{ \texttt {[}} \varphi \otimes { \texttt {[}} \varphi { \texttt {]}}\psi { \texttt {]}}}, \varGamma ) \,\,\models \,\, \chi$ iff $(\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}{ \texttt {[}} \psi { \texttt {]}}}, \varGamma ) \,\,\models \,\, \chi$ (since $\mathfrak {M}^{{ \texttt {[}} \varphi \otimes { \texttt {[}} \varphi { \texttt {]}}\psi { \texttt {]}}} = \mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}{ \texttt {[}} \psi { \texttt {]}}}$ by (xi)) iff $(\mathfrak {M}, \varGamma ) \,\,\models \,\, { \texttt {[}} \varphi { \texttt {]}}{ \texttt {[}} \psi { \texttt {]}}\chi$.    $\square$

Theorem 1

$\varphi$ is a theorem of $\mathsf {RPAC}$ iff $\varphi$ is valid in all relevant epistemic models.

Proof

Soundness follows from Lemma 1. Completeness is established using the Pair Extension Lemma, the Truth Lemma and Lemma 3: If $\varphi$ is not a theorem, then neither is $\mathrm {t}\rightarrow \varphi$. Take $\varPhi$ the closure of $\{ \mathrm {t}\rightarrow \varphi \}$ and consider $\mathfrak {M}_{\varPhi }$, which is a relevant epistemic model by Lemma 3. By the Pair Extension Lemma, there is a $\varGamma \in L$ such that $\varphi \not \in \varGamma$. By the Truth Lemma, $\varphi$ is not valid in $\mathfrak {M}_{\varPhi }$.    $\square$

4 Information Models

The semantics used in the previous sections builds on the framework introduced in [25], which has been in this paper adjusted to the background logic $\mathsf {R}$ and extended with common knowledge. Another approach to a public announcement logic with a substructural basis was developed in [14]. It turns out that these two approaches are closely related, which will be discussed in detail in this section. The merit of the alternative perspective that we will now describe is that it will allow us in the next section to enrich our logic with a further dimension that forms a crucial ingredient of informational dynamics. In particular, this perspective will allow us to express in the object language not only statements but also questions. For definition of the semantic models of this alternative framework we will need the following notion of a situation.

Definition 9

Let $(P, \le )$ be a complete lattice, where for any $X \subseteq P$, $\bigsqcup X$ denotes the join of X. An element $s \in P$ is called a situation in $(P, \le )$ iff it is completely join-irreducible, i.e. iff for every $X \subseteq P$, $s= \bigsqcup X$ only if $s=x$, for some $x \in X$. The set of situations in $(P, \le )$ will be denoted as Sit(P). For any $x \in P$, the set of situations below x, i.e. the set $\{s \in Sit(P)~|~s \le x \}$, will be denoted as Sit(x).

Note that if meet distributes over arbitrary joins in a complete lattice $(P, \le )$ then for every situation $s \in Sit(P)$ and every $X \subseteq P$, if $s \le \bigsqcup X$ then $s \le x$ for some $x \in X$.

Definition 10

An information model for G is $\mathfrak {N} = (P, \le , 1, \cdot , C, \sigma , V)$ such that (a) $\langle P, \le \rangle$ is a complete lattice; (b) every state from P is identical to the join of a set of situations, that is, for any $x \in P$, $x=\bigsqcup Sit(x)$; (c) 1 is an identity with respect to the binary operation $\cdot$ on P, i.e. $1 \cdot x = x$; (d) $\sqcap$ (i.e. the finite meet) and $\cdot$ distribute over arbitrary joins from both directions; (e) C is symmetric binary relation on P, and $Cx \bigsqcup Y$ iff there is $y \in Y$ such that Cxy; (f) $\sigma$ is a map that assigns to each agent $a \in G$ a function $\sigma (a)$ (we will often write $\sigma _a$) from situations to states; (g) if s, t are situations such that $s \le t$ then $\sigma _a (s) \le \sigma _a (t)$; (h) $V(p) \in S$, for every atomic formula p.

P represents a set of information states, $x \le y$ expresses that the state x is an informational refinement of the state y (i.e. x is informationally stronger than y), 1 is called a logical state, $x \cdot y$ is called fusion of the states x and y, Cxy says that x is compatible with y, $\sigma$ is called an information state map, V is a valuation that assigns to every atomic formula an informational content, represented as a state in P.

Note that distributivity of fusion over joins implies its monotonicity, i.e. $x_1 \le x_2$ and $y_1 \le y_2$ only if $x_1 \cdot y_1 \le x_2 \cdot y_2$. Moreover, there is the least element 0 in $\mathfrak {N}$ that can be defined as $\bigsqcup \emptyset$.

Definition 11

A relevant information model for G is an information model $\mathfrak {N} = (P, \le , 1, \cdot , C, \sigma , V)$ for G where (i) fusion is associative, commutative, and $x \le x \cdot x$, (ii) for every situation $s \in Sit(P)$ there is a state $x \in P$ such that Cxy if and only if $s \le y$, (iii) for all states $x, y, z \in S$, if $Cx(y \cdot z)$ then $C(x \cdot y) z$.

Let $\sigma$ be an inquisitive state map, $A \subseteq G$ a set of agents, and s a situation. We define $\sigma _A(s)=\bigsqcup _{a \in A} \sigma _a(s)$. Moreover, we define:

• .

The support relation between pointed relevant information models and formulas from $\mathcal {L}$ is defined as follows:

• $(\mathfrak {N}, x) \Vdash p$ iff $x \le V(p)$;

• $(\mathfrak {N}, x) \Vdash \mathrm {t}$ iff $x \le 1$;

• $(\mathfrak {N}, x) \Vdash \lnot \varphi$ iff, $\forall y$, if Cxy, then $(\mathfrak {N}, y) \nVdash \varphi$;

• $(\mathfrak {N}, x) \Vdash \varphi \wedge \psi$ iff $(\mathfrak {N}, x) \Vdash \varphi$ and $(\mathfrak {N}, x) \Vdash \psi$;

• $(\mathfrak {N}, x) \Vdash \varphi \rightarrow \psi$ iff, $\forall y$, if $(\mathfrak {N}, y) \Vdash \varphi$, then $(\mathfrak {N}, x \cdot y) \Vdash \psi$;

• $(\mathfrak {N}, x) \Vdash \varphi \otimes \psi$ iff, $\exists yz$, $(\mathfrak {N}, y) \Vdash \varphi$, $(\mathfrak {N}, z) \Vdash \psi$, and $x \le y \cdot z$;

• $(\mathfrak {N}, x) \Vdash B_a \varphi$ iff, for all $s \in Sit(x)$, $(\mathfrak {N}, \sigma _a(s)) \Vdash \varphi$;

• $(\mathfrak {N}, x) \Vdash C_A \varphi$ iff, for all $s \in Sit(x)$, $(\mathfrak {N}, \sigma ^*_A(s)) \Vdash \varphi$;

• $(\mathfrak {N}, x) \Vdash { \texttt {[}} \varphi { \texttt {]}}\psi$ iff $(\mathfrak {N}^{{ \texttt {[}} \varphi { \texttt {]}}}, x) \Vdash \psi$, where $\mathfrak {N}^{{ \texttt {[}} \varphi { \texttt {]}}}$ differs from $\mathfrak {N}$ only in that $\sigma ^{{ \texttt {[}} \varphi { \texttt {]}}}_a (s)=\bigsqcup \{ \sigma _a (s) \cdot y~|~(\mathfrak {N}, y) \Vdash \varphi \}$.

A formula $\varphi$ is valid in a relevant information model $\mathfrak {N}$ if $(\mathfrak {N}, 1) \Vdash \varphi$. Note that since 1 is an identity for fusion an implication $\varphi \rightarrow \psi$ is valid in $\mathfrak {N}$ iff $\psi$ is supported by all states of $\mathfrak {N}$ that support $\varphi$.

Lemma 6

For any relevant information model $\mathfrak {N}$ and any formula $\varphi$ from $\mathcal {L}$, there is a state $info^{\mathfrak {N}}(\varphi )$ in $\mathfrak {N}$ such that $\mathfrak {N}, x \Vdash \varphi$ iff $x \le info^{\mathfrak {N}}(\varphi )$.

Proof

The claim follows from the fact that for any $\varphi$ from $\mathcal {L}$ the set of states supporting $\varphi$ contains 0, is downward closed and closed under $\bigsqcup$. This can be shown by induction on $\varphi$. We will consider only the inductive steps for modal operators. The inductive steps for $\lnot , \wedge , \rightarrow$ are discussed in [15]. Support by 0 and downward persistence for the operators $B_a, C_A, { \texttt {[}} \varphi { \texttt {]}}$ is straightforward. Let us prove that the set of states supporting $B_a \varphi$ is closed under $\bigsqcup$. Assume $(\mathfrak {N}, x_i) \Vdash B_a \varphi$, for each $i \in I$. Take any $s \in Sit (\bigsqcup _{i \in I} x_i)$. Since s is a situation, we obtain $s \in Sit (x_i)$, for some $i \in I$. It follows that $(\mathfrak {N}, \sigma _a(s)) \Vdash \varphi$. Hence $(\mathfrak {N}, \bigsqcup _{i \in I} x_i) \Vdash B_a \varphi$. The inductive step for $C_A$ is analogous and the step for ${ \texttt {[}} \varphi { \texttt {]}}$ is straightforward.   $\square$

The state $info^{\mathfrak {N}}(\varphi )$, the existence of which is guaranteed by the previous lemma, represents the informational content of the formula $\varphi$ in $\mathfrak {N}$. (If no confusion arises the superscript will be omitted.) Its existence allows us to characterize update of states in the following simplified way.

Lemma 7

$\sigma ^{{ \texttt {[}} \varphi { \texttt {]}}}_a (s)= \sigma _a (s) \cdot info(\varphi )$.

The semantics based on relevant information models is closely related to the semantics based on relevant epistemic models. In order to spell out the exact connection we will use the notion of duality of two semantic frameworks introduced in [15]. Let $S_1$ and $S_2$ be two semantic frameworks based respectively on some classes of models $C_1$ and $C_2$ and equipped with semantic clauses determining which formulas are valid in which models. We say that models $\mathfrak {M} \in C_1$ and $\mathfrak {N} \in C_2$ are $\mathcal {L}$-equivalent if they validate exactly the same formulas from $\mathcal {L}$. We say that the semantic system $S_2$ is a dual counterpart of $S_1$ w.r.t. the language $\mathcal {L}$ if there are two maps $f: C_1 \rightarrow C_2$ and $g: C_2 \rightarrow C_1$ such that (a) every $\mathfrak {M} \in C_1$ is $\mathcal {L}$-equivalent to $f(\mathfrak {M})$, and (b) for every $\mathfrak {M} \in C_1$ and $\mathfrak {N} \in C_2$ it holds that $g(f(\mathfrak {M}))$ is isomorphic to $\mathfrak {M}$ and $f(g(\mathfrak {N}))$ is isomorphic to $\mathfrak {N}$.

The main goal of this section is to show that the semantics based on relevant information models is a dual counterpart of the semantics based on relevant epistemic models. (As already pointed out, the added value of this dual counterpart is that it will allow us to capture not only statements but also questions.) This result extends the results from [15] that established similar duality between information models and Routley–Meyer models for a basic propositional language involving only the operators $\{\wedge , \rightarrow , \lnot \}$.

We will now describe an operation that transforms relevant epistemic models into relevant information models. We will use the following notation: Let $(S, \sqsubseteq )$ be a partial order and $s \in S$. Then UpS denotes the set of all up-sets of S, and $s^{\uparrow }$ denotes the set $\{t \in S~|~s \sqsubseteq t \}$. Note that the sets of the form $s^{\uparrow }$ are exactly the situations in the complete lattice $(UpS, \subseteq )$.

Definition 12

Let $\mathfrak {M} = (S, \sqsubseteq , L, R, C, E, V)$ be a relevant epistemic model. We define a corresponding structure $\mathfrak {M}^i = (P^i, \le ^i, 1^i, \cdot ^i, C^i, \sigma ^i, V^i)$, where $P^i=UpS$; $\le ^i=\subseteq$; $1^i=L$; $x \cdot ^i y=\{s \in S~|~\exists t \in x, u \in y \text { such that } Rtus\}$; $C^i xy$ iff there are $s \in x$ and $t \in y$ such that Cst; $\sigma ^i_a(s^{\uparrow })=E_a(s)$; $V^i=V$.

Lemma 8

If $\mathfrak {M}$ is a relevant epistemic model then $\mathfrak {M}^i$ is a relevant information model.

Theorem 2

$\mathfrak {M}^i$ is $\mathcal {L}$-equivalent to $\mathfrak {M}$, for every relevant epistemic model $\mathfrak {M}$.

Proof

Let $\mathfrak {M} = (S, \sqsubseteq , L, R, C, E, V)$ be a relevant epistemic model, and $\mathfrak {M}^i = (P^i, \le ^i, 1^i, \cdot ^i, C^i, \sigma ^i, V^i)$ the corresponding relevant information model. We have to show that for any $\theta$ from $\mathcal {L}$, $(\mathfrak {M}^i, L) \Vdash \theta$ iff for all $s \in L$, $(\mathfrak {M}, s) \,\,\models \,\, \theta$. We prove something more general:

• (*) For any $X \in UpS$, $(\mathfrak {M}^i, X) \Vdash \theta$ iff, for all $s \in X$, $(\mathfrak {M}, s) \,\,\models \,\, \theta$.

This can be proved by induction on $\theta$. We will go only through the inductive steps for the operators $B_a$, $C_A$, and ${ \texttt {[}} \varphi { \texttt {]}}$. Take any $X \in UpS$. As the induction hypothesis, assume that the claim (*) holds for some given formulas $\varphi , \psi$.

Assume that $\theta = B_a \varphi$. Then it holds: $(\mathfrak {M}^i, X) \Vdash B_a \varphi$ iff, for all $s \in X$, $(\mathfrak {M}^i, \sigma _a^i(s^{\uparrow })) \Vdash \varphi$ iff, for all $s \in X$, $(\mathfrak {M}^i, E_a(s)) \Vdash \varphi$ iff (by induction hypothesis), for all $s \in X$ and for all $t \in E_a(s)$, $(\mathfrak {M}, t) \,\,\models \,\, \varphi$ iff, for all $s \in X$, $(\mathfrak {M}, s) \,\,\models \,\, B_a \varphi$.

Assume that $\theta = C_A \varphi$. It holds that $(\sigma _A^i)^*(s^{\uparrow })=E_A^*(s)$ so we can proceed in the same way as in the case of $B_a \varphi$.

Finally assume that $\theta = { \texttt {[}} \varphi { \texttt {]}} \psi$. It can be shown that $(\mathfrak {M}^i)^{{ \texttt {[}} \varphi { \texttt {]}}}=(\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}})^i$. So, we can proceed as follows: $(\mathfrak {M}^i, X) \Vdash { \texttt {[}} \varphi { \texttt {]}} \psi$ iff $((\mathfrak {M}^i)^{{ \texttt {[}} \varphi { \texttt {]}}}, X) \Vdash \psi$ iff $((\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}})^i, X) \Vdash \psi$ iff, for all $s \in X$, $(\mathfrak {M}^{{ \texttt {[}} \varphi { \texttt {]}}}, s) \,\,\models \,\, \psi$ iff, for all $s \in X$, $(\mathfrak {M}, s) \,\,\models \,\, { \texttt {[}} \varphi { \texttt {]}} \psi$.

Now we will define an inverse operation that transforms relevant information models into relevant epistemic models.

Definition 13

Let $\mathfrak {N} = (P, \le , 1, \cdot , C, \sigma , V)$ be a relevant information model. We define a corresponding structure $\mathfrak {N}^e = (S^e, \sqsubseteq ^e, L^e, R^e, C^e, E^e, V^e)$, where $S^e=Sit(P)$; $s \sqsubseteq ^e t$ iff $t \le s$; $L^e = Sit(1)$; $R^e stu$ iff $u \le s \cdot t$; $C^e st$ iff Cst; $E^e_a(s)=Sit(\sigma _a(s))$; $V^e(p)=Sit(V(p))$.

Lemma 9

If $\mathfrak {N}$ is a relevant information model then $\mathfrak {N}^e$ is a relevant epistemic model.

Lemma 10

Let $\mathfrak {M} = (S, \sqsubseteq , L, R, C, E, V)$ be a relevant epistemic model and let $\mathfrak {M}^{ie} = (S^{ie}, \sqsubseteq ^{ie}, L^{ie}, R^{ie}, C^{ie}, E^{ie}, V^{ie})$. Then the map assigning to any $s \in S$ the set $s^{\uparrow }$ is a bijection between S and $S^{ie}$. Moreover, the following holds: (a) $s \sqsubseteq t$ iff $s^{\uparrow } \sqsubseteq ^{ie} t^{\uparrow }$, (b) $s \in L$ iff $s^{\uparrow } \in L^{ie}$, (c) Rstu iff $R^{ie}s^{\uparrow }t^{\uparrow }u^{\uparrow }$, (d) Cst iff $C^{ie}s^{\uparrow }t^{\uparrow }$, (e) $E_a st$ iff $E^{ie}_a s^{\uparrow }t^{\uparrow }$, (f) $s \in V(p)$ iff $s^{\uparrow } \in V^{ie}(p)$.

Proof

For an illustration, we will just show how to prove (c) and (e). The proof of (c) goes as follows: $R^{ie}s^{\uparrow }t^{\uparrow }u^{\uparrow }$ iff $u^{\uparrow } \le ^i s^{\uparrow }\cdot ^i t^{\uparrow }$ iff $u^{\uparrow } \subseteq s^{\uparrow }\cdot ^i t^{\uparrow }$ iff $u \in s^{\uparrow }\cdot ^i t^{\uparrow }$ iff $\exists v \in s^{\uparrow } \exists w \in t^{\uparrow }$: Rvwu iff Rstu. (e) can be proved in the following way: $E_a st$ iff $t \in \sigma ^i_a(s^{\uparrow })$ iff $t^{\uparrow } \le ^i \sigma ^i_a(s^{\uparrow })$ iff $E^{ie}_a s^{\uparrow }t^{\uparrow }$.

Lemma 11

Let $\mathfrak {N} = (P, \le , 1, \cdot , C, \sigma , V)$ be a relevant information model and let $\mathfrak {N}^{ei} = (P^{ei}, \le ^{ei}, 1^{ei}, \cdot ^{ei}, C^{ei}, \sigma ^{ei}, V^{ei})$. The map assigning to any $x \in P$ the set Sit(x) is a bijection between P and $P^{ei}$. Moreover, the following holds: (a) $x \le y$ iff $Sit(x) \le ^{ei} Sit(y)$, (b) $Sit(1)=1^{ei}$, (c) $Sit(x \cdot \,y) = Sit(x) \cdot ^{ei} Sit(y)$, (d) Cxy iff $C^{ei}Sit(x)Sit(y)$, (e) $Sit(\sigma _a (s))=\sigma ^{ei}_a (Sit(s))$, (f) $Sit(V(p))=V^{ei}(p)$.

Lemmas 10 and 11 lead directly to the following theorem.

Theorem 3

$\mathfrak {M}$ is isomorphic to $\mathfrak {M}^{ie}$, for every relevant epistemic model $\mathfrak {M}$, and $\mathfrak {N}$ is isomorphic to $\mathfrak {N}^{ei}$, for every relevant information model $\mathfrak {N}$.

Theorems 3 and 2 together show that the the semantics based on relevant information models is indeed a dual counterpart of the semantics based on relevant epistemic models. As a consequence, $\mathsf {RPAC}$ is also complete with respect to relevant information models.

5 Questions

In this section we will extend the language $\mathcal {L}$ so that it will be possible to express not only statements but also questions. To this end, we will borrow some techniques from inquisitive semantics (see, e.g., [5, 7]). Let $\mathcal {L}^{inq}$ denote the language $\mathcal {L}$ enriched with a binary connective called inquisitive disjunction. The operator can be embedded arbitrarily under any operator with the exception of the public announcement modality. We will assume that ${ \texttt {[}} \varphi { \texttt {]}} \nu$ is in the language $\mathcal {L}^{inq}$ only if $\varphi$ is a formula of the language $\mathcal {L}$ (but $\nu$ may contain inquisitive disjunction).

The formulas of the language $\mathcal {L}$ will be called declarative. The connective produces questions from declarative formulas. Given declarative formulas $\varphi , \psi$, the formula expresses the question whether $\varphi$ or $\psi$. This can be contrasted with $\varphi \vee \psi$ which expresses the statement that $\varphi$ or $\psi$. (Recall that $\varphi \vee \psi$ is defined as $\lnot (\lnot \varphi \wedge \lnot \psi )$). The support condition for this additional connective is defined as follows:

• iff $(\mathfrak {N}, x) \Vdash \nu$ or $(\mathfrak {N}, x) \Vdash \mu$.

This captures the idea that an information state resolves a question if it provides some answer to the question. Compare the clause to the support condition for the declarative disjunction $\vee$ spelled out in the following lemma.

Lemma 12

$(\mathfrak {N}, x) \Vdash \nu \vee \mu$ iff for all $s \in Sit(x)$, $(\mathfrak {N}, s) \Vdash \nu$ or $(\mathfrak {N}, s) \Vdash \mu$.

In the language $\mathcal {L}^{inq}$ we can express directly, for example, that the agent’s information state resolves the question $\nu$ ($B_a \nu$), that the question is resolved by the common knowledge in a group ($C_A \nu$), or that $\nu$ would be resolved after the public announcement of $\varphi$ (${ \texttt {[}} \varphi { \texttt {]}} \nu$).

It is obvious from the semantic clause for inquisitive disjunction that the set of states supporting is the union of the set of states supporting $\nu$ and the set of states supporting $\mu$. As a consequence, Lemma 6 cannot be formulated for the whole language $\mathcal {L}^{inq}$. Sets of states supporting formulas of $\mathcal {L}^{inq}$ are not in general closed under join, though they are always downward closed and nonempty (contain always the least element).

Let $\mathsf {InqRPAC}$ be the logic consisting of all formulas from the language $\mathcal {L}^{inq}$ that are valid in all relevant information models. In formulation of an axiomatic system for $\mathsf {InqRPAC}$ we have to be careful to specify which schemata of $\mathsf {RPAC}$ are semantically valid for the whole language $\mathcal {L}^{inq}$ and which must be restricted to the declarative language $\mathcal {L}$. In particular, we can take the axiomatization of $\mathsf {RPAC}$ as specified in Fig. 1 and assume that we can substitute any formulas of $\mathcal {L}^{inq}$ for the variables in the axiom and rule schemata, with the exception of the variables occurring in the scope of the public announcement modality and in the double negation axiom (which is among the axioms of $\mathsf {R}$), the reduction axiom for the belief modality (A7), and the rules (R6) and (R7). That is, the exception concerns the public announcement modality and the following axioms and rules:

To secure soundness we must assume that only declarative formulas can be substituted for $\varphi$ and $\psi$ in these four schemata (but any formula of $\mathcal {L}^{inq}$ can be substituted for $\nu$). Let us illustrate the reason behind this restriction on the rule R6. Assume that $\nu \rightarrow (\varphi \wedge B_A \nu )$ is valid in a relevant information model $\mathfrak {N}$ and assume that $\mathfrak {N}, x \Vdash \nu$. Then $\mathfrak {N}, x \Vdash \varphi \wedge B_A \nu$. Let $s \in Sit(x)$. Then $\varphi$ is supported by every state in . Since we assume that $\varphi$ is in $\mathcal {L}$, it is supported also by the join of this set, i.e. by $\sigma ^*_A(s)$. Since this holds for every $s \in Sit(x)$, we obtain $\mathfrak {N}, x \Vdash C_A \varphi$ as desired. Hence, $\nu \rightarrow C_A \varphi$ is valid in $\mathfrak {N}$.

The system for $\mathsf {InqRPAC}$ consists of the system for $\mathsf {RPAC}$, adjusted to the language $\mathcal {L}^{inq}$ in the just described way, and extended with the axioms in Fig. 2 that characterize inquisitive disjunction. Note that while $\nu , \mu , \theta$ range over arbitrary formulas of $\mathcal {L}^{inq}$, $\varphi$ (in the axioms Inq7 and Inq10) is again restricted to formulas of $\mathcal {L}$. The axioms Inq1-Inq3 are the standard (introduction and elimination) axioms for disjunction. The axioms Inq4-Inq10 specify how the other operators of the language distribute over inquisitive disjunction. Note that the inverse implications of Inq4-Inq10 are provable from the other axioms.

Fig. 2.

The axioms for inquisitive disjunction in the system for $\mathsf {InqRPAC}$.

Lemma 13

The system for $\mathsf {InqRPAC}$ is sound with respect to all relevant information models.

We can prove completeness of the system $\mathsf {InqRPAC}$ using a strategy that is common in inquisitive logic (see, e.g., [15]). In our specific setting this strategy amounts to the reduction of completeness for $\mathsf {InqRPAC}$ to completeness for $\mathsf {RPAC}$ (which was proved in Sect. 3). Such a reduction is possible due to two characteristic properties of the logic that need to be proved: (1) disjunctive normal form, and (2) disjunction property.

Lemma 14

For any formula $\nu$ of $\mathcal {L}^{inq}$ there are formulas $\varphi _1, \ldots , \varphi _n$ of $\mathcal {L}$ such that is a theorem of $\mathsf {InqRPAC}$.

Proof

This is a straightforward extension of a standard theorem in inquisitive logic. (For more details, see, e.g., [13].) One can proceed by induction on the complexity of $\nu$ using the distributive axioms Inq4-Inq10 and their converses.

Lemma 15

Let $\nu , \mu$ be formulas of $\mathcal {L}^{inq}$. Then is valid in every relevant information model only if $\nu$ is valid in every relevant information model or $\mu$ is valid in every relevant information model.

Proof

To prove this claim, we will adapt to our current setting a technique developed in [13]. For any relevant information models $\mathfrak {N}_1 = (P_1, \le _1, 1_1, \cdot _1, C_1, \sigma _1, V_1)$ and $\mathfrak {N}_2 = (P_2, \le _2, 1_2, \cdot _2, C_2, \sigma _2, V_2)$ we can define their product $\mathfrak {N}_1 \times \mathfrak {N}_2 = (P, \le , 1, \cdot , C, \sigma , V)$ where $P = P_1 \times P_2$ (the Cartesian product of $P_1$ and $P_2$); $(x,y) \le (v,w)$ iff $x \le _1 v$ and $y \le _2 w$; $1=(1_1, 1_2)$; $(x,y) \cdot (v,w)=(x \cdot _1 v, y \cdot _2 w)$; C(x, y)(v, w) iff $C_1xv$ or $C_2yw$; $\sigma _a((s,t))=(\sigma _1(a)(s), \sigma _2(a)(t))$; $V(p)=(V_1(p),V_2(p))$. It can be shown that $\mathfrak {N}_1 \times \mathfrak {N}_2$ is again a relevant information model. Assume that $0_1$ is the least element of $\mathfrak {N}_1$ and $0_2$ is the least element of $\mathfrak {N}_2$. The following holds for any formula $\nu$ of $\mathcal {L}^{inq}$:

• (a) $(\mathfrak {N}_1 \times \mathfrak {N}_2, (x, 0_2)) \Vdash \nu$ iff $(\mathfrak {N}_1, x) \Vdash \nu$,

• (b) $(\mathfrak {N}_1 \times \mathfrak {N}_2, (0_1, y)) \Vdash \nu$ iff $(\mathfrak {N}_2, y) \Vdash \nu$.

These claims can be proved by induction on the complexity of $\nu$. For an illustration, let us consider the inductive step for ${ \texttt {[}} \varphi { \texttt {]}}$. Assume that (a) and (b) hold for some $\varphi$ from $\mathcal {L}$ and $\mu$ from $\mathcal {L}^{inq}$. Using the induction hypothesis it can be shown that $(\mathfrak {N}_1 \times \mathfrak {N}_2)^{{ \texttt {[}} \varphi { \texttt {]}}} = \mathfrak {N}^{{ \texttt {[}} \varphi { \texttt {]}}}_1 \times \mathfrak {N}^{{ \texttt {[}} \varphi { \texttt {]}}}_2$. Using this fact we can prove the inductive step for ${ \texttt {[}} \varphi { \texttt {]}}$ as follows: $(\mathfrak {N}_1 \times \mathfrak {N}_2, (x, 0_2)) \Vdash { \texttt {[}} \varphi { \texttt {]}}\mu$ iff $((\mathfrak {N}_1 \times \mathfrak {N}_2)^{{ \texttt {[}} \varphi { \texttt {]}}}, (x, 0_2)) \Vdash \mu$ iff $(\mathfrak {N}^{{ \texttt {[}} \varphi { \texttt {]}}}_1 \times \mathfrak {N}^{{ \texttt {[}} \varphi { \texttt {]}}}_2, (x, 0_2)) \Vdash \mu$ iff $(\mathfrak {N}^{{ \texttt {[}} \varphi { \texttt {]}}}_1, x) \Vdash \mu$ iff $(\mathfrak {N}_1, x) \Vdash { \texttt {[}} \varphi { \texttt {]}} \mu$. The step for (b) is analogous.

Assuming that we have proved (a) and (b) we can prove disjunction property as follows. Assume that there is a relevant information model $\mathfrak {N}_1$ in which $\nu$ is not valid, and a relevant information model $\mathfrak {N}_2$ in which $\mu$ is not valid. Then $(\mathfrak {N}_1, 1_1) \nVdash \nu$ and $(\mathfrak {N}_2, 1_2) \nVdash \mu$. If follows from (a) and (b) that $(\mathfrak {N}_1 \times \mathfrak {N}_2, (1_1, 0_2)) \nVdash \nu$ and $(\mathfrak {N}_1 \times \mathfrak {N}_2, (0_1, 1_2)) \nVdash \mu$. By persistence, and thus is not valid in $\mathfrak {N}_1 \times \mathfrak {N}_2$.

Theorem 4

$\nu$ is a theorem of $\mathsf {InqRPAC}$ iff $\nu$ is valid in all relevant information models.

Proof

The left-to-right direction amounts to Lemma 13. For the right-to-left direction assume that $\nu$ is valid in all relevant information models. Then, by disjunctive normal form (Lemma 14), there are $\varphi _1, \ldots , \varphi _n$ in $\mathcal {L}$ such that is a theorem of $\mathsf {InqRPAC}$. By soundness (Lemma 13), is valid in all relevant information models. By disjunction property (Lemma 15), for some i, $\varphi _i$ is valid in all relevant information models. By duality between relevant information models and relevant epistemic models for $\mathcal {L}$ (Theorems 3 and 2) we obtain that $\varphi _i$ is valid in every relevant epistemic model. By completeness of $\mathsf {RPAC}$ w.r.t. relevant epistemic models (Theorem 1), $\varphi _i$ is a theorem of $\mathsf {RPAC}$. Since $\mathsf {InqRPAC}$ is an extension of $\mathsf {RPAC}$, $\varphi _i$ is also a theorem of $\mathsf {InqRPAC}$. It follows that is a theorem of $\mathsf {InqRPAC}$. Hence, $\nu$ is a theorem of $\mathsf {InqRPAC}$.

The semantics based on information models allows us to equip agents not only with information states but also with issues.⁴ Then one can define also a public utterance of questions and the inquisitive analogues of the modalities $B_a$ and $C_A$.⁵ This would be an interesting further extension of the language $\mathcal {L}^{inq}$. However, the methods employed in this paper cannot be directly applied to this extension. The reason is that completeness for such a language cannot be straightforwardly reduced to completeness of its non-inquisitive fragment, which was possible in the case of the language $\mathcal {L}^{inq}$. The inquisitive analogue of $B_a$ was studied in the context of substructural inquisitive logics in [16]. The investigation of the inquisitive analogue of $C_A$ is left for future research.

6 Conclusion

This paper can be seen as a further expansion of our previous work on modal and inquisitive substructural logics [13,14,15,16, 24, 25]. In particular, we have extended the relevant logic $\mathsf {R}$ with various epistemic operators and studied their interactions. The main novelty of the paper is the incorporation of common knowledge into this rich context. The main result of the paper is a completeness of $\mathsf {R}$, extended with a belief modality, public announcement and common knowledge, with respect to a suitable relational semantics (Theorem 1). We also considered an alternative semantics that allowed us to express also questions in the object language and we presented a completeness proof also for this enriched language (Theorem 4).