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, BContextSet) remains in
Core/Semantics/CommonGround.lean.
Individual Knowledge #
Agent i knows φ at world w iff φ holds at all worlds accessible to i.
This re-uses kripkeEval from ModalLogic.lean with agent-indexed
accessibility relations.
Agent i knows φ at world w: Kᵢ(φ)(w) = □ᵢ φ(w).
Equations
Instances For
Everyone Knows #
E_G(φ) holds at w iff every agent in group G knows φ at w. E_G(φ) = ∧ᵢ∈G Kᵢ(φ).
Everyone in group G knows φ at w.
Equations
- Semantics.Modality.EpistemicLogic.everyoneKnows Rs group φ w = group.all fun (i : E) => Semantics.Modality.EpistemicLogic.knows Rs i φ w
Instances For
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 until fixpoint. Since there are finitely many truth assignments, this terminates.
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 = φ
Instances For
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 = (List.range (bound + 1)).all fun (n : ℕ) => Semantics.Modality.EpistemicLogic.everyoneKnowsIter Rs group φ n w
Instances For
Common knowledge implies everyone knows (at depth 1).
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ᵢ(φ).
Intersection of accessibility relations for a group.
Equations
- Semantics.Modality.EpistemicLogic.groupAccessRel Rs group w v = group.all fun (i : E) => Rs i w v
Instances For
Distributed knowledge: D_G(φ)(w) = □_{∩R} φ(w).
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
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
Instances For
Everyone in group G believes φ at w.
Equations
- Semantics.Modality.EpistemicLogic.everyoneBelieves Rs group φ w = group.all fun (i : E) => Semantics.Modality.EpistemicLogic.believes Rs i φ w
Instances For
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 = φ
Instances For
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 = (List.range (bound + 1)).all fun (n : ℕ) => Semantics.Modality.EpistemicLogic.everyoneBeliefIter Rs group φ n w
Instances For
Distributed belief: DB_G(φ)(w) = □_{∩R_B} φ(w).
Equations
Instances For
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.ModalLogic.AgentAccessRel W E
Knowledge accessibility relations (should satisfy S5: reflexive + Euclidean)
- believesRel : Core.ModalLogic.AgentAccessRel W E
Belief accessibility relations (should satisfy KD45: serial + transitive + Euclidean)
Belief accessibility implies knowledge accessibility
Instances For
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.
Belief is consistent: Bᵢ(φ) → ◇ᵢφ (the D axiom). Follows from seriality of the belief accessibility relation.
Positive introspection: Bᵢ(φ) → Bᵢ(Bᵢ(φ)) (the 4 axiom). Follows from transitivity of the belief accessibility relation.
Negative introspection: ¬Bᵢ(φ) → Bᵢ(¬Bᵢ(φ)) (the 5 axiom). Follows from Euclideanness of the belief accessibility relation.
Stated contrapositively using ◇: if ◇ᵢBᵢ(φ) then Bᵢ(φ). Equivalently: ◇Bφ → □◇Bφ, which combined with ¬Bφ → ¬◇Bφ → □¬Bφ gives the standard negative introspection.
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.
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 ↔ (cg.propositions.all fun (p : BProp W) => Semantics.Modality.EpistemicLogic.commonKnowledge Rs group p bound w) = true
Instances For
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/).
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 = true)
Instances For
An S5 frame yields an EpistemicSystemW via l-lifting.
The reflexivity of R gives reflexivity of the world ordering;
halpernSystemW does the rest.