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 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]