Bias in Commitment Space Semantics #

@cite{krifka-2015} @cite{cohen-krifka-2014} @cite{ginzburg-2012} @cite{bring-gunlogson-2000}

Worked examples exercising the commitment-space framework of @cite{krifka-2015} ("Bias in Commitment Space Semantics: Declarative questions, negated questions, and question tags"). Each worked example uses a 2-world Weather model and verifies a specific paper claim.

Coverage #

§1 — 2-world model fixture
§2 — Assertion (paper §2): speaker-indexed commitment lands in root
§3 — Monopolar vs bipolar polar questions (paper §3, eqs. 23, 27): bipolar produces two non-contradictory siblings, NOT a stacked pair of monopolars
§4 — Negated polar questions (paper §4, eqs. 38–39, Table 1 p. 341): low-neg = commit addressee ¬φ, high-neg = refuse addressee φ, pragmatically weaker than low-neg
§5 — Question tags (paper §5, eqs. 44–45): matching = conjunction, reverse = disjunction, NOT sequential composition
§N — Reciprocal cross-framework contrasts: - vs @cite{ginzburg-2012} KOS (per Phenomena/Dialogue/Studies/Ginzburg2012.lean lines 49–52, which delegates Krifka contrasts here) - vs @cite{farkas-bruce-2010} discourse-table model. Krifka §1 (paper p. 331) cites F&B as the inspiration for his rejection operator ℜ; this section makes the structural relationship Lean-checkable.
§∞ — Deep structure: the Dialogue Completeness observation — framework-agnostic agreement on observable CG at completed traces.

Out of scope (explicit) #

Speech-act denegation ~𝔄 (paper §1, eq. 5) — substrate gained the denegate operator at 0.230.656. The first consumer is Phenomena/Assertion/Studies/CohenKrifka2014.lean (anchored on the prior @cite{cohen-krifka-2014} introduction of denegation). This file could now exercise denegation but doesn't need to for the §§1–5 scope; reverse-tag worked examples are blocked on a separate applyComplex .disj substrate gap.
JP/ComP layered clause structure — that's @cite{krifka-2020} material; see Phenomena/Assertion/Studies/Krifka2020.lean.
Cross-framework contrasts with Stalnaker, Brandom, Lauer, Gunlogson, Inquisitive Semantics. Future work; substrates are present.

source

inductive Phenomena.Assertion.Studies.Krifka2015.Weather :

Type

Two-world model: it's raining or it's not. Used by all sections, including the cross-framework contrast (no second world type).

rain : Weather
noRain : Weather

Instances For

source

@[implicit_reducible]

instance Phenomena.Assertion.Studies.Krifka2015.instDecidableEqWeather :

DecidableEq Weather

Equations

Phenomena.Assertion.Studies.Krifka2015.instDecidableEqWeather x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Phenomena.Assertion.Studies.Krifka2015.instReprWeather.repr :

Weather → ℕ → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance Phenomena.Assertion.Studies.Krifka2015.instReprWeather :

Repr Weather

Equations

Phenomena.Assertion.Studies.Krifka2015.instReprWeather = { reprPrec := Phenomena.Assertion.Studies.Krifka2015.instReprWeather.repr }

source

def Phenomena.Assertion.Studies.Krifka2015.isRaining :

Weather → Prop

Proposition: it's raining.

Equations

Instances For

source

def Phenomena.Assertion.Studies.Krifka2015.isNotRaining :

Weather → Prop

Proposition: it's NOT raining.

Equations

Instances For

source

def Phenomena.Assertion.Studies.Krifka2015.s₀ :

Dialogue.Krifka.KrifkaState Weather

Initial discourse state: empty commitments, no open continuations.

Equations

Phenomena.Assertion.Studies.Krifka2015.s₀ = Dialogue.Krifka.KrifkaState.empty

Instances For

source

theorem Phenomena.Assertion.Studies.Krifka2015.assert_root_eq :

(s₀.assert isRaining).space.root = [Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.speaker isRaining]

After asserting "it's raining", the root contains the speaker-indexed commitment S₁⊢φ — NOT bare φ. This is the central content of @cite{krifka-2015} eq. (14): ⟨..., C*⟩ +^S₁ S₁⊢φ = ⟨..., C*, [C + S₁⊢φ]^S₁⟩.

source

theorem Phenomena.Assertion.Studies.Krifka2015.assert_speakerCS_records :

(s₀.assert isRaining).speakerCS.commitments = [isRaining]

The speaker's commitment slate records the assertion.

source

theorem Phenomena.Assertion.Studies.Krifka2015.assert_addresseeCS_unchanged :

(s₀.assert isRaining).addresseeCS.commitments = []

The addressee's slate is unchanged (they haven't accepted yet).

source

theorem Phenomena.Assertion.Studies.Krifka2015.assert_no_open_continuations :

(s₀.assert isRaining).hasNoOpenContinuations

Assertion adds no continuations to a previously-empty space.

source

theorem Phenomena.Assertion.Studies.Krifka2015.assert_by_addressee_root_eq :

(s₀.assert isRaining Core.Discourse.DiscourseRole.addressee).space.root = [Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.addressee isRaining]

Assertion-by-addressee (the Yes-as-acceptance path) lands the indexed commitment with .addressee as committer.

source

theorem Phenomena.Assertion.Studies.Krifka2015.monopolar_root_unchanged :

(s₀.monopolarQuestion isRaining).space.root = []

Monopolar question preserves the root (CG unchanged) — paper p. 335.

source

theorem Phenomena.Assertion.Studies.Krifka2015.monopolar_continuations_length_eq_one :

(s₀.monopolarQuestion isRaining).space.continuations.length = 1

Monopolar question adds exactly one continuation.

source

theorem Phenomena.Assertion.Studies.Krifka2015.monopolar_continuation_committer_eq_addressee :

(s₀.monopolarQuestion isRaining).space.continuations = [[Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.addressee isRaining]]

The continuation's commitment is by the addressee, not the speaker (paper p. 337 around eq. 30: "the ? head identifies the committer as S₂").

source

theorem Phenomena.Assertion.Studies.Krifka2015.bipolar_root_unchanged :

(s₀.bipolarQuestion isRaining).space.root = []

Bipolar question preserves the root (paper eq. 23).

source

theorem Phenomena.Assertion.Studies.Krifka2015.bipolar_continuations_length_eq_two :

(s₀.bipolarQuestion isRaining).space.continuations.length = 2

Bipolar question adds exactly two sibling continuations (paper eq. 23, Figure 8 p. 335).

source

theorem Phenomena.Assertion.Studies.Krifka2015.bipolar_continuations_eq :

∃ (φ : Weather → Prop) (ψ : Weather → Prop), (s₀.bipolarQuestion isRaining).space.continuations = [[Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.addressee φ], [Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.addressee ψ]] ∧ φ = isRaining ∧ ∀ (w : Weather), ψ w ↔ ¬isRaining w

The bipolar continuations are commit addressee φ and commit addressee ¬φ — both indexed to the addressee.

This is the bug-fix theorem: the deleted Krifka2015.lean modeled "bipolar" as two stacked monopolar questions, producing a contradictory continuation [¬φ, φ]. The faithful Krifka eq. 23 derivation gives two SEPARATE alternatives, neither of which contains both φ and ¬φ.

source

theorem Phenomena.Assertion.Studies.Krifka2015.bipolar_continuations_not_internally_contradictory (cont : List (Core.Discourse.Commitment.IndexedWeightedCommitment Weather Prop)) :

cont ∈ (s₀.bipolarQuestion isRaining).space.continuations → cont.length = 1

Neither bipolar continuation is internally contradictory: each is a singleton list, so it cannot contain both φ and ¬φ.

source

theorem Phenomena.Assertion.Studies.Krifka2015.accept_monopolar_root_eq :

(s₀.monopolarQuestion isRaining).acceptContinuation.space.root = [Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.addressee isRaining]

Accepting a monopolar question's continuation puts the addressee-indexed commitment in the root. The pathway models the Yes confirmation: addressee commits to φ.

source

theorem Phenomena.Assertion.Studies.Krifka2015.monopolarQuestion_accept_eq_assert_addressee :

(s₀.monopolarQuestion isRaining).acceptContinuation.space.root = (s₀.assert isRaining Core.Discourse.DiscourseRole.addressee).space.root

Bridge: acceptContinuation ∘ monopolarQuestion φ and assert φ .addressee produce the same root. The two pathways for addressee-commitment converge.

High vs low negation — the paper's titular contribution #

@cite{krifka-2015} §4 distinguishes:

Low negation: Did I not win? — TP-internal negation, monopolar question with commit addressee ¬φ. The addressee is asked to commit to ¬φ.
High negation: Didn't I win? — ComP-level non-commitment, modeled as refuse addressee φ. The addressee is asked NOT to commit to φ.

Per paper p. 340: "adding ¬S₂⊢φ to the commitment space precludes commitment to φ, but is compatible with commitment to ¬φ. Hence ¬S₂⊢φ is pragmatically weaker than S₂⊢¬φ." This pragmatic strength asymmetry licenses the contextual-evidence pattern in Table 1 (p. 341).

source

theorem Phenomena.Assertion.Studies.Krifka2015.low_neg_continuation_eq :

(s₀.negatedQuestionLow isRaining).space.continuations = [[Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.addressee fun (w : Weather) => ¬isRaining w]]

Low negation: Did I not win? adds an addressee commitment to ¬φ.

source

theorem Phenomena.Assertion.Studies.Krifka2015.high_neg_continuation_eq :

(s₀.negatedQuestionHigh isRaining).space.continuations = [[Core.Discourse.Commitment.IndexedCommitment.refuse Core.Discourse.DiscourseRole.addressee isRaining]]

High negation: Didn't I win? adds an addressee REFUSAL to commit to φ. Distinct from commit addressee ¬φ.

source

theorem Phenomena.Assertion.Studies.Krifka2015.high_neg_uses_refuse (ic : Core.Discourse.Commitment.IndexedWeightedCommitment Weather Prop) :

ic ∈ (s₀.negatedQuestionHigh isRaining).space.continuations.flatten → ¬ic.IsCommit

High-negation polarity is refuse, not commit.

source

theorem Phenomena.Assertion.Studies.Krifka2015.high_neg_weaker_than_low_neg (w : Weather) :

(∀ ic ∈ [Core.Discourse.Commitment.IndexedCommitment.refuse Core.Discourse.DiscourseRole.addressee isRaining], ic.toCommitment w) ∧ ∀ ic ∈ [Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.addressee fun (w : Weather) => ¬isRaining w], ic.toCommitment w ↔ ¬isRaining w

Pragmatic-strength asymmetry (paper p. 340): the high-negation continuation, projected to a context-set constraint, is WEAKER than the low-negation continuation — refuse projects to the trivial True constraint, while commit ¬φ projects to actual ¬φ.

Table 1 (paper p. 341) — Büring & Gunlogson 2000 licensing #

@cite{bring-gunlogson-2000} (cited by @cite{krifka-2015} p. 341) identifies a 3×3 contextual-evidence × negation-type acceptability pattern. Contexts (rows): contextual evidence FOR φ / NEUTRAL / AGAINST φ. Question types (columns): no negation / low negation / high negation.

Krifka's analysis (paper p. 341) explains the pattern in terms of which READING is licensed when no negation is present:

(a) FOR-φ: no-neg ok via the monopolar reading
(b) NEUTRAL: no-neg ok via the bipolar reading
(c) AGAINST-φ: no-neg degraded — both readings fail

Cell values use Features.Acceptability (ok / marginal / anomalous). The paper's (#) parenthesised hash maps to marginal; bare # maps to anomalous. The ContextualEvidence enum is reused from Core.Discourse.Commitment (originally introduced for @cite{bring-gunlogson-2000}).

source

inductive Phenomena.Assertion.Studies.Krifka2015.NegationType :

Type

The three negation columns of Krifka's Table 1.

noNeg : NegationType
Column (i): no negation — Is there a vegetarian restaurant?
lowNeg : NegationType
Column (ii): low (TP) negation — Is there no vegetarian restaurant?
highNeg : NegationType
Column (iii): high (ComP) negation — Isn't there a vegetarian restaurant?

Instances For

source

@[implicit_reducible]

instance Phenomena.Assertion.Studies.Krifka2015.instDecidableEqNegationType :

DecidableEq NegationType

Equations

Phenomena.Assertion.Studies.Krifka2015.instDecidableEqNegationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

@[implicit_reducible]

instance Phenomena.Assertion.Studies.Krifka2015.instReprNegationType :

Repr NegationType

Equations

Phenomena.Assertion.Studies.Krifka2015.instReprNegationType = { reprPrec := Phenomena.Assertion.Studies.Krifka2015.instReprNegationType.repr }

source

def Phenomena.Assertion.Studies.Krifka2015.instReprNegationType.repr :

NegationType → ℕ → Std.Format

Equations

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

Instances For

source

inductive Phenomena.Assertion.Studies.Krifka2015.NoNegReading :

Type

Which reading licenses the no-negation question in each context (per @cite{krifka-2015} p. 341 prose).

monopolarLicensed : NoNegReading
Setting (a): monopolar reading licenses (speaker has prior evidence).
bipolarLicensed : NoNegReading
Setting (b): bipolar reading licenses (alternatives equally likely).
bothDegraded : NoNegReading
Setting (c): both readings fail (mono lacks evidence, bi suggests equipoise).

Instances For

source

@[implicit_reducible]

instance Phenomena.Assertion.Studies.Krifka2015.instDecidableEqNoNegReading :

DecidableEq NoNegReading

Equations

Phenomena.Assertion.Studies.Krifka2015.instDecidableEqNoNegReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Phenomena.Assertion.Studies.Krifka2015.instReprNoNegReading.repr :

NoNegReading → ℕ → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance Phenomena.Assertion.Studies.Krifka2015.instReprNoNegReading :

Repr NoNegReading

Equations

Phenomena.Assertion.Studies.Krifka2015.instReprNoNegReading = { reprPrec := Phenomena.Assertion.Studies.Krifka2015.instReprNoNegReading.repr }

source

def Phenomena.Assertion.Studies.Krifka2015.table1 :

Core.Discourse.Commitment.ContextualEvidence → NegationType → Features.Acceptability

Krifka's Table 1 (p. 341): 3×3 contextual-evidence × negation-type acceptability matrix.

Equations

Instances For

source

def Phenomena.Assertion.Studies.Krifka2015.noNegLicensing :

Core.Discourse.Commitment.ContextualEvidence → NoNegReading

Per @cite{krifka-2015} p. 341 prose: which reading licenses the no-negation question in each contextual-evidence setting.

Equations

Instances For

source

theorem Phenomena.Assertion.Studies.Krifka2015.table1_predictions :

Table 1 as a decide-checked predictive bundle. The pattern is what Krifka §4 explains via his monopolar/bipolar/high-vs-low contrast.

source

theorem Phenomena.Assertion.Studies.Krifka2015.noNeg_licensing_distinguishes_contexts :

noNegLicensing Core.Discourse.Commitment.ContextualEvidence.forP = NoNegReading.monopolarLicensed ∧ noNegLicensing Core.Discourse.Commitment.ContextualEvidence.neutral = NoNegReading.bipolarLicensed ∧ noNegLicensing Core.Discourse.Commitment.ContextualEvidence.againstP = NoNegReading.bothDegraded

Per the paper's prose: the no-negation cell licensing diverges across contexts — mono in (a), bipolar in (b), both fail in (c).

Tags as speech-act conjunction / disjunction #

Per @cite{krifka-2015} p. 342: matching tags are speech-act CONJUNCTION applied as ONE complex move — explicitly NOT sequential assert; question. The substrate's Dialogue.Krifka.matchingTag and reverseTag (Theories/Dialogue/CommitmentSpace.lean §4) capture this directly.

source

theorem Phenomena.Assertion.Studies.Krifka2015.matching_tag_is_conjunction :

∃ (a : Dialogue.Krifka.SpeechAct Weather) (b : Dialogue.Krifka.SpeechAct Weather), Dialogue.Krifka.matchingTag isRaining = Dialogue.Krifka.ComplexSpeechAct.conj a b

Substrate's matchingTag φ is structurally a conj of two atomic speech acts (paper eq. 44).

source

theorem Phenomena.Assertion.Studies.Krifka2015.matching_tag_shared_content_eq :

List.map Dialogue.Krifka.SpeechAct.content (Dialogue.Krifka.matchingTag isRaining).components = [isRaining, isRaining]

The matching tag's two speech acts share content — both are about φ.

source

theorem Phenomena.Assertion.Studies.Krifka2015.matching_tag_committers_diverge_eq :

List.map (fun (x : Dialogue.Krifka.SpeechAct Weather) => x.roles.committer) (Dialogue.Krifka.matchingTag isRaining).components = [Core.Discourse.DiscourseRole.speaker, Core.Discourse.DiscourseRole.addressee]

The committers diverge: speaker for the assertion-leg, addressee for the question-leg (paper p. 342).

source

theorem Phenomena.Assertion.Studies.Krifka2015.reverse_tag_is_disjunction :

∃ (a : Dialogue.Krifka.SpeechAct Weather) (b : Dialogue.Krifka.SpeechAct Weather), Dialogue.Krifka.reverseTag isRaining isNotRaining = Dialogue.Krifka.ComplexSpeechAct.disj a b

Substrate's reverseTag φ ¬φ is structurally a disj (paper eq. 45).

source

theorem Phenomena.Assertion.Studies.Krifka2015.matching_tag_apply_root_eq :

(s₀.applyComplex (Dialogue.Krifka.matchingTag isRaining)).space.root = [Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.speaker isRaining]

Worked example: applying a matching tag to the empty state via applyComplex produces a state where speaker has committed to φ (assertion-leg) and a continuation proposes addressee committing to φ (question-leg). The substrate sequentialises per paper eq. 6's "≈" approximation (no anaphoric ties at this level).

source

theorem Phenomena.Assertion.Studies.Krifka2015.matching_tag_apply_continuations_eq :

(s₀.applyComplex (Dialogue.Krifka.matchingTag isRaining)).space.continuations = [[Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.addressee isRaining, Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.speaker isRaining]]

The matching tag's continuation contains the addressee-commit on top of the speaker-commit already in the root. Both are present, both are non-contradictory (different committers, same content).

Krifka commitment-spaces vs KOS per-DGB stance #

Per the chronological-dependency rule, this post-2012 study engages the 2012 framework: @cite{krifka-2015} commitment-spaces and @cite{ginzburg-2012} KOS make structurally different but observationally similar predictions about identical event sequences.

Reciprocal entry to Phenomena/Dialogue/Studies/Ginzburg2012.lean lines 49–52, which delegates Krifka contrasts here.

Question	Krifka 2015	Ginzburg 2012 (KOS)
Is CG a single object or per-agent?	Single object, but its entries are speaker-indexed (`IndexedCommitment.commit S₁ φ`)	Per-agent (`DGB.facts`)
When does an assertion narrow CG?	Immediately (assert puts `commit S₁ φ` in root)	Only after Accept (one-sided FACTS)
Are commitments separable from CG?	Yes — root carries indexed commitments + per-agent slates	Only via separate DGBs

The architectures cannot be unified by a Galois connection that preserves both Krifka's eager-narrowing root behaviour and KOS's per-DGB asymmetry.

source

theorem Phenomena.Assertion.Studies.Krifka2015.krifka_eager_vs_ginzburg_lazy :

(s₀.assert isRaining).space.root.length = 1 ∧ Dialogue.KOS.DGB.initial.facts = []

The contrast theorem: post-assertion, Krifka's space.root narrows to a singleton list [commit speaker isRaining] (immediate, with speaker indexing); KOS's addressee DGB.facts stays [] (only the speaker side narrows; addressee waits for Accept).

source

theorem Phenomena.Assertion.Studies.Krifka2015.krifka_indexed_root_vs_kos_split_dgbs (p : Weather → Prop) :

(s₀.assert p).space.root = [Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.speaker p] ∧ have kosSpeaker := Dialogue.KOS.DGB.initial.addFact p; have kosAddressee := Dialogue.KOS.DGB.initial; kosSpeaker.facts ≠ kosAddressee.facts

Krifka's root carries indexed commitments (one per committer contribution); KOS speaker-side DGB has the fact in their slate while addressee-side stays empty. The architectures store the commitment in different shapes.

Krifka commitment-spaces vs Farkas-Bruce discourse-table model #

Per @cite{krifka-2015} §1 p. 331: "The last of these commitment stages would correspond to the notion of a 'Table' in Farkas & Bruce 2010, i.e., the conversational stage under negation." Krifka cites @cite{farkas-bruce-2010} as the explicit inspiration for his rejection operator ℜ. The two frameworks are observationally similar but structurally distinct on identical event sequences.

Question	Krifka 2015	Farkas-Bruce 2010
When does an assertion narrow CG?	Immediately (`commit speaker φ` in root)	Only after addressee accept (one-sided dcS until then)
Where does the assertion live pre-acceptance?	Root entry (already in CG, speaker-indexed)	`dcS` slate + `table` issue
What does acceptance update?	Adds `commit addressee φ` to root	Pops table issue, adds φ to cg + dcL
What's the "stable" predicate?	`hasNoOpenContinuations` (no pending proposals)	`table.isEmpty` (no items on table)

The eager/lazy distinction is real and non-collapsible at intermediate states. But at the end of a "completed" assertion+acceptance sequence, both frameworks agree on the observable CG content modulo Krifka's speaker indexing — see the Dialogue Completeness observation below.

source

Divergence at the assert-only intermediate state: Krifka's CG narrows immediately (one indexed entry in root); F&B's joint CG stays empty because the assertion lives on the table awaiting acceptance. The two frameworks DISAGREE on what's "in CG" mid-trace.

@cite{krifka-2015} p. 332 eq. (14) puts S₁⊢φ directly in the commitment state; @cite{farkas-bruce-2010}'s assertDeclarative only updates dcS and pushes a table issue.

source

theorem Phenomena.Assertion.Studies.Krifka2015.krifka_double_assert_eq_farkasBruce_assert_accept :

have kState := (s₀.assert isRaining).assert isRaining Core.Discourse.DiscourseRole.addressee; have fbState := (Dialogue.FarkasBruce.DiscourseState.empty.assertDeclarative isRaining).acceptTop; kState.speakerCS.commitments = [isRaining] ∧ kState.addresseeCS.commitments = [isRaining] ∧ kState.space.root = [Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.addressee isRaining, Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.speaker isRaining] ∧ fbState.cg = [isRaining] ∧ fbState.dcS = [isRaining] ∧ fbState.dcL = [isRaining] ∧ fbState.table = []

Bridge at the completed-trace state: after the addressee accepts the assertion, both frameworks have φ in the joint CG (modulo Krifka's speaker indexing on the root entries; F&B's cg is bare Set W).

Krifka's "addressee accepts" pathway is assert φ .addressee (the Yes reaction, paper p. 334 eq. 21). F&B's pathway is acceptTop after assertDeclarative. Both end with φ in the common ground at the propositional level.

source

theorem Phenomena.Assertion.Studies.Krifka2015.krifka_contextSet_at_completed_trace (w : Weather) :

have kState := (s₀.assert isRaining).assert isRaining Core.Discourse.DiscourseRole.addressee; kState.contextSet w ↔ isRaining w

The headline observation: at a completed assertion+acceptance trace, the two frameworks agree on the context-set projection — Krifka's projected CG content is exactly isRaining.

The frameworks disagree on what they STORE at intermediate states (root vs table, indexed vs flat) but agree on the observable they project to (worlds compatible with all committed propositions). This is the simplest concrete instance of the Dialogue Completeness observation in §∞.

The Dialogue Completeness observation #

The cross-framework theorems above (krifka_contextSet_at_completed_trace paired with krifka_double_assert_eq_farkasBruce_assert_accept, the parallel vsGinzburg2012 block) are concrete instances of a deeper structural claim. We articulate it here as prose; the typeclass-mediated universal version is future work.

Statement #

For any two commitment-tracking dialogue frameworks F₁ and F₂ over the same world type W, equipped with:

A shared event signature DialogueEvent W (assert, monopolar question, bipolar question, low/high negated question, accept, reject, …);
A step function step_i : Sᵢ → DialogueEvent W → Sᵢ;
A context-set projection contextSet_i : Sᵢ → Set W (the observable CG content);
A "completed" predicate isCompleted_i : Sᵢ → Prop (no pending proposals, no orphan issues),

the conjecture is:

∀ events : List (DialogueEvent W),
  isCompleted_F₁ (events.foldl step_F₁ initial_F₁) →
  isCompleted_F₂ (events.foldl step_F₂ initial_F₂) →
  contextSet_F₁ (events.foldl step_F₁ initial_F₁) =
  contextSet_F₂ (events.foldl step_F₂ initial_F₂)

Plain English: dialogue frameworks differ in the journey through intermediate states; they agree on the observable destination. The eager/lazy timing of CG updates, the per-agent commitment slate shape, the proposal-tracking apparatus — all of these are framework-internal bookkeeping invisible at completed traces. What's publicly committed (in the projected context-set sense) at the end of a completed dialogue is framework-invariant.

Why it's deep #

The conjecture says that contextSet is the maximal observable shared across all reasonable models of dialogue. Anything more fine-grained (commitment indexing, per-agent slates, intermediate proposal stacks, reaction-pathway distinctions) is a free choice the modeler makes — and choices on that level don't constrain what counts as a model of dialogue dynamics per se. Mathematically, this is the shape of an observational equivalence in a coalgebraic / process-theory sense: framework states form a coalgebra for the functor X ↦ (DialogueEvent → X) × (Set W), and the completed-trace agreement is bisimilarity at the Set W observable.

Status in linglib #

This file proves the conjecture's restriction to a 2-element framework class {Krifka2015, FarkasBruce2010} and a 2-event trace (assert; accept). The general statement requires:

A DialogueState typeclass in Theories/Dialogue/Common.lean (does not yet exist) parameterising over the four operations above.
Per-framework instances for Krifka, Farkas-Bruce, KOS, Stalnaker, Brandom, Gunlogson, Lauer.
The universal theorem proved either generically (likely needs an axiom about how each instance's step interprets DialogueEvent) or per-pair (n² theorems for n frameworks).

The per-pair route is more tractable; the generic route requires articulating what "interpret an event correctly" means as a coherence law on instances. Either route lifts cross-framework reconciliation in linglib from per-file vsX2010 sections to a structural theorem about what counts as a dialogue framework at all.

The framework that refuses the typeclass instance is the most informative: @cite{lauer-2013}'s gradient-credence assertion has no sharp commit event in the Krifka/F&B sense, so it would either reject the DialogueState instance or implement it with a non-trivial projection (mapping credence ≥ θ to commitment for some threshold θ). The refusal would surface a genuine architectural break between gradient-pragmatic and categorical-pragmatic models of dialogue.

Documentation

Linglib.Phenomena.Assertion.Studies.Krifka2015

Bias in Commitment Space Semantics #

Coverage #

Out of scope (explicit) #

High vs low negation — the paper's titular contribution #

Table 1 (paper p. 341) — Büring & Gunlogson 2000 licensing #

Tags as speech-act conjunction / disjunction #

Krifka commitment-spaces vs KOS per-DGB stance #

Krifka commitment-spaces vs Farkas-Bruce discourse-table model #

The Dialogue Completeness observation #

Statement #

Why it's deep #

Status in linglib #