Knowledge-Probability Structures #
@cite{fagin-halpern-1994}
Bridges Boolean epistemic logic (EpistemicLogic.lean) and graded
probability operators (EpistemicProbability.lean) by defining
Kripke probability structures — the combined framework from
@cite{fagin-halpern-1994} where agents have both an information partition
(S5 accessibility) and a probability assignment at each state.
Key contributions #
KripkeKP: bundlesAgentAccessRel(knowledge) +WorldCredence(probability) into a single structure.Structural conditions: CONS, OBJ, UNIF, SDP as predicates on
KripkeKP, capturing how probability assignments interact with information partitions.Bridge theorem: under CONS + normalization, Boolean knowledge (
K_i φ) implies probability-1 belief (w_i(φ) = 1), which is @cite{fagin-halpern-1994}'s axiom W7.Probabilistic group operators:
E_G^b(everyone assigns probability ≥ b) andC_G^b(common probabilistic knowledge), generalizing the Boolean operators fromEpistemicLogic.lean. Probabilistic CK uses @cite{fagin-halpern-1994}'sF_G^boperator (Section 5), NOT the naive iteration(E_G^b)^n.Condition hierarchy:
sdp_implies_unifunder S5 — proves FH94's observation that W7 + W10 imply W9.UNIF and introspection: uniformity yields both positive and negative introspection for probabilistic beliefs (axiom W9).
Connection to the Epistemic Scale Hierarchy #
The indirect path from Kratzer ordering to RSA worldPrior goes through @cite{holliday-icard-2013}'s epistemic likelihood hierarchy:
Kratzer ordering → l-lifting → EpistemicSystemW → ... → RSA worldPrior
KnowledgeProbability provides @cite{fagin-halpern-1994}'s more direct
path: a KripkeKP structure already packages both the accessibility
relation (for knowledge operators) and the probability assignment
(for RSA). Under CONS, the two are coherently linked.
A Kripke probability structure: agents have both an information partition (S5 accessibility) and a probability assignment at each state.
This is M = (S, π, K₁,...,Kₙ, P), where:
accessRel= the accessibility relations Kᵢ (information partitions)worldCredence= the probability assignment P mapping (i, s) to Pᵢ,ₛ
The truth assignment π is implicit in our framework (handled by BProp).
Structural conditions (CONS, UNIF, etc.) are separate predicates.
- accessRel : Core.ModalLogic.AgentAccessRel W E
Agent-indexed accessibility relation (information partition)
- worldCredence : EpistemicProbability.WorldCredence E W
World-dependent agent credence (probability spaces)
Instances For
CONS (Consistency): each agent's probability is concentrated on their accessible worlds. Two propositions agreeing on all i-accessible worlds from w receive the same credence.
literal CONS (p. 350) says the sample space
Sᵢ,ₛ is a subset of Kᵢ(s). Since our WorldCredence abstraction does
not model explicit sample spaces, we capture the operational consequence:
propositions agreeing on accessible worlds receive equal credence.
This is equivalent to CONS for finite models where all subsets are
measurable.
This is the key condition connecting knowledge and probability: it ensures the agent's probability measure "respects" their information partition. Without CONS, an agent could assign positive probability to worlds they "know" are impossible.
Equations
- Semantics.Modality.KnowledgeProbability.CONS kp = ∀ (i : E) (w : W) (φ ψ : BProp W), (∀ (v : W), kp.accessRel i w v = true → φ v = ψ v) → kp.worldCredence i w φ = kp.worldCredence i w ψ
Instances For
OBJ (Objectivity): all agents share the same probability at each state. Probability differences arise only from different information sets, not from different priors.
OBJ (p. 350): Pᵢ,ₛ = Pⱼ,ₛ for all i, j, and s. Axiomatized by W8.
Equations
- Semantics.Modality.KnowledgeProbability.OBJ kp = ∀ (i j : E) (w : W) (φ : BProp W), kp.worldCredence i w φ = kp.worldCredence j w φ
Instances For
UNIF (Uniformity): agents assign the same probability at indistinguishable states. If w' is accessible from w, credence is the same at w and w'.
Under S5 (equivalence relations), probability is constant within each information cell.
Note: distinguishes UNIF (t ∈ Sᵢ,ₛ, the
sample space) from SDP (t ∈ Kᵢ(s), the accessible worlds).
Since our WorldCredence abstraction does not model explicit sample
spaces, this definition uses accessibility (Kᵢ) and thus corresponds
to SDP restricted to a single agent
rather than their literal UNIF. For finite models where Sᵢ,ₛ = Kᵢ(s)
(which holds under CONS when the sample space equals the accessible
worlds), the two are equivalent. Axiomatized by W9.
Equations
- Semantics.Modality.KnowledgeProbability.UNIF kp = ∀ (i : E) (w w' : W), kp.accessRel i w w' = true → ∀ (φ : BProp W), kp.worldCredence i w φ = kp.worldCredence i w' φ
Instances For
SDP (State-determined probability): the probability distribution is determined by the information set.
SDP (p. 351) is a single-agent condition: for all i, s, t, if t ∈ Kᵢ(s) then Pᵢ,ₛ = Pᵢ,ₜ. Our formulation generalizes to the multi-agent case: if two (agent, state) pairs have the same accessible worlds, they have the same credence. This captures both FH94's SDP (set i = j) and OBJ (when agents share accessibility). Axiomatized by W10.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Normalization: the credence function assigns 1 to the trivially true proposition. This is axiom W2.
Equations
- Semantics.Modality.KnowledgeProbability.Normalized kp = ∀ (i : E) (w : W), (kp.worldCredence i w fun (x : W) => true) = 1
Instances For
Nonnegativity: credences are non-negative. This is axiom W1.
Equations
- Semantics.Modality.KnowledgeProbability.Nonnegative kp = ∀ (i : E) (w : W) (φ : BProp W), 0 ≤ kp.worldCredence i w φ
Instances For
Measure monotonicity for world-dependent credence: each agent's
credence function at each world is Monotone (from Mathlib) under
the pointwise Bool ordering on BProp W.
Since Bool is ordered false ≤ true, φ ≤ ψ in W → Bool
means ∀ v, φ v = true → ψ v = true — i.e., set inclusion.
So Monotone (wcr i w) says: if φ ⊆ ψ then P(φ) ≤ P(ψ).
This is a standard property of probability measures, following from
nonnegativity + additivity (W1 + W3 of).
It is the hypothesis needed for probCKIter_monotone.
By reducing to Mathlib's Monotone, this connects to the same
abstract notion used throughout linglib:
IsUpwardEntailing = Monotone(Entailment/Polarity.lean)ScopeUpwardMono ↔ ∀ R, Monotone (q R)(Core/Quantification.lean)IsSumHom.monotone : Monotone f(Core/Mereology.lean)MeasureMonotone ↔ ∀ i w, Monotone (wcr i w)(this definition)
The world-independent special case isProbabilistic from
EpistemicThreshold.lean is identical in structure (∀ a, Monotone);
measureMonotone_isProbabilistic projects to a fixed world.
Equations
- Semantics.Modality.KnowledgeProbability.MeasureMonotone wcr = ∀ (i : E) (w : W), Monotone (wcr i w)
Instances For
MeasureMonotone implies isProbabilistic when projected to any
fixed world. Both are Monotone — this just fixes the world parameter.
This connects the FH94 probability axioms (world-dependent) to the
LaBToM threshold semantics (world-independent via liftCredence).
Under CONS + normalization, knowledge implies probability 1.
K_i(φ)(w) → w_i(φ)(w) = 1
If φ is true at all i-accessible worlds, and probability is concentrated on accessible worlds, then φ is indistinguishable from truth — hence has probability 1.
This is axiom W7: K_i φ ⇒ (w_i(φ) = 1).
Probabilistic "everyone knows": every agent in the group assigns probability ≥ b to φ at world w.
E_G^b(φ)(w) = ∧_{i∈G} [w_i(φ)(w) ≥ b]
When b = 1, coincides with Boolean everyoneKnows (under CONS).
This is E_G^b operator (Section 5).
Equations
- Semantics.Modality.KnowledgeProbability.everyoneProbably wcr group b φ w = group.all fun (i : E) => Semantics.Modality.EpistemicProbability.nestedThreshold wcr b i φ w
Instances For
F_G^b iteration for probabilistic common
knowledge (Section 5). Unlike the naive iteration (E_G^b)^n, each
level conjoins φ with the previous level before applying E_G^b:
(F_G^b)^0(φ) = true (F_G^b)^{k+1}(φ) = E_G^b(φ ∧ (F_G^b)^k(φ))
FH94 shows that the naive definition using (E_G^b)^k fails:
a 4-state counterexample (Figure 1) satisfies
E_G^{1/2} p ∧ (E_G^{1/2})² p ∧ ⋯ at s₁ but NOT the correct
F_G^b-based C_G^{1/2} p. The F_G^b operator correctly maintains
φ at each iteration level, preventing this false positive.
Equations
- One or more equations did not get rendered due to their size.
- Semantics.Modality.KnowledgeProbability.probCKIter wcr group b φ Nat.zero = fun (x : W) => true
Instances For
Probabilistic common knowledge: C_G^b(φ)(w) iff (F_G^b)^k(φ)(w) for all k = 1, ..., bound.
C_G^b is the greatest fixed point of
X ⟺ E_G^b(φ ∧ X) (Lemma 5.1). The iteration probCKIter (F_G^b)^k
converges to this fixed point from above.
Unlike Boolean common knowledge, C_G^b(φ) does NOT imply φ for b < 1. Probabilistic CK only asserts recursive confidence: everyone assigns probability ≥ b to φ, everyone assigns probability ≥ b that everyone assigns probability ≥ b to φ, etc.
Equations
- Semantics.Modality.KnowledgeProbability.commonProbKnowledge wcr group b φ bound w = (List.range bound).all fun (n : ℕ) => Semantics.Modality.KnowledgeProbability.probCKIter wcr group b φ (n + 1) w
Instances For
The F_G^b iterates are monotonically decreasing: (F_G^b)^{k+1}(φ) ⟹ (F_G^b)^k(φ).
This follows because φ ∧ F^k ⊆ φ ∧ F^{k-1} (by induction) and probability is monotone (P(A) ≤ P(B) when A ⊆ B). Consequently, checking C_G^b with bound n is equivalent to checking just the highest level (F_G^b)^n(φ).
The MeasureMonotone hypothesis requires that credence respects
set inclusion — a standard property of probability measures that
follows from nonnegativity + additivity (W1 + W3).
SDP implies UNIF under S5 accessibility.
notes (p. 351) that CONS + SDP together imply UNIF. Under S5 (reflexive + Euclidean), if w' is accessible from w then w and w' have the same accessible worlds, so SDP with i = j directly gives UNIF.
This is the semantic content of the paper's observation that W7 + W10 imply W9 (CONS + SDP axioms imply the UNIF axiom).
Under CONS + normalization, Boolean everyone-knows implies probabilistic everyone-probably at threshold 1.
Under UNIF, the threshold operator is stable across accessible worlds:
if w' is accessible from w, nestedThreshold θ i φ gives the same
value at w and w'.
This is the formal content of observation that UNIF enables introspection for probabilistic beliefs. Under UNIF, an i-probability formula (w_i(φ) ≥ b) has the same truth value at all states within an information cell, which is exactly what this theorem states.
Under UNIF, probabilistic belief is positively introspective: if the agent assigns probability ≥ θ to φ, the agent knows this.
w_i(φ) ≥ θ → K_i(w_i(φ) ≥ θ)
This is axiom W9 for the case where the formula is a positive i-probability formula. Combined with the case where w_i(φ) < θ (which gives K_i(w_i(φ) < θ)), UNIF yields Miller's principle: agents are always certain of their own credences.
This is the probabilistic analogue of KD45 axiom 4 (Bφ → BBφ), lifting Boolean introspection to graded credence.
Under UNIF, probabilistic belief is negatively introspective: if the agent assigns probability < θ to φ, the agent knows this.
¬(w_i(φ) ≥ θ) → K_i(¬(w_i(φ) ≥ θ))
Together with unif_positive_introspection, this completes
axiom W9: under UNIF, every
i-probability formula or its negation is known by agent i.
The empty proposition has credence 0.
This is axiom W5: w_i(false) = 0.
In standard probability, P(∅) = 0 follows from normalization +
additivity. We state it separately since WorldCredence does not
include additivity as a structural axiom.
Equations
- Semantics.Modality.KnowledgeProbability.NullEmpty kp = ∀ (i : E) (w : W), (kp.worldCredence i w fun (x : W) => false) = 0
Instances For
Miller's principle: w_i(φ) ≥ b · w_i(w_i(φ) ≥ b).
(p. 352): under UNIF, this axiom connecting higher-order probabilities to first-order probabilities holds. It says that the agent's credence in φ is at least b times the agent's credence that the agent's credence in φ is at least b.
Under UNIF, the i-probability formula (w_i(φ) ≥ b) is constant within
each information cell (by unif_threshold_stable), so the inner
credence w_i(w_i(φ) ≥ b) is either 0 or 1:
- If w_i(φ) ≥ b: the formula is true everywhere in the cell, so w_i(w_i(φ) ≥ b) = 1 (by CONS + Normalized), and RHS = b ≤ w_i(φ). ✓
- If w_i(φ) < b: the formula is false everywhere in the cell, so w_i(w_i(φ) ≥ b) = 0 (by CONS + NullEmpty), and RHS = 0 ≤ w_i(φ). ✓
Miller's principle completely characterizes uniform structures (citing Halpern 1991). It is the probabilistic analogue of the KD45 introspection axioms.
Lemma 5.1 (Section 5): C_G^b(φ) is the greatest fixed-point solution of X ⟺ E_G^b(φ ∧ X).
This theorem proves the "greatest" direction: if ψ is a pre-fixed-point of the operator X ↦ E_G^b(φ ∧ X), meaning ψ(w) → E_G^b(φ ∧ ψ)(w), then ψ ≤ (F_G^b)^k(φ) for all k.
Together with the trivial observation that probCKIter is itself
a fixed point (by definition), this characterizes commonProbKnowledge
as the greatest pre-fixed-point.
The proof is by induction on k. The base case (k=0) is trivial since
(F_G^b)⁰ = true. The inductive step uses MeasureMonotone: since
ψ ≤ (F_G^b)^k (by IH), we have φ ∧ ψ ≤ φ ∧ (F_G^b)^k, and
monotonicity of credence gives E_G^b(φ ∧ ψ) ≤ E_G^b(φ ∧ (F_G^b)^k)
= (F_G^b)^{k+1}. Combined with the pre-fixed-point hypothesis
ψ ≤ E_G^b(φ ∧ ψ), we get ψ ≤ (F_G^b)^{k+1}.
Figure 1 Counterexample #
(Section 5) shows that the "obvious" definition of probabilistic common knowledge C_G^b as the infinite conjunction E_G^b φ ∧ (E_G^b)² φ ∧ ··· is incorrect. Their 4-state counterexample (Figure 1) demonstrates a structure where the naive iteration succeeds at all levels but the correct F_G^b-based definition fails.
The structure M has states s₁, s₂, s₃, s₄ (encoded as Fin 4 = 0, 1, 2, 3):
- Agent 1 partitions worlds into {s₁,s₂} | {s₃,s₄}
- Agent 2 partitions worlds into {s₁,s₃} | {s₂,s₄}
- p = true at s₂ and s₃ (false at s₁ and s₄)
- Probability: uniform within first cell, all mass on s₄ in second cell
At s₁:
- E_G^{1/2} p holds (both agents assign probability 1/2 to p)
- The naive (E_G^{1/2})^k p holds for all k (stabilizes at {s₁})
- But p is FALSE at s₁, so p ∧ E_G^{1/2} p = ∅
- Therefore (F_G^{1/2})² p = E_G^{1/2}(∅) = false
- The correct C_G^{1/2} p is false at s₁
Naive iteration (E_G^b)^k: just iterates everyoneProbably without
conjoining φ at each level. This is the incorrect definition
that shows fails for probabilistic CK.
Compare with probCKIter which uses the correct F_G^b operator.
Equations
- One or more equations did not get rendered due to their size.
- Semantics.Modality.KnowledgeProbability.naiveIter wcr group b φ Nat.zero = φ
Instances For
At s₁, the naive iteration succeeds at level 1: E_G^{1/2} p is true.
At s₁, the naive iteration succeeds at level 2: (E_G^{1/2})² p is true.
The naive iteration succeeds at s₁ for ALL levels k ≥ 1. Since levels 1 and 2 agree pointwise, all higher levels also agree.
At s₁, the CORRECT F_G^{1/2} iteration fails at level 2. This is because p ∧ E_G^{1/2} p = ∅ (p is false at s₁, the only world where E_G^{1/2} p holds).
The core counterexample: the naive iteration succeeds at s₁ where the correct F_G^b-based definition fails. This proves that the definitions are genuinely different and justifies FH94's use of the F_G^b operator for probabilistic common knowledge.