## 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 conjunction of [Δ]i for each iI, 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]