## Sets of agents

As a precursor to common knowledge consider knowledge in groups of agents. For example we could write

This notation can be a useful short hand for formulas with many agents.
It will also allow us to write □_{All} or simply □ for knowledge that *all* agents have.
This modal operator is commonly called E in epistemic logic.
The previous case of □_{i} can be considered a subset of group knowledge among a singleton set of agents, □_{{i}}.

Just to be clear, the semantics of group knowledge are simply

Or equivalently

## Adjusting our rules

For our proof system we can extend nested sequents in the same way as boxes.
So we write [Δ]_{I}. This means that the box rule can stay the same:

On the other hand the □^{-} rule becomes considerably more complicated:

The reason for the two sequents above the line is that [Δ]_{I} is a *con*junction of [Δ]_{i} for each i∈I,
and we have no direct way of representing conjunctions in our sequents.
Only for the matching subset of agents can φ^{-} be added to the world's sequent, for the remaining agents nothing changes.

To understand this rule, remember that □_{A ∪ B}φ = □_{A}φ ∧ □_{B}φ and also for nested sequents, [Δ]_{A ∪ B} = [Δ]_{A} ∧ [Δ]_{B}.
So we can write down the following pseudo-derivation for the □^{-}-group rule:

In the case that A or B is ∅ the left or right branch will contain [Γ]_{∅} = True,
so that branch can then be ignored.

## Rules for restricted models

The rules for restricted classes of models such as rule 4 and 5 become considerably more complicated. Rule D and T on the other hand do not change at all, since in these rules the set of agents is not important.

For rules 4 and 5 it may not be possible to do something interesting beyond fully expanding the sequent to a conjunction of worlds for each single agent.

[[CONT: common-knowledge.html|Common knowledge]