Doxastic / Deontic Commitment Frame

[Hin62] [Sta84]

Multi-relational Kripke frame for doxastic-deontic discourse logic: per-agent belief accessibility (KD45 — [Hin62]) plus pair-indexed commitment accessibility (K4 + Euclidean, not serial — so commitment violations are expressible). The Sincere and Competent frame conditions ([Sta84]) bridge commitment to belief.

Main definitions

• PairAccessRel W A — pair-indexed deontic accessibility.
• CommitmentState W A — frame: belief + commitment + valuation + bundled per-agent KD45 and per-pair K4-Euclidean frame conditions.
• Believes, Committed — modal operators.
• Sincere, Competent — frame conditions linking belief and commitment.
• committed_implies_believes_of_sincere and corollaries — the [Hin62]/[Sta84] transfer theorems.

@[reducible, inline]

abbrev Discourse.Commitment.Frame.PairAccessRel (W : Type u_1) (A : Type u_2) : Type (max u_2 u_1)

Pair-indexed deontic accessibility: commitment a b w v means at w, the world v is among those satisfying everything a is committed-towards-b to. Genuinely ternary; no analogue in linglib's unary-belief substrate.

Equations

• Discourse.Commitment.Frame.PairAccessRel W A = (A → A → Core.Logic.Modal.AccessRel W)

structure Discourse.Commitment.Frame.CommitmentState (W : Type u_1) (A : Type u_2) : Type (max u_1 u_2)

Multi-relational Kripke frame: belief (KD45) + commitment (K4 + Eucl., not serial) + atomic valuation.

• belief : Core.Logic.Modal.AgentAccessRel W A

  Per-agent doxastic accessibility.

• commitment : PairAccessRel W A

  Pair-indexed deontic accessibility.

• interp : String → Set W

  Atomic-proposition valuation.

• belief_kd45 (a : A) : Core.Logic.Modal.IsKD45Frame (self.belief a)

  Belief is KD45 (serial + transitive + euclidean) per agent.

• commitment_k4eucl (a b : A) : Core.Logic.Modal.IsK4EuclFrame (self.commitment a b)

  Commitment is K4-Euclidean (no seriality — violations are expressible) per pair.

instance Discourse.Commitment.Frame.CommitmentState.instIsKD45FrameBelief {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) (a : A) : Core.Logic.Modal.IsKD45Frame (c.belief a)

instance Discourse.Commitment.Frame.CommitmentState.instIsK4EuclFrameCommitment {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) (a b : A) : Core.Logic.Modal.IsK4EuclFrame (c.commitment a b)

def Discourse.Commitment.Frame.CommitmentState.trivial {W : Type u_1} {A : Type u_2} : CommitmentState W A

The trivial state: every world doxastically/commitmentally accessible from every world; every atom true everywhere.

Equations

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

def Discourse.Commitment.Frame.CommitmentState.commitmentEmpty {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) (a b : A) : Prop

a's commitment-towards-b is empty — operationally, a is committed to a contradiction.

Equations

• c.commitmentEmpty a b = ∀ (w v : W), ¬c.commitment a b w v

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

Restrict a's commitment-towards-b edges to π-targets; leave other edges unchanged. O^c[π]_{a,b} = O^c_{a,b} ∩ {(w, v) | v ∈ π}.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem Discourse.Commitment.Frame.CommitmentState.restrictCommitment_interp {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) (a b : A) (π : Set W) : (c.restrictCommitment a b π).interp = c.interp

Modal operators

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

a believes π at w: every belief-accessible world from w lies in π. KD45 belief (Hintikka 1962).

Equations

• Discourse.Commitment.Frame.Believes c a π w = Semantics.Modality.EpistemicLogic.knows c.belief a (fun (v : W) => v ∈ π) w

theorem Discourse.Commitment.Frame.Believes_eq_box {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) (a : A) (π : Set W) (w : W) : Believes c a π w ↔ Core.Logic.Modal.box (c.belief a) (fun (v : W) => v ∈ π) w

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

a committed towards b to π at w: every O_{a,b}-accessible world from w lies in π. K4 + Eucl. (Stalnaker 1984).

Equations

• Discourse.Commitment.Frame.Committed c a b π w = Core.Logic.Modal.box (c.commitment a b) (fun (v : W) => v ∈ π) w

theorem Discourse.Commitment.Frame.believes_four {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) (a : A) (π : Set W) (w : W) (h : Believes c a π w) : Believes c a (fun (v : W) => Believes c a π v) w

Belief satisfies the 4 axiom (positive introspection).

theorem Discourse.Commitment.Frame.committed_four {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) (a b : A) (π : Set W) (w : W) (h : Committed c a b π w) : Committed c a b (fun (v : W) => Committed c a b π v) w

Commitment satisfies the 4 axiom.

Frame conditions linking belief and commitment

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

Sincerity ([Sta84]): for every agent pair, belief is contained in commitment. "If you believe it, you act as if committed to it."

Equations

• Discourse.Commitment.Frame.Sincere c = ∀ (x y : A) (w v : W), c.belief x w v → c.commitment x y w v

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

Competence ([Sta84]): for every pair (x, y), y's doxastically accessible worlds are also x-accessible. "x is well-informed about what y considers possible."

Equations

• Discourse.Commitment.Frame.Competent c = ∀ (x y : A) (w v : W), c.belief y w v → c.belief x w v

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

In a Sincerity-satisfying state, commitment entails belief. [Hin62] / [Sta84] transfer, used as a lemma in [van-der-leer-2026].

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

In a Competence-satisfying state, a's belief entails b's belief ([van-der-leer-2026]).

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

Composed: Sincerity + Competence ⇒ a's commitment-to-b of π entails b's belief in π. The mediated CommonGround-update of [bary-2025], derived not stipulated ([van-der-leer-2026]).

Refinement: information-narrowing preorder on commitment states

def Discourse.Commitment.Frame.CooperativeExt {W : Type u_1} {A : Type u_2} (c c' : CommitmentState W A) : Prop

c' strictly refines c: belief and commitment relations narrow, valuation is preserved, and the states are distinct. The substrate notion of "discourse progress" — any later state in a coherent conversation refines the earlier.

Equations

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

def Discourse.Commitment.Frame.CooperativeExtRefl {W : Type u_1} {A : Type u_2} (c c' : CommitmentState W A) : Prop

Reflexive closure of CooperativeExt.

Equations

• Discourse.Commitment.Frame.CooperativeExtRefl c c' = (c = c' ∨ Discourse.Commitment.Frame.CooperativeExt c c')

theorem Discourse.Commitment.Frame.cooperativeExtRefl_refl {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) : CooperativeExtRefl c c

theorem Discourse.Commitment.Frame.not_cooperativeExt_self {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) : ¬CooperativeExt c c

Mutual commitment (per-state)

def Discourse.Commitment.Frame.MutuallyCommittedAt {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) (π : Set W) (w : W) : Prop

All agent pairs are mutually committed to π at w. The deontic analogue of EpistemicLogic.commonBelief.

Equations

• Discourse.Commitment.Frame.MutuallyCommittedAt c π w = ∀ (a b : A), Discourse.Commitment.Frame.Committed c a b π w