Common knowledge
If some formula φ is knowledge in a group then all agents know φ. But φ is not yet common knowledge. We consider something to be common knowledge only if everyone knows that it is common knowledge.
Intuitively the common knowledge operator □*I φ can be defined as
More formally, the semantics is given by
Where RI* is the reflexive transitive closure of the relation RI.
Assumptions of common knowledge
We can use the first definition of the common knowledge operator as a rule. When we encounter □*I φ we can expand this for one step to obtain φ ∧ □I □*I φ. This gives the following rule:
A problem with using this rule in a proof search is that we are making formulas larger. Usually everything goes well, because the new □I operators are only taken apart when there is a matching nested sequent. But what if the expansion of the common knowledge operator create these sequents?
Consider the formula ¬□I*◇I p. The proof search would go as follows (ignoring used formulas):
This search can go on forever, the same world for ◇I p- is created over and over again. We need a way to detect this loop, and stop the search. Fortunately in systems with rule 4 such as system S5 this situation does not occur, since with that rule a ◇- is never used inside a nested sequent for agent i.
Proving common knowledge
Rules for common knowledge as a goal are more complicated. We could try the same trick as for group knowledge, and have nested worlds [Δ]I* for common knowledge. This might work in some cases, but it will not easily lead to a complete system.
For that we will have to use some kind of induction rule. For example, consider the formula □* p → □*□* p. This formula is obviously true, and the implication in the other direction is simple to proof.
It is not clear yet what rules are needed to proof all possible cases of common knowledge.