Evidence Logics with Relational Evidence

TL;DR

This paper introduces a new family of dynamic logics for reasoning about relational evidence, specifically involving plausibility orderings of states, with sound and complete axiomatizations and dynamic actions.

Contribution

It presents novel logics for relational evidence with formal axiomatizations and extends them to dynamic actions, filling a gap in evidence reasoning frameworks.

Findings

Provided sound and complete axiomatizations for the new logics.

Developed dynamic logics with evidential actions and proved their soundness and completeness.

Enhanced formal tools for reasoning about evidence involving plausibility orderings.

Abstract

Dynamic evidence logics are logics for reasoning about the evidence and evidence-based beliefs of agents in a dynamic environment. In this paper, we introduce a family of logics for reasoning about relational evidence: evidence that involves an orderings of states in terms of their relative plausibility. We provide sound and complete axiomatizations for the logics. We also present several evidential actions and prove soundness and completeness for the associated dynamic logics.

Tables

Table 1. Table 1: The systems 𝖫 ∩ subscript 𝖫 \mathsf{L}_{\cap} and 𝖫 𝗅𝖾𝗑 subscript 𝖫 𝗅𝖾𝗑 \mathsf{L}_{\mathsf{lex}}

Axioms and inference rules	System(s)
All tautologies of propositional logic	both
$\mathrm{𝖲𝟧}$ axioms for $\forall$, $\mathrm{𝖲𝟦}$ axioms for $\square$, axiom $\mathrm{𝟦}$ for ${\square }_0$	both
$\forall \phi \to {\square }_0\phi$ (Universality for ${\square }_0$)	both
$\left({\square }_0\phi \wedge \forall \psi \right)\leftrightarrow {\square }_0\left(\phi \wedge \forall \psi \right)$ (Pullout)	both
${\square }_0\phi \to \square \phi$	${𝖫}_{\cap }$
Axioms $𝖳$ and $𝖭$ for ${\square }_0$	${𝖫}_{\mathrm{𝗅𝖾𝗑}}$
$\forall \phi \to \square \phi$ (Universality for $\square$)	${𝖫}_{\mathrm{𝗅𝖾𝗑}}$
Modus ponens	both
Necessitation Rule for $\bullet \in \{\forall ,\square \}$ (from $\phi$ infer $\bullet \phi$)	both
Monotonicity Rule for ${\square }_0$ (from $\phi \to \psi$ infer ${\square }_0\phi \to {\square }_0\psi$)	both

Equations

$$(w,v)\in \mathsf{lex}(⟨\mathcal{R},⪯⟩)\text{ iff }\forall R^{\prime }\in \mathcal{R}(R^{\prime }wv\vee \exists R\in \mathcal{R}(R^{\prime }\prec R\wedge R^{<}wv))$$

$$\phi ::=p\mid \neg \phi \mid \phi \wedge \phi \mid {\square }_0\phi \mid \square \phi \mid \forall \phi (p\in \mathsf{P})$$

$$\displaystyle\begin{array}[]{@{}>{\displaystyle}l@{}>{\displaystyle{}}l@{}>{\displaystyle{{}}}l@{{}}}M,w\models p&\text{ iff }w\in V(p)\\ M,w\models\neg\varphi&\text{ iff }M,w\not\models\varphi\\ M,w\models\varphi\wedge\psi&\text{ iff }M,w\models\varphi\text{ and }M,w\models\psi\\ M,w\models\Box_{0}\varphi&\text{ iff }\text{there is }R\in\mathscr{R}\text{ such that, for all }v\in W,Rwv\text{ implies }M,v\models\varphi\\ M,w\models\Box\varphi&\text{ iff }\text{for all }v\in W,Ag(\langle\mathscr{R},\preceq\rangle)wv\text{ implies }M,v\models\varphi\\ M,w\models\forall\varphi&\text{ iff }\text{for all }v\in W,M,v\models\varphi\end{array}$$

$$\pi ::=A\mid ?\phi \mid \pi \cup \pi \mid \pi ;\pi \mid {\pi }^{\ast }$$

$${\pi }^t({\phi }_1,\dots ,{\phi }_n):=(A;?{\phi }_1)$$

$$\cup (?\neg {\phi }_1;\neg {\phi }_2;A;?\neg {\phi }_1;?\neg {\phi }_2;?{\phi }_3)$$

$$\cup \dots$$

$$\cup (?\neg {\phi }_1;\dots ;?\neg {\phi }_n;A;?\neg {\phi }_1;\dots ;?\neg {\phi }_{n-1};?{\phi }_n)$$

$$\displaystyle\begin{array}[]{@{}>{\displaystyle}l@{}>{\displaystyle{}}l@{}>{\displaystyle{{}}}l@{{}}}M,w\models\Box_{0}\varphi&\text{ iff }\text{there is }e\in E_{0}\text{ such that }w\in e\subseteq\llbracket\varphi\rrbracket_{M}\\ M,w\models\Box\varphi&\text{ iff }\text{there is }e\in E\text{ such that }w\in e\subseteq\llbracket\varphi\rrbracket_{M}\\ M,w\models\forall\varphi&\text{ iff }W=\llbracket\varphi\rrbracket_{M}\end{array}$$

$$⟨W,E_0,V⟩\mapsto ⟨Rel(W),⟨Rel(E_0),⪯⟩,Rel(V),A{g}_{\cap }⟩$$

$$\displaystyle\begin{array}[]{@{}>{\displaystyle}l@{}>{\displaystyle{}}l@{}>{\displaystyle{{}}}l@{{}}}\varphi&\Coloneqq&\ p\mid\neg\varphi\mid\varphi\wedge\varphi\mid\Box_{0}\varphi\mid\Box\varphi\mid\forall\varphi\mid[!\varphi]\varphi\ \ \ (p\in\mathsf{P})\end{array}$$

$$\displaystyle\begin{array}[]{@{}>{\displaystyle}l@{}>{\displaystyle{}}l@{}>{\displaystyle{{}}}l@{{}}}\varphi&\Coloneqq&\ p\mid\neg\varphi\mid\varphi\wedge\varphi\mid\Box_{0}\varphi\mid\Box\varphi\mid\forall\varphi\mid[\bullet\pi^{*}]\varphi\ \ (p\in\mathsf{P})\\ \pi&\Coloneqq&\ A\mid?\varphi\mid\pi\cup\pi\mid\pi;\pi\mid\pi^{*}\end{array}$$

$$J(\mathbf{\phi }):=$$

$${\pi }^{\cap }(\chi ):=$$

$${\pi }^{<}(\chi ):=$$

$$\mathsf{su}{\mathsf{c}}^{<}(\chi ):=$$

$$\displaystyle\begin{array}[]{@{}>{\displaystyle}l@{}>{\displaystyle{}}l@{}>{\displaystyle{{}}}l@{{}}}\varphi&\Coloneqq&\ p\mid\neg\varphi\mid\varphi\wedge\varphi\mid\Box_{0}\varphi\mid\Box\varphi\mid\forall\varphi\mid[\oplus\pi^{*}]\varphi\ \ (p\in\mathsf{P})\\ \pi&\Coloneqq&\ A\mid?\varphi\mid\pi\cup\pi\mid\pi;\pi\mid\pi^{*}\end{array}$$

$${\pi }^{<}(\chi ):=$$

$$\mathsf{su}{\mathsf{c}}^{<}(\chi ):=$$

$${⪯}^{\oplus \vec{R}}:=⪯$$

$$\cup \dots$$

$$\cup \{(R,R_n)\mid R\in \mathcal{R}\cup \{R_j\mid j\in \{1,\dots ,n-1\}\}\}$$

$$\phi ::=p\mid \neg \phi \mid \phi \wedge \phi \mid {\square }_0\phi \mid {\square }^{\vec{\pi }}\phi \mid \forall \phi (p\in \mathsf{P});\pi ::=A\mid ?\phi \mid \pi \cup \pi \mid \pi ;\pi \mid {\pi }^{\ast }$$

$$\phi ::=p\mid \neg \phi \mid \phi \wedge \phi \mid {\square }_0\phi \mid {\square }^{\pi }\phi \mid \forall \phi \mid [\oplus \vec{\pi }]\phi (p\in \mathsf{P});\pi ::=A\mid ?\phi \mid \pi \cup \pi \mid \pi ;\pi \mid {\pi }^{\ast }$$

$$M,w\models {\square }_0\psi \text{ iff }$$

$$\text{there is an }{R}_e\in Rel(E_0)\text{ such that }{R}_e[w]=e\text{ and }e\subseteq [[\psi {]]}_M$$

$$\stackrel{i.h.}{\mathrm{iff}}$$

$$Rel(M),w\models {\square }_0\psi$$

$$M,w\models \square \psi \text{ iff }$$

$$\text{ there are }{e}_1,\dots ,e_n\in E_0\text{ such that }\bigcap _{i=1}^n{e}_i=e$$

$$\text{ and }w\in e\subseteq [[\psi {]]}_M$$

$$\text{ there are }{R}_{e_1},\dots ,R_{e_n}\in Rel(E_0)\text{ such that }{R}_{e_i}[w]=e_i$$

$$\text{ and }w\in e\subseteq [[\psi {]]}_M$$

$$\text{ there are }{R}_{e_1},\dots ,R_{e_n}\in Rel(E_0)\text{ such that }(\bigcap _{i=1}^n{R}_{e_i})[w]\subseteq [[\psi {]]}_M$$

$$(\bigcap \mathcal{R})[w]\subseteq (\bigcap _{i=1}^n{R}_{e_i})[w]\subseteq [[\psi {]]}_M$$

$$\stackrel{i.h.}{\mathrm{iff}}$$

$$Rel(M),w\models \square \psi$$

$$(\bigcap _{R\in Rel(E_0)}R)[0]=\bigcap _{e\in E_0}(R_e[0])$$

$$\bigcap _{e\in E_0}(R_e[0])=\bigcap _{e\in E_0}(e)=\bigcap E_0$$

$$\pi^{\prime}\coloneqq\bigcup_{s\in S_{0}(I)}\Big{(}?(\varphi_{s_{1}}\wedge\bigwedge^{\mathsf{len}(s)}_{k=2}(\exists(\psi_{s_{k-1}}\wedge\varphi_{s_{k}})));A;?\psi_{s_{\mathsf{len}(s)}})\Big{)}\cup(?\top)$$

Full text

Dynamic evidence logics [18, 17, 19, 20, 2] are logics for reasoning about the evidence and evidence-based beliefs of agents in a dynamic environment. Evidence logics are concerned with scenarios in which an agent collects several pieces of evidence about a situation of interest, from a number of sources, and uses this evidence to form and revise her beliefs about this situation. The agent is typically uncertain about the actual state of affairs, and as a result takes several alternative descriptions of this state as possible (these descriptions are typically called possible worlds or possible states). The existing evidence logics, i.e., neighborhood evidence logics (NEL) [18, 17, 19, 20, 2], have the following features:

All evidence is ‘binary’. Each piece of evidence is modeled as a set of possible states. This set indicates which states are good candidates for the actual state, and which ones are not, according to the source. Hence the name binary; every state is either a good candidate (‘in’), or a bad candidate (‘out’). 2. 2.

All evidence is equally reliable. The agent treats all evidence pieces on a par. There is no explicit modeling of the relative reliability of pieces of evidence. 3. 3.

One procedure to combine evidence. The logics developed so far study the evidence and beliefs held by an agent relying on one specific procedure for combining evidence.

This work presents a family of dynamic evidence logics which we call relational evidence logics (REL). Relational evidence logics aim to contribute to the existing work on evidence logic as follows.

Relax the assumption that all evidence is binary. This is accomplished by modeling pieces of evidence by evidence relations. Evidence relations are preorders over the set of possible states. The ordering is meant to represent the relative plausibility of states given an evidence item. While a special type of evidence relation – dichotomous weak order – can be used to represent binary evidence, less ‘black-and-white’ forms of evidence can also be encoded in REL models. 2. 2.

Model levels of evidence reliability. In general, not all evidence is equally reliable. Expert advice and gossip provide very different grounds for belief, and a rational agent should weight the evidence that it is exposed to accordingly. To model evidence reliability, we equipped our models with priority orders, i.e., orderings of the family of evidence relations according to their relative reliability. Priority orders were introduced in [1], and have already been used in other DEL logics (see, e.g. [11, 14]). Here, we use them to model the relative reliability of pieces of evidence. 3. 3.

Explore alternative evidence aggregation rules. Our evidence models come equipped with an aggregator, which merges the available evidence relations into a single relation representing the combined plausibility of the possible states. The beliefs of the agent are then defined on the basis of this combined plausibility order. By focusing on different classes of evidence models, given by their underlying aggregator, we can then compare the logics of belief arising from different approaches to combining evidence.

1 Relational Evidence Models

Relational evidence. We call relational evidence any type of evidence that induces an ordering of states in terms of their relative plausibility. A suitable representation for relational evidence, which we adopt, is given by the class of preorders. We call preorders representing relational evidence, evidence relations, or evidence orders. As is well-known, preorders can represent several meaningful types of orderings, including those that feature incomparable or tied alternatives.

Definition 1 (Preorder)

A preorder is a binary relation that is reflexive and transitive. We denote the set of all preorders on a set $X$ by $Pre(X)$. For a preorder $R$ on $X$ and an element $x\in X$, we define the following associated notions: $R[x]\coloneqq\{y\in X\mid Rxy\}$; $R^{<}\coloneqq\{(x,y)\in X^{2}\mid Rxy\text{ and }\neg Ryx\}$; $R^{\sim}\coloneqq\{(x,y)\in X^{2}\mid Rxy\text{ and }Ryx\}$.

Evidence reliability. In general, not all sources are equally trustworthy, so an agent combining evidence may be justified in giving priority to some evidence items over others. Thus, as suggested in [20], a next reasonable step in evidence logics is modeling levels of reliability of evidence. One general format for this is given by the priority graphs of [1], which have already been used extensively in dynamic epistemic logic (see, e.g., [11, 14]). In this thesis, we will use the related, yet simpler format of a ‘priority order’, as used in [4, 5], to represent hierarchy among pieces of evidence. Our definition of a priority order is as follows:

Definition 2 (Priority order)

Let $\mathscr{R}$ be a family of evidence orders over $W$. A priority order for $\mathscr{R}$ is a preorder $\preceq$ on $\mathscr{R}$. For $R,R^{\prime}\in\mathscr{R}$, $R\preceq R^{\prime}$ reads as: “the evidence order $R^{\prime}$ has at least the same priority as evidence order $R$”.

Intuitively, priority orders tell us which pieces of evidence are more reliable according to the agent. They give the agent a natural way to break stalemates when faced with inconsistent evidence.

Evidence aggregators. We are interested in modeling a situation in which an agent integrates evidence obtained from multiple sources to obtain and update a combined plausibility ordering, and forms beliefs based on this ordering. When we consider relational evidence with varying levels of priority, a natural way model the process of evidence combination is to define a function that takes as input a family of evidence orders $\mathscr{R}$ together with a priority order $\preceq$ defined on them, and combines them into a plausibility order. The agent’s beliefs can then be defined in terms of this output.

Definition 3 (Evidence aggregator)

Let $W$ be a set of alternatives. Let $\mathcal{W}$ be the set of preorders on $W$. An evidence aggregator for $W$ is a function $Ag$ mapping any preordered family $P=\langle\mathscr{R},\preceq\rangle$ to a preorder $Ag(P)$ on $W$, where $\emptyset\not\in\mathscr{R}\subseteq\mathcal{W}$ and $\preceq$ is a preorder on $\mathscr{R}$. $\mathscr{R}$ is seen here as a family of evidence orders over $W$, $\preceq$ as a priority order for $\mathscr{R}$, and $Ag(P)$ as an evidence-based plausibility order on $W$.

At first glance, our definition of an aggregator may seem to impose mild constraints that are met by most natural aggregation functions. However, as it is well-known, the output of some common rules, like the majority rule, may not be transitive (thus not a preorder), and hence they don’t count as aggregators. A specific aggregator that does satisfy the constraints is the lexicographic rule. This aggregator was extensively studied in [1], where it was shown to satisfy several nice aggregative properties. The definition of the aggregator is the following:

Definition 4

The (anti-)lexicographic rule is the aggregator $\mathsf{lex}$ given by

[TABLE]

Intuitively, the lexicographic rule works as follows. Given a particular hierarchy $\preceq$ over a family of evidence $\mathscr{R}$, aggregation is done by giving priority to the evidence orders further up the hierarchy in a compensating way: the agent follows what all evidence orders agree on, if it can, or follows more influential pieces of evidence, in case of disagreement. Other well-known aggregators that satisfy the constraints, but don’t make use of the priority structure, are the intersection rule (defined below), or the Borda rule.

Definition 5

The intersection rule is the aggregator $Ag_{\cap}$ given by $(w,v)\in Ag_{\cap}(\langle\mathscr{R},\preceq\rangle)\text{ iff }(w,v)\in\bigcap\mathscr{R}$.

The models. Having defined relational evidence and evidence aggregators, we are now ready to introduce relational evidence models.

Definition 6 (Relational evidence model)

Let $\mathsf{P}$ be a set of propositional variables. A relational evidence model (REL model, for short) is a tuple $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,Ag\rangle$ where $W$ is a non-empty set of states; $\langle\mathscr{R},\preceq\rangle$ is an ordered family of evidence, where: $\mathscr{R}$ is a set of evidence orders on $W$ with $W^{2}\in\mathscr{R}$ and $\preceq$ is a priority order for $\mathscr{R}$; $V:\mathsf{P}\to 2^{W}$ is a valuation function; $Ag$ is an evidence aggregator for $W$. $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,Ag\rangle$ is said to be an $f$-model iff $Ag=f$.

$W^{2}\in\mathscr{R}$ is called the trivial evidence order. It represents the evidence stating that “the actual state is in $W$”. This evidence represents full uncertainty and is taken to be always available to the agent as a starting point.

1.0.1 Syntax and semantics.

We now introduce a static language for reasoning about relational evidence, which we call $\mathscr{L}$. In [2], this language is interpreted over NEL models (there, the language is called $\mathscr{L}_{\forall\Box\Box_{0}}$).

Definition 7 ($\mathscr{L}$)

Let $\mathsf{P}$ be a countably infinite set of propositional variables. The language $\mathscr{L}$ is defined by:

[TABLE]

We define $\bot\coloneqq p\wedge\neg p$ and $\top\coloneqq\neg\bot$. The Boolean connectives $\lor$ and $\to$ are defined in terms of $\neg$ and $\wedge$ in the usual manner. The duals of the modal operators are defined in the following way: $\Diamond_{0}\coloneqq\neg\Box_{0}\neg$, $\Diamond\coloneqq\neg\Box\neg$, $\exists\coloneqq\neg\forall\neg$.

The intended interpretation of the modalities is as follows. $\Box_{0}\varphi$ reads as: ‘the agent has basic, factive evidence for $\varphi$’; $\Box\varphi$ reads as: ‘the agent has combined, factive evidence for $\varphi$’. The language $\mathscr{L}$ is interpreted over REL models as follows.

Definition 8 (Satisfaction)

Let $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,Ag\rangle$ be an REL model and $w\in W$. The satisfaction relation $\models$ between pairs $(M,w)$ and formulas $\varphi\in\mathscr{L}$ is defined as follows:

[TABLE]

Definition 9 (Truth map)

Let $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,Ag\rangle$ be a REL model. We define a truth map $\llbracket\cdot\rrbracket_{M}:\mathscr{L}\to 2^{W}$ given by: $\llbracket\varphi\rrbracket_{M}=\{w\in W\mid M,w\models\varphi\}$

Next, we introduce some definable notions of evidence and belief over $\mathsf{REL}$ models. Fix a model $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,Ag\rangle$.

1.0.2 Basic (factive) evidence.

We say that a piece of evidence $R\in\mathscr{R}$ supports $\varphi$ at $w\in W$ iff $R[w]\subseteq\llbracket\varphi\rrbracket_{M}$. That is, every world that is at least as plausible as $w$ under $R$ satisfies $\varphi$. Using this notion of support, we say that the agent has basic, factive evidence for $\varphi$ at $w\in W$ if there is a piece of evidence $R\in\mathscr{R}$ that supports $\varphi$ at $w$. That is: ‘the agent has basic evidence for $\varphi$ at $w\in W$’ iff $\exists R\in\mathscr{R}(R[w]\subseteq\llbracket\varphi\rrbracket_{M})$ iff $M,w\models\Box_{0}\varphi$. We also have a non-factive version of this notion, which says that the agent has basic evidence for $\varphi$ if there is a piece of evidence $R$ that supports $\varphi$ at some state, i.e.: ‘the agent has basic evidence for $\varphi$ (at any state)’ iff $\exists w(\exists R\in\mathscr{R}(R[w]\subseteq\llbracket\varphi\rrbracket_{M}))$ iff $M,w\models\exists\Box_{0}\varphi$. We can also have a conditional version of basic evidence: ‘the agent has basic, factive evidence for $\psi$ at $w$, conditional on $\varphi$ being true’. Putting $\Box_{0}^{\varphi}\psi\coloneqq\Box_{0}(\varphi\to\psi)$, we have: ‘the agent has basic, factive evidence for $\psi$ at $w$, conditional on $\varphi$ being true’ iff $\exists R\in\mathscr{R}(\forall v(Rwv\Rightarrow(v\in\llbracket\varphi\rrbracket_{M}\Rightarrow v\in\llbracket\psi\rrbracket_{M})))$ iff $M,w\models\Box_{0}^{\varphi}\psi$. The notion of conditional evidence reduces to that of plain evidence when $\varphi=\top$.

1.0.3 Aggregated (factive) evidence.

We propose a notion of aggregated evidence based on the output of the aggregator: the agent has aggregated, factive evidence for $\varphi$ at $w\in W$ iff $Ag(\langle\mathscr{R},\preceq\rangle)[w]\subseteq\llbracket\varphi\rrbracket_{M}$ iff $M,w\models\Box\varphi$. The non-factive version of the previous notion is as follows: the agent has aggregated evidence for $\varphi$ (at any state) iff $\exists w(Ag(\langle\mathscr{R},\preceq\rangle)[w]\subseteq\llbracket\varphi\rrbracket_{M})$ iff $M,w\models\exists\Box\varphi$. As we did with basic evidence, we can define a conditional notion of aggregated evidence in $\varphi$ by putting $\Box^{\varphi}\psi\coloneqq\Box(\varphi\to\psi)$. The unconditional version is given by $\varphi=\top$.

1.0.4 Evidence-based belief.

The notion of belief we will work with is based on the agent’s plausibility order, which in REL models corresponds to the output of the aggregator. As we don’t require the plausibility order to be converse-well founded, it may have no maximal elements, which means that Grove’s definition of belief may yield inconsistent beliefs. For this reason, we adopt a usual generalization of Grove’s definition, which defines beliefs in terms of truth in all ‘plausible enough’ worlds (see, e.g., [19, 3]). Putting $B\varphi\coloneqq\forall\Diamond\Box\varphi$, we have: the agent believes $\varphi$ (at any state) iff $\forall w(\exists v((w,v)\in Ag(\langle\mathscr{R},\preceq\rangle)\text{ and }Ag(\langle\mathscr{R},\preceq\rangle)[v]\subseteq\llbracket\varphi\rrbracket_{M}))$ iff $M,w\models\forall\Diamond\Box\varphi$. That is, the agent believes $\varphi$ iff for every state $w\in W$, we can always find a more plausible state $v\in\llbracket\varphi\rrbracket_{M}$, all whose successors are also in $\llbracket\varphi\rrbracket_{M}$. When the plausibility relation is indeed converse well-founded, this notion of belief coincides with Grove’s one, while ensuring consistency of belief otherwise. We can also define a notion of conditional belief. Putting $B^{\varphi}\psi\coloneqq\forall(\varphi\to\Diamond(\varphi\to(\Box\varphi\to\psi)))$, we have: ‘the agent believes $\psi$ conditional on $\varphi$ iff $\forall w(w\in\llbracket\varphi\rrbracket_{M}\Rightarrow\exists v(Ag(\langle\mathscr{R},\preceq\rangle)wv\text{ and }v\in\llbracket\varphi\rrbracket_{M}\text{ and }Ag(\langle\mathscr{R},\preceq\rangle)[v]\cap\llbracket\varphi\rrbracket_{M}\subseteq\llbracket\psi\rrbracket_{M}))$ iff $M,w\models B^{\varphi}\psi$. As before, this conditional notion reduces to that of absolute belief when $\varphi=\top$.

Example 1 (The diagnosis)

Consider an agent seeking medical advice on an ongoing health issue. To keep thing simple, assume that there are four possible diseases: asthma ($a$), allergy ($al$), cold ($c$), and flu ($f$). This can be described by a set $W$ consisting of four possible worlds, $\{w_{a},w_{al},w_{c},w_{f}\}$ and a set of atomic formulas $\{a,al,c,f\}$ (each true at the corresponding world). The agent consults three sources, a medical intern ($IN$), a family doctor ($FD$) and an allergist ($AL$). The doctors inspect the patient, observing fairly non-specific symptoms: cough, no fever, and some inconclusive swelling at an allergen test spot. Given the non-specificity of the symptoms, the doctors can’t single out a condition that best explains all they observed. Instead, comparing the diseases in terms of how well they explain the observed symptoms and drawing on their experience, each doctor arrives at a ranking of the possible diseases. Let us denote by $R_{IN}$, $R_{FD}$ and $R_{AL}$ the evidence orders representing the judgment of the intern, family doctor and allergist, respectively, which we assume to be as depicted below. If the agent has no information about how reliable each doctor is, she may just trust them all equally. We can model this by a priority order $\preceq$ over the evidence orders $R_{IN}\sim R_{FD}\sim R_{AL}$ that puts all evidence as equally likely. On the other hand, if the agent knows that the intern is the least experienced of the doctors, she may give consider his evidence as strictly less reliable than the one provided by the other doctors. Similarly, if allergist has a very strong reputation, the agent may wish to give the allergist’s judgment strict priority over the rest. We can model this by a different priority order $\preceq^{\prime}$ given by $R_{IN}\prec^{\prime}R_{FD}\prec^{\prime}R_{AL}$ (note that this is meant to be reflexive and transitive). If, e.g., the agent uses the lexicographic rule, we arrive at the following scenarios, with different aggregated evidence depending on the priority order used:

a$$al$$c$$f$$al$$a$$c$$f$$a$$al$$c$$f$$R_{IN}$$R_{FD}$$R_{AL}$$a$$al$$c$$fINFDALLexicographic aggregation based on \preceq$$\sim$$\sim$$a$$al$$c$$fLexicographic aggregation based on \preceq^{\prime}$$R_{IN}$$R_{FD}$$R_{AL}$$\prec$$\prec

The best candidates for the actual disease, in each case, are depicted in white. Note that, e.g., the agent has basic evidence for $a\vee al\vee c$, but she doesn’t have evidence for $f$. Moreover, in the scenario based on $\preceq^{\prime}$, the agent believes that the allergy is the actual disease, but she doesn’t in the scenario based on $\preceq$.

1.0.5 A $\mathsf{PDL}$ language for relational evidence

Later in this work, we will discuss evidential actions by which the agent, upon receiving a new piece of relational evidence, revises its existing body of evidence. To encode syntactically the evidence pieces featured in evidential actions, we will enrich our basic language $\mathscr{L}$ with formulas that stand for specific evidence relations. A natural way to introduce relation-defining expressions, in a modal setting such as ours, is to employ suitable program expressions from Propositional Dynamic Logic ($\mathsf{PDL}$). We will follow this approach, augmenting $\mathscr{L}$ with $\mathsf{PDL}$-style evidence programs that define pieces of relational evidence. As evidence orders are preorders, we will employ a set of program expressions whose terms are guaranteed to always define preorders. An natural fragment of $\mathsf{PDL}$ meeting this condition is the one provided by programs of the form $\pi^{*}$, which always define the reflexive transitive closure of some relation.

Definition 10 (Evidence programs)

The set $\Pi$ has all program symbols $\pi$ defined as follows:

[TABLE]

where $\varphi\in\mathscr{L}$. Here $A$ denotes the universal program, while the rest of the programs have their usual $\mathsf{PDL}$ meanings (see, e.g., [12]). We call $\Pi_{*}\coloneqq\{\pi^{*}\mid\pi\in\Pi\}$ the set of evidence programs.

To interpret evidence programs in REL models, we extend the truth map $\llbracket\cdot\rrbracket_{M}$ as follows:

Definition 11 (Truth map)

Let $M=\langle W,\langle\mathscr{R},\prec\rangle,V,Ag\rangle$ be an REL model. We define an extended truth map $\llbracket\cdot\rrbracket_{M}:\mathscr{L}\cup\Pi\to 2^{W}\cup 2^{W^{2}}$ given by: $\llbracket\varphi\rrbracket_{M}=\{w\in W\mid M,w\models\varphi\}$; $\llbracket A\rrbracket_{M}=W^{2}$; $\llbracket?\varphi\rrbracket_{M}=\{(w,w)\in W^{2}\mid w\in\llbracket\varphi\rrbracket^{M}\}$; $\llbracket\pi\cup\pi^{\prime}\rrbracket_{M}=\llbracket\pi\rrbracket_{M}\cup\llbracket\pi^{\prime}\rrbracket_{M}$; $\llbracket\pi;\pi^{\prime}\rrbracket_{M}=\llbracket\pi\rrbracket_{M}\circ\llbracket\pi^{\prime}\rrbracket_{M}$; $\llbracket\pi^{*}\rrbracket_{M}=\llbracket\pi\rrbracket_{M}^{*}$.

1.0.6 Some examples of definable evidence programs.

Here are some natural types of relational evidence that can be constructed with programs from $\Pi_{*}$.

Dichotomous evidence. For a formula $\varphi$, let $\pi_{\varphi}\coloneqq(A;?\varphi)\cup(?\neg\varphi;A;?\neg\varphi)$. $\pi_{\varphi}$ puts the $\varphi$ worlds strictly above the $\neg\varphi$ worlds, and makes every world equally plausible within each of these two regions. It is easy to see that $\pi_{\varphi}$ always defines a preorder, and therefore $(\pi_{\varphi})^{*}$ is an evidence program equivalent to $\pi_{\varphi}$.

Totally ordered evidence. Several programs can be used to define total orders. For example, for formulas $\varphi_{1},\dots,\varphi_{n}$, we can define the program

[TABLE]

This type of program, described in [22], puts the $\varphi_{1}$ worlds above everything else, the $\neg\varphi_{1}\wedge\varphi_{2}$ worlds above the $\neg\varphi_{1}\wedge\neg\varphi_{2}$ worlds, and so on, and the $\neg\varphi_{1}\wedge\neg\varphi_{2}\wedge\dots\wedge\neg\varphi_{n-1}\wedge\varphi_{n}$ above the $\neg\varphi_{1}\wedge\neg\varphi_{2}\wedge\dots\wedge\neg\varphi_{n}$ worlds. $\pi^{t}({\varphi_{1},\dots,\varphi_{n}})$ always defines a preorder, so the evidence program $(\pi^{t}({\varphi_{1},\dots,\varphi_{n}}))^{*}$ is equivalent to it.

Partially ordered evidence. Several programs can be used to define evidence orders featuring incomparabilities. To illustrate this, let us consider the program $\pi_{\varphi\wedge\psi}\coloneqq(A;?\varphi\wedge\psi)\cup(?\neg\varphi\wedge\neg\psi;A;?\varphi\vee\psi)\cup(?\neg\varphi\wedge\psi;A;?\neg\varphi\wedge\psi)\cup(?\varphi\wedge\neg\psi;A;?\varphi\wedge\neg\psi)$. As depicted in Figure 3, this program puts the $\varphi\wedge\psi$ worlds above everything else, the $\neg\varphi\wedge\psi$ and $\varphi\wedge\neg\psi$ as incomparable ‘second-best’ worlds, and the $\neg\varphi\wedge\neg\psi$ below everything else. As with the other programs $\pi_{\varphi\wedge\psi}$ always defines a preorder, so $(\pi_{\varphi\wedge\psi})^{*}$ is an equivalent evidence program.

1.0.7 Normal form programs

We now introduce a ‘normal form’ lemma for the programs in $\Pi$. This lemma shows that, for any evidence program $\pi\in\Pi$, we can find another program $\pi^{\prime}\in\Pi$, which is a union of certain programs, and which is equivalent to $\pi$. Of special interest for us is the normal form established for programs of the shape $\pi^{*}$. The fact that every evidence program $\pi^{*}$ is equivalent to a program with a specific syntactic shape is used extensively in the completeness proofs for dynamic extensions of $\mathscr{L}$ discussed later on. We first introduce some notation and necessary definitions:

Notation 1

For $\pi_{1},\dots,\pi_{n}\in\Pi$ we write $\bigcup^{n}_{i=1}\pi_{i}$ to denote the program $\pi_{1}\cup\dots\cup\pi_{n}$. We denote the set of all finite sequences of elements of a set $X$ by $S_{0}(X)$. Moreover, we denote by $\mathsf{len}(s)$ the length of a sequence $s=(s_{1},s_{2},\dots,s_{\mathsf{len}(s)})$ and by $s|s^{\prime}$ the concatenation of sequences $s$ and $s^{\prime}$.

Definition 12 (Program equivalence)

Two programs $\pi,\pi^{\prime}\in\Pi$ are equivalent iff for every REL model $M$, $\llbracket\pi\rrbracket_{M}=\llbracket\pi^{\prime}\rrbracket_{M}$.

Definition 13 (Normal form)

A normal form for a program $\pi\in\Pi$ is a program $\pi^{\prime}\in\Pi$ such that (1) $\pi^{\prime}$ has the form $\bigcup_{i\in I}(?\varphi_{i};A;?\psi_{i})\cup(?\theta)$, where $\varphi_{i},\psi_{i},\theta\in\mathscr{L}$ and $I$ is a finite index set; and (2) $\pi$ and $\pi^{\prime}$ are equivalent.

The proofs for the following lemma, as well as the other results presented in this paper, can be found in the ‘Proofs Appendix’ at the end of the paper.

Lemma 1** (Normal Form Lemma)**

Given any program $\pi\in\Pi$, we can find a normal form $\pi^{\prime}$ for it. In particular, the normal form for program $\pi^{*}$, where $\pi$ has a normal form $\bigcup_{i\in I}(?\varphi_{i};A;?\psi_{i})\cup(?\theta)$, is \bigcup_{s\in S_{0}(I)}\big{(}?(\varphi_{s_{1}}\wedge\bigwedge^{\mathsf{len}(s)}_{k=2}(\exists(\psi_{s_{k-1}}\wedge\varphi_{s_{k}})));A;?\psi_{s_{\mathsf{len}(s)}})\big{)}\cup(?\top).

As the normal form for $*$-programs is a rather long program, we will generally use the following abbreviation to ease reading.

Notation 2

Let $I$ be an index set. Let $s\in S_{0}(I)$ be a sequence. We will use the following abbreviation: $s(\bm{\varphi},\bm{\psi})\coloneqq(\varphi_{s_{1}}\wedge\bigwedge^{\mathsf{len}(s)}_{k=2}(\exists(\psi_{s_{k-1}}\wedge\varphi_{s_{k}})))$. With this abbreviation, the union normal form for $*$-programs will be written as \bigcup_{s\in S_{0}(I)}\big{(}?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}})\big{)}\cup(?\top).

2 The Logics of $Ag_{\cap}$-Models and $\mathsf{lex}$-Models

2.0.1 Static logics.

We initiate here our logical study of the statics of belief and evidence in the REL setting. We first zoom into two specific classes of REL models, the classes of $Ag_{\cap}$-models and $\mathsf{lex}$-models, and study the static logics for belief and evidence based on these models. In particular, we introduce systems $\mathsf{L}_{\cap}$ and $\mathsf{L}_{\mathsf{lex}}$ that axiomatize the class of $Ag_{\cap}$-models and the class of $\mathsf{lex}$-models, respectively. (To simplify notation, we write $\cap$-models instead of $Ag_{\cap}$-models hereafter). In later sections, after extending our basic static language appropriately, we will ‘zoom out’ and study the class of all REL models. Our decision to study $\cap$ and $\mathsf{lex}$ models in some detail is as follows. The class of $\cap$-models is interesting because it links our relational evidence setting back to the NEL setting that inspired it. Indeed, as we show below, given any NEL model with finitely many pieces of evidence, we can always find a $\cap$-model that is modally equivalent to it (with respect to language $\mathscr{L}$). This $\cap$-model represents binary evidence in a relational way, thereby encoding the same information present in the NEL model. $\mathsf{lex}$-models, on the other hand, provide a good study case for the REL setting, as they exemplify its main novel features: non-binary evidence and reliability-sensitive aggregation. We start by recalling the definition of a NEL model. The definition of these models follows the one in [2]. For a more general notion, see [18], where the models we consider are called uniform models.

Definition 14 (Neighborhood evidence model)

A neighborhood evidence model is a tuple $M=\langle W,E_{0},V\rangle$ where: $W$ is a non-empty set of states; $E_{0}\subseteq\mathscr{P}(W)$ is a family of evidence sets, such that $\emptyset\not\in E_{0}$ and $W\in E_{0}$; $V:\mathsf{P}\to\mathscr{P}(W)$ is a valuation function. A model is called feasible if $E_{0}$ is finite.

Definition 15 (Satisfaction)

Let $M=\langle W,E_{0},V\rangle$ be an NEL model and $w\in W$. The satisfaction relation $\models$ between pairs $(M,w)$ and formulas $\varphi\in\mathscr{L}$ is:

[TABLE]

We now present a way to ‘transform’ a NEL model into a matching REL model. To do that, we first encode binary evidence, the type of evidence considered in NEL models, as relational evidence.

Definition 16

Let $W$ be a set. For each $e\subseteq W$, we denote by $R_{e}$ the relation given by: $(w,v)\in R_{e}\text{ iff }w\in e\Rightarrow v\in e$.

That is, $R_{e}$ is a preorder with at most two indifference classes (i.e., a dichotomous weak order) of ‘good’ and ‘bad’ candidates for the actual state, which puts all the ‘bad’ candidates strictly below the ‘good’ ones. Having fixed this connection evidence sets and evidence orders, we can now consider a natural way to transform every NEL into a $\cap$-model in which each evidence order is dichotomous. To fix this connection, we define a mapping between NEL and REL models.

Definition 17

Let $Rel$ be a map from NEL to REL models given by:

[TABLE]

where $Rel(W)\coloneqq W$, $Rel(V)\coloneqq V$ $Rel(E_{0})\coloneqq\{R_{e}\mid e\in E_{0}\}$ and $\preceq=Rel(E_{0})^{2}$.

We can then observe that feasible NEL models and their images under $Rel$ are modally equivalent, in the sense of having point-wise equivalent modal theories.

Proposition 1

Let $M=\langle W,E_{0},V\rangle$ be a feasible NEL model. For any $\varphi\in\mathscr{L}$ and any $w\in W$, we have: $M,w\models\varphi\emph{ iff }Rel(M),w\models\varphi$.

That is, feasible NEL models can be seen as ‘special cases’ of REL models in which all evidence is dichotomous and equally reliable. As the following proposition shows, the modal equivalence result does not extend to non-feasible NEL models. This is because, in models with infinitely many pieces of evidence, the notion of combined evidence presented in [2] differs from the one proposed here for REL models. To clarify this, consider a NEL model $M=\langle W,E_{0},V\rangle$. Recall that the agent has combined evidence for a proposition $\varphi$ at $w$ if there is a finite body of evidence whose combination contains $w$ and supports $\varphi$, i.e., if there is some finite $F\subseteq E_{0}$ such that $w\in\bigcap F\subseteq\llbracket\varphi\rrbracket_{M}$. Suppose $M$ is a non-feasible model in which we have $w\in\bigcap E_{0}\subseteq\llbracket\varphi\rrbracket_{M}$, while no finite family $F\subseteq E_{0}$ is such that $w\in\bigcap F\subseteq\llbracket\varphi\rrbracket_{M}$. That is, the combination of all the evidence supports $\varphi$ at $w$, but no combination of a finite subfamily of $E_{0}$ does. In a NEL model like this, the agent does not have combined evidence for $\varphi$ at $w$. That is, $M,w\not\models\Box\varphi$. However, our proposed notion of aggregated evidence for REL models is based on combining all the available evidence, and as a result in $Rel(M)$ the agent does have aggregated evidence for $\varphi$ (i.e., $Rel(M),w\models\Box\varphi$). A concrete example of such a model is $M=\langle W,E_{0},V\rangle$ with $W=\mathbb{N}$, $E_{0}=\{\mathbb{N}\setminus\{2n+1\}\mid n\in\mathbb{N}\}$ and $V(p)=\{2n\mid n\in\mathbb{N}\}$. It is easy to verify that $M,0\not\models p$, while $Rel(M),0\models p$.

Proposition 2

Non-feasible NEL models need not be modally equivalent to their images under $Rel$. In particular, the left-to-right direction of Proposition 1 holds for non-feasible evidence models, but the right-to-left direction doesn’t: there are non-feasible neighborhood models $M$ s.t. $Rel(M),w\models\Box\psi$ but $M,w\not\models\Box\psi$.

Having motivated our interest in $\cap$-models via their connection to neighborhood evidence logics, we now focus again on the static logics of $\cap$- and $\mathsf{lex}$-models. Table 1 lists the axioms and rules in $\mathsf{L}_{\cap}$ and $\mathsf{L}_{\mathsf{lex}}$.

Theorem 1

$\mathsf{L}_{\cap}$* and $\mathsf{L}_{\mathsf{lex}}$ are sound and strongly complete with respect to $\cap$-models and $\mathsf{lex}$-models, respectively.*

2.0.2 Evidence dynamics for $\cap$-models.

Having established the soundness and completeness of the static logics, we now turn to evidence dynamics, starting with $\cap$-models. In line with the work on NEL, we consider update, evidence addition and evidence upgrade actions for $\cap$-models. As the intersection rule is insensitive to the priority order, when we consider $\cap$-models, it is convenient to treat the models as if they came with a family of evidence orders $\mathscr{R}$ only, instead of an ordered family $\langle\mathscr{R},\preceq\rangle$. Accordingly, hereafter we will write $\cap$-models as follows: $M=\langle W,\mathscr{R},V,Ag_{\cap}\rangle$. Throughout this section, we fix a $\cap$-model $M=\langle W,\mathscr{R},V,Ag_{\cap}\rangle$, some proposition $P\subseteq W$ and some evidence order $R\in Pre(W)$.

Update. We first consider updates that involve learning a new fact $P$ with absolute certainty. Upon learning $P$, the agent rules out all possible states that are incompatible with it. For REL models, this means keeping only the worlds in $\llbracket P\rrbracket_{M}$ and restricting each evidence order accordingly.

Definition 18 (Update)

The model $M^{!P}=\langle W^{!P},\mathscr{R}^{!P},V^{!P},Ag^{!P}_{\cap}\rangle$ has $W^{!P}\coloneqq P$, $\mathscr{R}^{!P}\coloneqq\{R\cap P^{2}\mid R\in\mathscr{R}\}$, $Ag^{!P}_{\cap}\coloneqq Ag_{\cap}$ restricted to $P$, and for all $p\in\mathsf{P}$, $V^{!P}(p)\coloneqq V(p)\cap P$.

Evidence addition. Unlike update, which is standardly defined in terms of an incoming proposition $P\subseteq W$, our proposed notion of evidence addition for $\cap$-models involves accepting a new piece of relational evidence $R$ from a trusted source. That is, relational evidence addition consists of adding a new piece of relational evidence $R\subseteq Pre(W)$ to the family $\mathscr{R}$.

Definition 19 (Evidence addition)

The model $M^{+R}=\langle W^{+R},\mathscr{R}^{+R},V^{+R},Ag^{+R}_{\cap}\rangle$ has $W^{+R}\coloneqq W$, $\mathscr{R}^{+R}\coloneqq\mathscr{R}\cup\{R\}$, $V^{+R}\coloneqq V$ and $Ag^{+R}_{\cap}\coloneqq Ag_{\cap}$.

Evidence upgrade. Finally, we consider an action of upgrade with a piece of relational evidence $R$. This upgrade action is based on the notion of binary lexicographic merge from Andréka et. al. [1].

Definition 20 (Evidence upgrade)

The model $M^{\Uparrow R}=\langle W^{\Uparrow R},\mathscr{R}^{\Uparrow R},V^{\Uparrow R},Ag^{\Uparrow R}_{\cap}\rangle$ has $W^{\Uparrow R}\coloneqq W$, $\mathscr{R}^{\Uparrow R}\coloneqq\{R^{<}\cup(R\cap R^{\prime})\mid R^{\prime}\in\mathscr{R}\}$, $V^{\Uparrow R}\coloneqq V$ and $Ag^{\Uparrow R}_{\cap}\coloneqq Ag_{\cap}$.

Intuitively, this operation modifies each existing piece of evidence $R^{\prime}$ with $R$ following the rule: “keep whatever $R$ and $R^{\prime}$ agree on, and where they conflict, give priority to $R$”. To encode syntactically the evidential actions described above, we present extensions of $\mathscr{L}$, obtained by adding to $\mathscr{L}$ dynamic modalities for update, evidence addition and evidence upgrade. The modalities for update will be standard, i.e., modalities of the form $[!\varphi]\psi$. The new formulas of the form $[!\varphi]\psi$ are used to express the statement: “$\psi$ is true after $\varphi$ is publicly announced”.

Definition 21 ($\mathscr{L}^{!}$)

The language $\mathscr{L}^{!}$ is defined recursively by:

[TABLE]

Definition 22 (Satisfaction for $[!\varphi]\psi$)

Let $M=\langle W,\mathscr{R},V,Ag_{\cap}\rangle$ be a $\cap$-model and $w\in W$. The satisfaction relation $\models$ between pairs $(M,w)$ and formulas $[!\varphi]\psi\in\mathscr{L}^{!}$ is defined by: $M,w\models[!\varphi]\psi\text{ iff }M,w\models\varphi\text{ implies }M^{!\llbracket\varphi\rrbracket_{M}},w\models\psi$.

For the remaining actions, we extend $\mathscr{L}$ with dynamic modalities of the form $[+\pi]\psi$ for addition and $[\Uparrow\pi]\psi$ for upgrade, where the symbol $\pi$ occurring inside the modality is an evidence program.

Definition 23 ($\mathscr{L}^{\bullet}$)

Let $\bullet\in\{+,\Uparrow\}$. The language $\mathscr{L}^{\bullet}$ is defined by:

[TABLE]

The new formulas of the form $[+\pi]\varphi$ are used to express the statement: “$\varphi$ is true after the evidence order defined by $\pi$ is added as a piece of evidence”, while the $[\Uparrow\pi]\varphi$ are used to express: “$\varphi$ is true after the existing evidence is upgraded with the relation defined by $\pi$”. We extend the satisfaction relation $\models$ to cover formulas of the form $[\bullet\pi]\varphi$ as follows:

Definition 24 (Satisfaction for $[\bullet\pi]\varphi$)

Let $M=\langle W,\mathscr{R},V,Ag_{\cap}\rangle$ be a $\cap$-model, $w\in W$ and $\bullet\in\{+,\Uparrow\}$. The satisfaction relation $\models$ between pairs $(M,w)$ and formulas $[\bullet\pi]\varphi\in\mathscr{L}^{\bullet}$ is defined by: $M,w\models[\bullet\pi]\varphi\text{ iff }M^{\bullet\llbracket\pi\rrbracket_{M}},w\models\varphi$.

We now introduce proof systems whose logics are sound and complete with respect to $\cap$-models. The soundness and completeness proofs work via a standard reductive analysis, appealing to reduction axioms. We refer to [13] for an extensive explanation of this technique.

Definition 25 ($\mathsf{L}^{!}$, $\mathsf{L}^{+}$ and $\mathsf{L}^{\Uparrow}$)

The proof system $\mathsf{L}^{!}$ extends $\mathsf{L}$ with the following reduction axioms:

• $\text{PA1}_{\cap}$: $[!\varphi]p\leftrightarrow(\varphi\to p)$ for all $p\in\mathsf{P}$
• $\text{PA2}_{\cap}$: $[!\varphi]\neg\psi\leftrightarrow(\varphi\to\neg[!\varphi]\psi)$
• $\text{PA3}_{\cap}$: $[!\varphi](\psi\wedge\psi^{\prime})\leftrightarrow[!\varphi]\psi\wedge[!\varphi]\psi^{\prime}$
• $\text{PA4}_{\cap}$: $[!\varphi]\Box_{0}\psi\leftrightarrow(\varphi\to\Box_{0}(\varphi\to[!\varphi]\psi))$
• $\text{PA5}_{\cap}$: $[!\varphi]\Box\psi\leftrightarrow(\varphi\to\Box(\varphi\to[!\varphi]\psi))$
• $\text{PA6}_{\cap}$: $[!\varphi]\forall\psi\leftrightarrow(\varphi\to\forall[!\varphi]\psi)$

Let $\pi$ be an evidence program with normal form \bigcup_{s\in S_{0}(I)}\big{(}?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}}\big{)}\cup(?\top). The proof system $\mathsf{L}^{+}$ extends $\mathsf{L}$ with the following reduction axioms:

• $\text{EA1}_{\cap}$: $[+\pi]p\leftrightarrow p$ for all $p\in\mathsf{P}$
• $\text{EA2}_{\cap}$: $[+\pi]\neg\chi\leftrightarrow\neg[+\pi]\chi$
• $\text{EA3}_{\cap}$: $[+\pi](\chi\wedge\chi^{\prime})\leftrightarrow[+\pi]\chi\wedge[+\pi]\chi^{\prime}$
• $\text{EA4}_{\cap}$: [+\pi]\Box_{0}\chi\leftrightarrow\Box_{0}[+\pi]\varphi\lor\big{(}[+\pi]\chi\wedge\bigwedge_{s\in S_{0}(I)}(s(\bm{\varphi},\bm{\psi})\to\forall(\psi_{s_{\mathsf{len}(s)}}\to[+\pi]\chi))\big{)}
• $\text{EA5}_{\cap}$: [+\pi]\Box\chi\leftrightarrow\big{(}[+\pi]\chi\wedge\bigwedge_{s\in S_{0}(I)}(s(\bm{\varphi},\bm{\psi})\to\Box(\psi_{s_{\mathsf{len}(s)}}\to[+\pi]\chi))\big{)}
• $\text{EA6}_{\cap}$: $[+\pi]\forall\chi\leftrightarrow\forall[+\pi]\chi$

The proof system $\mathsf{L}^{\Uparrow}$ extends $\mathsf{L}$ with the following reduction axioms:

• $\text{EU1}_{\cap}$: $[\Uparrow\pi]p\leftrightarrow p$ for all $p\in\mathsf{P}$
• $\text{EU2}_{\cap}$: $[\Uparrow\pi]\neg\chi\leftrightarrow\neg[\Uparrow\pi]\chi$
• $\text{EU3}_{\cap}$: $[\Uparrow\pi](\chi\wedge\chi^{\prime})\leftrightarrow[\Uparrow\pi]\chi\wedge[\Uparrow\pi]\chi^{\prime}$
• $\text{EU4}_{\cap}$: $[\Uparrow\pi]\Box_{0}\chi\leftrightarrow[\Uparrow\pi]\chi\wedge\pi^{<}(\chi)\wedge\pi^{\cap}(\chi)$
• $\text{EU5}_{\cap}$ : $[\Uparrow\pi]\Box\chi\leftrightarrow[\Uparrow\pi]\chi\wedge\pi^{<}(\chi)\wedge\bigwedge_{s\in S_{0}(I)}(s(\bm{\varphi},\bm{\psi})\to\Box(\psi_{s_{\mathsf{len}(s)}}\to[\Uparrow\pi]\chi))$
• $\text{EU6}_{\cap}$: $[\Uparrow\pi]\forall\chi\leftrightarrow\forall[\Uparrow\pi]\chi$

where the formulas $\pi^{<}(\chi)$ and $\pi^{\cap}(\chi)$ in ${EU4}_{\cap}$ and ${EU5}_{\cap}$ are given by:

[TABLE]

Theorem 2

$\mathsf{L}^{!}$, $\mathsf{L}^{+}$ and $\mathsf{L}^{\Uparrow}$ are sound and complete with respect to $\cap$-models.

Evidence dynamics for $\mathsf{lex}$-models. We now have a first look at the dynamics of evidence over $\mathsf{lex}$ models. In the REL setting, evidential actions can be seen as complex actions involving two possible transformations on the initial model: (i) modifying the stock of evidence, $\mathscr{R}$, perhaps by adding a new evidence relation $R$ to it, or modifying the existing evidence with $R$; and (ii) updating the priority order, $\preceq$, e.g. to ‘place’ a new evidence item where it fits, according to its reliability. We may also have actions involving evidence, not about the world, but about evidence itself or its sources (sometimes called ‘higher-order evidence‘ [8]), which trigger a reevaluation of the priority order without changing the stock of evidence (for instance, upon learning that a specific source is less reliable than we initially thought, we may want to lower the priority of the evidence provided by this source). To illustrate the type of actions that can be explored in this setting, here we study an action of prioritized addition over $\mathsf{lex}$ models. For the sake of generality, we describe this action over REL models.

Prioritized addition. Let $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,Ag\rangle$ be a REL model and $R\in Pre(W)$ a piece of relational evidence. The prioritized addition of $R$ adds $R$ to the set of available evidence $\mathscr{R}$, giving the highest priority to the new evidence.

Definition 26 (Prioritized addition)

The model $M^{\oplus R}=\langle W^{\oplus R},\langle\mathscr{R}^{\oplus R},\preceq^{\oplus R}\rangle,V^{\oplus R},Ag^{\oplus R}\rangle$ has $W^{\oplus R}\coloneqq W$, $\mathscr{R}^{\oplus R}\coloneqq\mathscr{R}\cup\{R\}$, $V^{\oplus R}\coloneqq V$, $Ag^{\oplus R}\coloneqq Ag$ and $\preceq^{\oplus R}\coloneqq\preceq\cup\{(R^{\prime},R)\mid R^{\prime}\in\mathscr{R}\}$.

To encode prioritized addition, we add formulas of the form $[\oplus\pi]\varphi$, used to express the statement that $\varphi$ is true after the prioritized addition of the evidence order defined by $\pi$.

Definition 27 ($\mathscr{L}^{\oplus}$)

The language $\mathscr{L}^{\oplus}$ is given by:

[TABLE]

Definition 28 (Satisfaction for $[\oplus\pi]\varphi$)

Let $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,Ag\rangle$ be an REL model and $w\in W$. The satisfaction relation $\models$ between pairs $(M,w)$ and formulas $[\oplus\pi]\varphi\in\mathscr{L}^{\oplus}$ is defined as follows: $M,w\models[\oplus\pi]\varphi\text{ iff }M^{\oplus\llbracket\pi\rrbracket_{M}},w\models\varphi$.

As we did with the dynamic extensions presented for actions in $\cap$-models, we wish to obtain a matching proof system for our dynamic language $\mathscr{L}^{\oplus}$. We do this via reduction axioms. Before presenting the proof system $\mathsf{L}^{\oplus}$, we introduce some abbreviations that will be used in the definition of these axioms.

Notation 3

Let $\pi$ be a normal form \pi\coloneqq\bigcup_{s\in S_{0}(I)}\big{(}?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}}\big{)}\cup(?\top). For a formula $[\oplus\pi]\chi$, we define the following abbreviations:

[TABLE]

Definition 29 ($\mathsf{L}^{\oplus}$)

Let $\chi,\chi^{\prime}\in\mathscr{L}^{\oplus}$ and let $\pi\in\Pi_{*}$ be an evidence program with normal form $\bigcup_{s\in S_{0}(I)}(?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}})\cup(?\top)$. The proof system $\mathsf{L}^{\oplus}$ extends $\mathsf{L}_{0}$ with the following reduction axioms:

• $\oplus$EA1: $[\oplus\pi]p\leftrightarrow p$ for all $p\in\mathsf{P}$
• $\oplus$EA2: $[\oplus\pi]\neg\chi\leftrightarrow\neg[\oplus\vec{\pi}]\chi$
• $\oplus$EA3: $[\oplus\pi](\chi\wedge\chi^{\prime})\leftrightarrow[\oplus\pi]\chi\wedge[\oplus\vec{\pi}]\chi^{\prime}$
• $\oplus$EA4: [\oplus\pi]\Box_{0}\chi\leftrightarrow\Box_{0}[\oplus\pi]\varphi\lor\big{(}[\oplus\pi]\chi\wedge\bigwedge_{s\in S_{0}(I)}(s(\bm{\varphi},\bm{\psi})\to\forall(\psi_{s_{\mathsf{len}(s)}}\to[\oplus\pi]\chi))\big{)}
• $\oplus$EA5: $[\oplus\pi]\Box\chi\leftrightarrow[\oplus\pi]\chi\wedge\pi^{<}(\chi)\wedge\bigwedge_{s\in S_{0}(I)}(s(\bm{\varphi},\bm{\psi})\to\Box(\psi_{s_{\mathsf{len}(s)}}\to[\oplus\pi]\chi))$
• $\oplus$EA6: $[\oplus\pi]\forall\chi\leftrightarrow\forall[\oplus\vec{\pi}]\chi$

Theorem 3

$\mathsf{L}^{\oplus}$* is sound and strongly complete with respect to $\mathsf{lex}$ models.*

3 The Logic of REL Models

In this section, we study the logic of evidence and belief based on some abstract aggregator. That is, instead of fixing an aggregator, we are now interested in reasoning about the beliefs that an agent would form, based on her evidence, irrespective of the aggregator used. With respect to dynamics, we will focus on the action of prioritized addition introduced for $\mathsf{lex}$-models, considering an iterated version of prioritized addition, defined with a (possibly empty) sequence of evidence orders $\vec{R}=\langle R_{1},\dots,R_{n}\rangle$ as input.

Definition 30 (Iterated prioritized addition)

Let $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,Ag\rangle$ be a REL model and $\vec{R}=\langle R_{1},\dots,R_{n}\rangle$ be a sequence of evidence orders.The model $M^{\oplus R}=\langle W^{\oplus\vec{R}},\langle\mathscr{R}^{\oplus\vec{R}},\preceq^{\oplus\vec{R}}\rangle,V^{\oplus\vec{R}},Ag^{\oplus\vec{R}}\rangle$ has $W^{\oplus\vec{R}}\coloneqq W$, $\mathscr{R}^{\oplus\vec{R}}\coloneqq\mathscr{R}\cup\{R_{i}\mid i\in\{1,\dots n\}\}$, $V^{\oplus\vec{R}}\coloneqq V$, $Ag^{\oplus\vec{R}}\coloneqq Ag$ and

[TABLE]

That is, first $R_{1}$ is added as the highest priority evidence, then $R_{2}$ is added as the highest priority evidence, on top of every other evidence (including $R_{1}$), and so on, up to $R_{n}$. Naturally, when $\vec{R}$ has one element, we are back to the basic notion of prioritized addition.

Syntax and semantics. To pre-encode part of the dynamics of iterated prioritized addition, we will modify our basic language $\mathscr{L}$ with conditional aggregated evidence modalities of the form $\Box^{\vec{\pi}}$, where $\vec{\pi}$ is a finite, possibly empty sequence of evidence programs $\pi_{1},\dots,\pi_{n}$ (i.e., $\pi_{i}\in\Pi_{*}$, for $i\in\{1,\dots n\}$). The intended interpretation of $\Box^{\vec{\pi}}\varphi$ is “the agent would have aggregated evidence for $\varphi$, if she performed the iterated prioritized addition of the evidence orders defined by $\vec{\pi}$”.

Definition 31 ($\mathscr{L}_{c}$)

The language $\mathscr{L}_{c}$ is defined as follows:

[TABLE]

where $\vec{\pi}$ is a (possibly empty) finite sequence of evidence programs (i.e. $*$-programs).

As we allow $\vec{\pi}$ to be empty, $\Box^{\vec{\pi}}$ reduces to the $\Box\varphi$ from $\mathscr{L}$ when $\vec{\pi}$ is the empty sequence, giving us a fully static sub-language.

Notation 4

We abuse the notation for the truth map $\llbracket\cdot\rrbracket_{M}$ and write $\llbracket\vec{\pi}\rrbracket_{M}$ to denote $\langle\llbracket\pi_{1}\rrbracket_{M},\dots,\llbracket\pi_{n}\rrbracket_{M}\rangle$, where $\vec{\pi}=\langle\pi_{1},\dots,\pi_{n}\rangle$.

Satisfaction for formulas $\Box^{\vec{\pi}}\varphi\in\mathscr{L}_{c}$ is given as follows.

Definition 32

Let $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,Ag\rangle$ be an REL model and $w\in W$. The satisfaction relation $\models$ between pairs $(M,w)$ and formulas $\Box^{\vec{\pi}}\varphi\in\mathscr{L}_{c}$ is defined as follows: $M,w\models\Box^{\vec{\pi}}\varphi\text{ iff }Ag(\langle\mathscr{R}^{\oplus\llbracket\vec{\pi}\rrbracket_{M}},\preceq^{\oplus\llbracket\vec{\pi}\rrbracket_{M}}\rangle)[w]\subseteq\llbracket\varphi\rrbracket_{M}$.

That is, $\Box^{\vec{\pi}}\varphi$ is true at a state $w$ if the agent would have aggregated evidence for $\varphi$, assuming that the current ordered body of evidence is transformed by the iterated prioritized addition of $\llbracket\vec{\pi}\rrbracket_{M}$. Note that, as we allow $\vec{\pi}$ to be empty, $\Box^{\vec{\pi}}$ reduces to the standard $\Box\varphi$ from $\mathscr{L}$ when $\vec{\pi}$ is the empty sequence.

Static logic. Next, we introduce a complete proof system for the language with conditional modalities.

Definition 33 ($\mathsf{L}_{c}$)

The system $\mathsf{L}_{c}$ includes the same axioms and inference rules as $\mathsf{L}_{\mathsf{lex}}$, with axioms and inference rules for $\Box$ in $\mathsf{L}_{\mathsf{lex}}$ applying to $\Box^{\vec{\pi}}$ in $\mathsf{L}_{c}$.

Theorem 4

$\mathsf{L}_{c}$* is sound and strongly complete with respect to REL models.*

Evidence dynamics for REL models. Having established the soundness and completeness of the static logic, we now turn to evidence dynamics, focusing on prioritized evidence addition. To encode prioritized addition, we add formulas of the form $[\oplus\vec{\pi}]\varphi$, used to express the statement that $\varphi$ is true after the prioritized addition of the sequence of evidence orders defined by $\vec{\pi}$.

Definition 34 ($\mathscr{L}_{c}^{\oplus}$)

The language $\mathscr{L}_{c}^{\oplus}$ is given by:

[TABLE]

where ${\vec{\pi}}$ is a (possibly empty) finite sequence of evidence programs (i.e. $*$-programs).

Definition 35 (Satisfaction for $[\oplus\pi]\varphi$)

Let $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,Ag\rangle$ be an REL model and $w\in W$. The satisfaction relation $\models$ between pairs $(M,w)$ and formulas $[\oplus\pi]\varphi\in\mathscr{L}^{\oplus}$ is defined as follows: $M,w\models[\oplus{\vec{\pi}}]\varphi\text{ iff }M^{\oplus\llbracket{\vec{\pi}}\rrbracket_{M}},w\models\varphi$.

Having fixed our dynamic language, we now present reduction axioms for it.

Definition 36 ($\mathsf{L}_{c}^{\oplus}$)

Let $\chi,\chi^{\prime}\in\mathscr{L}_{\vec{\pi}}^{\oplus}$ and let $\vec{\pi}=\langle\pi_{1},\dots,\pi_{n}\rangle\in S_{0}(\Pi_{*})$ be a sequence of evidence programs where each $\pi_{i}$ has a normal form $\pi_{i}\coloneqq\bigcup_{s\in S_{0}(I_{i})}(?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}})\cup(?\top)$. The proof system $\mathsf{L}_{c}^{\oplus}$ includes all axioms schemas and inference rules of $\mathsf{L}_{c}$, together with the following reduction axioms:

• PEA1: $[\oplus\vec{\pi}]p\leftrightarrow p$ for all $p\in\mathsf{P}$
• PEA2: $[\oplus\vec{\pi}]\neg\chi\leftrightarrow\neg[\oplus\vec{\pi}]\chi$
• PEA3: $[\oplus\vec{\pi}](\chi\wedge\chi^{\prime})\leftrightarrow[\oplus\vec{\pi}]\chi\wedge[\oplus\vec{\pi}]\chi^{\prime}$
• PEA4: [\oplus\vec{\pi}]\Box_{0}\chi\leftrightarrow\Box_{0}[\oplus\vec{\pi}]\varphi\lor\big{(}[+\vec{\pi}]\chi\wedge\bigvee_{1\leq i\leq n}(\bigwedge_{s\in S_{0}(I_{i})}(s(\bm{\varphi},\bm{\psi})\to\forall(\psi_{s_{\mathsf{len}(s)}}\to[\oplus\vec{\pi}]\chi)))\big{)}
• PEA5: $[\oplus\vec{\pi}]\Box^{\vec{\rho}}\chi\leftrightarrow\Box^{\vec{\pi}\vec{\rho}}\chi$, for $\vec{\rho}\in S_{0}(\Pi_{*})$
• PEA6: $[\oplus\vec{\pi}]\forall\chi\leftrightarrow\forall[\oplus\vec{\pi}]\chi$

where $\vec{\pi}\vec{\rho}$ denotes the concatenation of the sequences $\vec{\pi}$ and $\vec{\rho}$.

Theorem 5

$\mathsf{L}_{c}^{\oplus}$* is sound and complete with respect to REL models.*

4 Conclusions and Future Work

We have presented evidence logics that use a novel representation for evidence and incorporate reliability-sensitive forms of evidence aggregation. Clearly, many open problems remain. Here are a few more specific avenues for future research:

• •

Additional aggregators: We studied two natural aggregators. As we know from the social choice literature, many other aggregators have nice properties. An interesting extension to this work could involve developing logics based on other well-known aggregators.

• •

Additional evidential actions: As we saw, in a setting with ordered evidence, evidence actions are complex transformations, both of the stock of evidence and the priority order. For the lexicographic case, we studied a form of prioritized addition. It could be interesting to consider more general forms of addition, or actions that transform the priority order (re-evaluation of reliability) without affecting the stock of evidence.

• •

Probabilistic evidence: We moved from the binary evidence case to the relational evidence case. Another important form of evidence is probabilistic evidence, i.e., evidence that comes in the form of a probability distribution over the set of states. The aggregation of probability functions is studied in probabilistic opinion pooling [9] and pure inductive logic [15], but a dynamic-logic study has yet to be developed.

PROOFS APPENDIX

PROOF OF PROPOSITIONS 1 AND 2

See 1

Proof

By induction on the structure of $\varphi$. The base case for $\varphi=p$ ($p\in\mathsf{P}$) and the inductive step for $\varphi=\neg\psi$,$\varphi=\psi\wedge\chi$ and $\varphi=\forall\psi$ are shown by unfolding the definitions. We show now the cases involving $\Box_{0}$ and $\Box$ modalities.

• •

$\varphi=\Box_{0}\psi$. Note that:

[TABLE]

• •

$\varphi=\Box\psi$. Note that:

[TABLE]

See 2

Proof

That the left-to-right direct holds is clear from the fact that the proofs for this direction don’t depend on the cardinality of $E_{0}$. For the right-to-left direction, the following is a counterexample. Let $M=\langle W,E_{0},V\rangle$, with $W=\mathbb{N}$, $E_{0}=\{\mathbb{N}\setminus\{2n+1\}\mid n\in\mathbb{N}\}$ and $V(p)=\{2n\mid n\in\mathbb{N}\}$. Note that for all $e\in E$, $e\not\subseteq\llbracket p\rrbracket_{M}$ and thus $M,0\not\models\Box p$. Moreover, we have:

[TABLE]

And as $0\in e$ for all $e\in E_{0}$, by the fact that $0\in e$ implies $R_{e}[0]=e$, we have $R_{e}[0]=e$ for each $e\in E_{0}$. Hence

[TABLE]

Note that $\bigcap E_{0}=\llbracket p\rrbracket_{M}$, and thus, $(\bigcap_{R\in Rel(E_{0})}R)[0]=\llbracket p\rrbracket_{M}$. We also have $\llbracket p\rrbracket_{M}=\llbracket p\rrbracket_{Rel(M)}$ and hence $(\bigcap_{R\in Rel(E_{0})}R)[0]=\llbracket p\rrbracket_{Rel(M)}$, which implies $Rel(M),0\models\Box p$.

PROOF OF LEMMA 1

The following well-known results about relational composition will be used in the normal form lemma.

Proposition 3

Relational composition distributes over arbitrary unions. That is, for any binary relation $R$ and any indexed family of binary relations $Q_{i}$: (1) $R\circ(\bigcup_{i}Q_{i})=\bigcup_{i}(R\cup Q_{i})$; (2) $(\bigcup_{i}Q_{i})\circ R=\bigcup_{i}(Q_{i}\circ R)$.

Proof

See, e.g., **[12, 8]**.

The following standard PDL facts will also be used.

Proposition 4

Let $M$ be a REL model. Then:

$(x,y)\in\llbracket?\varphi;A;?\psi\rrbracket_{M}$* iff $x\in\llbracket\varphi\rrbracket_{M}$ and $x\in\llbracket\psi\rrbracket_{M}$.* 2. 2.

$(x,y)\in\llbracket?\varphi;?\psi\rrbracket_{M}$* iff $(x,y)\in\llbracket?(\varphi\wedge\psi)\rrbracket_{M}$.* 3. 3.

$(x,y)\in\llbracket?\varphi_{1};A;?(\psi_{1}\wedge\varphi_{2});A;?\psi_{2}\rrbracket_{M}$* iff $(x,y)\in\llbracket?(\varphi_{1}\wedge\exists(\psi_{1}\wedge\varphi_{2});A;?\psi_{2}\rrbracket_{M}$*

In the step of the normal form lemma concerning $*$-programs, we will make use of the following definitions and results.

Definition 37 (Walks and paths)

Let $R\subseteq W\times W$. A walk along $R$ is a sequence of (not necessarily distinct) vertices $w_{1},w_{2},\dots,w_{k}$, where $w_{i}\in W$ for $i=1,2,\dots,k$, such that $(v_{i},v_{i+1})\in R$ for $i=1,2,\dots,k-1$. A path is a walk in which all vertices are distinct (except possibly the first and last). A $wv$-walk is a walk with first vertex $w$ and last vertex $v$. A $wv$-path is defined similarly. The length of a walk (path) is its number of edges.

Proposition 5

Let $R\subseteq W\times W$. Every $wv$-walk along $R$ contains a $wv$-path along $R$.

Proof

This is a standard result. For a proof, see, e.g., [16, 19].

Proposition 6

Let $M$ be a REL model. Every $wv$-path along $\llbracket\bigcup^{n}_{i=1}(?\varphi_{i};A;?\psi_{i})\rrbracket_{M}$ of length $\ell>n$ contains a $wv$-path along $\llbracket\bigcup^{n}_{i=1}(?\varphi_{i};A;?\psi_{i})\rrbracket_{M}$ of length at most $n$.

Proof

Straightforward proof by induction on the length $\ell$ of a $wv$-path $\mathcal{P}=wu_{1}u_{2}\dots u_{\ell}v$.

Proposition 7

Let $M$ be an REL model. Then $\llbracket\pi\cup?\varphi\rrbracket^{*}_{M}=\llbracket\pi\rrbracket^{*}_{M}$.

Proof

Straightforward.

After fixing the auxiliary results, we get to the proof of Lemma 1.

See 1

Proof

The proof is by induction on the structure of $\pi$. Let $M$ be any REL model.

• •

$\pi=A$. Let $\pi^{\prime}$ be the union form $\pi^{\prime}\coloneqq(?\top;A;?\top)\cup(?\bot)$. It is straightforward to check that $\pi^{\prime}$ and $\pi$ are equivalent.

• •

$\pi=?\varphi$. Let $\pi^{\prime}$ be the union form $\pi^{\prime}\coloneqq(?\bot;A;?\bot)\cup(?\varphi)$. Again, it is straightforward to check that $\pi^{\prime}$ and $\pi$ are equivalent.

• •

$\pi=\pi_{1}\cup\pi_{2}$. By induction hypothesis, we can find normal forms for $\pi_{1}$ and $\pi_{2}$. Let the forms be $\pi^{\prime}_{1}\coloneqq\bigcup_{i\in I}(?\varphi_{i};A;?\psi_{i})\cup?\theta$ and $\pi^{\prime}_{2}\coloneqq\bigcup_{j\in J}(?\varphi_{j};A;?\psi_{j})\cup?\theta^{\prime}$ respectively. Let $\pi^{\prime}$ be the union form $\pi^{\prime}\coloneqq(\bigcup_{k\in I\cup J}?\varphi_{k};A;?\psi_{k})\cup(?\theta\lor\theta^{\prime})$. Again, it is straightforward to check that $\pi^{\prime}$ and $\pi$ are equivalent.

• •

$\pi=\pi_{1};\pi_{2}$. By induction hypothesis, we can find normal forms for $\pi_{1}$ and $\pi_{2}$. Let the forms be $\pi^{\prime}_{1}\coloneqq\bigcup_{i\in I}?(\varphi_{i};A;?\psi_{i})\cup?\theta$ and $\pi^{\prime}_{2}\coloneqq\bigcup_{j\in J}(?\varphi_{j};A;?\psi_{j})\cup?\theta^{\prime}$ respectively. It is not difficult to transform $\pi$ into a normal form shape, essentially using (several times) the fact that composition distributes over union (proposition 3) to pull the big unions to the left side of the program, and re-indexing the formulas appropriately.

• •

$\pi=\pi_{1}^{*}$. By induction hypothesis, we can find a normal form for $\pi_{1}$. Let this normal form be $\pi^{\prime}_{1}\coloneqq\bigcup_{i\in I}(?\varphi_{i};A;?\psi_{i})\cup?\theta$. We recall here that $S_{0}(I)$ denotes the set of all finite sequences of elements from $I$, and $\mathsf{len}(s)$ denotes the length of sequence $s=(s_{1},s_{2},\dots,s_{\mathsf{len}(s)})$. Let $\pi^{\prime}$ be the union form:

[TABLE]

We will show that $\pi^{\prime}$ is a normal form for $\pi$. Observe that:

[TABLE]

PROOF OF THEOREM 1

We recall the theorem:

See 1

We prove the soundness and completeness of $\mathsf{L}_{\cap}$ and $\mathsf{L}_{\mathsf{lex}}$ separately.

Soundness and completeness of $\mathsf{L}_{\cap}$.

The soundness proof is straightforward; it suffices to check that each axiom is valid and that the inference rules preserve truth. We focus on the completeness proof. The completeness of $\mathsf{L}$ w.r.t $\cap$-models follows from Proposition 1 and the fact that $\mathsf{L}$ is complete, and has the finite model property, w.r.t NEL models (a result from [2]). We recall Proposition 1.

See 1

Next, we recall a result proven in [2]:

Theorem 6, [2]. $\mathsf{L}$ is sound, strongly complete and has the finite model property with respect to the class of NEL models.

The theorem above, together with the fact that feasible NEL models are modally equivalent to their images under $Rel$, gives us the completeness of $\mathsf{L}$ w.r.t $\cap$-models.

Claim

$\mathsf{L}$ is complete w.r.t $\cap$-models.

Proof

As indicated, e.g., in [6, 194-195], a logic $\Lambda$ is strongly complete with respect to a class of models iff every $\Lambda$-consistent set of formulas is satisfiable on some model in this class. Hence, it suffices to show that every $\mathsf{L}$-consistent set of formulas is satisfiable on some $\cap$-model. Let $\Gamma$ be an $\mathsf{L}$-consistent set of formulas. As $\mathsf{L}$ is complete and has the finite model property with respect to NEL models, there is a finite (and hence feasible) NEL model $M$ and a state $w$ in $M$ such that $M,w\models\varphi$ for all $\varphi\in\Gamma$. By proposition 1, we have $Rel(M),w\models\varphi$ for all $\varphi\in\Gamma$. Thus, $\Gamma$ is satisfiable on a $\cap$-model.

Soundness and completeness of $\mathsf{L}_{\mathsf{lex}}$.

The soundness proof is straightforward; we focus on completeness. The approach to the proof is similar to the one used by Fagin et. al. [10] to prove completeness for the logic of distributed knowledge. Before going into the details of the proof, we give an outline of the main steps in it.

Step 1: Completeness of $\mathsf{L}_{\mathsf{lex}}$ with respect to pre-models. First, we define a specific type of canonical REL model for each $\mathsf{L}_{\mathsf{lex}}$-consistent theory $T_{0}$, which we call a pre-model for $T_{0}$. Then we prove completeness of $\mathsf{L}_{\mathsf{lex}}$ via canonical pre-models. 2. 2.

Step 2: Unraveling. In the second step, we unravel the canonical pre-model for $T_{0}$ (see Chapter 4.5 in [6] for details about this technique). This involves creating all possible histories in the pre-model rooted at $T_{0}$. The histories are the paths of the canonical pre-model that start at $T_{0}$. These histories are related in such a way that they form a tree. 3. 3.

Step 3: Completeness of $\mathsf{L}_{\mathsf{lex}}$ with respect to $\mathsf{lex}$ models. In the third step, we take the tree we just constructed, and from we define a $\mathsf{lex}$ model for $T_{0}$. Then we define a variant of a bounded morphism between the canonical pre-model and the $\mathsf{lex}$ model generated from the tree, which makes completeness with respect to those models immediate.

Step 1: Completeness with respect to pre-models. We build a canonical pre-model for each $\mathsf{L}_{\mathsf{lex}}$-consistent set of formulas $T_{0}$. We first fix a standard lemma.

Lemma 1 (Lindenbaum’s Lemma)

Every consistent set of formulas of $\mathscr{L}$ can be extended to a maximally consistent one.

Proof

The proof is a special case of **[6, 197]**.

We recall some properties of maximally consistent sets:

Proposition 1

Let $T_{0}$ be a maximally consistent set. The following hold:

For any formula $\varphi$: $\varphi\in T_{0}$ or $\neg\varphi\in T_{0}$. 2. 2.

$\varphi\in T_{0}$* iff $T_{0}\vdash_{\mathsf{L}_{\mathsf{lex}}}\varphi$.* 3. 3.

$T_{0}$* is closed under modus ponens: $\varphi,\varphi\to\psi\in T_{0}$ implies $\psi\in T_{0}$.* 4. 4.

$\neg\varphi\in T_{0}$* iff $\varphi\not\in T_{0}$.* 5. 5.

$\varphi\wedge\psi\in T_{0}$* iff $\varphi\in T_{0}$ and $\psi\in T_{0}$.*

Proof

The proofs are all standard. See, e.g., **[7, 53]**.

We now define the notion of a canonical pre-model that we will use in the completeness proof of Step 1.

Definition 38 (Canonical pre-model for $T_{0}$)

Let $T_{0}$ be a $\mathsf{L}_{\mathsf{lex}}$-consistent set of formulas. A canonical pre-model for $T_{0}$ is a structure $M^{c}=\langle W^{c},\langle\mathscr{R}^{c},\preceq^{c}\rangle,V^{c},Ag^{c}\rangle$ with:

• •

$W^{c}\coloneqq\{T\mid T\text{ is a maximally consistent theory and }R^{\forall}T_{0}T\}$.

• •

$\mathscr{R}^{c}\coloneqq\{R^{\Box_{0}\varphi}\mid\varphi\in\mathscr{L}\text{ and }(\exists\Box_{0}\varphi)\in T_{0}\}\cup\{R^{\prime}\}$.

• •

$\preceq^{c}$ is the reflexive closure of $\{(R,R^{\prime})\mid R\in\mathscr{R}\}$.

• •

$V^{c}$ is a valuation function given by $V^{c}(p)\coloneqq\|p\|$.

• •

$Ag^{c}$ is an aggregator for $W^{c}$ given by

[TABLE]

Where:

• •

$R^{\forall}\subseteq W^{c}\times W^{c}$ is given by: $R^{\forall}TS$ iff for all $\varphi\in\mathscr{L}$: $(\forall\varphi)\in T\Rightarrow(\forall\varphi)\in S$.

• •

for each $\varphi\in\mathscr{L}$, $R^{\Box_{0}\varphi}\subseteq W^{c}\times W^{c}$ is given by: $R^{\Box_{0}\varphi}TS$ iff $\Box_{0}\varphi\in T\Rightarrow\Box_{0}\varphi\in S$.

• •

$R^{\Box}\subseteq W^{c}\times W^{c}$ is given by: $R^{\Box}TS$ iff for all $\varphi\in\mathscr{L}$: $\Box\varphi\in T\Rightarrow\varphi\in S$.

• •

$F:W^{c}\times\mathscr{L}\to W^{c}$ is a function given by cases:

• (a)

for every pair $(T,\varphi)$ such that $(\Box_{0}\varphi)\not\in T$, choose some theory $S\in W^{c}$ such that $\varphi\not\in S$, and put $F(T,\varphi)\coloneqq S$;

• (b)

for every pair $(T,\varphi)$ not satisfying the condition of case (a), put $F(T,\varphi)\coloneqq T$.

• •

$R^{\prime}\coloneqq(R^{\Box}\cup\{(T,F(T,\varphi))\mid T\in W^{c}\text{ and }\varphi\in\mathscr{L}\})^{*}$

• •

for each $\varphi\in\mathscr{L}$, $\|\varphi\|_{c}\coloneqq\{T\in W^{c}\mid\varphi\in T\}$

We first need to show that this canonical pre-model is indeed a REL model.

Proposition 2

$M^{c}$* is a REL model.*

Proof

In order to show that $M^{c}$ is an REL model, we have to show that:

$\mathscr{R}^{c}$* is a family of evidence, i.e., every $R\in\mathscr{R}$ is a preorder.* 2. 2.

$W^{c}\times W^{c}\in\mathscr{R}^{c}$. 3. 3.

$R^{\Box}$* is a preorder, and thus $Ag^{c}$ is well-defined.*

For item 1, let $\varphi\in\mathscr{L}$ be arbitrary. Let $R\in\mathscr{R}$ be arbitrary. Then either $R=R^{\prime}$ or $R=R^{\Box_{0}\varphi}$ for some $\varphi$. As $R^{\prime}$ is the reflexive transitive closure of the relation $R^{\Box}\cup\{(T,F(T,\varphi))\mid T\in W^{c}\text{ and }\varphi\in\mathscr{L}\}$, it is a preorder, as required. Now consider $R=R^{\Box_{0}\varphi}$ for some $\varphi$. The reflexivity of $R$ is immediate from the definition of $R^{\Box_{0}\varphi}$. For the transitivity, let $T,S,U\in M^{c}$ and suppose that $R^{\Box_{0}\varphi}TS$ and $R^{\Box_{0}\varphi}SU$. Either $\Box_{0}\varphi\not\in T$ or $\Box_{0}\varphi\in T$. Note that, by definition of $R^{\Box_{0}\varphi}$, if $\Box_{0}\varphi\not\in T$, then $R^{\Box_{0}\varphi}[T]=W^{c}$ and thus $R^{\Box_{0}\varphi}TU$. Suppose now that $\Box_{0}\varphi\in T$. Then by definition of $R^{\Box_{0}\varphi}$, given $R^{\Box_{0}\varphi}TS$ we have $\Box_{0}\varphi\in S$, and thus as $R^{\Box_{0}\varphi}SU$ we get $\Box_{0}\varphi\in U$, which implies $R^{\Box_{0}\varphi}TU$. For item 2, observe that $\mathsf{N}_{\Box}$, i.e., $\Box_{0}\top$, is an axiom of our system. Thus it is a member of any maximal consistent set, which implies that $R^{\Box_{0}\top}=W^{c}\times W^{c}$. Now we consider item 3. For reflexivity, suppose that $(\Box\varphi)\in T$ for some $T\in M^{c}$. As $\mathsf{T}_{\Box}$ is an axiom and $T$ is maximal consistent, $(\Box\varphi\to\varphi)\in T$. As $(\Box\varphi)\in T$ and $T$ is closed under modus ponens, we have $\varphi\in T$. Thus $R^{\Box}TT$. For transitivity, let $T,S,U\in M^{c}$ and suppose that $R^{\Box}TS$ and $R^{\Box}SU$. Suppose $(\Box\varphi)\in T$. As $\mathsf{4}_{\Box}$ is an axiom and $T$ is maximally consistent, $(\Box\varphi\to\Box\Box\varphi)\in T$. As $(\Box\varphi)\in T$ and $T$ is closed under modus ponens, we have $\Box\Box\varphi\in T$. As $R^{\Box}TS$, we then have $\Box\varphi\in S$. Hence, as $R^{\Box}SU$, we have $\varphi\in U$. As $\varphi$ was arbitrary, this holds for each $\varphi$ and hence we have $R^{\Box}TU$.

Having established that $M^{c}$ is a REL model, we prove now the standard lemmas to show that the canonical pre-model works as expected.

Lemma 2 (Existence Lemma for $\forall$)

$\|\exists\varphi\|\neq\emptyset$* iff $\|\varphi\|\neq\emptyset$.*

Proof

($\Rightarrow$). Assume $T\in\|\exists\varphi\|$, i.e., $(\exists\varphi)\in T\in W^{c}$. We first prove the following:

Claim

The set $\Gamma\coloneqq\{\forall\psi\mid(\forall\psi)\in T\}\cup\{\varphi\}$ is consistent.

Proof

Suppose that $\Gamma$ is inconsistent, i.e., $\Gamma\vdash_{\mathsf{L}_{\mathsf{lex}}}\bot$. Then there are finitely many sentences $\forall\psi_{1},\dots,\forall\psi_{n}\in T$ such that $\vdash_{\mathsf{L}_{\mathsf{lex}}}\forall\psi_{1}\wedge\dots\wedge\forall\psi_{n}\to\neg\varphi$. By Necessitation for $\forall$ we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}\forall(\forall\psi\wedge\dots\wedge\forall\psi_{n}\to\neg\varphi)$ and from this, by $\mathsf{K}_{\forall}$ and modus ponens we get $\vdash_{\mathsf{L}_{\mathsf{lex}}}\forall(\forall\psi_{1}\wedge\dots\wedge\forall\psi_{n})\to\forall\neg\varphi$. The system $\mathsf{S5}$ has the theorem $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\forall\forall\psi_{1}\wedge\dots\wedge\forall\forall\psi_{n})\to\forall(\forall\psi_{1}\wedge\dots\wedge\forall\psi_{n})$ (see, e.g., **[7, 20]**). Hence by propositional logic we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\forall\forall\psi_{1}\wedge\dots\wedge\forall\forall\psi_{n})\to\forall\neg\varphi$. Given $\mathsf{4}_{\forall}$ we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}\forall\psi_{1}\to\forall\forall\psi_{1},\dots,\vdash_{\mathsf{L}_{\mathsf{lex}}}\forall\psi_{n}\to\forall\forall\psi_{n}$, which by propositional logic implies $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\forall\psi_{1}\wedge\dots\wedge\forall\psi_{n})\to\forall\forall\psi_{1}\wedge\dots\wedge\forall\forall\psi_{n}$. Thus we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\forall\psi_{1}\wedge\dots\wedge\forall\psi_{n})\to\forall\neg\varphi$. Hence as $T$ is maximal consistent and closed under modus ponens, we get $(\forall\neg\varphi)\in T$. But we also have $(\exists\varphi)\in T$, i.e., $(\neg\forall\neg\varphi)\in T$, and since $T$ is maximal consistent, this means that $(\forall\neg\varphi)\not\in T$. Contradiction.

Given the Claim, by Lindenbaum’s Lemma, there is some maximally consistent theory $S$ such that $\Gamma\subseteq S$. As $\varphi\in\Gamma$ we have $\varphi\in S$. Moreover, as $\{\forall\psi\mid(\forall\psi)\in T\}\subseteq\{\forall\chi\mid(\forall\chi)\in S\}$ we have $R^{\forall}TS$. As $T\in W^{c}$, we also have $R^{\forall}T_{0}T$. That is, $\{\forall\theta\mid(\forall\theta)\in T_{0}\}\subseteq\{\forall\psi\mid(\forall\psi)\in T\}$. Thus $\{\forall\theta\mid(\forall\theta)\in T_{0}\}\subseteq\{\forall\chi\mid(\forall\chi)\in S\}$ and thus $R^{\forall}T_{0}S$. Hence $S\in W^{c}$, which together with $\varphi\in S$ gives us $S\in\|\varphi\|$.

($\Leftarrow$) Assume $T\in\|\varphi\|$, i.e., $\varphi\in T$. Given $\mathsf{T}_{\forall}$ we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}\forall\neg\varphi\to\neg\varphi$, and by contraposition we get $\vdash_{\mathsf{L}_{\mathsf{lex}}}\neg\neg\varphi\to\neg\forall\neg\varphi$, i.e., $\vdash_{\mathsf{L}_{\mathsf{lex}}}\varphi\to\exists\varphi$. Hence $(\varphi\to\exists\varphi)\in T$ and as $T$ is closed under modus ponens, given also $\varphi\in T$ we get $(\exists\varphi)\in T$, i.e., $T\in\|\exists\varphi\|$.

Lemma 3 (Existence Lemma for $\Box$)

$T\in\|\Diamond\varphi\|$* iff there is an $S\in\|\varphi\|$ such that $R^{\Box}TS$.*

Proof

($\Rightarrow$). Assume $T\in\|\Diamond\varphi\|$, i.e., $\Diamond\varphi\in T\in W^{c}$. We first prove the following:

Claim

The set $\Gamma\coloneqq\{\psi\mid(\Box\psi)\in T\}\cup\{\forall\theta\mid\forall\theta\in T_{0}\}\cup\{\varphi\}$ is consistent.

Proof

Suppose that $\Gamma$ is inconsistent. Then there is a finite $\Gamma_{0}\subseteq\Gamma$ such that $\Gamma_{0}\vdash_{\mathsf{L}_{\mathsf{lex}}}\bot$. By the theorems $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box(\psi_{i_{1}}\wedge\dots\wedge\psi_{i_{n}})\leftrightarrow(\Box\psi_{i_{1}}\wedge\dots\wedge\Box\psi_{i_{n}})$ and $\vdash_{\mathsf{L}_{\mathsf{lex}}}\forall(\theta_{j_{1}}\wedge\dots\wedge\theta_{j_{n}})\leftrightarrow(\forall\theta_{j_{1}}\wedge\dots\wedge\forall\theta_{j_{n}})$ we can assume that $\Gamma_{0}=\{\Box\psi,\forall\theta,\neg\varphi\}$ for some $\Box\psi,\forall\theta\in T$. That is, we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box\psi\wedge\forall\theta\to\neg\varphi$. By Necessitation for $\Box$ we obtain $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box(\Box\psi\wedge\forall\theta\to\neg\varphi)$. From this, by $\mathsf{K}_{\Box}$ we get $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box(\Box\psi\wedge\forall\theta)\to\Box\neg\varphi$. By the theorem $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box(\Box\psi\wedge\forall\theta)\leftrightarrow(\Box\Box\psi\wedge\Box\forall\theta)$, from propositional logic we get $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\Box\Box\psi\wedge\Box\forall\theta)\to\Box\neg\varphi$. Given the axioms in our system we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box\psi\to\Box\Box\psi$ and $\vdash_{\mathsf{L}_{\mathsf{lex}}}\forall(\forall\theta)\to\Box(\forall\theta)$. Using these, by propositional logic we obtain $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\Box\psi\wedge\forall\forall\theta)\to\Box\neg\varphi$. Given our axioms, we also have $\vdash_{\mathsf{L}_{\mathsf{lex}}}\forall\theta\to\forall\forall\theta$. Hence by propositional logic we get $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\Box\psi\wedge\forall\theta)\to\Box\neg\varphi$. As $\Box\psi,\forall\theta\in T$ and $T$ is closed under modus ponens, we get $(\Box\neg\varphi)\in T$. But we also have $(\Diamond\varphi)\in T$, i.e., $(\neg\Box\neg\varphi)\in T$, and since $T$ is maximal consistent, this means that $(\Box\neg\varphi)\not\in T$. Contradiction.

Given the Claim, by Lindenbaum’s Lemma, there is some maximally consistent theory $S$ such that $\Gamma\subseteq S$. As $\varphi\in\Gamma$ we have $\varphi\in S$. Moreover, as $\{\psi\mid(\Box\psi)\in T\}\subseteq S$, we have $R^{\Box}TS$. Additionally, we have $\{\forall\theta\mid(\forall\theta)\in T_{0}\}\subseteq S$ and thus $R^{\forall}T_{0}S$. Hence $S\in W^{c}$, which together with $\varphi\in S$ gives us $S\in\|\varphi\|$.

($\Leftarrow$) Assume $T\in\|\varphi\|$, i.e., $\varphi\in T$. Given $\mathsf{T}_{\Box}$ we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box\neg\varphi\to\neg\varphi$, and by contraposition we get $\vdash_{\mathsf{L}_{\mathsf{lex}}}\neg\neg\varphi\to\neg\Box\neg\varphi$, i.e., $\vdash_{\mathsf{L}_{\mathsf{lex}}}\varphi\to\Diamond\varphi$. Hence, $(\varphi\to\Diamond\varphi)\in T$ and as $T$ is closed under modus ponens, given also $\varphi\in T$ we get $(\Diamond\varphi)\in T$, i.e., $T\in\|\Diamond\varphi\|$.

Lemma 4 (Existence Lemma for $\Box_{0}$)

$T\in\|\Box_{0}\varphi\|$* iff there is an $R\in\mathscr{R}^{c}$ such that $R[T]\subseteq\|\varphi\|$.*

Proof

($\Rightarrow$). Assume $T\in\|\Box_{0}\varphi\|$, i.e., $(\Box_{0}\varphi)\in T\in W^{c}$. We first prove the following:

Claim

$\exists\Box_{0}\varphi\in T_{0}$.

Proof

Suppose not. As $T_{0}$ is maximal consistent, we have $\neg\exists\Box_{0}\varphi\in T_{0}$, i.e., $\forall\neg\Box_{0}\varphi\in T_{0}$. As $T\in W^{c}$, we have $R^{\forall}T_{0}T$. So given $\forall\neg\Box_{0}\varphi\in T_{0}$ we have $\forall\neg\Box_{0}\varphi\in T$. By $\mathsf{T}_{\forall}$ we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}\forall\neg\Box_{0}\varphi\to\neg\Box_{0}\varphi$, i.e., $(\forall\neg\Box_{0}\varphi\to\neg\Box_{0}\varphi)\in T$. As $T$ is closed under modus ponens, given $(\forall\neg\Box_{0}\varphi)\in T$ we get $(\neg\Box_{0}\varphi)\in T$. But we also have $(\Box_{0}\varphi)\in T\in W^{c}$ and thus $T$ is inconsistent. Contradiction.

Hence $R^{\Box_{0}\varphi}\in\mathscr{R}^{c}$. We will show that $R^{\Box_{0}\varphi}[T]\subseteq\|\varphi\|$. Let $S\in W^{c}$ be arbitrary and suppose that $R^{\Box_{0}\varphi}TS$. By definition of $R^{\Box_{0}\varphi}$, we have $(\Box_{0}\varphi)\in T$ implies $(\Box_{0}\varphi)\in S$. As $(\Box_{0}\varphi)\in T$ we get $(\Box_{0}\varphi)\in S$. Given $\mathsf{T}_{\Box_{0}}$ we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box_{0}\varphi\to\varphi$ and thus $(\Box_{0}\varphi\to\varphi)\in S$. Since $S$ is closed under modus ponens we thus get $\varphi\in S$, i.e., $S\in\|\varphi\|$. As $S$ was picked arbitrarily, we have $R^{\Box_{0}\varphi}[T]\subseteq\|\varphi\|$.

($\Leftarrow$) Let $T\in W^{c}$ and suppose there is an $R\in\mathscr{R}^{c}$ such that $R[T]\subseteq\|\varphi\|$. By definition of ${R}^{c}$, (i) $R=R^{\prime}$ or (ii) $R=R^{\Box_{0}\theta}$ for some $\theta\in\mathscr{L}$ such that $(\exists\Box_{0}\theta)\in T_{0}$.

We first consider the case (i), i.e., $R=R^{\prime}$. We need to show that $T\in\|\Box_{0}\varphi\|$. Suppose not, i.e., $\Box_{0}\varphi\not\in T$. Recall that, given the definition of $F:W^{c}\times\mathscr{L}\to W^{c}$, given that $(\Box_{0}\varphi)\not\in T$, we have $F(T,\varphi)=S$ for some theory $S\in W^{c}$ such that $\varphi\not\in S$. Moreover, $R^{\prime}$ is the reflexive transitive closure of the relation $R^{\Box}\cup\{(T,F(T,\varphi))\mid T\in W^{c}\text{ and }\varphi\in\mathscr{L}\}$. Hence $(T,S)\in\{(T,F(T,\varphi))\mid T\in W^{c}\text{ and }\varphi\in\mathscr{L}\}$ and thus $(T,S)\in R^{\prime}$. But then, as $S\in W^{c}$ and $\varphi\not\in S$, we have $S\not\in\|\varphi\|$. This implies $R^{\prime}[T]\not\subseteq\|\varphi\|$, contradicting our assumption to the contrary.

We now consider case (ii), i.e., $R=R^{\Box_{0}\theta}$ for some $\theta\in\mathscr{L}$ such that $(\exists\Box_{0}\theta)\in T_{0}$. Either $\Box_{0}\theta\in T$ or $\Box_{0}\theta\not\in T$. We consider both cases.

Case 1: Suppose that $\Box_{0}\theta\in T\in W^{c}$. We first prove the following:

Claim

The set $\Gamma\coloneqq\{\Box_{0}\theta\}\cup\{\forall\psi\mid(\forall\psi)\in T\}\cup\{\neg\varphi\}$ is inconsistent.

Proof

Suppose that $\Gamma$ is consistent. By Lindenbaum’s Lemma there is some maximal consistent theory $S$ such that $\Gamma\subseteq S$. Moreover, as $\{\forall\psi\mid(\forall\psi)\in T_{0}\}\subseteq\{\forall\psi\mid(\forall\psi)\in T\}\subseteq S$, we have $R^{\forall}T_{0}S$ and thus $S\in W^{c}$. As $\neg\varphi\in\Gamma$ we have $\neg\varphi\in S$. Since $S$ is consistent we have $\varphi\not\in S$, i.e., $S\not\in\|\varphi\|$. From $\Box_{0}\theta\in\Gamma$ we have $\Box_{0}\theta\in S$. By definition of $R^{\Box_{0}\theta}$, we get $R^{\Box_{0}\theta}TS$. But then, given $S\not\in\|\varphi\|$, we have $R^{\Box_{0}\theta}[T]\not\subseteq\|\varphi\|$. Contradiction.

Given the Claim, there is a finite $\Gamma_{0}\subseteq\Gamma$ such that $\Gamma_{0}\vdash_{\mathsf{L}_{\mathsf{lex}}}\bot$. By the theorem $\vdash_{\mathsf{L}_{\mathsf{lex}}}\forall(\psi_{1}\wedge\dots\wedge\psi_{n})\leftrightarrow(\forall\psi_{1}\wedge\dots\wedge\forall\psi_{n})$ we can assume that $\Gamma_{0}=\{\Box_{0}\theta,\forall\psi,\neg\varphi\}$ for some $\psi\in T$. Since $\Gamma_{0}\vdash_{\mathsf{L}_{\mathsf{lex}}}\bot$ we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\Box_{0}\theta\wedge\forall\psi\wedge\neg\varphi)\to\bot$, so by propositional logic $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\Box_{0}\theta\wedge\forall\psi)\to(\neg\varphi\to\bot)$, i.e., $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\Box_{0}\theta\wedge\forall\psi)\to(\neg\neg\varphi)$, i.e., $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\Box_{0}\theta\wedge\forall\psi)\to\varphi$. Given the Pullout axiom, we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box_{0}(\theta\wedge\forall\psi)\to(\Box_{0}\theta\wedge\forall\psi)$ and thus $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box_{0}(\theta\wedge\forall\psi)\to\varphi$. By the Monotonicity Rule for $\Box_{0}$, we get $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box_{0}\Box_{0}(\theta\wedge\forall\psi)\to\Box_{0}\varphi$. By $\mathsf{4}_{\Box_{0}}$, we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box_{0}(\theta\wedge\forall\psi)\to\Box_{0}\Box_{0}(\theta\wedge\forall\psi)$ and thus $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box_{0}(\theta\wedge\forall\psi)\to\Box_{0}\varphi$. By the Pullout axiom, we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\Box_{0}\theta\wedge\forall\psi)\to\Box_{0}(\theta\wedge\forall\psi)$. Hence $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\Box_{0}\theta\wedge\forall\psi)\to\Box_{0}\varphi$. Therefore $((\Box_{0}\theta\wedge\forall\psi)\to\Box_{0}\varphi)\in T$. As $(\Box_{0}\theta)\in T$ and $(\forall\psi)\in T$, by closure under modus ponens, we have $\Box_{0}\varphi\in T$. That is, $T\in\|\Box_{0}\varphi\|$.

Case 2: Suppose that $\Box_{0}\theta\not\in T$. Note that $\Box_{0}\theta\not\in T$ implies that $R^{\Box_{0}\theta}[T]=W^{c}$, and since we have $R=R^{\Box_{0}\theta}$ and $R[T]\subseteq\|\varphi\|$, all this gives us that $W^{c}\subseteq\|\varphi\|_{c}$, i.e. all theories in the canonical model contain $\varphi$. We now prove the following:

Claim

The set $\Gamma\coloneqq\{\forall\psi\mid(\forall\psi)\in T\}\cup\{\neg\varphi\}$ is inconsistent.

Proof

Suppose that $\Gamma$ is consistent. By Lindenbaum’s Lemma there is some maximal consistent theory $S$ such that $\Gamma\subseteq S$. Moreover, as $\{\forall\psi\mid(\forall\psi)\in T_{0}\}\subseteq\{\forall\psi\mid(\forall\psi)\in T\}\subseteq S$, we have $R^{\forall}T_{0}S$ and thus $S\in W^{c}$. As $\neg\varphi\in\Gamma$ we have $\neg\varphi\in S$ and thus $S\in\|\neg\varphi\|$. Therefore $W^{c}\not\subseteq\|\varphi\|$ (contradiction).

Given the Claim, there is a finite $\Gamma_{0}\subseteq\Gamma$ such that $\Gamma_{0}\vdash_{\mathsf{L}_{\mathsf{lex}}}\bot$. By the theorem $\vdash_{\mathsf{L}_{\mathsf{lex}}}\forall(\psi_{1}\wedge\dots\wedge\psi_{n})\leftrightarrow(\forall\psi_{1}\wedge\dots\wedge\forall\psi_{n})$ we can assume that $\Gamma_{0}=\{\forall\psi,\neg\varphi\}$ for some $\psi\in T$. Since $\Gamma_{0}\vdash_{\mathsf{L}_{\mathsf{lex}}}\bot$ we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\forall\psi\wedge\neg\varphi)\to\bot$, so by propositional logic $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\forall\psi)\to(\neg\varphi\to\bot)$, i.e., $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\forall\psi)\to(\neg\neg\varphi)$, i.e., $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\forall\psi)\to\varphi$. By propositional logic, given $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\forall\psi)\to\varphi$ we can strengthen the antecedent getting $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\Box_{0}\top\wedge\forall\psi)\to\varphi$. Given the $\text{Pullout axiom}^{\leftrightarrow}$, we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box_{0}(\top\wedge\forall\psi)\leftrightarrow(\Box_{0}\top\wedge\forall\psi)$ and thus $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box_{0}(\top\wedge\forall\psi)\to\varphi$. By the Monotonicity Rule for $\Box_{0}$, we get $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box_{0}\Box_{0}(\top\wedge\forall\psi)\to\Box_{0}\varphi$. By $\mathsf{4}_{\Box_{0}}$, we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box_{0}(\top\wedge\forall\psi)\to\Box_{0}\Box_{0}(\top\wedge\forall\psi)$ and thus $\vdash_{\mathsf{L}_{\mathsf{lex}}}\Box_{0}(\top\wedge\forall\psi)\to\Box_{0}\varphi$. By the $\text{Pullout axiom}^{\leftrightarrow}$, we have $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\Box_{0}\top\wedge\forall\psi)\leftrightarrow\Box_{0}(\top\wedge\forall\psi)$. Hence $\vdash_{\mathsf{L}_{\mathsf{lex}}}(\Box_{0}\top\wedge\forall\psi)\to\Box_{0}\varphi$. Therefore $((\Box_{0}\top\wedge\forall\psi)\to\Box_{0}\varphi)\in T$. As $\Box_{0}\top$ is an axiom of our system, we have $(\Box_{0}\top)\in T$ and $(\forall\psi)\in T$. Hence by closure under modus ponens, we have $\Box_{0}\varphi\in T$. That is, $T\in\|\Box_{0}\varphi\|$.

Lemma 5 (Truth Lemma)

For every $\varphi\in\mathscr{L}$, we have: $\llbracket\varphi\rrbracket_{M^{c}}=\|\varphi\|$.

Proof

The proof is by induction on the complexity of $\varphi$. The base case follows from the definition of $V^{c}$. For the inductive case, suppose that for all $T\in W^{c}$ and all formulas $\psi$ of lower complexity than $\varphi$, we have $\llbracket\psi\rrbracket_{M^{c}}=\|\psi\|$. The Boolean cases where $\varphi=\neg\psi$ and $\varphi=\psi_{1}\wedge\psi_{2}$ follow from the induction hypothesis together with the standard facts about maximal consistent theories included in proposition 1. Only the modalities remain. Let $\varphi=\exists\psi$ and consider any $T\in M^{c}$. We have $T\in\|\exists\psi\|$ iff (proposition 2) $\|\varphi\|\neq\emptyset$ iff (induction hypothesis) $\llbracket\psi\rrbracket_{M^{c}}$ iff $\llbracket\exists\psi\rrbracket_{M^{c}}=W^{c}$ iff $T\in\llbracket\exists\psi\rrbracket_{M^{c}}$. Now let $\varphi=\Box_{0}\psi$ and consider any $T\in M^{c}$. We have $T\in\|\Box_{0}\psi\|$ iff (proposition 4) there is an $R\in\mathscr{R}^{c}$ such that $R[T]\subseteq\|\psi\|$ iff (induction hypothesis) there is an $R\in\mathscr{R}^{c}$ such that $R[T]\subseteq\llbracket\psi\rrbracket_{M^{c}}$ iff $T\in\llbracket\Box_{0}\psi\rrbracket_{M^{c}}$. Let $\varphi=\Diamond\psi$. We have $T\in\|\Diamond\psi\|$ iff (proposition 3) there is an $S\in\|\psi\|$ such that $R^{\Box}TS$ iff (induction hypothesis) there is an $S\in\llbracket\psi\rrbracket_{M^{c}}$ such that $R^{\Box}TS$ iff there is an $S\in\llbracket\psi\rrbracket_{M^{c}}$ such that $(T,S)\in Ag^{c}(\langle\mathscr{R}^{c},\preceq^{c}\rangle)$ iff $T\in\llbracket\Diamond\psi\rrbracket_{M^{c}}$.

Lemma 6

$\mathsf{L}_{\mathsf{lex}}$* is strongly complete with respect to the class of pre-models (and hence it is also complete with respect to REL models).*

Proof

It suffices to show that every $\mathsf{L}_{\mathsf{lex}}$-consistent set of formulas is satisfiable on some $\mathsf{lex}$ model. Let $\Gamma$ be an $\mathsf{L}_{\mathsf{lex}}$-consistent set of formulas. By Lindenbaum’s Lemma, there is a maximally consistent set $T_{0}$ such that $\Gamma\subseteq T_{0}$. Choose any canonical pre-model $M^{c}$ for $T_{0}$. By Lemma 5: $M^{c},T_{0}\models\varphi$ for all $\varphi\in T_{0}$.

4.1 Step 2: Unravelling the canonical pre-model

Next, we will unravel the canonical pre-model. We first fix some preliminary notions. First, define a set of “evidential indices”

[TABLE]

where $l$ is a symbol for “left” copy and $r$ is a symbol for “right” copy. We use $\epsilon,\epsilon^{\prime}$ as meta-variables ranging over evidential indices in I. To each $\epsilon\in\emph{I}$, we associate a corresponding relation $R^{\epsilon}$ on the canonical model $W^{c}$, as follows: $R^{\Box_{0}\varphi}$ and $R^{\Box}$ are as before (the relations in the canonical pre-model), and $R^{(\varphi,l)}=R^{(\varphi,r)}\coloneqq\{(T,S)\mid S=F(T,\varphi)\}$.

Definition 39 (Histories)

Let $M^{c}=\langle W^{c},\langle\mathscr{R}^{c},\preceq^{c}\rangle,V^{c},Ag^{c}\rangle$ be a canonical pre-model for $T_{0}$. The set of histories rooted at $T_{0}$ is the following set of finite sequences:

[TABLE]

The set $\tilde{W}$ forms the set of worlds of the unravelled tree.

Basically, histories record all finite sequences of worlds in $M^{c}$ starting with $T_{0}$ and passing to $R^{\epsilon}$-successors at each step, where $\epsilon\in I$.

Definition 40 ($\beta$)

We denote by $\beta:\tilde{W}\to W^{c}$ the map returning the last theory in each history, i.e. $\beta(T_{0},\epsilon_{1},T_{1},\epsilon_{2},\ldots,\epsilon_{n},T_{n})\coloneqq T_{n}$ for all histories in $\tilde{W}$.

We now define the relations that will feature in the unravelling of $M^{c}$ around $T_{0}$.

Definition 41 ($\to^{\epsilon}$ relations)

For a history $w=(T_{0},\epsilon_{1},T_{1},\epsilon_{2},\ldots,\epsilon_{n},T_{n})\in\tilde{W}$, we denote by

[TABLE]

the history obtained by extending the history $w$ with the sequence $(\epsilon,T)$ (where $T\in W^{c}$). Using this notation, we define the following relations $\to^{\epsilon}$ over $\tilde{W}$, labelled by indices in I:

[TABLE]

We now define the unravelled tree for $T_{0}$.

Definition 42 (Unravelled tree)

Let $M^{c}=\langle W^{c},\langle\mathscr{R}^{c},\preceq^{c}\rangle,V^{c},Ag^{c}\rangle$ be a canonical pre-model for $T_{0}$. The unravelling of $M^{c}$ around $T_{0}$ is the structure $\tilde{K}=\langle\tilde{W},\{\to^{\epsilon}\mid\epsilon\in I\},\tilde{V}\rangle$ with

[TABLE]

In the tree unravelling, one history has another history accessible if the second is one step longer than the first. The valuation on histories is copied from that on their last nodes. We now define paths on this tree of histories.

Definition 43 ($\mathcal{R}$-path)

Let $w,w^{\prime}\in\tilde{W}$ and let $\mathcal{R}\subseteq\{\to^{\epsilon}\mid\epsilon\in I\}$. An $\mathcal{R}$-path from $w$ to $w^{\prime}$ is a finite sequence

[TABLE]

where $w_{0}=w$, $w_{n}=w^{\prime}$, $w_{k}\in\tilde{W}$ for $k=1,2,\dots,n$, $\epsilon_{k}\in I$ for $k=1,2,\dots,n-1$ and $w_{k}\to^{\epsilon_{k}}w_{k+1}$ for $k=1,2,\dots,n-1$. For an $\mathcal{R}$-path $p=(w_{0},\epsilon_{1},w_{1},\epsilon_{2},\dots,\epsilon_{n-1},w_{n})$ from $w$ to $w^{\prime}$, we denote by

[TABLE]

the path obtained by extending the path $p$ with $(\epsilon,w^{\prime\prime})$. If $\mathcal{R}$ is not specified, we speak of a path. For any path $p=(w_{0},\epsilon_{1},w_{1},\epsilon_{2},\dots,\epsilon_{n-1},w_{n})$ we define $first(p)=w_{0}$ and $last(p)=w_{n}$.

The following is a standard results about (unravelled) trees, which we will refer to later on.

Lemma 7 (Uniqueness of paths)

Let $\tilde{K}$ be the unravelling of $M^{c}$ around $T_{0}$. Let $w,w^{\prime}\in\tilde{W}$ and $\mathcal{R}\subseteq\{\to^{\epsilon}\mid\epsilon\in I\}$. Then, there is at most one $\mathcal{R}$-path $p$ from $w$ to $w^{\prime}$.

4.2 Step 3: Completeness with respect to $\mathsf{lex}$-models

Step 2 unravelled the canonical pre-model from step 1. Using the structure from the unravelled tree, we now define a REL model $\tilde{M}$ from it. We then show that this model is in fact a $\mathsf{lex}$-model. Finally, we define a variant of a bounded morphism defined for REL models, which we call bounded aggregation-morphism. Bounded aggregation-morphisms work on REL models in the same way as standard bounded-morphisms do on Kripke models: for REL models, modal satisfaction is invariant under bounded aggregation-morphisms. We then show that $M^{c}$ is a bounded-morphic image of $\tilde{M}$, which gives us completeness. We first define the model $\tilde{M}$.

Definition 44 ($\tilde{M}$)

Let $\tilde{K}$ be the unravelling of $M^{c}$ around $T_{0}$. The structure $\tilde{M}=\langle\tilde{W},\langle\tilde{\mathscr{R}},\tilde{\preceq}\rangle,\tilde{V},\tilde{Ag}\rangle$ has:

[TABLE]

where:

[TABLE]

[TABLE]

[TABLE]

Moreover, $\tilde{\preceq}$ is the reflexive closure of $\{(R,Q)\mid R\in\tilde{\mathscr{R}},Q\in\{R^{\prime}_{l},R^{\prime}_{r}\}\}$ Finally, the aggregator $\tilde{Ag}$ is given by:

[TABLE]

Proposition 3

All the evidence relations in $\tilde{\mathscr{R}}\setminus\{\tilde{W}\times\tilde{W}\}$ are reflexive, transitive and anti-symmetric.

Proof

Reflexivity and transitivity follow immediately from the fact that each $R\in\tilde{\mathscr{R}}\setminus\{\tilde{W}\times\tilde{W}\}$ is the reflexive transitive closure of some other relation, and $\tilde{W}\times\tilde{W}$ is reflexive and transitive. Hence we just need to show the anti-symmetry of the relations. Let $R\in\tilde{\mathscr{R}}\setminus\{\tilde{W}\times\tilde{W}\}$ and suppose $Rwv$ and $Rvw$. First, we consider the case $R=\tilde{R}^{\Box_{0}\varphi}$ for some $\varphi$ such that $\exists\Box_{0}\varphi\in T_{0}$. I.e. $R=(\to^{\Box_{0}\varphi})^{*}$. Given $Rwv$ there is some $n\geq 0$ such that:

[TABLE]

Similarly, given $Rvw$ there is some $m\geq 0$ such that:

[TABLE]

By definition of $\to^{\Box_{0}\varphi}$, we have $w_{1}=(w,\Box_{0}\varphi,T_{1})$ for some $T_{1}\in W^{c}$, $w_{2}=(w,\Box_{0}\varphi,T_{1},\Box_{0}\varphi,T_{2})$ for some $T_{2}\in W^{c}$, and proceeding in this way we get

[TABLE]

Similarly, we have $w^{\prime}_{1}=(v,\Box_{0}\varphi,T^{\prime}_{1})$ for some $T^{\prime}_{1}\in W^{c}$, $w^{\prime}_{2}=(v,\Box_{0}\varphi,T^{\prime}_{1},\Box_{0}\varphi,T^{\prime}_{2})$ for some $T^{\prime}_{2}\in W^{c}$, and proceeding in this way we get

[TABLE]

Hence we must have $n=m=0$. For otherwise, substituting $v$ in 2 with the expression in 1 we get

[TABLE]

which is impossible. Therefore $w=w_{0}=w_{n}=v$, as required.

Now we consider the case $R=R^{\prime}_{l}$, i.e. $R=(\to^{\Box}\cup\bigcup\{\to^{(\varphi,l)}\mid\varphi\in\mathscr{L}\})^{*}$. Given $Rwv$ there is some $n\geq 0$ such that:

[TABLE]

Similarly, given $Rvw$ there is some $m\geq 0$ such that:

[TABLE]

Reasoning as we did in the case of $R=\tilde{R}^{\Box_{0}\varphi}$, we conclude that $m=n=0$ and hence $w=v$. The case of $R=R^{\prime}_{r}$ is analogous to the one just discussed, and we are done.

Proposition 4

In $\tilde{M}$ we have:

[TABLE]

Proof

($\subseteq$) Let $(w,v)\in R^{\prime}_{l}\cap R^{\prime}_{d}$. Then we have $(w,v)\in R^{\prime}_{l}$, i.e.,

[TABLE]

Hence, there is some $n\geq 0$ such that:

[TABLE]

Similarly, we have $(w,v)\in R^{\prime}_{r}$, i.e.,

[TABLE]

Hence, there is some $m\geq 0$ such that:

[TABLE]

By definition of $\to^{i_{k}}$, we have $w_{1}=(w,i_{0},T_{1})$ for some $T_{1}\in W^{c}$, $w_{2}=(w,i_{0},T_{1},i_{1},T_{2})$ for some $T_{2}\in W^{c}$, and proceeding in this way we get

[TABLE]

where $T_{i}\in W^{c}$ and $i_{k}\in\{\Box\}\cup\{(\varphi,l)\mid\varphi\in\mathscr{L}\}$, for $k=1,\dots,n-1$. Reasoning in a similar way, we get

[TABLE]

*where $T^{\prime}_{i}\in W^{c}$ and $j_{k}\in\{\Box\}\cup\{(\varphi,r)\mid\varphi\in\mathscr{L}\}$, for $k=1,\dots,m-1$.

Given the expressions 3 and 4, we have $w_{n}=v=w^{\prime}_{m}$. Hence $n=m$ and for all $k<n$, $i_{k}=j_{k}$. Hence we must have $i_{k}=\Box=j_{k}$ for all $k<n$. This means that the path

[TABLE]

can be rewritten as

[TABLE]

*which is an $\{\Box\}$-path from $w$ to $v$. Hence $(w,v)\in\tilde{R}^{\Box}=(\to^{\Box})^{*}$.

$(\supseteq)$* Let $(w,v)\in\tilde{R}^{\Box}=(\to^{\Box})^{*}$. Then there is some $n\geq 0$ such that:*

[TABLE]

The $\{\Box\}$-path described above is also an $\{\Box\}\cup\bigcup\{(\varphi,l)\mid\varphi\in\mathscr{L}\}$-path and an $\{\Box\}\cup\bigcup\{(\varphi,r)\mid\varphi\in\mathscr{L}\}$-path. Hence we have $(w,v)\in R^{\prime}_{l}$ and $(w,v)\in R^{\prime}_{r}$. Thus $(w,v)\in R^{\prime}_{l}\cap R^{\prime}_{r}$.

Proposition 5

$\tilde{M}$* is a $\mathsf{lex}$ model.*

Proof

To establish that $\tilde{M}$ is a $\mathsf{lex}$ model, we need to show that it meets the condition of a REL model and that $\tilde{Ag}=\mathsf{lex}$. That is, we have to show:

$\tilde{\mathscr{R}}$* is a family of evidence, i.e., every $R\in\tilde{\mathscr{R}}$ is a preorder.* 2. 2.

$\tilde{W}\times\tilde{W}\in\tilde{\mathscr{R}}$, i.e., the trivial evidence order is a piece of available evidence. 3. 3.

$\tilde{R}^{\Box}=\mathsf{lex}(\langle\tilde{\mathscr{R}},\tilde{\preceq}\rangle)$* (which given the definition of $\tilde{Ag}$, gives $\tilde{Ag}=\mathsf{lex}$ as required)*

*Item 1 follows from 3, and Item 2 follows from the definition of $\tilde{M}$. Hence Item 3 remains to be shown. Note first that by 4, we have $R^{\prime}_{l}\cap R^{\prime}_{d}=\tilde{R}^{\Box}$. *

($\subseteq$) Suppose that $(w,v)\in\mathsf{lex}(\langle\tilde{\mathscr{R}},\tilde{\preceq})$. Note that $\mathsf{lex}$ is given here by

[TABLE]

Suppose for reductio that $(w,v)\not\in R^{\prime}_{l}\cap R^{\prime}_{d}$. Then $(w,v)\not\in R^{\prime}_{l}$ or $(w,v)\not\in R^{\prime}_{r}$. Without loss of generality, suppose $(w,v)\not\in R^{\prime}_{l}$. Given 5, we have in particular:

[TABLE]

Note that the definition of $\tilde{\preceq}$ is such that $R^{\prime}_{l}$ has no relation strictly above it other than $\tilde{W}\times\tilde{W}$. And $\tilde{W}\times\tilde{W}$ is symmetric and thus it is not the case that $(\tilde{W}\times\tilde{W})^{<}wv$. Hence the right disjunct in 6 is false. Therefore we must have $R^{\prime}_{l}wv$, contradicting our assumption to the contrary.

Suppose that $(w,v)\in R^{\prime}_{l}\cap R^{\prime}_{d}$. Then $R^{\prime}_{l}wv$ and $R^{\prime}_{r}wv$. Suppose first that $w=v$. As $\mathsf{lex}(\langle\tilde{\mathscr{R}},\tilde{\preceq}\rangle)$ is a preorder, we have $(w,v)\in\mathsf{lex}(\langle\tilde{\mathscr{R}},\tilde{\preceq}\rangle)$ and we are done. Suppose now that $w\neq v$. By proposition 3, $R^{\prime}_{l}$ and $R^{\prime}_{r}$ are antisymmetric. Thus from $w\neq v$, $R^{\prime}_{l}wv$ and $R^{\prime}_{r}wv$, we get $(R^{\prime}_{l})^{<}wv$ and $(R^{\prime}_{r})^{<}wv$. Hence, as we have

[TABLE]

from the definition of $\mathsf{lex}$ we get $(w,v)\in\mathsf{lex}(\langle\tilde{\mathscr{R}},\tilde{\preceq})$ as required.

We now introduce the notion of a bounded aggregation-morphism. This is, as we will show, a truth-preserving map between REL models, which works similarly to standard bounded morphisms for Kripke models.

Definition 45 (Bounded aggregation-morphism)

Let $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,Ag\rangle$ and $M^{\prime}=\langle W^{\prime},\langle\mathscr{R}^{\prime},\preceq^{\prime}\rangle,V^{\prime},Ag^{\prime}\rangle$ be two REL models. A mapping $f:W\to W^{\prime}$ is a bounded aggregation-morphism if the following hold:

Valuation condition: for all $w\in W$, $w\in V(p)$ iff $f(w)\in V^{\prime}(p)$ 2. 2.

Forth conditions:

1. (a)

for all $R\in{\mathscr{R}}$, for all $w\in W$, there exists some $R^{\prime}\in\mathscr{R}^{\prime}$ such that $R^{\prime}[f(w)]\subseteq\{f(v)\mid Rwv\}$ 2. (b)

for all $w,v\in W$, if $Ag(\langle{\mathscr{R}},\preceq\rangle)wv$ then $Ag^{\prime}(\langle{\mathscr{R}}^{\prime},\preceq^{\prime}\rangle)f(w)f(v)$ 3. 3.

Back conditions:

1. (a)

for all $R^{\prime}\in{\mathscr{R}}^{\prime}$ and all $w\in W$ there exists some $R\in{\mathscr{R}}$ such that $\{f(v)\mid Rwv\}\subseteq R^{\prime}[f(w)]$. 2. (b)

for all $w\in W$, $v^{\prime}\in W^{\prime}$, if $Ag^{\prime}(\langle{\mathscr{R}}^{\prime},\preceq^{\prime}\rangle)f(w)v^{\prime}$ then there exists some world $v\in W$ such that $Ag(\langle{\mathscr{R}},\preceq\rangle)wv$ and $f(v)=v^{\prime}$.

Proposition 6

Let $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,Ag\rangle$ and $M^{\prime}=\langle W^{\prime},\langle\mathscr{R}^{\prime},\preceq^{\prime}\rangle,V^{\prime},Ag^{\prime}\rangle$ be two REL models. Let $f:W\to W^{\prime}$ be a surjective bounded aggregation-morphism. Then for all $w\in W$ and $\varphi\in\mathscr{L}$: $M,w\models\varphi$ iff $M^{\prime},f(w)\models\varphi$. That is: modal satisfaction is invariant under surjective bounded aggregation-morphisms.

Proof

By induction on the structure of $\varphi$. The base case holds by the valuation condition. The boolean cases are shown by unfolding the definitions, so we consider the cases involving modalities.

Suppose $M,w\models\Diamond_{0}\psi$. Then for all $R\in\mathscr{R}$ there is some $v\in W$ such that $Rwv$ and $M,v\models\psi$. Now we want to show: $M,f(w)\models\Diamond_{0}\psi$. That is, for all $R^{\prime}\in\mathscr{R}^{\prime}$ there is some $v^{\prime}\in W^{\prime}$ such that $R^{\prime}f(w)v^{\prime}$ and $M^{\prime},v^{\prime}\models\psi$. Let $R^{\prime}\in\mathscr{R}^{\prime}$ be arbitrary. By the back condition 3(a), there is some $R\in{\mathscr{R}}$ such that $\{f(v)\mid Rwv\}\subseteq R^{\prime}[f(w)]$. Hence given $Rwv$, we have $f(v)\in R^{\prime}[f(w)]$. That is, $R^{\prime}f(w)f(v)$. By induction hypothesis, given $M,v\models\psi$ we have $M^{\prime},f(v)\models\psi$. As $R^{\prime}$ was arbitrarily picked, this holds for all relations in $\mathscr{R}^{\prime}$. Hence $M^{\prime},f(w)\models\Diamond_{0}\psi$.

Suppose now that $M^{\prime},f(w)\models\Diamond_{0}\psi$. Then for all $R^{\prime}\in\mathscr{R}^{\prime}$ there is some $v^{\prime}\in W^{\prime}$ such that $R^{\prime}f(w)v^{\prime}$ and $M^{\prime},v^{\prime}\models\psi$. Now we want to show: $M,w\models\Diamond_{0}\psi$. That is, for all $R\in\mathscr{R}$ there is some $v\in W$ such that $Rwv$ and $M,v\models\psi$. Let $R\in\mathscr{R}$ be arbitrary. By the forth condition $2(a)$, there exists some $R^{\prime}\in\mathscr{R}^{\prime}$ such that $R^{\prime}[f(w)]\subseteq\{f(v)\mid Rwv\}$. We have $R^{\prime}f(w)v^{\prime}$ and $M^{\prime},v^{\prime}\models\psi$ for some $v^{\prime}\in W^{\prime}$. As $f$ is surjective, we have $v^{\prime}=f(u)$ for some $u\in W$. Hence given $R^{\prime}[f(w)]\subseteq\{f(v)\mid Rwv\}$ and $f(u)\in R^{\prime}[f(w)]$, we get $f(u)\in\{f(v)\mid Rwv\}$. Hence $Rwu$. By induction hypothesis, given $M^{\prime},f(u)\models\psi$ we get $M,u\models\psi$. As $R$ was arbitrarily picked, this holds for all relations in $\mathscr{R}$. Hence we have $M,w\models\diamond_{0}\psi$.

Now suppose $M,w\models\Diamond\psi$. Then there is some $v\in W$ such that $Ag(\rangle\mathscr{R},\preceq\langle)wv$ and $M,v\models\psi$. By the forth condition $2(b)$, we have $Ag^{\prime}(\rangle\mathscr{R}^{\prime},\preceq^{\prime}\langle)f(w)f(v)$. By induction hypothesis, $M^{\prime},f(v)\models\psi$. Hence $M^{\prime},f(w)\models\psi$.

Lastly, suppose $M,f(w)\models\Diamond\psi$. Then there is some $v^{\prime}\in W^{\prime}$ such that $Ag^{\prime}(\rangle\mathscr{R}^{\prime},\preceq^{\prime}\langle)wv$ and $M^{\prime},v^{\prime}\models\psi$. Hence by the back condition $3(b)$, there is some world $v\in W$ such that $Ag(\rangle\mathscr{R},\preceq\langle)wv$ and $f(v)=v^{\prime}$. By induction hypothesis, we get $M,v\models\psi$. Hence $M,w\models\Diamond\psi$.

Proposition 7

The map $\beta:\tilde{W}\to W^{c}$ is a surjective bounded aggregation-morphism.

Proof

We need to check that $\beta$ satisfies the conditions of a surjective bounded aggregation-morphism.

Surjectivity: Let $T\in W^{c}$ be arbitrary. We need to show that there is some $h\in\tilde{W}$ such that $\beta(h)=T$. Recall that we showed in 2.2. that $W^{c}\times W^{c}=R^{\Box_{0}\top}\in\mathscr{R^{c}}$. Hence $R^{\Box_{0}\top}T_{0}T$. Thus the history $h=(T_{0},\Box_{0}\top,T)$ is an element of $\tilde{W}$ with $\beta(h)=T$, as required. 2. 2.

Valuation condition. This follows from the definition of $\tilde{V}$. 3. 3.

Forth conditions:

1. (a)

We need to show that for all $R\in\tilde{{\mathscr{R}}}$, for all $w\in\tilde{W}$, there exists some $R^{\prime\prime}\in\mathscr{R}^{c}$ such that $R^{\prime\prime}[\beta(w)]\subseteq\{\beta(v)\mid Rwv\}$. Let $R\in\tilde{{\mathscr{R}}}$ and $w\in\tilde{W}$ be arbitrary. Suppose first that $R=\tilde{R}^{\Box_{0}\varphi}$ for some $\varphi$ with $\exists\Box_{0}\varphi\in T_{0}$. Consider $R^{\Box_{0}\varphi}\in\mathscr{R}^{c}$. Take any $T\in R^{\Box_{0}\varphi}[\beta(w)]$, i.e., $R^{\Box_{0}\varphi}\beta(w)T$. We will show that $T\in\{\beta(v)\mid\tilde{R}^{\Box_{0}\varphi}wv\}$. Note that, given $R^{\Box_{0}\varphi}\beta(w)T$, the history $w^{\prime}=(w,\Box_{0}\varphi,T)$ is in $\tilde{W}$. This means that $w\to^{\Box_{0}\varphi}w^{\prime}$. Hence $(\to^{\Box_{0}\varphi})^{*}ww^{\prime}$, i.e., $\tilde{R}^{\Box_{0}\varphi}ww^{\prime}$. Given $\beta(w^{\prime})=T$, we get $T\in\{\beta(v)\mid\tilde{R}^{\Box_{0}\varphi}wv\}$, as required.

Suppose now that $R=R^{\prime}_{l}=(\to^{\Box}\cup\bigcup\{\to^{(\varphi,l)}\mid\varphi\in\mathscr{L}\})^{*}$. Consider $R^{\prime}=(R^{\Box}\cup\bigcup\{R^{(\varphi,l)}\})^{*}\in\mathscr{R}^{c}$. Take any $T\in R^{\prime}[\beta(w)]$, i.e., $R^{\prime}\beta(w)T$. We will show that $T\in\{\beta(v)\mid R^{\prime}_{l}wv\}$. Given $R^{\prime}\beta(w)T$, for some $n\geq 0$, there is a path:

[TABLE]

where $S_{i}\in W^{c}$, $\epsilon_{k}\in\{\Box\}\cup\{(\varphi,l)\mid\varphi\in\mathscr{L}\}$, for $k<n$. Hence there are histories $w_{1}=(w,\epsilon_{0},S_{1})$, $w_{2}=(w,\epsilon_{0},S_{1},\epsilon_{1},S_{2})$, up to $w_{n}=(w,\epsilon_{0},S_{1},\epsilon_{1},S_{2},\dots,\epsilon_{n-1},T)$. Hence, by definition of $\to^{\epsilon_{k}}$, for each $k<n$, we have $w_{k}\to^{\epsilon_{k}}w_{k+1}$. Hence there is a path

[TABLE]

And hence $R^{\prime}_{l}ww_{n}$. Given $\beta(w_{n})=T$, we get $T\in\{\beta(v)\mid R^{\prime}_{l}wv\}$, as required.

The case of $R=R^{\prime}_{r}$ is analogous to the one above. Hence we have left the case $R=\tilde{W}\times\tilde{W}$. Consider $R^{\Box_{0}\top}=W^{c}\times W^{c}\in\mathscr{R}^{c}$. Take any $T\in R^{\Box_{0}\top}[\beta(w)]$, i.e., $R^{\Box_{0}\top}\beta(w)T$. This just means that $T\in W^{c}$. We will show that $T\in\{\beta(v)\mid(w,v)\in\tilde{W}\times\tilde{W}\}=\{\beta(v)\mid v\in\tilde{W}\}$. As $\beta$ is surjective, we know that there is some $u\in\tilde{W}$ such that $\beta(u)=T$, and we are done. 2. (b)

We need to show that for all $w,v\in\tilde{W}$, if $\tilde{Ag}(\langle\tilde{{\mathscr{R}}},\tilde{\preceq}\rangle)wv$ then $Ag^{c}(\langle{\mathscr{R}}^{c},\preceq^{c}\rangle)\beta(w)\beta(v)$. Let $w,v\in\tilde{W}$ be arbitrary and suppose that $\tilde{Ag}(\langle\tilde{{\mathscr{R}}},\tilde{\preceq}\rangle)wv$. By proposition 5.3, given $\tilde{Ag}(\langle\tilde{{\mathscr{R}}},\tilde{\preceq}\rangle)wv$ we have $\tilde{R}^{\Box}wv$, i.e., $(\to^{\Box})^{*}wv$. Hence, for some $n\geq 0$, there is a path:

[TABLE]

Hence there are histories $w_{1}=(w,\Box,S_{1})$, $w_{2}=(w,\Box,S_{1},\Box,S_{2})$, up to $w_{n}=v=(w,\Box,S_{1},\Box,S_{2},\dots,\Box,S_{n})$. Hence by definition of $w_{n}$ we have

[TABLE]

And since $R^{\Box}$ is transitive, we get $R^{\Box}\beta(w)S_{n}$, i.e., $R^{\Box}\beta(w)\beta(v)$, as required. 4. 4.

Back conditions:

1. (a)

We need to show that for all $R^{\prime\prime}\in{\mathscr{R}}^{c}$ and all $w\in\tilde{W}$ there exists some $R\in\tilde{{\mathscr{R}}}$ such that $\{\beta(v)\mid Rwv\}\subseteq R^{\prime\prime}[\beta(w)]$. Let $R^{\prime\prime}\in{\mathscr{R}}^{c}$ and $w\in\tilde{W}$ be arbitrary. We reason by cases. First, suppose that $R^{\prime\prime}=R^{\Box_{0}\varphi}$. Consider $\tilde{R}^{\Box_{0}\varphi}\in\tilde{{\mathscr{R}}}$. We will show that $\{\beta(v)\mid\tilde{R}^{\Box_{0}\varphi}wv\}\subseteq R^{\Box_{0}\varphi}[\beta(w)]$. Take any $\beta(u)\in\{\beta(v)\mid\tilde{R}^{\Box_{0}\varphi}wv\}$. We have $\tilde{R}^{\Box_{0}\varphi}wu$, i.e., $(\to^{\Box_{0}\varphi})^{*}wu$. Hence for some $n\geq 0$, there is a path:

[TABLE]

where $w_{i}\in\tilde{W}$, for $k\leq n$. Hence there are histories $w_{1}=(w,\Box_{0}\varphi,S_{1})$, $w_{2}=(w,\Box_{0}\varphi,S_{1},\Box_{0}\varphi,S_{2})$, up to $w_{n}=u=(w,\Box_{0}\varphi,S_{1},\Box_{0}\varphi,S_{2},\dots,\Box_{0}\varphi,S_{n})$. Hence, by definition of $w_{n}$, we have

[TABLE]

And since $R^{\Box_{0}}$ is transitive, we get $R^{\Box_{0}}\beta(w)\beta(u)$, as required.

Suppose now that $R^{\prime\prime}=R^{\prime}\in W^{c}$. Consider $R^{\prime}_{l}\in\tilde{{\mathscr{R}}}$. We will show that $\{\beta(v)\mid R^{\prime}_{l}wv\}\subseteq R^{\prime}[\beta(w)]$. Take any $\beta(u)\in\{\beta(v)\mid R^{\prime}_{l}wv\}$. We have $R^{\prime}_{l}wu$, i.e., $(\to^{\Box}\cup\bigcup\{\to^{(\varphi,l)}\mid\varphi\in\mathscr{L}\})^{*}wu$. Hence for some $n\geq 0$, there is a path:

[TABLE]

where $w_{i}\in\tilde{W}$, $\epsilon_{k}\in\{\Box\}\cup\bigcup\{(\varphi,l)\mid\varphi\in\mathscr{L}\}$ for $k<n$. By definition of $\to^{\epsilon_{k}}$, $w_{1}=(w,\epsilon_{0},S_{1})$ for some $S_{1}\in W^{c}$, $w_{2}=(w,\epsilon_{0},S_{1},\epsilon_{1}\varphi,S_{2})$ for some $S_{2}\in W^{c}$, up to $w_{n}=u=(w,\epsilon_{0},S_{1},\epsilon_{1},S_{2},\dots,\epsilon_{n-1},S_{n})$ where $S_{i}\in W^{c}$ for $i\leq n$. Hence, by definition of $w_{n}$, we have a path

[TABLE]

Since $R^{\prime}=(R^{\Box}\cup\bigcup\{R^{(\varphi,l)}\})^{*}$, the path above is a path from $\beta(w)$ to $\beta(u)$ along $R^{\prime}$, i.e., we have $R^{\prime}\beta(w)\beta(u)$, as required. 2. (b)

We need to show that for all $w\in\tilde{W}$, $T\in W^{c}$, if $Ag^{c}(\langle{\mathscr{R}}^{c},\preceq^{c}\rangle)\beta(w)T$ then there exists some history $v\in\tilde{W}$ such that $\tilde{Ag}(\langle\tilde{{\mathscr{R}}},\tilde{\preceq}\rangle)wv$ and $\beta(v)=T$. Let $w\in\tilde{W}$ and $T\in W^{c}$ be arbitrary, and suppose that $Ag^{c}(\langle{\mathscr{R}}^{c},\preceq^{c}\rangle)\beta(w)T$, i.e., $R^{\Box}\beta(w)T$. Then the history $w^{\prime}=(w,\Box,T)$ is in $\tilde{W}$ and $\beta(w^{\prime})=T$, as required.

With the results established above, we can now show the main result.

Claim

$\mathsf{L}_{\mathsf{lex}}$ is complete w.r.t. $\mathsf{lex}$ models.

Proof

Let $\Gamma$ be a $\mathsf{L}_{\mathsf{lex}}$-consistent set of formulas. By Lindenbaum’s Lemma, $\Gamma$ can be extended to a maximal consistent set $T_{0}$. Choose any canonical pre-model $M^{c}$ for $T_{0}$. By Lemma 14, $M^{c},T_{0}\models\varphi$ for all $\varphi\in T_{0}$. Let $\tilde{K}$ be the unraveling of $M^{c}$ around $T_{0}$ and let $\tilde{M}$ be the $\mathsf{lex}$ model generated from $\tilde{K}$. Note that the history $(T_{0})\in\tilde{W}$. Let $\beta:\tilde{W}\to W^{c}$ be the map defined above. By proposition 7, $\beta$ is a surjective bounded aggregation-morphism. By proposition 6, we have $M^{c},T_{0}\models\psi$ iff $\tilde{M},\beta(T_{0})\models\psi$. Hence, in particular, $\tilde{M},\beta(T_{0})\models\varphi$ for all $\varphi\in T_{0}$.

PROOF OF THEOREM 2

We recall the theorem:

See 2

We prove the soundness and completeness of $\mathsf{L}^{!}$, $\mathsf{L}^{+}$ and $\mathsf{L}^{\Uparrow}$ separately.

Soundness and completeness of $\mathsf{L}^{!}$.

Claim

$\mathsf{L}^{!}$ is sound w.r.t. $\cap$-models.

Proof

A straighforward validity check.

Claim. $\mathsf{L}^{!}$ is complete w.r.t $\cap$-models.

Proof

The proof is standard, following the approach presented, e.g., in [21], Chapter 7.

Soundness and completeness of $\mathsf{L}^{+}$.

As before, we first consider soundness.

Claim

$\mathsf{L}^{+}$ is sound w.r.t $\cap$-models.

Proof

Let $M=\langle W,\mathscr{R},V,Ag_{\cap}\rangle$ be a $\cap$-model, $w$ a world in $M$, $\pi$ be an evidence program with normal form $\bigcup_{s\in S_{0}(I)}(?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}})\cup(?\top)$.

Axiom $\text{EA4}_{\cap}$: We first prove the following:

Claim

$\llbracket\pi\rrbracket_{M}[w]\subseteq\llbracket[+\pi]\chi\rrbracket_{M}$ iff $M,w\models[+\pi]\chi\wedge\bigwedge_{s\in S_{0}(I)}(s(\bm{\varphi},\bm{\psi})\to\forall(\psi_{s_{\mathsf{len}(s)}}\to[+\pi]\chi))$.

Proof

($\Rightarrow$) Suppose $\llbracket\pi\rrbracket_{M}[w]\subseteq\llbracket[+\pi]\chi\rrbracket_{M}$. As $\pi$ is a $*$-program, $\llbracket\pi\rrbracket_{M}$ is reflexive and thus $M,w\models[+\pi]\chi$. It remains to be shown that

[TABLE]

Take any $s\in S_{0}(I)$ and suppose that $M,w\models s(\bm{\varphi},\bm{\psi})$. We need to show that $M,w\models\forall(\psi_{s_{\mathsf{len}(s)}}\to[+\pi]\chi)$. Take any $v\in W$ and suppose $M,v\models\psi_{s_{\mathsf{len}(s)}}$. If we show that $M,v\models[+\pi]\chi$, we are done. Given $M,w\models s(\bm{\varphi},\bm{\psi})$ and $M,v\models\psi_{s_{\mathsf{len}(s)}}$, by Proposition 4, we have $(w,v)\in\llbracket?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}}\rrbracket_{M}$. Thus

[TABLE]

Hence as

[TABLE]

we have $(w,v)\in\llbracket\pi\rrbracket_{M}$. Hence, given $\llbracket\pi\rrbracket_{M}[w]\subseteq\llbracket[+\pi]\chi\rrbracket_{M}$ we have $M,v\models[+\pi]\chi$, as required.

$(\Leftarrow$) Suppose that $M,w\models[+\pi]\chi\wedge\bigwedge_{s\in S_{0}(I)}(s(\bm{\varphi},\bm{\psi})\to\forall(\psi_{s_{\mathsf{len}(s)}}\to[+\pi]\chi))$. We will show that $\llbracket\pi\rrbracket_{M}[w]\subseteq\llbracket[+\pi]\chi\rrbracket_{M}$. Take any $v$ and suppose $(w,v)\in\llbracket\pi\rrbracket_{M}$. We need to show that $v\in\llbracket[+\pi]\chi\rrbracket_{M}$. If $v=w$, given $M,w\models[+\pi]\chi$ we are done. So suppose $v\neq w$. Note that

[TABLE]

Since we have $M,w\models\bigwedge_{s\in S_{0}(I)}(s(\bm{\varphi},\bm{\psi})\to\forall(\psi_{s_{\mathsf{len}(s)}}\to[+\pi]\chi))$, we get in particular

[TABLE]

Thus from $w\in\llbracket s^{\prime}(\bm{\varphi},\bm{\psi})\rrbracket_{M}$ we get $M,w\models\forall(\psi_{s^{\prime}_{\mathsf{len}(s^{\prime})}}\to[+\pi]\chi)$. And given $v\in\llbracket\psi_{s^{\prime}_{\mathsf{len}(s^{\prime})}}\rrbracket_{M}$ we get $M,v\models[+\pi]\chi$, as required.

Given the Claim, we have:

[TABLE] 2. 2.

Axiom $\text{EA5}_{\cap}$: We first prove the following:

Claim

$\bigcap(\mathscr{R}\cup\{\llbracket\pi\rrbracket_{M}\})[w]\subseteq\llbracket[+\pi]\chi\rrbracket_{M}$ iff $M,w\models[+\pi]\chi\wedge\bigwedge_{s\in S_{0}(I)}(s(\bm{\varphi},\bm{\psi})\to\Box(\psi_{s_{\mathsf{len}(s)}}\to[+\pi]\chi))$.

Proof

($\Rightarrow$) Suppose $\bigcap(\mathscr{R}\cup\{\llbracket\pi\rrbracket_{M}\})[w]\subseteq\llbracket[+\pi]\chi\rrbracket_{M}$. As $\bigcap(\mathscr{R}\cup\{\llbracket\pi\rrbracket_{M}\})$ is reflexive, we have $M,w\models[+\pi]\chi$. It remains to be shown that

[TABLE]

Take any $s\in S_{0}(I)$ and suppose that $M,w\models s(\bm{\varphi},\bm{\psi})$. We need to show that $M,w\models\Box(\psi_{s_{\mathsf{len}(s)}}\to[+\pi]\chi)$. Take any $v\in\bigcap(\mathscr{R})[w]$ and suppose $M,v\models\psi_{s_{\mathsf{len}(s)}}$. If we show that $M,v\models[+\pi]\chi$, we are done. Given $M,w\models s(\bm{\varphi},\bm{\psi})$ and $M,v\models\psi_{s_{\mathsf{len}(s)}}$, by Proposition 4, we have $(w,v)\in\llbracket?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}}\rrbracket_{M}$. Thus

[TABLE]

Hence as

[TABLE]

we have $(w,v)\in\llbracket\pi\rrbracket_{M}$. Hence, given $\bigcap(\mathscr{R}\cup\{\llbracket\pi\rrbracket_{M}\})[w]\subseteq\llbracket\pi\rrbracket_{M}[w]\subseteq\llbracket[+\pi]\chi\rrbracket_{M}$ we have $M,v\models[+\pi]\chi$, as required.

$(\Leftarrow$) Suppose that $M,w\models[+\pi]\chi\wedge\bigwedge_{s\in S_{0}(I)}(s(\bm{\varphi},\bm{\psi})\to\Box(\psi_{s_{\mathsf{len}(s)}}\to[+\pi]\chi))$. We will show that $\bigcap(\mathscr{R}\cup\{\llbracket\pi\rrbracket_{M}\})[w]\subseteq\llbracket[+\pi]\chi\rrbracket_{M}$. Take any $v$ and suppose $(w,v)\in\bigcap(\mathscr{R}\cup\{\llbracket\pi\rrbracket_{M}\})$. We need to show that $v\in\llbracket[+\pi]\chi\rrbracket_{M}$. If $v=w$, given $M,w\models[+\pi]\chi$ we are done. So suppose $v\neq w$. Since $(w,v)\in\bigcap(\mathscr{R}\cup\{\llbracket\pi\rrbracket_{M}\})=\bigcap(\mathscr{R})\cap\llbracket\pi\rrbracket_{M}$, we have $(w,v)\in\llbracket\pi\rrbracket_{M}$. Reasoning as we did in the proof of $\text{EA4}_{\cap}$, we get

[TABLE]

Given that $M,w\models\bigwedge_{s\in S_{0}(I)}(s(\bm{\varphi},\bm{\psi})\to\Box(\psi_{s_{\mathsf{len}(s)}}\to[+\pi]\chi))$, we have in particular

[TABLE]

Thus from $w\in\llbracket s^{\prime}(\bm{\varphi},\bm{\psi})\rrbracket_{M}$ we get $M,w\models\Box(\psi_{s^{\prime}_{\mathsf{len}(s)}}\to[+\pi]\chi)$. And given $(w,v)\in\bigcap\mathscr{R}$ and $v\in\llbracket\psi_{s^{\prime}_{\mathsf{len}(s^{\prime})}}\rrbracket_{M}$, we get $M,v\models[+\pi]\chi$, as required.

Given the Claim, we have

[TABLE] 3. 3.

Axiom $\text{EA6}_{\cap}$:

[TABLE]

Claim

$\mathsf{L}^{+}$ is complete with respect to the class of $\cap$-models.

Proof

The proof follows the approach presented above for $\mathsf{L}^{!}$.

Soundness and completeness of $\mathsf{L}^{\Uparrow}$

As before, we first consider soundness. Before proving the main claim, we introduce a lemma about the formulas occurring in the reduction axioms.

Lemma 8

Let $M=\langle W,\mathscr{R},V,Ag_{\cap}\rangle$ be a $\cap$-model, $w$ a world in $M$, $\pi\in\Pi_{*}$ be a program with normal form $\bigcup_{s\in S_{0}(I)}(?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}})\cup(?\top)$. Then

$M,w\models\pi^{\cap}(\chi)$* iff there is an $R\in\mathscr{R}:(R\cap\llbracket\pi\rrbracket_{M})[w]\subseteq\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$* 2. 2.

$M,w\models[\Uparrow\pi]\chi\wedge\pi^{<}(\chi)$* iff $w\in\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$ and $\llbracket\pi\rrbracket^{<}_{M}[w]\subseteq\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$*

Proof

**

Item 1: ($\Rightarrow$) Let $M,w\models\pi^{\cap}(\chi)$, i.e.,

[TABLE]

We need to show that there is an $R\in\mathscr{R}:(R\cap\llbracket\pi\rrbracket_{M})[w]\subseteq\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$. Note first that we have

[TABLE]

Then, there is a $J\subseteq I$ such that $M,w\models J(\bm{\varphi})$ and

[TABLE]

Hence, there is some $R\in\mathscr{R}$ such that, for all $v$ with $Rwv$

[TABLE]

Now take any $u$ such that $(w,u)\in R\cap\llbracket\pi\rrbracket_{M}$. If we show that $u\in\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$, we are done. Note first that given $M,w\models\pi^{\cap}(\chi)$, we have $M,w\models[\Uparrow\pi]\chi$, so if $w=u$ we are done. Suppose $w\neq u$. As $(w,u)\in R\cap\llbracket\pi\rrbracket_{M}$, we have $(w,u)\in\llbracket\pi\rrbracket_{M}$. Note that

[TABLE]

Thus, we have $M,w\models s^{\star}(\bm{\varphi},\bm{\psi})$ and hence $M,u\models\exists(s^{\star}(\bm{\varphi},\bm{\psi}))$. Recall that

[TABLE]

Hence $M,w\models\varphi_{s^{\star}_{1}}$ and as $M,w\models J(\bm{\varphi})$, we must have $\varphi_{s^{\star}_{1}}=\varphi_{j}$ for some $j\in J$. This, together with $M,u\models\psi_{s^{\star}_{\mathsf{len}(s^{\star})}}$ gives us

[TABLE]

which, given the statement 7 above, implies $M,u\models[\Uparrow\pi]\chi$, as required.

$(\Leftarrow)$* Suppose that there is an $R\in\mathscr{R}$ such that $(R\cap\llbracket\pi\rrbracket_{M})[w]\subseteq\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$. First, note that $R\cap\llbracket\pi\rrbracket_{M}$ is reflexive, and hence $M,w\models[\Uparrow\pi]\chi$. Hence it remains to be shown that*

[TABLE]

It is clear that there is some $J\subseteq I$ such that $M,w\models J(\bm{\varphi})$, so we must show for this $J$ that

[TABLE]

Consider $R$ and take any $v$ such that $Rwv$. We need to show that

[TABLE]

Suppose that

[TABLE]

Then there is some $s\in S_{0}(I)$ with $s_{1}\in J$ such that $M,v\models\exists(s(\bm{\varphi},\bm{\psi}))\wedge\psi_{s_{\mathsf{len}(s)}}$. Hence there is some $u$ such that $M,u\models s(\bm{\varphi},\bm{\psi})$. Recall that

[TABLE]

Given $s_{1}\in J$ and $M,w\models J(\bm{\varphi})$, we have $M,w\models\varphi_{s_{1}}$ and thus $M,w\models s(\bm{\varphi},\bm{\psi})$. This, together with $M,v\psi_{s_{\mathsf{len}(s)}}$, implies $(w,v)\in\llbracket?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}}\rrbracket_{M}$ and hence $(w,v)\in\llbracket\textsf{nf}(\pi)\rrbracket_{M}$ (where $\textsf{nf}(\pi)$ is the normal form for $\pi$), which means $(w,v)\in\llbracket\pi\rrbracket_{M}$. As $(w,v)\in R$ and $(w,v)\in\llbracket\pi\rrbracket_{M}$ we have $(w,v)\in R\cap\llbracket\pi\rrbracket_{M}$. Thus given $(R\cap\llbracket\pi\rrbracket_{M})[w]\subseteq\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$ we have $M,v\models[\Uparrow\pi]\chi$, as required.

Item 2: ($\Rightarrow$) Let $M,w\models[\Uparrow\pi]\chi\wedge\pi^{<}(\chi)$. Then $w\in\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$, so it remains to be shown that $\llbracket\pi\rrbracket^{<}_{M}[w]\subseteq\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$. We have $M,w\models\pi^{<}(\chi)$, i.e.,

[TABLE]

Then, there is a $J\subseteq I$ such that $M,w\models J(\bm{\psi})$ and

[TABLE]

We need to show that $\llbracket\pi\rrbracket^{<}_{M}[w]\subseteq\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$. Take any $v$ such that $(w,v)\in\llbracket\pi\rrbracket_{M}^{<}$, i.e., $(w,v)\in\llbracket\pi\rrbracket_{M}$ and $(v,w)\not\in\llbracket\pi\rrbracket_{M}$. We will show that $v\in\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$. First, observe that

[TABLE]

Moreover, note that

[TABLE]

Hence we have $\exists s^{\star}\in S_{0}(I)(w\in\llbracket s^{\star}(\bm{\varphi},\bm{\psi})\rrbracket_{M}\text{ and }v\in\llbracket\psi_{s^{\star}_{\mathsf{len}(s^{\star})}}\rrbracket_{M})$ and $\forall s\in S_{0}(I)(v\in\llbracket s(\bm{\varphi},\bm{\psi})\rrbracket_{M}\text{ implies }w\not\in\llbracket\psi_{s_{\mathsf{len}(s)}}\rrbracket_{M})$. From 8, we have in particular

[TABLE]

We have $w\in\llbracket s^{\star}(\bm{\varphi},\bm{\psi})\rrbracket_{M}$, from which we get

[TABLE]

Thus, in particular

[TABLE]

We already have $v\in\llbracket\psi_{s^{\star}_{\mathsf{len}(s^{\star})}}\rrbracket_{M}$, so if we show that

[TABLE]

we will get $M,v\models[\Uparrow\pi]\chi$, as required. Take any $s^{\prime}\in S_{0}(I)$ and suppose that $M,v\models s^{\prime}(\bm{\varphi},\bm{\psi})$. We need to show that $M,v\models\forall(\psi_{s^{\prime}_{\mathsf{len}(s^{\prime})}}\to\bigwedge_{j\in J}\neg\varphi_{j}))$. Consider any $u\in W$ and suppose $M,u\models\psi_{s^{\prime}_{\mathsf{len}(s^{\prime})}}$. Towards a contradiction, suppose that $M,u\models\varphi_{j}$, for some $j\in J$. Consider the sequence $s^{\prime\prime}\coloneqq s^{\prime}|\langle j\rangle$. Note that

[TABLE]

Given $M,u\models\psi_{s^{\prime}_{\mathsf{len}(s^{\prime})}}$ and $M,u\models\varphi_{j}$, we have $M,v\models\exists(\psi_{s^{\prime}_{{\mathsf{len}(s^{\prime})}}}\wedge\varphi_{j})$. This, together with $M,v\models s^{\prime}(\bm{\varphi},\bm{\psi})$ gives us $M,v\models s^{\prime\prime}(\bm{\varphi},\bm{\psi})$. From $\forall s\in S_{0}(I)(v\in\llbracket s(\bm{\varphi},\bm{\psi})\rrbracket_{M}\text{ implies }w\not\in\llbracket\psi_{s_{\mathsf{len}(s)}}\rrbracket_{M})$ we have: $v\in\llbracket s^{\prime\prime}(\bm{\varphi},\bm{\psi})\rrbracket_{M}\text{ implies }w\not\in\llbracket\psi_{{s^{\prime\prime}}_{\mathsf{len}(s^{\prime\prime})}}\rrbracket_{M}$. Hence we have $w\not\in\llbracket\psi_{{s^{\prime\prime}}_{\mathsf{len}(s^{\prime\prime})}}\rrbracket_{M}$, i.e., $M,w\not\models\psi_{j}$. But since $M,w\models J(\bm{\psi})$, we also have $M,w\models\psi_{j}$ (contradiction). Thus we have $M,v\models\forall(\psi_{s^{\prime}_{\mathsf{len}(s^{\prime})}}\to\bigwedge_{j\in J}\neg\varphi_{j}))$. As $s^{\prime}$ was arbitrarily picked we get statement 9 above, which together with $M,v\models\psi_{s^{\star}_{\mathsf{len}(s^{\star})}}$ implies $M,v\models[\Uparrow\pi]\chi$. Since $v$ was picked arbitrarily, we get $\llbracket\pi\rrbracket^{<}_{M}[w]\subseteq\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$, as required.

$(\Leftarrow)$* Suppose that $w\in\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$ and $\llbracket\pi\rrbracket^{<}_{M}[w]\subseteq\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$. We need to show $M,w\models[\Uparrow\pi]\chi\wedge\pi^{<}(\chi)$. $M,w\models[\Uparrow\pi]\chi$ is immediate, so it remains to be shown that $M,w\models\pi^{<}(\chi)$, i.e.,*

[TABLE]

Clearly, there is a $J\subseteq I$ such that $M,w\models J(\bm{\psi})$, so it remains to be shown that;

[TABLE]

Take any $s\in S_{0}(I)$ and suppose that $M,w\models s(\bm{\varphi},\bm{\psi})$. We need to show that

[TABLE]

Take any $v\in W$ and suppose that

[TABLE]

We need to show that $M,v\models[\Uparrow\pi]\chi$. Note that, if $v=w$ we are done, so suppose that $v\neq w$. Since $\llbracket\pi\rrbracket^{<}_{M}[w]\subseteq\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$, if we show that $(w,v)\in\llbracket\pi\rrbracket^{<}_{M}$ we are done. We show this next, i.e., $(w,v)\in\llbracket\pi\rrbracket_{M}$ and $(v,w)\not\in\llbracket\pi\rrbracket_{M}$. Note that $M,w\models s(\bm{\varphi},\bm{\psi})$ and $M,v\models\psi_{s_{\mathsf{len}(s)}}$. Hence $(w,v)\in\llbracket?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}}\rrbracket_{M}$ and thus $(w,v)\in\llbracket\bigcup_{s^{\prime}\in S_{0}(I)}(?s^{\prime}(\bm{\varphi},\bm{\psi});A;?\psi_{s^{\prime}_{\mathsf{len}(s^{\prime})}})\cup(?\top)\rrbracket_{M}$, which gives $(w,v)\in\llbracket\pi\rrbracket_{M}$. Towards a contradiction, suppose that $(v,w)\in\llbracket\pi\rrbracket_{M}$. Then

[TABLE]

Since $v\neq w$ by assumption, $(v,w)\not\in\llbracket?\top\rrbracket_{M}$, so we must have

[TABLE]

By Lemma 1, this means that there is a finite $vw$-path along $\llbracket\bigcup_{i\in I}(?\varphi_{i};A;?\psi_{i})\rrbracket_{M}$. That is, for some $s^{\prime\prime}\in S_{0}(I)$, $v\in\llbracket\varphi_{s^{\prime\prime}_{1}}\rrbracket_{M}$ and there are $z_{1},z_{2},\dots,z_{\mathsf{len}(s^{\prime\prime})},z_{\mathsf{len}(s^{\prime\prime})+1}$ such that $z_{1}=v$ and $z_{\mathsf{len}(s^{\prime\prime})+1}=w$ and for each $k\in\{1,\dots,\mathsf{len}(s^{\prime\prime})\}$, $(z_{k},z_{k+1})\in\llbracket?\varphi_{s^{\prime\prime}_{k}};A;?\psi_{s^{\prime\prime}_{k}}\rrbracket_{M}$. Given $M,w\models J(\bm{\psi})$, we must have $\psi_{s^{\prime\prime}_{\mathsf{len}(s^{\prime\prime})}}=\psi_{j}$ for some $j\in J$. Let $s^{\star}=\langle s^{\prime\prime}_{1},\dots,s^{\prime\prime}_{\mathsf{len}(s^{\prime\prime})-1}\rangle$. As we have

[TABLE]

In particular, we also have

[TABLE]

As $M,v\models s^{\prime\prime}(\bm{\varphi},\bm{\psi})$, we also have $M,v\models s^{\star}(\bm{\varphi},\bm{\psi})$, which gives us

[TABLE]

Given that $\psi_{s^{\star}_{\mathsf{len}(s^{\star})}}=\psi_{s^{\prime\prime}_{\mathsf{len}(s^{\prime\prime})-1}}$, we get

[TABLE]

and thus from statement 10 above we get

[TABLE]

But then $(z_{\mathsf{len}(s^{\prime\prime})},w)\not\in\llbracket?\varphi_{s^{\prime\prime}_{\mathsf{len}(s^{\prime\prime})}};A;?\psi_{s^{\prime\prime}_{\mathsf{len}(s^{\prime\prime})}}\rrbracket_{M}$ (contradiction).

Having shown the lemmma above, we now consider the main soundness claim.

Claim

$\mathsf{L}^{\Uparrow}$ is sound w.r.t $\cap$-models.

Proof

Let $M=\langle W,\mathscr{R},V,Ag_{\cap}\rangle$ be a $\cap$-model, $w$ a world in $M$, $\pi\in\Pi_{*}$ be a program with normal form $\bigcup_{s\in S_{0}(I)}(?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}})\cup(?\top)$. The validity of $\text{EU1}_{\cap}$ follows from the fact that the evidence addition transformer does not change the valuation function. The validity of the Boolean reduction axioms $\text{EU2}_{\cap}$ and $\text{EU3}_{\cap}$ can be proven by unfolding the definitions.

Axiom $\text{EU4}_{\cap}$:

[TABLE] 2. 2.

Axiom $\text{EU5}_{\cap}$: We first prove the following:

Claim

$(\llbracket\pi\rrbracket_{M}\cap\bigcap\mathscr{R})[w]\subseteq\llbracket[\Uparrow\pi]\chi\rrbracket_{M}$ iff $M,w\models[\Uparrow\pi]\chi\wedge\bigwedge_{s\in S_{0}(I)}(s(\bm{\varphi},\bm{\psi})\to\Box(\psi_{s_{\mathsf{len}(s)}}\to[\Uparrow\pi]\chi))$.

Proof

The proof is identical to the one used for the proof of the validity of ‘Axiom $\text{EA5}_{\cap}$’.

Note next that

[TABLE]

Thus,

[TABLE] 3. 3.

Axiom $\text{EU6}_{\cap}$:

[TABLE]

Claim

$\mathsf{L}^{\Uparrow}$ is complete w.r.t. $\cap$-models.

Proof

The follows the same steps used to prove completeness of $\mathsf{L}^{!}$.

PROOF OF THEOREM 3

We recall the theorem:

See 3

We first introduce some lemmas. During our discussion of evidence upgrade in $\cap$-models, we showed in Lemma 8 that $[\Uparrow\pi]\chi\wedge\pi^{<}(\chi)$ is true at a state $w$ in a $\cap$-model $M$ if $[\Uparrow\pi]\chi$ is true at $w$ and $\llbracket\pi\rrbracket^{<}_{M}[w]\subseteq\llbracket[\oplus\pi]\chi\rrbracket_{M}$. It is easy to see that, since the formula $\pi^{<}(\chi)$ contains no occurrences of $\Box$ (only $\forall$), the result transfers to $\mathsf{lex}$ models, as the semantics of $\forall$ is the same in all REL models. Hence we have:

Lemma 9

Let $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,\mathsf{lex}\rangle$, $w$ a world in $M$, $\pi\in\Pi_{*}$ be a program with normal form $\bigcup_{s\in S_{0}(I)}(?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}})\cup(?\top)$. Then

[TABLE]

Proof

Follows from Lemma 8.

We now introduce another lemma which will be useful in the proof of the reduction axioms.

Lemma 10

Let $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,\mathsf{lex}\rangle$, $w$ a world in $M$, $\pi\in\Pi_{*}$ be a program with normal form $\bigcup_{s\in S_{0}(I)}(?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}})\cup(?\top)$. Then

[TABLE]

iff**

[TABLE]

Proof

Straightforward.

We now show one more lemma, before presenting the proof system $\mathsf{L}^{+}_{\mathsf{lex}}$. With these lemmas in place, the proofs of the validity of the reduction axioms in this system will be almost immediate.

Lemma 11

Let $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,\mathsf{lex}\rangle$, $w$ a world in $M$, $\pi\in\Pi_{*}$ be a program and $\varphi$ a formula. Then

[TABLE]

iff**

[TABLE]

Proof

Straighforward.

We now turn to the main soundness claim.

Claim

$\mathsf{L}^{\oplus}$ is sound w.r.t. $\mathsf{lex}$-models.

Proof

Let $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,\mathsf{lex}\rangle$, $w$ a world in $M$, $\pi$ be an evidence program with normal form $\bigcup_{s\in S_{0}(I)}(?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}})\cup(?\top)$.

Axiom $\oplus$EA4: Note that this same axiom was called $\text{EA4}_{\cap}$ in the system $\mathsf{L}^{+}_{\cap}$ for $\cap$-models. The effects on evidence possession (as expressed by $\Box_{0}$-formulas) of evidence addition in $\cap$-models are the same as the effects of prioritized evidence addition in $\mathsf{lex}$ models; in both cases, the piece of evidence $\llbracket\pi\rrbracket_{M}$ is added to the initial body of evidence $\mathscr{R}$. Thus, it is easy to see that the proof of the validity of $\text{EA4}_{\cap}$ in $\cap$-models can be straightforwardly adapted to show the validity of $\oplus$EA4 in $\mathsf{lex}$ models. 2. 2.

Axiom $\oplus$EA5:

[TABLE] 3. 3.

Axiom $\text{EA6}_{\cap}$:

[TABLE]

Claim

$\mathsf{L}^{\oplus}$ is complete w.r.t. $\mathsf{lex}$-models.

Proof

The proof follows the same steps used above to prove completeness for other proof systems with dynamic modalities.

PROOF OF THEOREM 4

We recall the theorem:

See 4

The soundness proof is straighforward. We focus on completeness. The proof is based on the the completeness-via-canonicity approach. In particular, we construct of a canonical REL model for each $\mathsf{L}_{c}$-consistent theory $T_{0}$. This model is almost identical to the pre-model used in the completeness proof for $\mathsf{L}_{\mathsf{lex}}$.

Definition 46 (Canonical model for $T_{0}$)

A canonical model for $T_{0}$ is a structure $M^{c}=\langle W^{c},\langle\mathscr{R}^{c},\preceq^{c}\rangle,V^{c},Ag^{c}\rangle$ with:

• •

$W^{c}\coloneqq\{T\mid T\text{ is a maximally consistent theory and }R^{\forall}T_{0}T\}$

• •

$\mathscr{R}^{c}\coloneqq\{R^{\Box_{0}\varphi}\mid\varphi\in\mathscr{L}_{c}\text{ and }(\exists\Box_{0}\varphi)\in T_{0}\}$

• •

$\preceq^{c}$ is some preorder on $\mathscr{R}^{c}$

• •

$V^{c}$ is a valuation function given by $V^{c}(p)\coloneqq\|p\|$

• •

$Ag^{c}$ is an aggregator for $W^{c}$ with

[TABLE]

where:

• •

$R^{\forall}$, and each $R^{\Box_{0}\varphi}$ are defined in the same way as in Definition 38.

• •

for each $\varphi\in\mathscr{L}_{c}$, $\|\varphi\|\coloneqq\{T\in W^{c}\mid\varphi\in T\}$

• •

for each sequence of evidence programs $\vec{\pi}$, $R^{\vec{\pi}}\subseteq W^{c}\times W^{c}$ is given by: $R^{\vec{\pi}}TS$ iff for all $\varphi\in\mathscr{L}_{c}$: $\Box^{\vec{\pi}}\varphi\in T\Rightarrow\varphi\in S$.

We first show that this canonical model is indeed a REL model.

Proposition 8

$M^{c}$* is a REL model.*

Proof

In order to show that $M^{c}$ is an REL model, we have to show that:

$\mathscr{R}^{c}$* is a family of evidence, i.e., every $R\in\mathscr{R}$ is a preorder.* 2. 2.

$R^{\Box_{0}\top}=W^{c}\times W^{c}$, i.e., the trivial evidence order is an element of $\mathscr{R}^{c}$, as required. 3. 3.

$R^{\vec{\pi}}$* is a preorder for each $\vec{\pi}$, and thus $Ag^{c}$ is well-defined.*

The proofs of all three items are analogous to the ones given in Proposition 2.

Having established that $M^{c}$ is a REL model, we prove now the standard lemmas to show that the canonical model works as expected.

Lemma 12 (Existence Lemma for $\forall$)

$\|\exists\varphi\|\neq\emptyset$* iff $\|\varphi\|\neq\emptyset$.*

Proof

Same as in Lemma 2.

Lemma 13 (Existence Lemma for $\Box^{\vec{\pi}}$)

Let $\vec{\pi}=\langle\pi_{1},\dots,\pi_{n}\rangle$ be arbitrary. $T\in\|\Diamond^{\vec{\pi}}\varphi\|$ iff there is an $S\in\|\varphi\|$ such that $R^{\vec{\pi}}TS$.

Proof

Analogous to the proof of Lemma 3.

Lemma 14 (Existence Lemma for $\Box_{0}$)

$T\in\|\Box_{0}\varphi\|$* iff there is an $R\in\mathscr{R}^{c}$ such that $R[T]\subseteq\|\varphi\|$.*

Proof

Same as in Lemma 4.

Lemma 15 (Truth Lemma)

For every formula $\varphi\in\mathscr{L}_{c}$, we have: $\llbracket\varphi\rrbracket_{M^{c}}=\|\varphi\|$.

Proof

Analogous to Lemma 5.

Lemma 16

$\mathsf{L}_{c}$* is strongly complete with respect to the class of REL models.*

Proof

Analogous to Lemma 6.

4.3 PROOF OF THEOREM 5

We recall the theorem:

See 5

We consider soundness first.

Claim

The axioms PEA1-PEA6 are valid.

Proof

Let $M=\langle W,\langle\mathscr{R},\preceq\rangle,V,Ag\rangle$ be an REL model, $w$ a world in $M$ and $\vec{\pi}=\langle\pi_{1},\dots,\pi_{n}\rangle$ be a sequence of evidence programs with normal form $\bigcup_{s\in S_{0}(I_{i})}(?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}})\cup(?\top)$ for each $i\in\{1,\dots,n\}$.

Axiom PEA4: We first prove the following:

Claim

There is an $k\in\{1,\dots,n\}$ such that $\llbracket\pi_{k}\rrbracket_{M}[w]\subseteq\llbracket[\oplus\vec{\pi}]\chi\rrbracket_{M}$ iff $M,w\models[\oplus\vec{\pi}]\chi\wedge\bigvee_{1\leq i\leq n}(\bigwedge_{s\in S_{0}(I_{i})}(s(\bm{\varphi},\bm{\psi})\to\forall(\psi_{s_{\mathsf{len}(s)}}\to[\oplus\vec{\pi}]\chi)))$.

Proof

($\Rightarrow$) Suppose there is an $k\in\{1,\dots,n\}$ such that $\llbracket\pi_{k}\rrbracket_{M}[w]\subseteq\llbracket[\oplus\vec{\pi}]\chi\rrbracket_{M}$. As $\pi_{k}$ is an evidence program, $\llbracket\pi_{k}\rrbracket_{M}$ is reflexive and thus $M,w\models[\oplus\vec{\pi}]\chi$. It remains to be shown that

[TABLE]

To show (11), it suffices to find one $i\in\{1,\dots,n\}$ such that

[TABLE]

Consider $i=k$, take any $s\in S_{0}(I_{k})$ and suppose that $M,w\models s(\bm{\varphi},\bm{\psi})$. We need to show that $M,w\models\forall(\psi_{s_{\mathsf{len}(s)}}\to[\oplus\vec{\pi}]\chi)$. Take any $v\in W$ and suppose $M,v\models\psi_{s_{\mathsf{len}(s)}}$. If we show that $M,v\models[\oplus\vec{\pi}]\chi$, we are done. Given $M,w\models s(\bm{\varphi},\bm{\psi})$ and $M,v\models\psi_{s_{\mathsf{len}(s)}}$, by Proposition 4, we have $(w,v)\in\llbracket?s(\bm{\varphi},\bm{\psi});A;?\psi_{s_{\mathsf{len}(s)}}\rrbracket_{M}$. Thus

[TABLE]

Hence as

[TABLE]

we have $(w,v)\in\llbracket\pi_{k}\rrbracket_{M}$. Hence, given $\llbracket\pi_{k}\rrbracket_{M}[w]\subseteq\llbracket[\oplus\vec{\pi}]\chi\rrbracket_{M}$ we have $M,v\models[\oplus\vec{\pi}]\chi$, as required.

$(\Leftarrow$) Suppose that $M,w\models[\oplus\vec{\pi}]\chi\wedge\bigvee_{1\leq i\leq n}(\bigwedge_{s\in S_{0}(I_{i})}(s(\bm{\varphi},\bm{\psi})\to\forall(\psi_{s_{\mathsf{len}(s)}}\to[\oplus\vec{\pi}]\chi)))$. Then there is some $k\in\{1,\dots,n\}$ such that

[TABLE]

We will show that $\llbracket\pi_{k}\rrbracket_{M}[w]\subseteq\llbracket[\oplus\vec{\pi}]\chi\rrbracket_{M}$. Take any $v$ and suppose $(w,v)\in\llbracket\pi_{k}\rrbracket_{M}$. We need to show that $v\in\llbracket[\oplus\vec{\pi}]\chi\rrbracket_{M}$. If $v=w$, given $M,w\models[\oplus\vec{\pi}]\chi$ we are done. So suppose $v\neq w$. Note that

[TABLE]

Given (12), we have in particular

[TABLE]

Thus from $w\in\llbracket s^{\prime}(\varphi)\rrbracket_{M}$ we get $M,w\models\forall(\psi_{s^{\prime}_{\mathsf{len}(s)}}\to[\oplus\vec{\pi}]\chi)$. And given $v\in\llbracket\psi_{s^{\prime}_{\mathsf{len}(s^{\prime})}}\rrbracket_{M}$ we get $M,v\models[\oplus\vec{\pi}]\chi$, as required.

Given the Claim, we have

[TABLE] 2. 2.

Axiom EA5: $M,w\models[\oplus\vec{\pi}]\Box^{\vec{\rho}}\chi$ iff $M^{\oplus\vec{\pi}},w\models\Box^{\vec{\rho}}\chi$ iff $\langle W^{\oplus\llbracket\vec{\pi}\rrbracket_{M}},\langle\mathscr{R}^{\oplus\llbracket\vec{\pi}\rrbracket_{M}},\preceq^{\oplus\llbracket\vec{\pi}\rrbracket_{M}}\rangle,V^{\oplus\llbracket\vec{\pi}\rrbracket_{M}},Ag^{\oplus\llbracket\vec{\pi}\rrbracket_{M}}\rangle,w\models\Box^{\vec{\rho}}\chi$ iff

[TABLE]

iff $M,w\models\Box^{\vec{\pi}\oplus\vec{\rho}}\chi$ 3. 3.

Axiom EA6: $M,w\models[\oplus\vec{\pi}]\forall\chi$ iff $M^{\oplus\vec{\pi}},w\models\forall\chi$ iff $\llbracket\chi\rrbracket_{M^{+\oplus\vec{\pi}}}=W^{+\oplus\vec{\pi}}$ iff $\llbracket[\oplus\vec{\pi}]\chi\rrbracket_{M}=W$ iff $M,w\models\forall[\oplus\vec{\pi}]\chi$.

Claim

$\mathsf{L}_{c}^{\oplus}$ is complete w.r.t. REL models.

Proof

Once we have established the validity of the reduction axioms, the proof is standard and follows the same steps used above to prove completeness for other proof systems with dynamic modalities.