Documentation

Linglib.Theories.Dialogue.SAL.Frame

SAL Commitment-State Frame #

@cite{van-der-leer-2026} @cite{bary-2025} @cite{cohen-krifka-2014} @cite{krifka-2015} @cite{krifka-2024} @cite{geurts-2019} @cite{asher-lascarides-2008}

CommitmentState W A is van der Leer 2026 Definition 2: the basic discourse state for SAL (Speech Act Logic). A multi-relational Kripke frame with separate doxastic and deontic accessibility relations, indexed respectively by single agents and ordered agent pairs:

c = ⟨W^c, {B^c_a}_{a∈A}, {O^c_{a,b}}_{(a,b)∈A²}, I^c⟩

The intentional weakening of seriality on the deontic relation is the substrate-level fact that lets SAL express commitment violation (van der Leer 2026 §2.2, around Theorem 33).

Why a separate frame from existing Kripke substrate #

Core/Logic/Intensional/Defs.lean provides single-relation Kripke infrastructure (AccessRel W, IsTransitive, IsEuclidean, IsSerial, ...). SAL needs a multi-relational frame: belief AND commitment, the latter indexed by ordered agent pairs. This file bundles both relation families with their KD45/K4 frame conditions and the valuation, into one record per discourse state.

Relation to existing dialogue substrate #

Theories/Dialogue/CommitmentSpace.lean (Krifka 2015) treats a "commitment state" as a list of IndexedCommitments (set-of- propositions). SAL refines this: each Krifka-state is now a full Kripke frame whose deontic relation is restricted to commitment- satisfying worlds. The Krifka level is recoverable as the projection that intersects all O_{a,b}-accessible worlds.

Frame conditions reuse #

We reuse the existing Core.Logic.Intensional.{IsTransitive, IsEuclidean, IsSerial} substrate — no fresh predicates.

source
@[reducible, inline]
abbrev Dialogue.SAL.PairAccessRel (W : Type u_1) (A : Type u_2) :
Type (max u_2 u_1)

Pair-indexed deontic accessibility: each ordered agent pair has its own commitment-relation over worlds. The deontic counterpart of Core.Logic.Intensional.AgentAccessRel, which is unary (only one accessing agent). The pair indexing reflects van der Leer 2026's point that commitment is ternary C_{a,b} π — a is committed towards b to π. No analogue exists in linglib's existing epistemic substrate (Theories/Semantics/Modality/EpistemicLogic.lean), which only formalises unary belief/knowledge.

Equations
Instances For
    source
    structure Dialogue.SAL.CommitmentState (W : Type u_1) (A : Type u_2) :
    Type (max u_1 u_2)

    A commitment state: the multi-relational Kripke frame at the heart of van der Leer 2026's SAL.

    W is the world type (typically a finite or countable set of possible discourse worlds). A is the agent type.

    The frame conditions are recorded as separate Prop-valued field-companions (rather than as typeclass instances) because the same CommitmentState may need to be inspected for partial properties — e.g. Theorem 33 produces a state where O_{a,b} is empty (the violation), so seriality of O is intentionally not required.

    Instances For
      source
      def Dialogue.SAL.CommitmentState.trivial {W : Type u_1} {A : Type u_2} :
      CommitmentState W A

      The trivial state where every world is doxastically accessible from every world for every agent, and similarly for commitment. All atoms are true everywhere. Useful as a baseline against which discourse updates restrict.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Dialogue.SAL.CommitmentState.commitmentEmpty {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) (a b : A) :
        Prop

        A state's commitment relation between two agents is empty when no world is accessible from any other — operationally, the agent is committed to a contradiction. This is the witness for van der Leer 2026 Definition 16 (Violation).

        Equations
        Instances For
          source
          def Dialogue.SAL.CommitmentState.restrictCommitment {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) (a b : A) (π : Set W) :
          CommitmentState W A

          Update the commitment relation between a and b to retain only those edges that point to worlds in restrict.

          Mathematical content: O^c[π]_{a,b} = O^c_{a,b} ∩ {(w, v) | v ∈ π}.

          This is the lift of van der Leer 2026 Definition 4 (commitment state update with proposition π) to the level of the underlying set of worlds. The full SAL update consumes a truth set π : Set W and restricts the commitment edges to π-worlds.

          All other relations are preserved. The frame conditions on the restricted relation are immediate from the unrestricted ones (intersection preserves transitivity/Euclideanness; we re-prove them locally for clarity).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem Dialogue.SAL.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

            Restricting commitment by π only narrows the (a,b) edge: for other pairs, the unchanged relation is recovered (the conjoined implication is vacuously true).

            source
            @[simp]
            theorem Dialogue.SAL.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

            Belief is unchanged by a commitment-restriction.

            source
            @[simp]
            theorem Dialogue.SAL.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

            The valuation is unchanged by a commitment-restriction.