Belief–commitment frames

The multi-relational Kripke frame of [vdL26] (Definition 2): per-agent belief accessibility B_a, the KD45 doxastic frame of [Hin62], and pair-indexed commitment accessibility O_{a,b}, K45 — transitive and Euclidean but not serial, so that an agent may be committed to a contradiction. Belief B_a π and commitment C_{a,b} π are ModalLogic.Box along these relations. Propositions are world-sets, so the valuation of Definition 2 is absorbed into them and every proposition is C_{a,b}-free in the thesis's sense.

Main definitions

• Commitment.Frame W A — the frame.
• Frame.Believes, Frame.Committed — B_a, C_{a,b}.
• Frame.restrictCommitment — the update c⌈π⌉_{a,b} (Definition 4): O_{a,b} restricted to π-targets, everything else unchanged.
• Frame.Sincere, Frame.Competent — the frame conditions of Definition 5, after [AL03]: belief is contained in commitment; the addressee's belief is contained in the speaker's.

Main results

• Frame.committed_restrictCommitment — the performative update, c⌈π⌉_{a,b} ⊨ C_{a,b} π.
• Frame.Sincere.believes_of_committed, Frame.Competent.believes_of_believes, Frame.Sincere.believes_of_committed_of_competent — Theorem 26: commitment transfers to the speaker's belief under Sincerity and on to the addressee's under Competence, the informative update.
• Frame.restrictCommitment_eq_self — the update is idle iff the commitment already holds globally.
• Frame.mem_slate_iff — the propositions a is committed to towards b at w form the principal filter of the O_{a,b}-successors, the projection onto the commitment sets of Commitment.Basic.

References

• T. van der Leer, Commitments, beliefs and expectations in conversation (2026)
• J. Hintikka, Knowledge and Belief: An Introduction to the Logic of the Two Notions (1962)
• N. Asher and A. Lascarides, Logics of Conversation (2003)

structure Commitment.Frame (W : Type u_3) (A : Type u_4) : Type (max u_3 u_4)

The belief–commitment frame of [vdL26] (Definition 2, there a commitment state): KD45 belief per agent and K45 commitment per ordered agent pair.

• belief : A → SetRel W W

  a's doxastic accessibility.

• commitment : A → A → SetRel W W

  w ~[commitment a b] v: at w, v satisfies everything a is committed towards b to.

• belief_kd45 (a : A) : ModalLogic.IsKD45Frame (self.belief a)
• commitment_k45 (a b : A) : ModalLogic.IsK45Frame (self.commitment a b)

theorem Commitment.Frame.ext_iff {W : Type u_3} {A : Type u_4} {x y : Frame W A} : x = y ↔ x.belief = y.belief ∧ x.commitment = y.commitment

theorem Commitment.Frame.ext {W : Type u_3} {A : Type u_4} {x y : Frame W A} (belief : x.belief = y.belief) (commitment : x.commitment = y.commitment) : x = y

instance Commitment.Frame.instIsKD45FrameBelief {W : Type u_1} {A : Type u_2} (c : Frame W A) (a : A) : ModalLogic.IsKD45Frame (c.belief a)

instance Commitment.Frame.instIsK45FrameCommitment {W : Type u_1} {A : Type u_2} (c : Frame W A) (a b : A) : ModalLogic.IsK45Frame (c.commitment a b)

@[instance_reducible]

instance Commitment.Frame.instInhabited {W : Type u_1} {A : Type u_2} : Inhabited (Frame W A)

Every world is accessible from every world.

Equations

• Commitment.Frame.instInhabited = { default := { belief := fun (x : A) => Set.univ, commitment := fun (x x_1 : A) => Set.univ, belief_kd45 := ⋯, commitment_k45 := ⋯ } }

def Commitment.Frame.restrictCommitment {W : Type u_1} {A : Type u_2} (c : Frame W A) (a b : A) (π : Set W) : Frame W A

c⌈π⌉_{a,b} ([vdL26] Definition 4): O_{a,b} restricted to π-targets, O_{a,b} ∩ {(w, v) | v ∈ π}; the other relations are unchanged.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Commitment.Frame.restrictCommitment_belief {W : Type u_1} {A : Type u_2} (c : Frame W A) (a b : A) (π : Set W) : (c.restrictCommitment a b π).belief = c.belief

@[simp]

theorem Commitment.Frame.restrictCommitment_self {W : Type u_1} {A : Type u_2} (c : Frame W A) (a b : A) (π : Set W) (w v : W) : (w, v) ∈ (c.restrictCommitment a b π).commitment a b ↔ (w, v) ∈ c.commitment a b ∧ v ∈ π

@[simp]

theorem Commitment.Frame.restrictCommitment_other {W : Type u_1} {A : Type u_2} (c : Frame W A) (a b : A) (π : Set W) (w : W) {a' b' : A} (h : ¬(a' = a ∧ b' = b)) (v : W) : (w, v) ∈ (c.restrictCommitment a b π).commitment a' b' ↔ (w, v) ∈ c.commitment a' b'

theorem Commitment.Frame.restrictCommitment_commitment_le {W : Type u_1} {A : Type u_2} (c : Frame W A) (a b : A) (π : Set W) (a' b' : A) : (c.restrictCommitment a b π).commitment a' b' ⊆ c.commitment a' b'

theorem Commitment.Frame.restrictCommitment_restrictCommitment {W : Type u_1} {A : Type u_2} (c : Frame W A) (a b : A) (π τ : Set W) : (c.restrictCommitment a b π).restrictCommitment a b τ = c.restrictCommitment a b (π ∩ τ)

theorem Commitment.Frame.restrictCommitment_mono {W : Type u_1} {A : Type u_2} (c : Frame W A) (a b : A) (π τ : Set W) (h : π ⊆ τ) (a' b' : A) : (c.restrictCommitment a b π).commitment a' b' ⊆ (c.restrictCommitment a b τ).commitment a' b'

Modal operators

def Commitment.Frame.Believes {W : Type u_1} {A : Type u_2} (c : Frame W A) (a : A) (π : Set W) (w : W) : Prop

a believes π at w: π holds at every B_a-accessible world ([vdL26] Definition 3).

Equations

• c.Believes a π w = ModalLogic.Box (c.belief a) (fun (x : W) => x ∈ π) w

def Commitment.Frame.Committed {W : Type u_1} {A : Type u_2} (c : Frame W A) (a b : A) (π : Set W) (w : W) : Prop

a is committed towards b to π at w: π holds at every O_{a,b}-accessible world ([vdL26] Definition 3).

Equations

• c.Committed a b π w = ModalLogic.Box (c.commitment a b) (fun (x : W) => x ∈ π) w

theorem Commitment.Frame.committed_restrictCommitment {W : Type u_1} {A : Type u_2} (c : Frame W A) (a b : A) (π : Set W) (w : W) : (c.restrictCommitment a b π).Committed a b π w

The performative update ([vdL26] Theorem 25 at the level of states): c⌈π⌉_{a,b} ⊨ C_{a,b} π.

theorem Commitment.Frame.restrictCommitment_eq_self {W : Type u_1} {A : Type u_2} (c : Frame W A) (a b : A) (π : Set W) : c.restrictCommitment a b π = c ↔ ∀ (w : W), c.Committed a b π w

theorem Commitment.Frame.restrictCommitment_restrictCommitment_eq_self_iff {W : Type u_1} {A : Type u_2} (c : Frame W A) (a b : A) (π τ : Set W) (a' b' : A) : (c.restrictCommitment a b π).restrictCommitment a' b' τ = c ↔ c.restrictCommitment a b π = c ∧ c.restrictCommitment a' b' τ = c

Two successive restrictions are idle iff each is.

Projection onto commitment sets

def Commitment.Frame.slate {W : Type u_1} {A : Type u_2} (c : Frame W A) (a b : A) (w : W) : Filter W

What a is committed to towards b at w: the principal filter of the O_{a,b}-successors of w.

Equations

• c.slate a b w = Filter.principal {v : W | (w, v) ∈ c.commitment a b}

theorem Commitment.Frame.mem_slate_iff {W : Type u_1} {A : Type u_2} (c : Frame W A) (a b : A) (π : Set W) (w : W) : π ∈ c.slate a b w ↔ c.Committed a b π w

Frame conditions linking belief and commitment

def Commitment.Frame.Sincere {W : Type u_1} {A : Type u_2} (c : Frame W A) : Prop

Sincerity ([vdL26] Definition 5, after [AL03]): for every agent pair, belief is contained in commitment.

Equations

• c.Sincere = ∀ (x y : A), c.belief x ⊆ c.commitment x y

def Commitment.Frame.Competent {W : Type u_1} {A : Type u_2} (c : Frame W A) : Prop

Competence ([vdL26] Definition 5, after [AL03]): for every pair (x, y), y's belief-accessible worlds are x-accessible too.

Equations

• c.Competent = ∀ (x y : A), c.belief y ⊆ c.belief x

theorem Commitment.Frame.Sincere.believes_of_committed {W : Type u_1} {A : Type u_2} {c : Frame W A} {a b : A} {π : Set W} {w : W} (h : c.Sincere) : c.Committed a b π w → c.Believes a π w

Under Sincerity, commitment entails belief ([vdL26] Theorem 26(1)).

theorem Commitment.Frame.Competent.believes_of_believes {W : Type u_1} {A : Type u_2} {c : Frame W A} {a b : A} {π : Set W} {w : W} (h : c.Competent) : c.Believes a π w → c.Believes b π w

Under Competence, a's belief entails b's ([vdL26] Theorem 26(2)).

theorem Commitment.Frame.Sincere.believes_of_committed_of_competent {W : Type u_1} {A : Type u_2} {c : Frame W A} {a b : A} {π : Set W} {w : W} (hsin : c.Sincere) (hcomp : c.Competent) : c.Committed a b π w → c.Believes b π w

Under Sincerity and Competence, a's commitment towards b entails b's belief: the informative update ([vdL26] Theorem 26(3)).