Multi-agent epistemic logic

The group knowledge operators of [FHMV95] over agent-indexed accessibility Rs : E → SetRel W W are boxes along lattice combinations of the agents' relations: agent i knows p at w when □[Rs i] p w, everyone in G knows it when □[⋃ i ∈ G, Rs i] p w, it is distributed knowledge when □[⋂ i ∈ G, Rs i] p w, and the hierarchy C_G ≤ E_G ≤ Kᵢ ≤ D_G is antitonicity in the relation (ModalLogic.box_restrict). Common knowledge is the box along the transitive closure of the union: p holds at every world reachable by a chain of members' accessibility ([Led14] Appendix 2.B's construction), equivalently the infinite conjunction E_G p ∧ E_G (E_G p) ∧ ⋯ (commonKnowledge_iff_forall_iterate). Belief is the same operator over a KD45 frame (ModalLogic.IsKD45Frame).

Main definitions

• ModalLogic.CommonKnowledge: C_G.
• Filter.GroundedIn: a common ground whose context set is exactly what is common knowledge ([Sta02]).

References

• [FHMV95] — group knowledge and its reachability semantics
• [Hal03] — the same operators in the uncertainty setting
• [FH94] — the probabilistic extension, Studies/FaginHalpern1994.lean
• [Hin62] — knowledge as □
• [Sta02] — common ground as common knowledge

def ModalLogic.CommonKnowledge {W : Type u_1} {E : Type u_2} (Rs : E → SetRel W W) (G : Set E) (p : W → Prop) (w : W) : Prop

Common knowledge among G: p holds at every world reachable from w by a chain of members' accessibility.

Equations

• ModalLogic.CommonKnowledge Rs G p w = ModalLogic.Box (SetRel.transGen (⋃ i ∈ G, Rs i)) p w

theorem ModalLogic.box_of_commonKnowledge {W : Type u_1} {E : Type u_2} {Rs : E → SetRel W W} {i : E} {G : Set E} {p : W → Prop} {w : W} (hi : i ∈ G) (h : CommonKnowledge Rs G p w) : Box (Rs i) p w

What is common knowledge is known by every member.

theorem ModalLogic.commonKnowledge_iff_forall_iterate {W : Type u_1} {E : Type u_2} {Rs : E → SetRel W W} {G : Set E} {p : W → Prop} {w : W} : CommonKnowledge Rs G p w ↔ ∀ (n : ℕ), (Box (⋃ i ∈ G, Rs i))^[n + 1] p w

Common knowledge is the infinite conjunction E_G p ∧ E_G (E_G p) ∧ ⋯.

theorem ModalLogic.commonKnowledge_imp {W : Type u_1} {E : Type u_2} {Rs : E → SetRel W W} {i : E} {G : Set E} {p : W → Prop} {w : W} (hi : i ∈ G) [(Rs i).IsRefl] (h : CommonKnowledge Rs G p w) : p w

Common knowledge is veridical once some member's accessibility is reflexive.

def Filter.GroundedIn {W : Type u_1} {E : Type u_2} (cg : Filter W) (Rs : E → SetRel W W) (G : Set E) : Prop

A common ground cg : Filter W is grounded in common knowledge when its context set cg.ker is exactly the set of worlds where each accepted proposition is common knowledge among G ([Sta02]).

Equations

• cg.GroundedIn Rs G = ∀ (w : W), w ∈ cg.ker ↔ ∀ p ∈ cg, ModalLogic.CommonKnowledge Rs G (fun (x : W) => x ∈ p) w

theorem Filter.GroundedIn.commonKnowledge {W : Type u_1} {E : Type u_2} {cg : Filter W} {Rs : E → SetRel W W} {G : Set E} (h : cg.GroundedIn Rs G) {w : W} (hw : w ∈ cg.ker) {p : Set W} (hp : p ∈ cg) : ModalLogic.CommonKnowledge Rs G (fun (x : W) => x ∈ p) w

An accepted proposition of a grounded common ground is common knowledge throughout its context set.