Commitment Space Semantics

@cite{krifka-2015} @cite{cohen-krifka-2014}

Krifka's commitment-space framework: the discourse state is a tree — the root (√C) is the current CG holding speaker-indexed commitments S⊢φ, and continuations are proposed future states from questions.

• Assertion narrows every state with commit speaker φ.
• Monopolar questions add a commit addressee φ continuation.
• Bipolar questions add two non-contradictory sibling continuations (commit addressee φ and commit addressee ¬φ).
• High-negation questions (Didn't I win?) add a refuse addressee φ continuation, distinct from low-negation (Did I not win?) which adds commit addressee ¬φ.

Per-agent commitment slates track individual public commitments, enabling the commitment/belief separation (lying, hedging).

Speaker indexing

The paper's central primitive is the Frege turnstile S⊢φ (p. 332): assertion is responsibility-undertaking, so what enters the CG is "speaker S is committed to the truth of φ", not bare φ. The substrate uses Core.Discourse.Commitment.IndexedCommitment to model this — the root holds indexed commitments, projected to a flat context set via IndexedCommitment.toCommitment for the CG-as-set view.

Sibling files

Theories/Dialogue/LayeredAssertion.lean houses Krifka 2020's TP/JP/ComP/ActP layered-clause framework. The two files are independent (neither imports the other); study files target whichever fits.

Substrate scope

The substrate is two-role discourse with doxastic/preferential force. Out of scope (would need substrate extensions):

• Brandom-style scorecards (Brandom 1994): commitment indexed by both a keeper and a scorer (per-keeper-per-scorer scoring). The substrate's single committer : DiscourseRole is keeper-only.
• Searle's full 5-force taxonomy (assertive, directive, commissive, expressive, declaration): collapsed here to doxastic/preferential per the @cite{lauer-2013} duality. Expressives (wishes, exclamatives) and declarations (performatives) are not modelled.
• Time-indexed commitments (Lauer 2013 PB/PEP carry a t index): the substrate has no time index; rejectFirst is the closest proxy for rescission. True time-indexed commitment dynamics need a separate layer.
• Anderson 2021 distributional CG: requires weight_nonneg on the per-world weight. Hosting Anderson via CommitmentSpace W ℝ would need an [OrderedAddCommMonoid G] constraint or an Anderson wrapper — current substrate does not enforce non-negativity.

Citation discipline

Equation/page citations to @cite{krifka-2015} throughout this file (eqs. 1, 2, 3, 5, 6, 7, 9, 10, 14, 23, 27, 29, 30, 38, 39, 44, 45 with their respective pages 329-343) were verified against the SALT 25 paper PDF when added (cf. CHANGELOG entries 0.230.652–0.230.654). Flag drift on re-audit if substrate operators are renamed or restructured.

@[reducible, inline]

abbrev Dialogue.Krifka.KAgent : Type

Agent type for two-participant discourse — abbreviation for the framework-agnostic Core.Discourse.DiscourseRole. The alias name KAgent mirrors Krifka's S₁/S₂ notation; semantically it IS DiscourseRole (no separate inductive, no bridge function).

Equations

• Dialogue.Krifka.KAgent = Core.Discourse.DiscourseRole

structure Dialogue.Krifka.CommitmentSpace (W : Type u_1) (G : Type u_2) : Type (max u_1 u_2)

A commitment space (@cite{krifka-2015}, eq. (2), p. 329).

A set of commitment states organized as root + continuations:

• root (√C): the current commitment state — a list of speaker-indexed commitments S⊢φ (IndexedCommitment.commit) or refusals ¬S⊢φ (IndexedCommitment.refuse). All worlds compatible with the commit-projected propositions are "live".
• continuations: proposed future states, each extending the root with additional commitments. Added by questions, resolved by acceptance (one becomes the new root) or rejection (one is pruned).

Correspondence to Krifka's set-theoretic model

Krifka's eq. (2) p. 329: C is a commitment space if C is a set of commitment states, ∩C ≠ ∅ and ∩C ∈ C. The set of states represented by this structure is root :: continuations — root IS √C (= ∩C, always present as a state in C), and continuations are the additional non-root states. Krifka's {√C} ∪ X operands in eqs. (23) and (27) correspond to keeping root as the always-present floor while unioning state-sets into continuations. The rejectFirst operation realises Krifka's ℜ retraction (eq. 10, p. 331): pruning a proposed continuation leaves √C as the only remaining floor, which is exactly the {√C} disjunct.

Krifka's key operations

• Assert C + S⊢φ (eq. (1) and (3), p. 329): adds commit S φ to root and continuations, narrowing every state.
• Monopolar question C + ?φ (eq. (27), p. 336): {√C} ∪ (C + S₂⊢φ) — preserve root, propose addressee committing to φ.
• Bipolar question (eq. (23), p. 335): {√C} ∪ (C + S₂⊢φ) ∪ (C + S₂⊢¬φ) — two non-contradictory siblings.
• Accept: take a continuation as the new root.
• Reject: prune a continuation (= return to {√C} disjunct).

The tree structure captures the assertion/question asymmetry: assertions modify the root (the CG changes), while questions only add continuations (the CG is preserved until acceptance).

• root : List (Core.Discourse.Commitment.IndexedWeightedCommitment W G)

  Root commitment state √C: indexed commitments currently in the CG. The grade type G lets the same shape host binary (G = Prop), distributional (G = ℝ), or credence-bounded (G = ℚ) commitments.

• continuations : List (List (Core.Discourse.Commitment.IndexedWeightedCommitment W G))

  Proposed future states. Questions add these; acceptance promotes one to root. Each continuation is a list of indexed commitments that extends (narrows) the root.

def Dialogue.Krifka.CommitmentSpace.empty {W : Type u_1} {G : Type u_2} : CommitmentSpace W G

The empty commitment space: no commitments, no continuations.

Equations

• Dialogue.Krifka.CommitmentSpace.empty = { root := [], continuations := [] }

def Dialogue.Krifka.CommitmentSpace.assert {W : Type u_1} {G : Type u_2} (cs : CommitmentSpace W G) (committer : Core.Discourse.DiscourseRole) (weight : W → G) (force : Core.Discourse.Commitment.CommitmentForce := Core.Discourse.Commitment.CommitmentForce.doxastic) : CommitmentSpace W G

Assert weight weight on behalf of committer (@cite{krifka-2015}, eq. (1) and (3), p. 329).

C + S⊢φ: adds commit committer force weight to the root and to every continuation. Any accepted continuation will also entail the weight (with the speaker index recorded). The force defaults to .doxastic (Krifka's standard declarative case); pass .preferential for the @cite{lauer-2013} imperative-as-PEP case.

Equations

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

def Dialogue.Krifka.CommitmentSpace.monopolarQuestion {W : Type u_1} {G : Type u_2} (cs : CommitmentSpace W G) (weight : W → G) (force : Core.Discourse.Commitment.CommitmentForce := Core.Discourse.Commitment.CommitmentForce.doxastic) : CommitmentSpace W G

Monopolar question: propose that the addressee commit to weight weight (@cite{krifka-2015}, eq. (27), p. 336).

C + ?φ = {√C} ∪ (C + S₂⊢φ)

The root stays unchanged (CG preserved). A new continuation is added where the addressee has committed to weight. Existing continuations are also extended by the addressee-commitment. The committer is hardcoded to .addressee per Krifka's discussion of (30), p. 337: "the ? head identifies the committer as S₂".

Equations

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

def Dialogue.Krifka.CommitmentSpace.negatedQuestionHigh {W : Type u_1} {G : Type u_2} (cs : CommitmentSpace W G) (φ : W → Prop) (force : Core.Discourse.Commitment.CommitmentForce := Core.Discourse.Commitment.CommitmentForce.doxastic) : CommitmentSpace W G

High-negation polar question (@cite{krifka-2015}, §4 around eq. (39), p. 340).

Didn't I win? = monopolar question with negation at the ComP layer (denegation of the addressee's commitment to φ). Proposes that the addressee NOT commit to φ — pragmatically weaker than committing to ¬φ.

Polymorphic in G: the refuse constructor's content is always W → Prop (a meta-fact about the agent's slate, not a graded weight), so this operator works for any grade type.

Per @cite{krifka-2015} p. 340: "adding ¬S₂⊢φ to the commitment space precludes commitment to φ, but is compatible with commitment to ¬φ. Hence ¬S₂⊢φ is pragmatically weaker than S₂⊢¬φ."

Equations

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

def Dialogue.Krifka.CommitmentSpace.hasNoOpenContinuations {W : Type u_1} {G : Type u_2} : CommitmentSpace W G → Prop

The space has no open continuations (no unresolved proposals).

Renamed from isSettled — Krifka has no stability/settledness notion in the paper; questions just "restrict legal continuations" (p. 335). The right characterization of this state is structural, not pragmatic.

Equations

• { root := root, continuations := [] }.hasNoOpenContinuations = True
• { root := root, continuations := head :: tail }.hasNoOpenContinuations = False

@[implicit_reducible]

instance Dialogue.Krifka.CommitmentSpace.instDecidablePredHasNoOpenContinuations {W : Type u_1} {G : Type u_2} : DecidablePred hasNoOpenContinuations

Equations

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

def Dialogue.Krifka.CommitmentSpace.acceptFirst {W : Type u_1} {G : Type u_2} : CommitmentSpace W G → CommitmentSpace W G

Accept the first continuation: it becomes the new root. The CG is updated to the accepted proposal's content.

Equations

• { root := root, continuations := c :: rest }.acceptFirst = { root := c, continuations := rest }
• x✝.acceptFirst = x✝

def Dialogue.Krifka.CommitmentSpace.rejectFirst {W : Type u_1} {G : Type u_2} : CommitmentSpace W G → CommitmentSpace W G

Reject the first continuation: prune it. The CG is unchanged; the proposal is discarded.

Equations

• { root := root, continuations := c :: rest }.rejectFirst = { root := root, continuations := rest }
• x✝.rejectFirst = x✝

def Dialogue.Krifka.CommitmentSpace.denegate {W : Type u_1} {G : Type u_2} (actMarker : Core.Discourse.Commitment.IndexedWeightedCommitment W G → Prop) [DecidablePred actMarker] (cs : CommitmentSpace W G) : CommitmentSpace W G

Denegate a speech act ~A. Originally introduced by @cite{cohen-krifka-2014} §2 (around eq. (26), p. 51, with full development through eqs. 31–38, pp. 52–53); inherited by @cite{krifka-2015} eq. (5), p. 330.

C + ~A = C — [C + A]: the result keeps √C and prunes the legal continuations that would arise from performing the act A. The caller supplies a Prop-valued predicate actMarker identifying the commitment that A would add to continuations, plus a DecidablePred instance for the filter. We keep continuations that do NOT contain a matching commitment.

Concrete example: denegate cs (fun ic => ic matches ASSERT(speaker, doxastic, φ)) is ~ASSERT(φ) — the GRANT(¬φ) of @cite{cohen-krifka-2014} eq. (38).

Polymorphic in G. The predicate-based formulation avoids the soundness issue of trying to decide equality on W → G (generally undecidable for infinite W).

Equations

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

@[simp]

theorem Dialogue.Krifka.CommitmentSpace.denegate_preserves_root {W : Type u_1} {G : Type u_2} (cs : CommitmentSpace W G) (actMarker : Core.Discourse.Commitment.IndexedWeightedCommitment W G → Prop) [DecidablePred actMarker] : (denegate actMarker cs).root = cs.root

Denegation preserves the root (CG unchanged) — Krifka 2015 p. 330: "denegation does not change the root of the commitment space, but prunes its legal developments."

theorem Dialogue.Krifka.CommitmentSpace.denegate_idempotent {W : Type u_1} {G : Type u_2} (cs : CommitmentSpace W G) (actMarker : Core.Discourse.Commitment.IndexedWeightedCommitment W G → Prop) [DecidablePred actMarker] : denegate actMarker (denegate actMarker cs) = denegate actMarker cs

Denegation is idempotent: filtering twice with the same marker is the same as filtering once (List.filter_filter over the same predicate). Worth noting because Krifka's set-difference semantics has the same property: (C - X) - X = C - X.

theorem Dialogue.Krifka.CommitmentSpace.denegate_continuation_count_le {W : Type u_1} {G : Type u_2} (cs : CommitmentSpace W G) (actMarker : Core.Discourse.Commitment.IndexedWeightedCommitment W G → Prop) [DecidablePred actMarker] : (denegate actMarker cs).continuations.length ≤ cs.continuations.length

Denegation never grows the continuation list — List.filter is length-monotone.

theorem Dialogue.Krifka.CommitmentSpace.denegate_no_match_eq_self {W : Type u_1} {G : Type u_2} (cs : CommitmentSpace W G) (actMarker : Core.Discourse.Commitment.IndexedWeightedCommitment W G → Prop) [DecidablePred actMarker] (h : ∀ cont ∈ cs.continuations, ¬∃ ic ∈ cont, actMarker ic) : denegate actMarker cs = cs

If no continuation matches the marker, denegation is the identity. The substrate-level form of "you can only denegate what's actually in play".

theorem Dialogue.Krifka.CommitmentSpace.denegate_surviving_no_match {W : Type u_1} {G : Type u_2} (cs : CommitmentSpace W G) (actMarker : Core.Discourse.Commitment.IndexedWeightedCommitment W G → Prop) [DecidablePred actMarker] (cont : List (Core.Discourse.Commitment.IndexedWeightedCommitment W G)) : cont ∈ (denegate actMarker cs).continuations → ¬∃ ic ∈ cont, actMarker ic

Converse of denegate_no_match_eq_self: every continuation that SURVIVES denegation does not match the marker. The structural fact that justifies calling denegate "filtering out matching paths".

Polymorphic operators via [CommitmentGrade G]

The following operators are polymorphic in G via the CommitmentGrade typeclass (Core/Discourse/Commitment.lean §4): bipolarQuestion and negatedQuestionLow use complement to construct the "no" branch; toContextSet and the force-aware variants use support to project per-world weights to Prop.

Instances are provided for G = Prop (complement := Not, support := id) and G = Bool (complement := !, support := (· = true)). For other G (ℚ, ℝ), provide the instance at the consumer's site.

def Dialogue.Krifka.CommitmentSpace.bipolarQuestion {W : Type u_1} {G : Type u_2} [Core.Discourse.Commitment.CommitmentGrade G] (cs : CommitmentSpace W G) (φ : W → G) : CommitmentSpace W G

Bipolar question: propose two sibling continuations, one where the addressee commits to φ and one where the addressee commits to complement φ (@cite{krifka-2015}, eq. (23), p. 335).

C + ?φ_bi = {√C} ∪ (C + S₂⊢φ) ∪ (C + S₂⊢¬φ)

Polymorphic in G via [CommitmentGrade G]'s complement.

Equations

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

def Dialogue.Krifka.CommitmentSpace.negatedQuestionLow {W : Type u_1} {G : Type u_2} [Core.Discourse.Commitment.CommitmentGrade G] (cs : CommitmentSpace W G) (φ : W → G) : CommitmentSpace W G

Low-negation polar question (@cite{krifka-2015}, §4 around eq. (29), p. 339).

Did I not win? = monopolar question with complement φ as TP content. Proposes that the addressee commit to ¬φ. Polymorphic in G via [CommitmentGrade G]'s complement.

Equations

• cs.negatedQuestionLow φ = cs.monopolarQuestion fun (w : W) => Core.Discourse.Commitment.CommitmentGrade.complement (φ w)

def Dialogue.Krifka.CommitmentSpace.toContextSet {W : Type u_1} {G : Type u_2} [Core.Discourse.Commitment.HasSupport G] (cs : CommitmentSpace W G) : Core.CommonGround.ContextSet W

Context set from root: worlds compatible with all root commitments, projected via IndexedWeightedCommitment.toCommitment (which uses the typeclass's support predicate per-grade-value).

Conflates doxastic and preferential commitments — both narrow the context set. For force-aware projections that separate the two attitudes (per @cite{condoravdi-lauer-2012}), use toDoxasticContextSet / toPreferentialContextSet.

Equations

• cs.toContextSet w = ∀ ic ∈ cs.root, ic.toCommitment w

def Dialogue.Krifka.CommitmentSpace.toDoxasticContextSet {W : Type u_1} {G : Type u_2} [Core.Discourse.Commitment.HasSupport G] (cs : CommitmentSpace W G) : Core.CommonGround.ContextSet W

Doxastic-only context set: worlds compatible with the root's force = .doxastic commitments only (preferential commitments are ignored).

Models @cite{condoravdi-lauer-2012}'s PB_w(Sp, p) projection: "the public BELIEFS the speaker is committed to". A declarative assertion contributes here; an imperative utterance does not.

Equations

• cs.toDoxasticContextSet w = ∀ ic ∈ cs.root, ic.force = Core.Discourse.Commitment.CommitmentForce.doxastic → ic.toCommitment w

def Dialogue.Krifka.CommitmentSpace.toPreferentialContextSet {W : Type u_1} {G : Type u_2} [Core.Discourse.Commitment.HasSupport G] (cs : CommitmentSpace W G) : Core.CommonGround.ContextSet W

Preferential-only context set: worlds compatible with the root's force = .preferential commitments only (doxastic commitments are ignored).

Models @cite{condoravdi-lauer-2012}'s PEP_w(Sp, p) projection: "the public PREFERENCES the speaker is committed to act on". An imperative utterance contributes here; a declarative assertion does not. The two projections are independent (Lauer 2013 Ch. 5 closure (5.33b) pep(p) ∈ PB ⟺ p ∈ PEP is a HIGHER-ORDER interaction not modeled by these flat projections).

Equations

• cs.toPreferentialContextSet w = ∀ ic ∈ cs.root, ic.force = Core.Discourse.Commitment.CommitmentForce.preferential → ic.toCommitment w

theorem Dialogue.Krifka.CommitmentSpace.toContextSet_eq_doxastic_and_preferential {W : Type u_1} {G : Type u_2} [Core.Discourse.Commitment.HasSupport G] (cs : CommitmentSpace W G) (w : W) : cs.toContextSet w ↔ cs.toDoxasticContextSet w ∧ cs.toPreferentialContextSet w

Sanity: the conflated toContextSet is the conjunction of the two force-projections. (refuse cases project to True regardless of force, so the doxastic and preferential projections agree on them.)

Theorems

theorem Dialogue.Krifka.CommitmentSpace.empty_no_open {W : Type u_1} {G : Type u_2} : empty.hasNoOpenContinuations

Empty space has no open continuations.

theorem Dialogue.Krifka.CommitmentSpace.assert_preserves_no_open {W : Type u_1} {G : Type u_2} (cs : CommitmentSpace W G) (_s : Core.Discourse.DiscourseRole) (_weight : W → G) (h : cs.hasNoOpenContinuations) : (cs.assert _s _weight).hasNoOpenContinuations

Assertion preserves the no-open-continuations property (no new continuations are added by assert).

theorem Dialogue.Krifka.CommitmentSpace.monopolar_opens {W : Type u_1} {G : Type u_2} (cs : CommitmentSpace W G) (_weight : W → G) (h : cs.hasNoOpenContinuations) : ¬(cs.monopolarQuestion _weight).hasNoOpenContinuations

Monopolar question creates an open continuation (negation of the no-open property).

theorem Dialogue.Krifka.CommitmentSpace.accept_monopolar_closes {W : Type u_1} {G : Type u_2} (cs : CommitmentSpace W G) (weight : W → G) (h : cs.hasNoOpenContinuations) : (cs.monopolarQuestion weight).acceptFirst.hasNoOpenContinuations

Accepting a monopolar question's sole continuation re-closes the space.

theorem Dialogue.Krifka.CommitmentSpace.assert_in_root {W : Type u_1} (cs : CommitmentSpace W Prop) (s : Core.Discourse.DiscourseRole) (φ : W → Prop) : Core.Discourse.Commitment.IndexedCommitment.commit s φ ∈ (cs.assert s φ).root

Root after assertion (binary case) contains the asserted indexed commitment.

@[simp]

theorem Dialogue.Krifka.CommitmentSpace.monopolarQuestion_preserves_root {W : Type u_1} {G : Type u_2} (cs : CommitmentSpace W G) (weight : W → G) : (cs.monopolarQuestion weight).root = cs.root

Monopolar question preserves the root (CG unchanged).

@[simp]

theorem Dialogue.Krifka.CommitmentSpace.bipolarQuestion_preserves_root {W : Type u_1} {G : Type u_2} [Core.Discourse.Commitment.CommitmentGrade G] (cs : CommitmentSpace W G) (φ : W → G) : (cs.bipolarQuestion φ).root = cs.root

Bipolar question preserves the root (CG unchanged).

structure Dialogue.Krifka.KrifkaState (W : Type u_1) : Type u_1

Krifka's discourse state: per-agent commitment slates + shared commitment space (tree).

The commitment space tracks the shared discourse structure: what's in the CG (root) and what's been proposed (continuations). Per-agent slates track individual public commitments, enabling the commitment/belief separation central to Krifka's theory.

• speakerCS : Core.Discourse.Commitment.CommitmentSlate W

  Speaker's individual commitment slate (binary, propositional).

• addresseeCS : Core.Discourse.Commitment.CommitmentSlate W

  Addressee's individual commitment slate.

• space : CommitmentSpace W Prop

  Shared commitment space (tree): CG + proposed updates. Binary specialisation CommitmentSpace W Prop of the polymorphic CommitmentSpace W G. Future graded-state extensions (Lauer-credence, Anderson-distributional) belong in a separate WeightedKrifkaState W G rather than here.

def Dialogue.Krifka.KrifkaState.empty {W : Type u_1} : KrifkaState W

Initial state: no commitments, empty space.

Equations

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

def Dialogue.Krifka.KrifkaState.assert {W : Type u_1} (s : KrifkaState W) (p : W → Prop) (committer : Core.Discourse.DiscourseRole := Core.Discourse.DiscourseRole.speaker) (force : Core.Discourse.Commitment.CommitmentForce := Core.Discourse.Commitment.CommitmentForce.doxastic) : KrifkaState W

Krifka's commitment operator +_S₁ S₁⊢p (@cite{krifka-2015}, eq. (14), p. 332).

Speaker (default) commits to p, narrowing the entire space and recording on the speaker's slate. Pass committer := .addressee for the addressee-commits case. The force defaults to .doxastic (declarative assertion); pass .preferential for the @cite{condoravdi-lauer-2012} imperative-as-PEP analysis.

Equations

• One or more equations did not get rendered due to their size.
• s.assert p Core.Discourse.DiscourseRole.speaker force = { speakerCS := s.speakerCS.add p, addresseeCS := s.addresseeCS, space := s.space.assert Core.Discourse.DiscourseRole.speaker p force }

def Dialogue.Krifka.KrifkaState.monopolarQuestion {W : Type u_1} (s : KrifkaState W) (φ : W → Prop) : KrifkaState W

Monopolar question (@cite{krifka-2015}, eq. (27), p. 336): speaker proposes that addressee commit to φ.

Equations

• s.monopolarQuestion φ = { speakerCS := s.speakerCS, addresseeCS := s.addresseeCS, space := s.space.monopolarQuestion φ }

def Dialogue.Krifka.KrifkaState.bipolarQuestion {W : Type u_1} (s : KrifkaState W) (φ : W → Prop) : KrifkaState W

Bipolar question (@cite{krifka-2015}, eq. (23), p. 335): propose two sibling continuations (φ-commit and ¬φ-commit).

Equations

• s.bipolarQuestion φ = { speakerCS := s.speakerCS, addresseeCS := s.addresseeCS, space := s.space.bipolarQuestion φ }

def Dialogue.Krifka.KrifkaState.negatedQuestionLow {W : Type u_1} (s : KrifkaState W) (φ : W → Prop) : KrifkaState W

Low-negation polar question (@cite{krifka-2015}, §4): Did I not win?.

Equations

• s.negatedQuestionLow φ = { speakerCS := s.speakerCS, addresseeCS := s.addresseeCS, space := s.space.negatedQuestionLow φ }

def Dialogue.Krifka.KrifkaState.negatedQuestionHigh {W : Type u_1} (s : KrifkaState W) (φ : W → Prop) : KrifkaState W

High-negation polar question (@cite{krifka-2015}, §4): Didn't I win?.

Equations

• s.negatedQuestionHigh φ = { speakerCS := s.speakerCS, addresseeCS := s.addresseeCS, space := s.space.negatedQuestionHigh φ }

def Dialogue.Krifka.KrifkaState.acceptContinuation {W : Type u_1} (s : KrifkaState W) : KrifkaState W

Accept the first continuation: it becomes the new CG root.

Equations

• s.acceptContinuation = { speakerCS := s.speakerCS, addresseeCS := s.addresseeCS, space := s.space.acceptFirst }

def Dialogue.Krifka.KrifkaState.rejectContinuation {W : Type u_1} (s : KrifkaState W) : KrifkaState W

Reject the first continuation: prune it.

Equations

• s.rejectContinuation = { speakerCS := s.speakerCS, addresseeCS := s.addresseeCS, space := s.space.rejectFirst }

def Dialogue.Krifka.KrifkaState.contextSet {W : Type u_1} (s : KrifkaState W) : Core.CommonGround.ContextSet W

Context set: from the commitment space root (= CG), via IndexedCommitment.toCommitment projection.

Equations

• s.contextSet = s.space.toContextSet

def Dialogue.Krifka.KrifkaState.hasNoOpenContinuations {W : Type u_1} (s : KrifkaState W) : Prop

The space has no open continuations.

Equations

• s.hasNoOpenContinuations = s.space.hasNoOpenContinuations

@[implicit_reducible]

instance Dialogue.Krifka.KrifkaState.instDecidablePredHasNoOpenContinuations {W : Type u_1} : DecidablePred hasNoOpenContinuations

Equations

• s.instDecidablePredHasNoOpenContinuations = Dialogue.Krifka.KrifkaState.instDecidablePredHasNoOpenContinuations._aux_1 s

theorem Dialogue.Krifka.commitment_closure {W : Type u_1} (s : KrifkaState W) (p : W → Prop) (committer : Core.Discourse.DiscourseRole) : (s.assert p committer).space.root = Core.Discourse.Commitment.IndexedCommitment.commit committer p :: s.space.root

Commitment Closure: assertion immediately narrows the commitment space. The root after asserting φ on behalf of committer is the original root with the indexed commit committer φ prepended.

In the tree model, this is definitional: assert adds the indexed commitment to all nodes including the root.

theorem Dialogue.Krifka.monopolarQuestion_preserves_cg {W : Type u_1} (s : KrifkaState W) (p : W → Prop) : (s.monopolarQuestion p).space.root = s.space.root

Questions don't change the CG: the root is preserved.

theorem Dialogue.Krifka.monopolarQuestion_accept_eq_assert_addressee_root {W : Type u_1} (s : KrifkaState W) (p : W → Prop) (h : s.space.hasNoOpenContinuations) : (s.monopolarQuestion p).acceptContinuation.space.root = (s.assert p Core.Discourse.DiscourseRole.addressee).space.root

Question then accept ≈ assert (on the root): accepting a monopolar question's sole continuation yields the same CG as the addressee directly asserting φ.

This connects the two modes of updating: direct assertion (committer imposes) and question-then-accept (speaker proposes, addressee accepts by committing themselves). The roots match because both produce commit .addressee φ :: root₀.

structure Dialogue.Krifka.ActorCommitter : Type

The two discourse roles in a speech act.

Every speech act has an actor (who performs the act) and a committer (who undertakes the commitment). These can diverge:

• Assertion: actor = speaker, committer = speaker
• Monopolar question: actor = speaker, committer = addressee (the speaker proposes that the addressee commit)

Per @cite{krifka-2015} p. 337 around eq. (30): the ? ActP head identifies the committer as S₂, the addressee; the actor of the speech act itself remains S₁.

• actor : KAgent
• committer : KAgent

@[implicit_reducible]

instance Dialogue.Krifka.instDecidableEqActorCommitter : DecidableEq ActorCommitter

Equations

• Dialogue.Krifka.instDecidableEqActorCommitter = Dialogue.Krifka.instDecidableEqActorCommitter.decEq

def Dialogue.Krifka.instDecidableEqActorCommitter.decEq (x✝ x✝¹ : ActorCommitter) : Decidable (x✝ = x✝¹)

Equations

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

def Dialogue.Krifka.instReprActorCommitter.repr : ActorCommitter → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Dialogue.Krifka.instReprActorCommitter : Repr ActorCommitter

Equations

• Dialogue.Krifka.instReprActorCommitter = { reprPrec := Dialogue.Krifka.instReprActorCommitter.repr }

def Dialogue.Krifka.assertionRoles : ActorCommitter

In assertions, speaker is both actor and committer.

Equations

• Dialogue.Krifka.assertionRoles = { actor := Core.Discourse.DiscourseRole.speaker, committer := Core.Discourse.DiscourseRole.speaker }

def Dialogue.Krifka.questionRoles : ActorCommitter

In monopolar questions, speaker acts but addressee commits (@cite{krifka-2015}, p. 337 discussion of eq. (30)).

Equations

• Dialogue.Krifka.questionRoles = { actor := Core.Discourse.DiscourseRole.speaker, committer := Core.Discourse.DiscourseRole.addressee }

theorem Dialogue.Krifka.actor_committer_diverge : assertionRoles.actor = questionRoles.actor ∧ assertionRoles.committer ≠ questionRoles.committer

Assertions and questions differ in who commits.

structure Dialogue.Krifka.SpeechAct (W : Type u_1) : Type u_1

A speech act in Krifka's framework: ActP content with its discourse function (assertion vs question).

@cite{krifka-2015} clause structure: ActP > ComP > TP (three layers). @cite{krifka-2020} refines this to ActP > ComP > JP > TP.

• content : W → Prop

  Propositional content (TP layer)

• actType : Core.Mood.IllocutionaryMood

  Speech act type: assertion (.) or question (?)

• roles : ActorCommitter

  Actor/committer assignment

def Dialogue.Krifka.monopolarQuestionAct {W : Type u_1} (φ : W → Prop) : SpeechAct W

Construct a monopolar question speech act (@cite{krifka-2015}, eq. (27), p. 336): proposes a single continuation where the addressee commits to φ.

Equations

• Dialogue.Krifka.monopolarQuestionAct φ = { content := φ, actType := Core.Mood.IllocutionaryMood.interrogative, roles := Dialogue.Krifka.questionRoles }

inductive Dialogue.Krifka.ComplexSpeechAct (W : Type u_1) : Type u_1

Complex speech act: conjunction or disjunction of atomic acts (@cite{krifka-2015}, eqs. (6)–(7), p. 330).

@cite{krifka-2015}, §5: question tags involve composition of speech acts. The difference between matching and reverse tags is conjunction vs disjunction:

• conj: both acts performed as one complex move (matching tag, eq. (44), p. 342)
• disj: addressee chooses one continuation (reverse tag, eq. (45), p. 343)

• atom {W : Type u_1} : SpeechAct W → ComplexSpeechAct W

  A single speech act.

• conj {W : Type u_1} : SpeechAct W → SpeechAct W → ComplexSpeechAct W

  Conjunction: both acts as one complex move (eq. (6), p. 330). "I have won the race, have I?" = ASSERT(rain) & ASK(rain).

• disj {W : Type u_1} : SpeechAct W → SpeechAct W → ComplexSpeechAct W

  Disjunction: offer alternative continuations (eq. (7), p. 330). "I have won the race, haven't I?" = ASSERT(φ) ∨ ASK(¬φ).

def Dialogue.Krifka.ComplexSpeechAct.components {W : Type u_1} : ComplexSpeechAct W → List (SpeechAct W)

Extract the component speech acts from a complex speech act.

Equations

• (Dialogue.Krifka.ComplexSpeechAct.atom a).components = [a]
• (Dialogue.Krifka.ComplexSpeechAct.conj a b).components = [a, b]
• (Dialogue.Krifka.ComplexSpeechAct.disj a b).components = [a, b]

def Dialogue.Krifka.matchingTag {W : Type u_1} (φ : W → Prop) : ComplexSpeechAct W

A matching question tag (@cite{krifka-2015}, eq. (44), p. 342): conjunction of assertion + monopolar question with same content.

"I have won the race, have I?" = speaker asserts φ AND asks addressee to confirm. Per Krifka p. 342: "this is not a move in which the speaker first makes an assertion and then asks the addressee to make the same assertion. Rather, the two speech acts are first conjoined, and then applied as one complex speech act to the commitment space."

The committers diverge: speaker for the assertion-leg, addressee for the question-leg.

Equations

• Dialogue.Krifka.matchingTag φ = Dialogue.Krifka.ComplexSpeechAct.conj { content := φ } (Dialogue.Krifka.monopolarQuestionAct φ)

def Dialogue.Krifka.reverseTag {W : Type u_1} (φ negφ : W → Prop) : ComplexSpeechAct W

A reverse question tag (@cite{krifka-2015}, eq. (45), p. 343): disjunction of assertion + monopolar question with opposite content.

"I have won the race, haven't I?" = speaker offers two continuations. The addressee picks one.

Equations

• Dialogue.Krifka.reverseTag φ negφ = Dialogue.Krifka.ComplexSpeechAct.disj { content := φ } (Dialogue.Krifka.monopolarQuestionAct negφ)

theorem Dialogue.Krifka.matching_tag_shared_content {W : Type u_1} (φ : W → Prop) : List.map SpeechAct.content (matchingTag φ).components = [φ, φ]

In a matching tag, the assertion and question share content.

theorem Dialogue.Krifka.matching_tag_same_actor {W : Type u_1} (φ : W → Prop) : List.map (fun (x : SpeechAct W) => x.roles.actor) (matchingTag φ).components = [Core.Discourse.DiscourseRole.speaker, Core.Discourse.DiscourseRole.speaker]

In a matching tag, the speaker is actor in both acts.

theorem Dialogue.Krifka.matching_tag_committers_diverge {W : Type u_1} (φ : W → Prop) : List.map (fun (x : SpeechAct W) => x.roles.committer) (matchingTag φ).components = [Core.Discourse.DiscourseRole.speaker, Core.Discourse.DiscourseRole.addressee]

In a matching tag, the committers differ: speaker for assertion, addressee for question.

theorem Dialogue.Krifka.tag_type_distinction {W : Type u_1} (φ negφ : W → Prop) : (∃ (a : SpeechAct W) (b : SpeechAct W), matchingTag φ = ComplexSpeechAct.conj a b) ∧ ∃ (a : SpeechAct W) (b : SpeechAct W), reverseTag φ negφ = ComplexSpeechAct.disj a b

Matching tags are conjunctions, reverse tags are disjunctions.

def Dialogue.Krifka.KrifkaState.applyAtom {W : Type u_1} (s : KrifkaState W) (a : SpeechAct W) : KrifkaState W

Apply a single atomic speech act, dispatching on actType and roles.committer to the right operator.

Equations

• s.applyAtom a = match a.actType with | Core.Mood.IllocutionaryMood.interrogative => s.monopolarQuestion a.content | x => s.assert a.content a.roles.committer

def Dialogue.Krifka.KrifkaState.applyComplex {W : Type u_1} (s : KrifkaState W) : ComplexSpeechAct W → KrifkaState W

Apply a complex speech act to a Krifka state.

For .conj a b: per Krifka eq. (6), [C + 𝔄 & 𝔅] = [C + 𝔄] ∩ [C + 𝔅] ≈ C + 𝔄 + 𝔅 ≈ C + 𝔅 + 𝔄 — sequential composition is the paper's own approximation when there are no anaphoric ties. We compose sequentially.

For .disj a b: speech-act disjunction (eq. (7), p. 330) is [C + 𝔄] ∪ [C + 𝔅] on commitment-space sets; the union of two list-shaped continuation structures is non-trivial and may produce a non-rooted space (per Krifka's prose on Figure 5, p. 330). Left as sorry to avoid silently returning a wrong answer. Reverse-tag worked examples are blocked on this; the structural theorem reverse_tag_is_disjunction does not depend on applyComplex.

Equations

• s.applyComplex (Dialogue.Krifka.ComplexSpeechAct.atom a) = s.applyAtom a
• s.applyComplex (Dialogue.Krifka.ComplexSpeechAct.conj a b) = (s.applyAtom a).applyAtom b
• s.applyComplex (Dialogue.Krifka.ComplexSpeechAct.disj a b) = sorry

@[implicit_reducible]

instance Dialogue.Krifka.instHasContextSetCommitmentSpaceOfHasSupport {W : Type u_1} {G : Type u_2} [Core.Discourse.Commitment.HasSupport G] : Core.CommonGround.HasContextSet (CommitmentSpace W G) W

A polymorphic commitment space projects to a context set via its root, using the [HasSupport G] typeclass's support projection. Recovers the binary case at G = Prop definitionally (via support := id in the Prop instance). Anderson 2021's distributional CG (G = ℝ) becomes a consumer via HasSupport ℝ provided in Anderson2021.lean.

Equations

• Dialogue.Krifka.instHasContextSetCommitmentSpaceOfHasSupport = { toContextSet := Dialogue.Krifka.CommitmentSpace.toContextSet }

@[implicit_reducible]

instance Dialogue.Krifka.instHasContextSetKrifkaState {W : Type u_1} : Core.CommonGround.HasContextSet (KrifkaState W) W

A Krifka state projects to a context set via the commitment space root.

Equations

• Dialogue.Krifka.instHasContextSetKrifkaState = { toContextSet := Dialogue.Krifka.KrifkaState.contextSet }

theorem Dialogue.Krifka.krifkaState_contextSet_eq_space {W : Type u_1} (s : KrifkaState W) : Core.CommonGround.HasContextSet.toContextSet s = Core.CommonGround.HasContextSet.toContextSet s.space

KrifkaState context set agrees with CommitmentSpace context set.