Augmenting Subset Spaces to Cope with Multi-agent Knowledge

Abstract

Subsequently, a particular extension of the bi-modal logic of subset spaces, LSS, to the case of several agents will be provided. The basic system, which originally was designed for revealing the intrinsic relationship between knowledge and topology, has been developed in several directions in recent years, not least towards a comprehensive knowledge-theoretic formalism. However, while subset spaces have been shown to be smoothly combinable with various epistemic concepts in the single-agent case, adjusting them to general multi-agent scenarios has brought about rather unsatisfactory results up to now. This is due to reasons inherent in the system so that one is led to consider more special cases. In the present paper, such a widening of LSS to the multi-agent setting is proposed. The peculiarity is here given by the case that the agents are supplied with certain knowledge-enabling functions allowing, in particular, for comparing their respective knowledge. It turns out that such circumstances can be modeled in corresponding logical terms to a considerable extent.

1 Introduction

The starting point for this paper is reasoning about knowledge. This important foundational issue has been given a solid logical basis right from the beginning of the research into theoretical aspects of artificial intelligence, as can be seen, e.g., from the classic textbooks [5, 14]. According to this, a binary accessibility relation $R_A$ connecting possible worlds or conceivable states of the world, is associated with every instance A of a given finite group G of agents. The knowledge of A is then defined through the set of all valid formulas, where validity is understood with regard to every state the agent considers possible at the actual one. This widespread and well-established view of knowledge is complemented by Moss and Parikh’s bi-modal logic of subset spaces, $\mathsf {LSS}$ (see [4, 15], or Ch. 6 of [1]), of which the basic idea is reported in the following.

The epistemic state of an agent in question, i.e., the set of all those states that cannot be distinguished by what the agent topically knows, can be viewed as a neighborhood U of the actual state x of the world. Formulas are now interpreted with respect to the resulting pairs x, U called neighborhood situations. Thus, both the set of all states and the set of all epistemic states constitute the relevant semantic domains as particular subset structures. The two modalities involved, $\mathsf {K}$ and $\square$, quantify over all elements of U and ‘downward’ over all neighborhoods contained in U, respectively. This means that $\mathsf {K}$ captures the notion of knowledge as usual (see [5] again), and $\square$ reflects a kind of effort to acquire knowledge since gaining knowledge goes hand in hand with a shrinkage of the epistemic state. In fact, knowledge acquisition is this way reminiscent of a topological procedure. Thus, it was natural to ask for the appropriate logic of ‘real’ topological spaces, which could be determined by Georgatos shortly afterwards; see [6]. The subsequent research into subset and topological spaces, respectively, is quoted in the handbook [1], whereas more recent developments include, among others, the papers [2, 16].

We focus on the knowledge-theoretic aspect of $\mathsf {LSS}$ as of now. Despite the fact that most treatises on this system deal with the single-agent case, a corresponding multi-agent version was proposed in the paper [9]. The key idea behind that approach is to implement the agents by means of additional modalities. This clearly leads to an essential modification of the logic, while the original semantics basically remains unchanged. On the contrary, if the agent structure shall be reflected in the neighborhood situations, then the scope of the modality $\mathsf {K}$ has to be restricted; see [10] for a detailed discussion on this topic. Anyway, it seems that a trade-off must be made between modifying the semantics and altering the logic in case of multiple agents.

For the scenarios considered in this paper, the additional semantic features will likewise appear on top of the subset space semantics. The variations of the basic logic, however, will be quite moderate. Such scenarios are constituted by, say, n agents whose knowledge need not be available at the actual situation instantaneously, but will be effective only after enabling. The process of enabling is formally described by agent-specific functions operating on neighborhood situations. When viewed ‘from the outside’, these functions quasi act as schedulers for individual reasoning. In the logic, they will be mirrored by additional modalities.¹

It should be possible to model settings like this with the aid of the common logic of knowledge with incorporated time (cf. [5], Sect. 4.3.) as well, since we have just introduced a kind of next step operator (albeit for every agent). But sometimes it is unnecessary or even undesirable to make time explicit. For example, a particular ordering of the agents with regard to knowledge, or the effort spent on closing a knowledge gap between two agents, could be rated as more important than the factual distance of the agents in that sequence or the amount of time that trial costs in order to meet with success. We shall, therefore, define n-agent subset spaces in a way that such kind of qualitative weighting of the agents can be reflected. For the sake of concision, however, just one sample application will actually be handled here, leadership in knowledge. This notion will be made precise below, with some new technical peculiarities coming along.

The rest of the paper is organized as follows. In the next section, we recapitulate the language and the logic of subset spaces for single agents. In Sect. 3, the ideas of both knowledge-enabling functions and leadership in knowledge are formalized. In Sect. 4, the soundness and completeness of the resulting logic is proved. In Sect. 5, the corresponding decidability problem is treated. Finally, we summarize and comment on some naturally arising questions.

All relevant facts from modal logic not explicitly introduced here can be found in the standard textbook [3].

2 The Language and the Logic of Subset Spaces Revisited

The purpose of this section is twofold: to clarify the starting point of our investigation on a technical level and to set up some concepts and results to be introduced and, respectively, proved later on.

First in this section, the language for (single-agent) subset spaces, $\mathcal{L}$, is defined precisely. Then, the semantics of $\mathcal{L}$ is linked with the common relational semantics of modal logic. Finally, the ensuing relationship is utilized after the most important facts on the logic of subset spaces have been recalled.

To begin with, we define the syntax of $\mathcal{L}$. Let $\mathsf {Prop}=\{p,q,\dots \}$ be a denumerably infinite set of symbols called proposition variables (which shall represent the basic facts about the states of the world). Then, the set $\mathsf {SF}$ of all subset formulas over $\mathsf {Prop}$ is defined by the rule

$$\alpha \;::=\; \top \mid p\mid \lnot \alpha \mid \alpha \wedge \alpha \mid \mathsf {K}\alpha \mid \square \alpha .$$

The missing boolean connectives are treated as abbreviations, as needed. The operators which are dual to $\mathsf {K}$ and $\square$ are denoted by $\mathsf {L}$ and $\Diamond$, respectively. In view of our remarks in the previous section, $\mathsf {K}$ is called the knowledge operator and $\Box$ the effort operator.

Second, we fix the semantics of $\mathcal{L}$. For a start, we single out the relevant domains. We let $\mathcal{P}(X)$ designate the powerset of a given set X.

Definition 1

(Semantic Domains).

• 1. Let X be a non-empty set (of states) and $\mathcal{O}\subseteq \mathcal{P}(X)$ a set of subsets of X. Then, the pair $\mathcal{S}=\left( X,\mathcal{O}\right)$ is called a subset frame.

• 2. Let $\mathcal{S}=\left( X,\mathcal{O}\right)$ be a subset frame. The set

  $$\mathcal{N}_\mathcal{S}:=\{(x,U)\mid x\in U \text{ and } U\in \,\mathcal{O}\}$$

  is then called the set of neighborhood situations of $\,\mathcal{S}$.

• 3. Let $\mathcal{S}=\left( X,\mathcal{O}\right)$ be a subset frame. Under an $\mathcal{S}$ -valuation we understand a mapping $V:\mathsf {Prop}\rightarrow \mathcal{P}(X)$.

• 4. Let $\mathcal{S}=\left( X,\mathcal{O}\right)$ be a subset frame and V an $\mathcal{S}$-valuation. Then, $\mathcal{M}:=\left( X,\mathcal{O},V\right)$ is called a subset space (based on $\mathcal{S}$ ).

Note that neighborhood situations denominate the semantic atoms of the bi-modal language $\mathcal{L}$. The first component of such a situation indicates the actual state of the world, while the second reflects the uncertainty of the agent in question about it. Furthermore, Definition 1.3 shows that values of proposition variables depend on states only. This is in accordance with the common practice in epistemic logic; see [5] once more.

For a given subset space $\mathcal{M}$, we now define the relation of satisfaction, $\models _\mathcal{M}\,,$ between neighborhood situations of the underlying frame and formulas from $\mathsf {SF}$. Based on that, we define the notion of validity of formulas in subset spaces. In the following, neighborhood situations are often written without parentheses.

Definition 2

(Satisfaction and Validity). Let $\mathcal{S}=\left( X,\mathcal{O}\right)$ be a subset frame.

• 1. Let $\mathcal{M}=\left( X,\mathcal{O},V\right)$ be a subset space based on $\mathcal{S}$, and let $\,x,U\in \mathcal{N}_\mathcal{S}$ be a neighborhood situation of $\mathcal{S}$. Then

  $$\begin{array}{lll} x,U\models _\mathcal{M}\top &{}&{} \text{ is } \text{ always } \text{ true }\\ x,U\models _\mathcal{M}p &{}:\iff &{} x\in V(p)\\ x,U\models _\mathcal{M}\lnot \alpha &{}:\iff &{} x,U\not \models _\mathcal{M}\alpha \\ x,U\models _\mathcal{M}\alpha \wedge \beta &{}:\iff &{} x,U\models _\mathcal{M}\alpha \text{ and } x,U\models _\mathcal{M}\beta \\ x,U\models _\mathcal{M}\mathsf {K}\alpha &{}:\iff &{} \forall \,y\in U: y,U\models _\mathcal{M}\alpha \\ x,U\models _\mathcal{M}\square \alpha &{}:\iff &{} \forall \, U'\in \mathcal{O}:\left[ x\in U' \subseteq U\Rightarrow x,U'\models _\mathcal{M}\alpha \right] , \end{array}$$

  where $p\in \mathsf {Prop}$ and $\alpha ,\beta \in \mathsf {SF}$. In case $x,U\models _\mathcal{M}\alpha$ is true we say that $\alpha$ holds in $\mathcal{M}$ at the neighborhood situation x, U.

• 2. Let $\mathcal{M}=\left( X,\mathcal{O},V\right)$ be a subset space based on $\mathcal{S}$. A subset formula $\alpha$ is called valid in $\mathcal{M}$ iff it holds in $\mathcal{M}$ at every neighborhood situation of $\,\mathcal{S}$.

Note that the idea of both knowledge and effort, as described in the introduction, is made precise by the first item of this definition. In particular, knowledge is here, too, defined as validity at all states that are indistinguishable to the agent.

Subset frames and subset spaces can be considered from a different perspective, as is known since [4] and reviewed in the following, for the reader’s convenience. Let a subset frame $\mathcal{S}=\left( X,\mathcal{O}\right)$ and a subset space $\mathcal{M}=\left( X,\mathcal{O},V\right)$ based on it be given. Take $X_\mathcal{S}:=\mathcal{N}_\mathcal{S}$ as a set of worlds, and define two accessibility relations $R_\mathcal{S}^\mathsf {K}$ and $R_\mathcal{S}^\square$ on $X_\mathcal{S}$ by

$$\begin{array}{rcl} (x,U)\,R_\mathcal{S}^\mathsf {K}\,(x',U') &{} :\iff &{} U=U' \text{ and }\\ (x,U)\,R_\mathcal{S}^\square \,(x',U') &{} :\iff &{} (x=x' \text{ and } U'\subseteq U), \end{array}$$

for all $(x,U),(x',U')\in X_\mathcal{S}$. Moreover, let a valuation be defined by $V_\mathcal{M}(p):=\{(x,U)\in X_\mathcal{S}\mid x\in V(p)\}$, for all $p\in \mathsf {Prop}$. Then, bi-modal Kripke structures $S_\mathcal{S}:=\left( X_\mathcal{S},\{R_\mathcal{S}^\mathsf {K},R_\mathcal{S}^\square \}\right)$ and $M_\mathcal{M}:=\left( X_\mathcal{S},\{R_\mathcal{S}^\mathsf {K},R_\mathcal{S}^\square \},V_\mathcal{M}\right)$ result in such a way that $M_\mathcal{M}$ is equivalent to $\mathcal{M}$ in the following sense.

Proposition 1

For all $\alpha \in \mathsf {SF}$ and $(x,U)\in X_\mathcal{S}$, we have that $x,U\models _\mathcal{M}\alpha$ iff $M_\mathcal{M},(x,U)\models \alpha$.

Here (and later on as well), the non-indexed symbol ‘$\models$’ denotes the usual satisfaction relation of modal logic.

The proposition can easily be proved by structural induction on $\alpha$. We call $S_\mathcal{S}$ and $M_\mathcal{M}$ the Kripke structures induced by the subset structures $\mathcal{S}$ and $\mathcal{M}$, respectively.

We now turn to the logic of subset spaces, $\mathsf {LSS}$. The subsequent axiomatization from [4] was proved to be sound and complete in Sect. 1.2 and, respectively, Sect. 2.2 there.

• 1. All instances of propositional tautologies

• 2. $\mathsf {K}(\alpha \rightarrow \beta )\rightarrow (\mathsf {K}\alpha \rightarrow \mathsf {K}\beta )$

• 3. $\mathsf {K}\alpha \rightarrow (\alpha \wedge \mathsf {K}\mathsf {K}\alpha )$

• 4. $\mathsf {L}\alpha \rightarrow \mathsf {K}\mathsf {L}\alpha$

• 5. $(p \rightarrow \square p)\wedge (\Diamond p\rightarrow p)$

• 6. $\square \left( \alpha \rightarrow \beta \right) \rightarrow (\square \alpha \rightarrow \square \beta )$

• 7. $\square \alpha \rightarrow (\alpha \wedge \square \square \alpha )$

• 8. $\mathsf {K}\square \alpha \rightarrow \square \mathsf {K}\alpha ,$

where $p\in \mathsf {Prop}$ and $\alpha ,\beta \in \mathsf {SF}$. Note that $\mathsf {LSS}$ comprises the standard modal proof rules (only), i.e., modus ponens and necessitation with respect to each modality.

The last schema is by far the most interesting one, as it displays the interrelation between knowledge and effort. The members of this schema are called the Cross Axioms since [15]. Note that the schema involving only proposition variables is in accordance with the remark on Definition 1.3 above. (In other words, it is expressed by the latter schema that the language $\mathcal{L}$ essentially speaks about the development of knowledge.)

As the next step, let us take a brief look at the effect of the axioms from the above list within the framework of common modal logic. To this end, we consider bi-modal Kripke models $M=\left( W,R,R',V\right)$ satisfying the following four properties:

• the accessibility relation R of M belonging to the knowledge operator $\mathsf {K}$ is an equivalence,

• the accessibility relation $R'$ of M belonging to the effort operator $\square$ is reflexive and transitive,

• the composite relation $R'\circ R$ is contained in $R\circ R'$ (this is usually called the cross property), and

• the valuation V of M is constant along every $R'$-path, for all proposition variables.

Such a model M is called a cross axiom model (and the frame underlying M a cross axiom frame). Now, it can be verified without difficulty that $\mathsf {LSS}$ is sound with respect to the class of all cross axiom models. And it is also easy to see that every induced Kripke model is a cross axiom model (and every induced Kripke frame a cross axiom frame). Thus, the completeness of $\mathsf {LSS}$ for cross axiom models follows from that of $\mathsf {LSS}$ for subset spaces (which is Theorem 2.4 in [4]) by means of Proposition 1. This inferred completeness result can be used for proving the decidability of $\mathsf {LSS}$; see [4], Sect. 2.3. We shall proceed in a similar way below, in Sect. 5.

3 Subset Spaces with Knowledge-Enabling Functions

The formalisms from the previous section will now be extended to the case of n agents, where $n\ge 2$ is a natural number. We again start with the logical language, which comprises n new operators $\mathsf {C}_1,\dots ,\mathsf {C}_n$ as of now. Thus, the set $n\mathsf {SF}$ of all n -subset formulas over $\mathsf {Prop}$ is defined by the rule

$$\alpha \;{:}{:}=\; \top \mid p\mid \lnot \alpha \mid \alpha \wedge \alpha \mid \mathsf {K}\alpha \mid \square \alpha \mid \mathsf {C}_1\alpha \mid \cdots \mid \mathsf {C}_n\alpha .$$

Note that $\mathsf {SF}\subseteq n\mathsf {SF}$. For $i=1,\dots ,n$, the modality $\mathsf {C}_i$ is called the knowledge-enabling operator associated with agent i. The syntactic conventions from Sect. 2 apply correspondingly here. Note that there is no need to consider the dual to $\mathsf {C}_i$ separately since $\mathsf {C}_i$ will turn out to be self-dual.

Concerning semantics, the crucial modifications follow right now. We directly turn to the case that there is a leader in knowledge.

Definition 3

(Augmented n -Agent Subset Structures).

• 1. Let $n\in \mathbb {N}$ be as above, and let $j\in \{1,\dots , n\}$. Furthermore, let $\mathcal{S}=\left( X,\mathcal{O}\right)$ be a subset frame. For all agents $i\in \{1,\dots ,n\}$ and states $x\in X$, let $f_{i,x}:\mathcal{O}\rightarrow \mathcal{O}$ be a partial function satisfying the following two conditions for every $U\in \mathcal{O}$.

  • (a) The value $f_{i,x}(U)$ exists iff $x\in U$, and

  • (b) if $f_{i,x}(U)$ exists, then $x\in f_{i,x}(U)\subseteq U$. (In this case, we also say that $f_{i,x}$ is contracting.)

  Moreover, assume that, for all $i\in \{1,\dots ,n\}$, the set $f_{j,x}(U)$ is contained in $f_{i,x}(U)$ whenever $x\in U$. Then, the quadruple

  $$\mathcal{S}=\left( X,\mathcal{O},\{f_{i,x}\}_{1\le i\le n,x\in X},j\right) $$

  is called an augmented n -agent subset frame (or an aa-subset frame for short), the mappings $f_{i,x}$, where $x\in X$, are called the knowledge-enabling functions for agent i, and j is called a leader in knowledge.

• 2. The notions of neighborhood situation, $\mathcal{S}$ -valuation and augmented- n -agent subset space (aa-subset space) are completely analogous to those introduced in Definition 1.

A detailed comment on this definition seems to be appropriate. For a start, note that the just introduced structures obviously do not correspond to the most general n-agent scenarios, but have already been adjusted to those indicated in the introduction. In fact, not only is an arbitrary agent capable of enabling its knowledge at any situation (according to (a) of the first item of the previous definition), but a particular one (namely j) is also doing better than all the others in this respect (because of the final assumption there). Note that an agent’s enabling is always a kind of improvement since it is given as a shrinkage of a knowledge state (due to (b) above). The enabling functions obviously depend on agents and states of the world.² Furthermore, the ‘distance’ to the leader can be measured by the set inclusion relation as well. This will make it possible for us to express that distance with the aid of the ‘global’ effort operator $\square$, quasi as a missing effort, later on. (Thus, $\square$ may be called the operator closing knowledge gaps.)

With regard to satisfaction and validity, we need not completely present the analogue of Definition 2 at this place, but may confine ourselves to the clause for the new operators.

Definition 4

(Satisfaction). Let $\mathcal{S}=\left( X,\mathcal{O},\{f_{i,x}\}_{1\le i\le n,x\in X},j\right)$ be an aa-subset frame, $\mathcal{M}$ an aa-agent subset space based on $\mathcal{S}$, and $\,x,U\in \mathcal{N}_\mathcal{S}$ a neighborhood situation of $\mathcal{S}$. Then, for every $i\in \{1,\dots ,n\}$ and $\alpha \in n\mathsf {SF}$,

$$\begin{array}{lll} x,U\models _\mathcal{M}\mathsf {C}_i\alpha&:\iff&x,f_{i,x}(U)\models _\mathcal{M}\alpha . \end{array}$$

Since the operator $\mathsf {K}$ can no longer be assigned to a particular agent unambiguously, the knowledge of the agents involved in an aa-scenario must still be defined. We now are in a position to do this, viz through the validity of the $\mathsf {K}$-prefixed formulas at the respective neighborhood situations. The latter are understood as those arising from the associated enabling functions as images. Thus we let, for $i\in \{1,\dots ,n\}$, agent i know $\alpha$ at x, U by definition, iff $x,U\models _\mathcal{M}\mathsf {K}\alpha$ and $U\in \mathrm {Im}(f_{i,x})$; in other words, $\mathsf {K}$ represents factual knowledge after enabling. (This also concerns the knowledge about another agent’s knowledge.)

This fixing clearly requires a justification. To this end, note that the link between the relevant knowledge formulas and the semantic structures is accomplished ‘externally’ here, i.e., by means of an additional condition having no direct counterpart in the object language, namely the requirement that the subset component U of the actual neighborhood situation be contained in the image set of the enabling function for the agent in question. Relating to this, it should be mentioned that all the knowledge of agents we talk about in this paper is an ‘ascribed’ one (cf. [5], p. 8), in fact, by the system designer utilizing epistemic logic as a formal tool for specifying certain multi-agent scenarios. This gives us a kind of freedom regarding the choice of the system properties, which is only limited by the suitability of the approach for the intended applications. These are clearly limited to some extent by the lesser expressiveness of formulas here, but the knowledge development of the involved agents can just as well be described as the leadership in knowledge of a particular agent; see below for some examples.

The final semantic issue to be mentioned is that of induced Kripke structures. Letting $\mathcal{S}=\left( X,\mathcal{O},\{f_{i,x}\}_{1\le i\le n,x\in X},j\right)$ be any aa-subset frame, the following definition suggests itself.

$$\begin{aligned} (x,U)\,R_\mathcal{S}^{\mathsf {C}_i}\,(x',U') :\iff \left( x=x' \text{ and } U'=f_{i,x}(U)\right) , \end{aligned}$$

where $i\in \{1,\dots ,n\}$, $x,x'\in X$, and $U,U'\in \mathcal{O}$. With that, the corresponding analogue of Proposition 1 is obviously valid.

The augmented logic of subset spaces, $\mathsf {ALSS}$, is given by the following list of axioms and the standard proof rules.³

• 1. All instances of propositional tautologies

• 2. $\mathsf {K}(\alpha \rightarrow \beta )\rightarrow (\mathsf {K}\alpha \rightarrow \mathsf {K}\beta )$

• 3. $\mathsf {K}\alpha \rightarrow (\alpha \wedge \mathsf {K}\mathsf {K}\alpha )$

• 4. $\mathsf {L}\alpha \rightarrow \mathsf {K}\mathsf {L}\alpha$

• 5. $(p \rightarrow \square p)\wedge (\Diamond p\rightarrow p)$

• 6. $\square \left( \alpha \rightarrow \beta \right) \rightarrow (\square \alpha \rightarrow \square \beta )$

• 7. $\square \alpha \rightarrow (\alpha \wedge \square \square \alpha )$

• 8. $\mathsf {K}\square \alpha \rightarrow \square \mathsf {K}\alpha$

• 9. $\mathsf {C}_i (\alpha \rightarrow \beta )\rightarrow (\mathsf {C}_i\alpha \rightarrow \mathsf {C}_i\beta )$

• 10. $\mathsf {C}_i\lnot \alpha \leftrightarrow \lnot \mathsf {C}_i\alpha$

• 11. $\mathsf {K}\mathsf {C}_i \alpha \rightarrow \mathsf {C}_i \mathsf {K}\alpha$

• 12. $\square \alpha \rightarrow \mathsf {C}_i \alpha$

• 13. $\mathsf {C}_i\square \alpha \rightarrow \mathsf {C}_j\alpha$,

where j is the preassigned leader, $i\in \{1,\dots ,n\}$, $p\in \mathsf {Prop}$, and $\alpha ,\beta \in n\mathsf {SF}$.

Obviously, the first eight schemata of this list coincide with the $\mathsf {LSS}$-axioms presented in Sect. 2. Thus we only comment on the others here, which are exactly those involving $\mathsf {C}_i$ for $i\in \{1,\dots ,n\}$. Axiom 9 is the usual distribution schema of modal logic, this time formulated for $\mathsf {C}_i$. The next axiom captures the functionality of the accessibility relation associated with $\mathsf {C}_i$; see, e.g., [7], Sect. 9 (for the operator next). In the present context, it comes along with the fact that we have assigned knowledge-enabling functions to the agents. The schema 11 is formally similar to the eighth one, thus comprising the Cross Axioms for $\mathsf {K}$ and $\mathsf {C}_i$. The last but one schema mirrors the fact that the enabling functions, when defined, are contracting. With regard to the relational semantics, it says that the accessibility relation for $\mathsf {C}_i$ is contained in that for $\square$. This schema, together with Axiom 10, is as well responsible for the fact that the counterpart of Axiom 5 is not needed for $\mathsf {C}_i$. The most interesting new schema is the last one. In case all the involved modalities were equal, we would have the axioms capturing the weak density of the corresponding accessibility relation; see [7], Sect. 1. However, regarding augmented n-agent scenarios, the leadership of agent j in knowledge is thereby expressed.

As to an example of a schema of derived $\mathsf {ALSS}$-sentences, let us recall the reliably known formulas $\alpha \in \mathsf {SF}$ from [4], which satisfy $\mathsf {K}\alpha \rightarrow \square \mathsf {K}\alpha \in \mathsf {LSS}$ by definition. We now define accessibly known formulas $\alpha \in n\mathsf {SF}$ by analogy with that through the condition that $\mathsf {K}\alpha \rightarrow \mathsf {C}_i\mathsf {K}\alpha$ be in $\mathsf {ALSS}$. Then, for every $\alpha \in n\mathsf {SF}$, the formula $\square \alpha$ is of this type, as expected. In fact, $\mathsf {K}\square \square \alpha$ can be deduced from $\mathsf {K}\square \alpha$ because of Axiom 7, from which we obtain $\square \mathsf {K}\square \alpha$ with the aid of Axiom 8. Now, Axiom 12 implies $\mathsf {C}_i\mathsf {K}\square \alpha$.

Finally in this section, it is proved that the logic $\mathsf {ALSS}$ is sound with respect to the class of all aa-subset spaces.

Proposition 2

Let $\mathcal{M}=\left( X,\mathcal{O},\{f_{i,x}\}_{1\le i\le n,x\in X},j,V\right)$ be an aa-subset space. Then, every axiom from the above list is valid in $\mathcal{M}$ and every rule preserves validity.

Proof

We confine ourselves to the last schema of the axioms. Let $\mathsf {C}_i \square \alpha \rightarrow \mathsf {C}_j\alpha$ be an instance of this, and let $x,U\models _\mathcal{M}\mathsf {C}_i\square \alpha$ be satisfied for any neighbourhood situation of the frame underlying $\mathcal{M}$. According to Definition 4, this means that $x,f_{i,x}(U)\models _\mathcal{M}\square \alpha$. Thus, $x,f_{i,x}(U)\models _\mathcal{M}\alpha$ for all $U'\in \mathcal{O}$ such that $x\in U'\subseteq f_{i,x}(U)$. It follows that $x,f_{j,x}(U)\models _\mathcal{M}\alpha$ holds in particular, because of the leader-in-knowledge condition from Definition 3.1. Consequently, $x,U\models _\mathcal{M}\mathsf {C}_j\alpha$. This proves (the particular case of) the proposition.

Regarding the relational semantics, it will be seen that a certain property of lying in between corresponds to the schema treated in the preceding proof, as it is the case with the related axioms for weak density. We, therefore, call that schema ad hoc the lying-in-between axioms. These will crucially be utilized in the next section.

4 Completeness

In this section, we present the peculiarities required for proving the semantic completeness of $\mathsf {ALSS}$ on the class of all aa-subset spaces. As it is mostly the case with subset space logics, the overall structure of such a proof consists of an infinite step-by-step model construction.⁴ Using such a procedure seems to be necessary, since subset spaces in a sense do not harmonize with the main modal means supporting completeness, viz canonical models.

The canonical model of $\mathsf {ALSS}$ will come into play nevertheless. So let us fix some notations concerning that model first. Let $\mathcal{C}$ be the set of all maximal $\mathsf {ALSS}$-consistent sets of formulas. Furthermore, let , , and be the accessibility relations induced on $\mathcal{C}$ by the modalities $\mathsf {K}$, $\square$, and $\mathsf {C}_i$, respectively, where $i\in \{1,\dots ,n\}$. And finally, let $\alpha \in n\mathsf {SF}$ be a formula which is not contained in $\mathsf {ALSS}$. Then, we have to find a model for $\lnot \alpha$.

This model is constructed stepwise and incrementally in such a way that better and better intermediary structures are obtained (which means that more and more existential formulas are realized). In order to ensure that the finally resulting limit structure behaves as desired, several requirements on those approximations have to be met at every stage. This makes up the technical core of the proof, of which the specific features are described reasonably accurately in a minute.

First, however, we need a lemma.

Lemma 1

Let $n,j\in \mathbb {N}$ be fixed as in the previous section. Suppose that $s,t\in \mathcal{C}$ are maximal $\mathsf {ALSS}$-consistent sets of formulas satisfying . Then, for all $i\in \{1,\dots ,n\}$, there is some $u\in \mathcal{C}$ such that .

Proof

One has to apply the lying-in-between axioms and can argue in a similar way as in the case of weak density in doing so; cf. [7], p. 26.⁵

We now describe the main ingredients of the above mentioned approximation structures. Their possible worlds are successively taken from a denumerably infinite set of points, Y, chosen in advance. Also, another denumerably infinite set, Q, is chosen such that $Y\cap Q=\emptyset$. The latter set shall gradually contribute to a partially ordered set representing the subset space structure of the desired limit model. Finally, we fix particular ‘starting elements’ $x_0\in Y$, $\bot \in Q$, and $\varGamma \in \mathcal{C}$ containing the formula $\lnot \alpha$ from above. Then, a sequence of quintuples $\left( X_m,P_m,j_m,\{g_{i}^m\}_{1\le i\le n},t_m\right)$ has to be defined inductively such that, for all $m\in \mathbb {N}$ and $i\in \{1,\dots ,n\}$,

• $X_m$ is a finite subset of Y containing $x_0$,

• $P_m$ is a finite subset of Q containing $\bot$ and carrying a partial order $\le _m$ with least element $\bot$,

• $j_m:P_m\rightarrow \mathcal{P}\left( X_m\right)$ is a function satisfying $\left( \pi \le _m\rho \iff j_m(\pi )\supseteq j_m(\rho )\right)$, for all $\pi ,\rho \in P_m$,

• $g_{i}^m:X_m\times P_m\rightarrow P_m$ is a partial function such that, for all $x\in X_m$ and $\pi \in P_m$,

  • if $g^m_{i}(x,\pi ) \text{ exists, } \text{ then } \left( x\in j_m\left( g^m_{i}(x,\pi )\right) \text{ and } \pi \le _mg^m_i(x,\pi )\right)$

  • if $g^m_{i}(x,\pi )$ and $g^m_{j}(x,\pi )$ exist, then $g^m_{i}(x,\pi )\le _m g^m_{j}(x,\pi )$,

• $t_m:X_m\times P_m\rightarrow \mathcal{C}$ is a partial function such that, for all $x,y\in X_m$ and $\pi ,\rho \in P_m$,

  • $t_m(x,\pi )$ is defined iff $x\in j_m(\pi )$; in this case it holds that

    • $*$ if $y\in j_m(\pi ),$ then

    • $*$ if $\pi \le _m \rho$, then

    • $*$ if $g^m_i(x,\pi )=\rho$, then

  • $t_m (x_0,\bot ) = \varGamma$.

It is now clear how to define the approximating partial functions $f^m_{i,x}:\mathrm {Im}(j_m)\rightarrow \mathrm {Im}(j_m)$. For all $x\in X_m$ and $\pi ,\rho \in P_m$, we let $f^m_{i,x}\left( j_m(\pi )\right) :=j_m(\rho )$ iff $g^m_{i}(x,\pi )=\rho$. Then, $f^m_{i,x}$ is contracting and satisfies, for every $\pi \in P_m$,

• $f^m_{i,x}\left( j_m(\pi )\right) \text{ exists } \text{ iff } g^m_i(x,\pi ) \text{ exists }$,

• $f^m_{j,x}\left( j_m(\pi )\right)$ is contained in $f^m_{i,x}\left( j_m(\pi )\right)$ in case both sets exist.

The next five conditions reveal to what extent the final model is approximated by the structures $\left( X_m,P_m,j_m,\{g_{i}^m\}_{1\le i\le n},t_m\right)$. Actually, it will be ensured that, for all $m\in \mathbb {N}$ and $i\in \{1,\dots ,n\}$,

• $X_m \subseteq X_{m+1}$,

• $P_{m+1}$ is an almost end extension of $P_{m}$, i.e., a superstructure of $P_{m}$ such that, if an element $\pi \in P_{m+1}\setminus P_m$ is strictly smaller than some element of $P_m$, then there are uniquely determined $\rho ,\sigma \in P_m$, $x\in X_m$, and $i\in \{1,\dots ,n\}$ satisfying $\rho \le _{m}\sigma$, $\sigma =g_j^{m}(x,\rho )$, $\pi \le _{m+1}\sigma$, and $\pi =g_i^{m+1}(x,\rho )$ (this means, in particular, that $g_j^{m}(x,\rho )$ and $g_i^{m+1}(x,\rho )$ are defined),

• $j_{m+1}(\pi )\cap X_m=j_m(\pi )$ for all $\pi \in P_m$,

• $g_i^{m+1}\mid _{X_m\times P_m}= g_i^m$,

• $t_{m+1}\mid _{X_m\times P_m}= t_m$.

Note that end extensions are usually dealt with at this point. In the present case, however, the new elements must suitably be edged in. This requires a different approach.

Finally, the construction complies with the following requirements on existential formulas: for all $m\in \mathbb {N}$, $x\in X_m$, $\pi \in P_m$, $\nabla \in \{\Diamond ,\mathsf {C}_1,\dots ,\mathsf {C}_n\}$, and $\beta \in n\mathsf {SF}$,

• if $\mathsf {L}\beta \in t_m(x,\pi ),$ then there are $m<k\in \mathbb {N}$ and $y\in j_k(\pi )$ such that $\beta \in t_k(y,\pi )$,

• if $\nabla \beta \in t_m(x,\pi ),$ then there are $m<k\in \mathbb {N}$ and $\pi \le _k\rho \in P_k$ such that $\beta \in t_k(x,\rho )$.

With that, the final model refuting $\alpha$ can be defined easily. Furthermore, a relevant Truth Lemma (cf. [3], 4.21) can be proved for it, from which the completeness of $\mathsf {ALSS}$ with respect to the augmented n-agent semantics follows immediately. Thus, it remains to specify, for all $m\in \mathbb {N}$, the approximating structures $\left( X_m,P_m,j_m,\{g_{i}^m\}_{1\le i\le n},t_m\right)$ in a way that all the above requirements are met.

Since the case $m=0$ is quite obvious, we only focus on the induction step. Here, some existential formula $\gamma$ contained in some maximal $\mathsf {ALSS}$-consistent set $t_m(x,\pi )$, where $x\in X_m$ and $\pi \in P_m$, must be made true according to the last group of the above requirements. We confine ourselves to the case of the enabling operator associated with agent i, where $i\in \{1,\dots ,n\}$. So let $\gamma =\mathsf {C}_i\beta \in t_m (x,\pi )$ be satisfied. Then, we distinguish two cases, each one of which having two subcases. First, let $i=j$. If $g_j^m(x,\pi )$ is undefined, then this case is less interesting because the same proceeding as in the $\Diamond$-case leads to success; cf. [4]. Note however that here is the place where the status of definiteness of the function $g_j$ is changed, namely for the argument $(x,\pi )$. On the other hand, if $g_j^m(x,\pi )$ is defined, then nothing has to be changed and everything goes well because of the functionality of $\mathsf {C}_j$. Now, let $i\not =j$. Then, we may assume that $\rho =g_j^m(x,\pi )$ has already been defined; see the remark right before Theorem 1 below. The case that $g_i^m(x,\pi )$ as well has been defined in advance is easy, too. Thus suppose that $g_i^m(x,\pi )$ is undefined. In this case, we choose both a new point $y\in Y$ and a fresh $\sigma \in Q$, and we let $X_{m+1}:=X_m\cup \{y\}$ and $P_{m+1}:=P_m\cup \{\sigma \}$. The partial order is extended to $P_{m+1}$ by letting $\pi \le _{m+1}\sigma \le _{m+1}\rho$ and $\sigma$ be not comparable with any other element not less than $\pi$. The function $j_{m+1}$ is defined as follows. We let $j_{m+1}(\tau ):=j_m(\tau )\cup \{y\}$ for all $\tau \le _m\pi$ and $j_{m+1}(\sigma ):= j_m(\rho )\cup \{y\}$; for all other arguments, $j_{m}$ remains unchanged. Furthermore, the extension of the function $g_i^m$ is defined by $g_i^{m+1}(x,\pi ):=\sigma$. Finally, the mapping $t_m$ has to be adjusted. From the Existence Lemma of modal logic (see [3], 4.20) we know that there is some point $\varGamma _i$ of $\mathcal{C}$ such that and $\beta \in \varGamma _i$. Thus, we define the new part of $t_{m+1}$ by $t_{m+1}(x,\sigma )=t_{m+1}(y,\sigma ):=\varGamma _i$, and $t_{m+1}(y,\tau ):=t_{m}(x,\tau )$ for all $\tau \le _m\pi$; moreover, the maximal consistent set which is to be assigned to a pair $(z,\sigma )$ where $x\not =z\in j_m(\rho )$, is obtained in the following way. We know from the induction hypothesis that is valid. From Lemma 1 we therefore obtain the existence of a maximal $\mathsf {ALSS}$-consistent set $\varDelta$ satisfying . Now we let $t_{m+1}(z,\sigma ):=\varDelta$. This completes the definition of $t_{m+1}$ and thus that of $\left( X_{m+1},P_{m+1},j_{m+1},\{g_{i}^{m+1}\}_{1\le i\le n},t_{m+1}\right)$ in the case under consideration.

We must now check that the properties stated in the second group of requirements are satisfied and that the validity of those stated in the first group is transferred from m to $m+1$. Doing so, several items prove to be evident from the construction. In some cases, however, the particularities of the accessibility relations on $\mathcal{C}$ like the two cross properties have to be applied. Further details regarding this must be omitted here.

As to the realization of existential formulas, it has to be ensured that all possible cases are eventually exhausted. To this end, processing must suitably be scheduled with regard to each of the involved modalities. This can be done with the aid of appropriate enumerations. Concerning details relating to this, the reader is referred to [4] again, but not before we have mentioned that one should keep in mind to rearrange, if need be, those enumerations in such a way that some $C_j$-formula is treated before any $C_i$-formula at all times, i.e., for any pair $(x,\pi )$ (which is clearly possible). All this finally yields the subsequent theorem.

Theorem 1

(Completeness). Let $\alpha \in n\mathsf {SF}$ be a formula which is valid in all aa-subset spaces. Then $\alpha$ belongs to the logic $\mathsf {ALSS}$.

Concluding this section, we would like to stress that the functionality of the knowledge-enabling operators is a decisive prerequisite for the success of the above model construction.

5 Decidability

The standard method for proving the decidability of a given modal logic is filtration. By that method, inspection of the relevant models is restricted to those not exceeding a specified size, in this way making a decision procedure possible. However, just as subset spaces do not harmonize with canonical models, they are incompatible with filtration. A detour is therefore required, which takes us back into the relational semantics. In the following, we shall single out a class of multi-modal Kripke structures for which $\mathsf {ALSS}$ is as well sound and complete, and which is closed under filtration in a suitable manner. This will give us the desired decidability result. Subsequently, ${\mathsf {K}}$ is supposed to correspond to R, $\square$ to $R'$, and $\mathsf {C}_i$ to $S_i$ for $i=1,\dots ,n$. Furthermore, let $j\in \{1,\dots ,n\}$ be given in advance.

Definition 5

(AA-Model). Let ${M}:=\left( W,R,R',S_1,\dots ,S_n,V\right)$ be a multi-modal Kripke model, where $R,R',S_1,\dots ,S_n\subseteq W\times W$ are binary relations and V is a valuation. Then M is called an aa-model (with j the leader in knowledge), iff the following conditions are satisfied.

• 1. R is an equivalence relation,

• 2. $R'$ is reflexive and transitive,

• 3. $S_i$ is a functional relation contained in $R'$, for every $i\in \{1,\dots ,n\}$,

• 4. each of the pairs $\left( R,R'\right)$, $\left( R,S_1\right)$, ..., $\left( R,S_n\right)$ satisfies the cross property,

• 5. $S_j\subseteq S_i\circ R'$ for every $i\in \{1,\dots ,n\}$, and

• 6. for all proposition variables, the valuation V of M is constant along every $R'$-path.

Note that the fifth item of the previous definition represents the relational version of the lying-in-between property.

The class of all Kripke models induced by an aa-subset space (see Sect. 2 and, respectively, Sect. 3 for this notion) is contained in the class of all aa-models, as can be seen easily. It follows that $\mathsf {ALSS}$ is (sound and) complete with respect to the latter class; see the remark at the end of Sect. 2. It suffices therefore, in order to prove the decidability of $\mathsf {ALSS}$, to show that the class of all aa-models is closed under filtration.

To this end, let an $\mathsf {ALSS}$-consistent formula $\alpha \in n\mathsf {SF}$ be given. Then, a filter set of formulas, involving the set $\mathrm {sf}(\alpha )$ of all subformulas of $\alpha$, is defined as follows. We start off with $\varSigma _0:= \mathrm {sf}(\alpha )\cup \{\lnot \beta \mid \beta \in \mathrm {sf}(\alpha )\}$. In the next step, we take the closure of $\varSigma _0$ under finite conjunctions of pairwise distinct elements of $\varSigma _0$. After that, we close under single applications of the operator $\mathsf {L}$. And finally, we join the sets of subformulas of all the elements of the set obtained last. (This final step is necessary because $\mathsf {L}$ was introduced as an abbreviation.) The resulting set of formulas, denoted by $\varSigma$, is quite similar to the one used for $\mathsf {LSS}$ in [4] and will meet the case-specific requirements here. Note that $\varSigma$ is a finite set.

Now, the canonical model of $\mathsf {ALSS}$ is filtered through $\varSigma$. As a filtration of the corresponding accessibility relations, we take the smallest one in each of the $n+2$ cases. Let ${M}=\left( W,R,R',S_1,\dots ,S_n,V\right)$ be the resulting model, where the valuation V shall be in accordance with Definition 5.6 for the proposition variables outside of $\varSigma$. Then, the following lemma is crucial.

Lemma 2

The structure M is a finite aa-model. Furthermore, the size of M can be computed from the length of $\alpha$.

Proof

The finiteness of W follows from that of $\varSigma$, and we must now show that the six conditions from Definition  5 are satisfied. Due to space limitations, we must be rather brief in doing so. Taking into account the way the filter set $\varSigma$ was formed, the verification of 1 and 4 is lengthy, but not very difficult. The reflexivity of $R'$ can easily be concluded from the mere fact that M is the result of a filtration. Moreover, establishing the transitivity of $R'$ is covered by the proof of Lemma 2.10 from [4]. Both the inclusions $S_i\subseteq R'$, where $i\in \{1,\dots ,n\}$, and the validity of 6 for the proposition variables occurring in $\varSigma$ arise from the circumstance that we have chosen the smallest filtration in each case. The same is true of the functionality of the relations $S_i$, but this is not completely obvious. In fact, the (suitably adapted) Fun-Lemma 9.9 from [7] must be applied for it, ensuring that every $S_i$-successor of an arbitrary point of W is of equal value in regard to the validity of the formulas from $\varSigma$ so that any of them can be selected. (It will become clear in a minute which one will actually be the right one.) Thus the verification of the fifth condition only still requires an argument. Fortunately, the characteristic features of a smallest filtration again help so that we are done after mentioning the following. For any starting point $w\in W$, the relational lying-in-between property can be realized with the aid of an arbitrarily chosen $S_j$-successor of w, with thereby determining the appropriate $S_i$-successor of that point through the correspondingly utilized lying-in-between relation on the canonical model; as to the validity of the latter, see Lemma 1. In this manner, the lemma is proved.

The desired decidability result is now an immediate consequence of Lemma 2 and the facts stated at the beginning of this section.

Theorem 2

(Decidability). The logic $\mathsf {ALSS}$ is a decidable set of formulas.

This is what we can say about the effectiveness properties of the logic $\mathsf {ALSS}$ for the moment.

6 Conclusion

First in this section, the results obtained in this paper are summarized. Then, we comment on some further points, including possible extensions of our approach.

A special subset space logic of n agents, denoted by $\mathsf {ALSS}$, has been introduced above. This system has been designed to cover leadership in knowledge, in particular. We proposed a corresponding axiomatization, which turned out to be sound and complete with respect to the intended class of models. This constitutes the first of our main results. The second assures the decidability of the new logic.

It is to be expected that the complexity of $\mathsf {ALSS}$ can be determined not until solving this problem for the usual logic of subset spaces. As to that, only partial results are known; see [2, 12].

The main reason for the (relative) progress in multi-agent subset spaces achieved in this paper is the relaxation of the underlying idea of knowledge. Accordingly, the agents come in rather indirectly, viz in terms of their enabling functions. To say it somewhat exaggeratedly, the absence of agent-specific knowledge operators even makes a multi-agent usage of subset spaces possible, at least for particular epistemic scenarios. Following that idea, a promising new field of research opens up, in which the issue of other interesting agent interrelationships and their effects on knowledge (not to forget the correspondingly adapted idea of common knowledge) could be tackled. Relating to this, both [13] (on the knowledge-theoretic side) and [9] (on multi-subset spaces) may serve as a starting point. (Contrasting the present approach which is new, the recent paper [11] is based on the latter article to some extent.)