SAL Commitment Spaces

@cite{van-der-leer-2026} @cite{cohen-krifka-2014} @cite{krifka-2015}

van der Leer 2026 Definitions 7–8: a commitment space is a set of commitment states organised by a cooperative continuation order ⊑, with a unique ⊑-minimal root representing the current discourse state. The non-root members are projected futures representing admissible continuations.

c ⊑ c'  iff  W^c = W^c'
              ∧ B^c'_a ⊆ B^c_a       (for all a)
              ∧ O^c'_{a,b} ⊆ O^c_{a,b} (for all a, b)
              ∧ at least one inclusion is strict

i.e. c' is a tightening of c — beliefs and commitments only narrow (or stay the same) as discourse progresses; the world type is fixed across the space.

The improper version ⊑' is ⊑ ∪ {(c,c)} (reflexive closure).

Heritage and projection

Krifka's commitment-space framework treats a "state" as a list of indexed commitments. Here a state is a full Kripke frame whose relations encode the same content. The Krifka level is recoverable by intersecting all O_{a,b}-accessible worlds at the root state — that intersection IS the propositions Krifka tracks.

Bary 2025's 5-tuple ⟨c, cg, dc_A, dc_B, P, Q⟩ likewise projects: cg is the intersection of all B_a-accessible worlds at the root, dc_x is the intersection of O_{x,y} for the relevant y.

def Dialogue.SAL.CooperativeExt {W : Type u_1} {A : Type u_2} (c c' : CommitmentState W A) : Prop

van der Leer 2026 Definition 7 (cooperative continuation, strict ⊑): c' cooperatively extends c iff:

1. They share the world type (W^c = W^c' is enforced structurally — both have type CommitmentState W A).
2. c''s belief relations are sub-relations of c's.
3. c''s commitment relations are sub-relations of c's.
4. At least one inclusion is strict somewhere — i.e. c ≠ c'.

The strict-extension flag (c ≠ c') is the formal counterpart of paper-(7)'s "at least one strict inclusion" — under the sub-relation conjunction, equality everywhere collapses to c = c'.

Equations

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

def Dialogue.SAL.CooperativeExtRefl {W : Type u_1} {A : Type u_2} (c c' : CommitmentState W A) : Prop

van der Leer 2026 improper-cooperative-extension: c ⊑' c' iff c = c' or c ⊑ c'.

Equations

• Dialogue.SAL.CooperativeExtRefl c c' = (c = c' ∨ Dialogue.SAL.CooperativeExt c c')

theorem Dialogue.SAL.cooperativeExtRefl_refl {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) : CooperativeExtRefl c c

The improper extension is reflexive.

theorem Dialogue.SAL.not_cooperativeExt_self {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) : ¬CooperativeExt c c

Cooperative extension is irreflexive (it requires c ≠ c').

structure Dialogue.SAL.CommitmentSpace (W : Type u_3) (A : Type u_4) : Type (max u_3 u_4)

van der Leer 2026 Definition 8: a commitment space is a set of commitment states with a unique ⊑-minimal element (the root).

The root is the current state of the discourse; the non-root members are projected futures representing admissible continuations (per the Collaborative Principle: silence after a speech act extends the space by tightening relations to those consistent with implicit acceptance).

• states : Set (CommitmentState W A)

  The set of commitment states comprising the space.

• root : CommitmentState W A

  The root: a distinguished current state.

• root_mem : self.root ∈ self.states

  The root is in the space.

• root_minimal (c : CommitmentState W A) : c ∈ self.states → CooperativeExtRefl self.root c

  The root is ⊑'-below every state in the space (it is the ⊑-minimum: every other state cooperatively extends it).

def Dialogue.SAL.CommitmentSpace.singleton {W : Type u_3} {A : Type u_4} (root : CommitmentState W A) : CommitmentSpace W A

The trivial commitment space: a single state (the root) with no proper extensions. Useful as a baseline; corresponds to "no commitments yet, no projected futures".

Equations

• Dialogue.SAL.CommitmentSpace.singleton root = { states := {root}, root := root, root_mem := ⋯, root_minimal := ⋯ }

@[simp]

theorem Dialogue.SAL.CommitmentSpace.singleton_root {W : Type u_3} {A : Type u_4} (c : CommitmentState W A) : (singleton c).root = c

@[simp]

theorem Dialogue.SAL.CommitmentSpace.singleton_states {W : Type u_3} {A : Type u_4} (c : CommitmentState W A) : (singleton c).states = {c}

def Dialogue.SAL.CommitmentSpace.MutuallyCommitted {W : Type u_3} {A : Type u_4} (C : CommitmentSpace W A) (π : Set W) : Prop

A proposition is mutually committed in a commitment space iff every agent is committed to every other agent at every state of the space. The Geurts 2019 fixed-point characterisation, lifted over the commitment-space level (van der Leer 2026 §2.1).

Equations

• C.MutuallyCommitted π = ∀ c ∈ C.states, ∀ (a b : A) (w : W), Dialogue.SAL.Committed c a b π w

def Dialogue.SAL.CommitmentSpace.CommonlyBelieved {W : Type u_3} {A : Type u_4} (c : CommitmentState W A) (group : List A) (π : Set W) (bound : ℕ) (w : W) : Prop

A proposition is commonly believed at world w of state c in the space iff EpistemicLogic.commonBelief holds for the given agent group up to the iteration bound. Delegates to the existing Theories/Semantics/Modality/EpistemicLogic.commonBelief substrate rather than re-stipulating; the SAL-side wrapper just selects the state's belief relation.

Equations

• Dialogue.SAL.CommitmentSpace.CommonlyBelieved c group π bound w = Semantics.Modality.EpistemicLogic.commonBelief c.belief group (fun (v : W) => v ∈ π) bound w