Multi-Agent Epistemic Logic

@cite{halpern-2003} @cite{fagin-halpern-1994}

Multi-agent epistemic operators from @cite{halpern-2003}: individual knowledge (Kᵢ), everyone knows (E_G), common knowledge (C_G), distributed knowledge (D_G), and their doxastic (KD45 belief) counterparts.

Connects to Stalnaker's common ground via CG.groundedIn: a common ground is grounded when its context set equals what is commonly known.

Operators

Operator	Symbol	Definition
Individual knowledge	Kᵢ(φ)	φ at all i-accessible worlds
Everyone knows	E_G(φ)	∧ᵢ∈G Kᵢ(φ)
Common knowledge	C_G(φ)	φ ∧ E(φ) ∧ E(E(φ)) ∧...
Distributed knowledge	D_G(φ)	φ at all (∩ᵢ Rᵢ)-accessible worlds

Architecture

This file lives in Theories/Semantics/Modality/ because it makes substantive theoretical commitments (S5 for knowledge, KD45 for belief, fixed-point characterization of common knowledge). The framework-agnostic context management (ContextSet, CG) lives in Core/Semantics/CommonGround.lean.

Following mathlib style, all operators are Prop-valued; computation on finite worlds goes through Decidable instances + decide.

Individual Knowledge

Agent i knows φ at world w iff φ holds at all worlds accessible to i. This re-uses boxR from RestrictedModality.lean with agent-indexed accessibility relations.

def Semantics.Modality.EpistemicLogic.knows {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (i : E) (φ : W → Prop) (w : W) : Prop

Agent i knows φ at world w: Kᵢ(φ)(w) = □ᵢ φ(w).

Equations

• Semantics.Modality.EpistemicLogic.knows Rs i φ w = Core.Logic.Intensional.boxR (Rs i) φ w

Everyone Knows

E_G(φ) holds at w iff every agent in group G knows φ at w. E_G(φ) = ∧ᵢ∈G Kᵢ(φ).

def Semantics.Modality.EpistemicLogic.everyoneKnows {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (group : List E) (φ : W → Prop) (w : W) : Prop

Everyone in group G knows φ at w.

Equations

• Semantics.Modality.EpistemicLogic.everyoneKnows Rs group φ w = ∀ i ∈ group, Semantics.Modality.EpistemicLogic.knows Rs i φ w

theorem Semantics.Modality.EpistemicLogic.everyoneKnows_implies_knows {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (group : List E) (φ : W → Prop) (w : W) (i : E) (hi : i ∈ group) (h : everyoneKnows Rs group φ w) : knows Rs i φ w

Everyone knows implies each individual knows.

Common Knowledge

C_G(φ) is the greatest fixed point of X = φ ∧ E_G(X). Equivalently, C_G(φ) = φ ∧ E_G(φ) ∧ E_G(E_G(φ)) ∧... (infinite conjunction).

For computation on finite worlds, we iterate E_G up to a bound. Since there are finitely many truth assignments, the iteration reaches a fixed point within a finite number of steps.

def Semantics.Modality.EpistemicLogic.everyoneKnowsIter {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (group : List E) (φ : W → Prop) : ℕ → W → Prop

Iterate "everyone knows" n times: E^n_G(φ).

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Modality.EpistemicLogic.everyoneKnowsIter Rs group φ Nat.zero = φ

def Semantics.Modality.EpistemicLogic.commonKnowledge {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (group : List E) (φ : W → Prop) (bound : ℕ) (w : W) : Prop

Common knowledge as a finite approximation: C_G(φ)(w) iff E^n_G(φ)(w) for all n up to the iteration bound.

For finite W with |W| = k, the fixed point is reached within 2^k iterations (since each iteration can only shrink the set of satisfying worlds).

Equations

• Semantics.Modality.EpistemicLogic.commonKnowledge Rs group φ bound w = ∀ n ≤ bound, Semantics.Modality.EpistemicLogic.everyoneKnowsIter Rs group φ n w

theorem Semantics.Modality.EpistemicLogic.commonKnowledge_implies_everyoneKnows {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (group : List E) (φ : W → Prop) (bound : ℕ) (w : W) (hbound : 1 ≤ bound) (h : commonKnowledge Rs group φ bound w) : everyoneKnows Rs group φ w

Common knowledge implies everyone knows (at depth 1).

theorem Semantics.Modality.EpistemicLogic.commonKnowledge_implies_prop {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (group : List E) (φ : W → Prop) (bound : ℕ) (w : W) (h : commonKnowledge Rs group φ bound w) : φ w

Common knowledge implies the proposition itself (depth 0).

Distributed Knowledge

D_G(φ) holds at w iff φ holds at all worlds accessible to EVERY agent in G simultaneously. The accessibility relation is the intersection: R_D = ∩ᵢ∈G Rᵢ.

Distributed knowledge is what the group WOULD know if they pooled all their information. It is stronger than individual knowledge but weaker than common knowledge in the opposite direction: D_G(φ) → Kᵢ(φ) for each i, but C_G(φ) → E_G(φ) → Kᵢ(φ).

def Semantics.Modality.EpistemicLogic.groupAccessRel {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (group : List E) : Core.Logic.Intensional.AccessRel W

Intersection of accessibility relations for a group.

Equations

• Semantics.Modality.EpistemicLogic.groupAccessRel Rs group w v = ∀ i ∈ group, Rs i w v

def Semantics.Modality.EpistemicLogic.distributedKnowledge {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (group : List E) (φ : W → Prop) (w : W) : Prop

Distributed knowledge: D_G(φ)(w) = □_{∩R} φ(w).

Equations

• Semantics.Modality.EpistemicLogic.distributedKnowledge Rs group φ w = Core.Logic.Intensional.boxR (Semantics.Modality.EpistemicLogic.groupAccessRel Rs group) φ w

theorem Semantics.Modality.EpistemicLogic.knows_implies_distributedKnowledge {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (group : List E) (φ : W → Prop) (w : W) (i : E) (hi : i ∈ group) (h : knows Rs i φ w) : distributedKnowledge Rs group φ w

Individual knowledge implies distributed knowledge: the intersection of accessibility relations is a subset of each component, so every group-accessible world is also i-accessible. Therefore if φ holds at all i-accessible worlds, it holds at all group-accessible worlds.

KD45 Belief Operators

Parallel to the S5 knowledge operators above, but with KD45 accessibility (serial + transitive + Euclidean, not reflexive).

Knowledge (S5) is veridical: Kφ → φ. Belief (KD45) is not: an agent can believe φ without φ being true. But belief is consistent (Bφ → ◇φ, from seriality), positively introspective (Bφ → BBφ, from transitivity), and negatively introspective (¬Bφ → B¬Bφ, from Euclideanness).

The connection Kφ → Bφ requires R_B ⊆ R_K: every belief-accessible world is knowledge-accessible. Since S5 frames are reflexive (more accessible worlds), knowledge is harder to achieve than belief.

def Semantics.Modality.EpistemicLogic.believes {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (i : E) (φ : W → Prop) (w : W) : Prop

Agent i believes φ at world w: Bᵢ(φ)(w) = □ᵢ φ(w). Same evaluation as knows, but the accessibility relation satisfies KD45 (serial + transitive + Euclidean) rather than S5 (reflexive + Euclidean).

Equations

• Semantics.Modality.EpistemicLogic.believes Rs i φ w = Core.Logic.Intensional.boxR (Rs i) φ w

def Semantics.Modality.EpistemicLogic.everyoneBelieves {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (group : List E) (φ : W → Prop) (w : W) : Prop

Everyone in group G believes φ at w.

Equations

• Semantics.Modality.EpistemicLogic.everyoneBelieves Rs group φ w = ∀ i ∈ group, Semantics.Modality.EpistemicLogic.believes Rs i φ w

def Semantics.Modality.EpistemicLogic.everyoneBeliefIter {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (group : List E) (φ : W → Prop) : ℕ → W → Prop

Iterate "everyone believes" n times: EB^n_G(φ).

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Modality.EpistemicLogic.everyoneBeliefIter Rs group φ Nat.zero = φ

def Semantics.Modality.EpistemicLogic.commonBelief {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (group : List E) (φ : W → Prop) (bound : ℕ) (w : W) : Prop

Common belief: CB_G(φ)(w) iff EB^n_G(φ)(w) for all n up to bound.

Equations

• Semantics.Modality.EpistemicLogic.commonBelief Rs group φ bound w = ∀ n ≤ bound, Semantics.Modality.EpistemicLogic.everyoneBeliefIter Rs group φ n w

def Semantics.Modality.EpistemicLogic.distributedBelief {W : Type u_1} {E : Type u_2} (Rs : Core.Logic.Intensional.AgentAccessRel W E) (group : List E) (φ : W → Prop) (w : W) : Prop

Distributed belief: DB_G(φ)(w) = □_{∩R_B} φ(w).

Equations

• Semantics.Modality.EpistemicLogic.distributedBelief Rs group φ w = Core.Logic.Intensional.boxR (Semantics.Modality.EpistemicLogic.groupAccessRel Rs group) φ w

structure Semantics.Modality.EpistemicLogic.KnowledgeBeliefFrame (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A knowledge-belief frame bundles S5 knowledge relations and KD45 belief relations for each agent, with the constraint that belief accessibility is a subset of knowledge accessibility.

R_B(i) ⊆ R_K(i) ensures Kφ → Bφ: if φ holds at all knowledge-accessible worlds (a superset), it holds at all belief-accessible worlds.

• knowsRel : Core.Logic.Intensional.AgentAccessRel W E

  Knowledge accessibility relations (should satisfy S5: reflexive + Euclidean)

• believesRel : Core.Logic.Intensional.AgentAccessRel W E

  Belief accessibility relations (should satisfy KD45: serial + transitive + Euclidean)

• believes_sub_knows (i : E) (w v : W) : self.believesRel i w v → self.knowsRel i w v

  Belief accessibility implies knowledge accessibility

theorem Semantics.Modality.EpistemicLogic.knows_implies_believes {W : Type u_1} {E : Type u_2} (frame : KnowledgeBeliefFrame W E) (i : E) (φ : W → Prop) (w : W) (h : knows frame.knowsRel i φ w) : believes frame.believesRel i φ w

Knowledge implies belief: Kᵢ(φ) → Bᵢ(φ).

Since every belief-accessible world is knowledge-accessible (R_B ⊆ R_K), if φ holds at all knowledge-accessible worlds then it holds at all belief-accessible worlds.

theorem Semantics.Modality.EpistemicLogic.believes_consistent {W : Type u_1} {E : Type u_2} {Rs : Core.Logic.Intensional.AgentAccessRel W E} (i : E) (hSerial : Core.Logic.Intensional.IsSerial (Rs i)) (φ : W → Prop) (w : W) (h : believes Rs i φ w) : Core.Logic.Intensional.diamondR (Rs i) φ w

Belief is consistent: Bᵢ(φ) → ◇ᵢφ (the D axiom). Follows from seriality of the belief accessibility relation.

theorem Semantics.Modality.EpistemicLogic.believes_positive_introspection {W : Type u_1} {E : Type u_2} {Rs : Core.Logic.Intensional.AgentAccessRel W E} (i : E) (hTrans : Core.Logic.Intensional.IsTransitive (Rs i)) (φ : W → Prop) (w : W) (h : believes Rs i φ w) : believes Rs i (believes Rs i φ) w

Positive introspection: Bᵢ(φ) → Bᵢ(Bᵢ(φ)) (the 4 axiom). Follows from transitivity of the belief accessibility relation.

theorem Semantics.Modality.EpistemicLogic.believes_negative_introspection {W : Type u_1} {E : Type u_2} {Rs : Core.Logic.Intensional.AgentAccessRel W E} (i : E) (hEucl : Core.Logic.Intensional.IsEuclidean (Rs i)) (φ : W → Prop) (w : W) (h : Core.Logic.Intensional.diamondR (Rs i) φ w) : Core.Logic.Intensional.boxR (Rs i) (Core.Logic.Intensional.diamondR (Rs i) φ) w

Negative introspection: ◇Bφ → □◇Bφ (the 5 axiom). Follows from Euclideanness of the belief accessibility relation.

theorem Semantics.Modality.EpistemicLogic.believes_not_veridical : ∃ (W : Type) (E : Type) (Rs : Core.Logic.Intensional.AgentAccessRel W E) (i : E) (φ : W → Prop) (w : W), believes Rs i φ w ∧ ¬φ w

Belief is not veridical: there exist frames where Bᵢ(φ) ∧ ¬φ. Unlike knowledge (which requires reflexivity), belief frames are serial but not reflexive, so an agent can believe φ at a world where φ is false.

Common Ground as Common Knowledge

@cite{stalnaker-2002}: the common ground is the set of propositions that are common knowledge among the discourse participants.

def Core.CommonGround.CG.groundedIn {W : Type u_1} {E : Type u_2} (cg : CG W) (Rs : Logic.Intensional.AgentAccessRel W E) (group : List E) (bound : ℕ) : Prop

A common ground is grounded in common knowledge when its context set equals the intersection of what is commonly known.

Equations

• cg.groundedIn Rs group bound = ∀ (w : W), cg.contextSet w ↔ ∀ p ∈ cg.propositions, Semantics.Modality.EpistemicLogic.commonKnowledge Rs group p bound w

Bridge to EpistemicScale

An S5 frame (reflexive + Euclidean accessibility) induces an EpistemicSystemW via Lewis's l-lifting. This connects the syntactic side (Kripke frames, correspondence theorems in ModalLogic.lean) to the algebraic side (plausibility measures, representation theorems in EpistemicScale/).

def Semantics.Modality.EpistemicLogic.s5ToWorldOrder {W : Type u_1} (R : Core.Logic.Intensional.AccessRel W) (w v : W) : Prop

An S5 accessibility relation induces a world ordering for halpernLift: w ≥ v iff w is accessible from v.

Equations

• Semantics.Modality.EpistemicLogic.s5ToWorldOrder R w v = R v w

def Semantics.Modality.EpistemicLogic.s5ToSystemW {W : Type u_1} (R : Core.Logic.Intensional.AccessRel W) (hRefl : Core.Logic.Intensional.IsReflexive R) : Core.Scale.EpistemicSystemW W

An S5 frame yields an EpistemicSystemW via l-lifting.

The reflexivity of R gives reflexivity of the world ordering; halpernSystemW does the rest.

Equations

• Semantics.Modality.EpistemicLogic.s5ToSystemW R hRefl = Core.Scale.halpernSystemW (Semantics.Modality.EpistemicLogic.s5ToWorldOrder R) ⋯