Fagin and Halpern (1994): Reasoning about Knowledge and Probability #

This file formalizes the Kripke structures for knowledge and probability of [FH94] and the probabilistic common knowledge of its Section 5. A KripkeProb adds to the accessibility relations of multi-agent epistemic logic (Logic/Modal/Epistemic) a probability space for each agent at each state: a sample space S_{i,s} of states and a probability measure μ_{i,s} carried by it. The probability formula w_i(φ) ≥ b, "according to agent i, φ holds with probability at least b", is the set of states AtLeast b i φ. Knowledge and probability are otherwise independent, so an agent need not know their own probability space, which is what lets the paper's coin-toss example come out right. The conditions the paper considers on the pair are CONS (the sample space lies within the states the agent considers possible), OBJ (all agents share one space), SDP (the space is determined by the agent's information cell) and UNIF (the space is the same at every state of the sample space); UNIF.of_cons_sdp is the paper's remark that the first and third imply the fourth. The correspondence of Section 4 between these conditions and axioms is proved in its sound direction: W7, knowledge implies probability one under CONS (real_eq_one_of_knows); W9, a probability formula true at a state has probability one there under UNIF (UNIF.real_atLeast_eq_one, UNIF.real_compl_atLeast_eq_one); W10, a probability formula true at a state is known there under SDP (SDP.knows_atLeast, SDP.knows_compl_atLeast); and Miller's principle w_i(φ) ≥ b · w_i(w_i(φ) ≥ b), which UNIF validates (UNIF.miller).

Section 5 defines E_G^b φ (EveryoneProb: every member of G knows that their probability of φ is at least b) and probabilistic common knowledge C_G^b φ (CommonProb) as the intersection of the iterates (F_G^b)^k φ of X ↦ E_G^b (φ ∩ X) rather than of the iterates of E_G^b alone. commonProb_eq_gfp is Lemma 5.1: C_G^b φ is the greatest fixed point of X ⇔ E_G^b (φ ∧ X). The four-state structure fig1 of Figure 1 is the paper's reason for the detour: the naive infinite conjunction E_G^b φ ∧ (E_G^b)² φ ∧ ⋯ (Naive) holds at s₁ (fig1_naive), E_G^{1/2} p fails at s₂ and s₃ (fig1_everyoneProb), and so the conjunction is not a solution of the equation (fig1_naive_not_fixedPoint) while the paper's C_G^{1/2} p is empty (fig1_commonProb).

Implementation notes #

Propositions are sets of states and w_i(φ) ≥ b reads μ_{i,s} on the set; since μ_{i,s} vanishes off the sample space, this is the paper's μ_{i,s}(S_{i,s}(φ)) (prob_inter_sample). The paper's inner measures for nonmeasurable sets are not modelled: mathlib evaluates every set by outer measure, and the one result that needs measurability, the fixed-point direction of Lemma 5.1 (continuity from above), assumes a discrete σ-algebra, the paper's MEAS in the finite case. Thresholds are real; the paper's rational coefficients embed.
The group operators take the paper's K_i^b φ = K_i(w_i(φ) ≥ b) literally: E_G^b φ asks each member to know their probability formula, not merely to satisfy it; the two coincide under SDP, as in Figure 1.
fig1 is built from Kernel.ofWeights over natural-number weights, so that every threshold comparison reduces to a decidable inequality between weight sums (fig1_atLeast_iff) and the four-state facts are decided.
Footnote 13's alternative equation X ⇔ E_G^b φ ∧ E_G^b X (Monderer and Samet), of which the naive conjunction is a solution, is not formalized.

Fagin and Halpern (1994): Reasoning about Knowledge and Probability #

Implementation notes #

References #

Conditions relating knowledge and probability #

Probabilistic common knowledge #

Figure 1 #