Discourse Commitments

@cite{brandom-1994} @cite{gunlogson-2001} @cite{krifka-2015} @cite{bring-gunlogson-2000} @cite{romero-2024}

Shared types for modeling public commitments in discourse, used by multiple theories of assertion (Krifka, Brandom, Gunlogson).

A CommitmentSlate is an agent's public discourse commitments — the propositions they have publicly committed to (which may differ from their private beliefs). This separation is crucial for:

• @cite{krifka-2015}: commitment ≠ belief; lying = commitment without belief
• @cite{brandom-1994}: commitments are normative statuses tracked by scorekeepers
• @cite{gunlogson-2001}: source-marking distinguishes self-generated from other-generated commitments

structure Core.Discourse.Commitment.CommitmentSlate (W : Type u_1) : Type u_1

An agent's public discourse commitments: a list of propositions the agent has publicly committed to.

Following @cite{krifka-2015}: the commitment slate tracks what an agent is publicly committed to, which may diverge from what they privately believe (as in lying, hedging, or performing).

• commitments : List (BProp W)

  The propositions the agent is publicly committed to

def Core.Discourse.Commitment.CommitmentSlate.empty {W : Type u_1} : CommitmentSlate W

The empty commitment slate: no public commitments.

Equations

• Core.Discourse.Commitment.CommitmentSlate.empty = { commitments := [] }

def Core.Discourse.Commitment.CommitmentSlate.add {W : Type u_1} (s : CommitmentSlate W) (p : BProp W) : CommitmentSlate W

Add a commitment to the slate.

Equations

• s.add p = { commitments := p :: s.commitments }

def Core.Discourse.Commitment.CommitmentSlate.retract {W : Type u_1} (s : CommitmentSlate W) (p : BProp W) [BEq (BProp W)] : CommitmentSlate W

Retract a commitment (remove first occurrence).

Not all theories support retraction. Stalnaker's CG model has no retraction mechanism; Krifka and Brandom do.

Equations

• s.retract p = { commitments := s.commitments.erase p }

def Core.Discourse.Commitment.CommitmentSlate.toContextSet {W : Type u_1} (s : CommitmentSlate W) : CommonGround.ContextSet W

Convert commitments to a context set: the worlds compatible with all committed propositions.

Equations

• s.toContextSet w = ((s.commitments.all fun (p : BProp W) => p w) = true)

def Core.Discourse.Commitment.CommitmentSlate.entails {W : Type u_1} (s : CommitmentSlate W) (p : BProp W) (worlds : List W) : Bool

Check if the slate entails a proposition (holds at all compatible worlds).

Equations

• s.entails p worlds = worlds.all fun (w : W) => (!s.commitments.all fun (q : BProp W) => q w) || p w

theorem Core.Discourse.Commitment.CommitmentSlate.empty_trivial {W : Type u_1} : empty.toContextSet = CommonGround.ContextSet.trivial

Empty slate is trivial: all worlds are compatible.

theorem Core.Discourse.Commitment.CommitmentSlate.add_restricts {W : Type u_1} (s : CommitmentSlate W) (p : BProp W) (w : W) : (s.add p).toContextSet w → s.toContextSet w

Adding a commitment restricts the context set.

theorem Core.Discourse.Commitment.CommitmentSlate.add_entails {W : Type u_1} (s : CommitmentSlate W) (p : BProp W) (w : W) : (s.add p).toContextSet w → p w = true

Adding a commitment entails the added proposition.

inductive Core.Discourse.Commitment.CommitmentSource : Type

The source of a discourse commitment.

@cite{gunlogson-2001}: commitments are marked by their epistemic source.

• .selfGenerated: the agent generated the commitment from their own evidence
• .otherGenerated: the commitment originates from another participant

The source determines challengeability: self-generated commitments can be challenged by the addressee; other-generated commitments can be challenged by the speaker.

• selfGenerated : CommitmentSource

  Commitment generated from agent's own evidence/beliefs

• otherGenerated : CommitmentSource

  Commitment attributed to another participant

instance Core.Discourse.Commitment.instDecidableEqCommitmentSource : DecidableEq CommitmentSource

Equations

• Core.Discourse.Commitment.instDecidableEqCommitmentSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Discourse.Commitment.instReprCommitmentSource.repr : CommitmentSource → ℕ → Std.Format

Equations

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

instance Core.Discourse.Commitment.instReprCommitmentSource : Repr CommitmentSource

Equations

• Core.Discourse.Commitment.instReprCommitmentSource = { reprPrec := Core.Discourse.Commitment.instReprCommitmentSource.repr }

instance Core.Discourse.Commitment.instBEqCommitmentSource : BEq CommitmentSource

Equations

• Core.Discourse.Commitment.instBEqCommitmentSource = { beq := Core.Discourse.Commitment.instBEqCommitmentSource.beq }

def Core.Discourse.Commitment.instBEqCommitmentSource.beq : CommitmentSource → CommitmentSource → Bool

Equations

• Core.Discourse.Commitment.instBEqCommitmentSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Core.Discourse.Commitment.instInhabitedCommitmentSource.default : CommitmentSource

Equations

• Core.Discourse.Commitment.instInhabitedCommitmentSource.default = Core.Discourse.Commitment.CommitmentSource.selfGenerated

instance Core.Discourse.Commitment.instInhabitedCommitmentSource : Inhabited CommitmentSource

Equations

• Core.Discourse.Commitment.instInhabitedCommitmentSource = { default := Core.Discourse.Commitment.instInhabitedCommitmentSource.default }

structure Core.Discourse.Commitment.TaggedCommitment (W : Type u_1) : Type u_1

A commitment tagged with its source.

• content : BProp W

  The propositional content

• source : CommitmentSource

  How the commitment was generated

structure Core.Discourse.Commitment.TaggedSlate (W : Type u_1) : Type u_1

A source-tagged commitment slate.

• commitments : List (TaggedCommitment W)

  The tagged commitments

def Core.Discourse.Commitment.TaggedSlate.empty {W : Type u_1} : TaggedSlate W

The empty tagged slate.

Equations

• Core.Discourse.Commitment.TaggedSlate.empty = { commitments := [] }

def Core.Discourse.Commitment.TaggedSlate.add {W : Type u_1} (s : TaggedSlate W) (p : BProp W) (src : CommitmentSource) : TaggedSlate W

Add a tagged commitment.

Equations

• s.add p src = { commitments := { content := p, source := src } :: s.commitments }

def Core.Discourse.Commitment.TaggedSlate.selfGenerated {W : Type u_1} (s : TaggedSlate W) : List (BProp W)

Get all self-generated commitments.

Equations

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

def Core.Discourse.Commitment.TaggedSlate.otherGenerated {W : Type u_1} (s : TaggedSlate W) : List (BProp W)

Get all other-generated commitments.

Equations

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

def Core.Discourse.Commitment.TaggedSlate.toSlate {W : Type u_1} (s : TaggedSlate W) : CommitmentSlate W

Convert to a plain (untagged) commitment slate.

Equations

• s.toSlate = { commitments := List.map (fun (x : Core.Discourse.Commitment.TaggedCommitment W) => x.content) s.commitments }

def Core.Discourse.Commitment.TaggedSlate.toContextSet {W : Type u_1} (s : TaggedSlate W) : CommonGround.ContextSet W

Convert to context set (ignoring source tags).

Equations

• s.toContextSet = s.toSlate.toContextSet

inductive Core.Discourse.Commitment.ContextualEvidence : Type

Contextual evidence bias.

Expectation about p induced by evidence available in the current discourse situation. Used as:

• A felicity condition on rising declaratives
• A bias dimension for polar questions

This type is shared between assertion theory and question bias theory because the same notion of contextual evidence governs both: evidence for p licenses rising declaratives about p and positive polar questions about p.

• forP : ContextualEvidence

  Current context provides evidence for p.

• neutral : ContextualEvidence

  No contextual evidence either way.

• againstP : ContextualEvidence

  Current context provides evidence against p.

instance Core.Discourse.Commitment.instDecidableEqContextualEvidence : DecidableEq ContextualEvidence

Equations

• Core.Discourse.Commitment.instDecidableEqContextualEvidence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.Discourse.Commitment.instBEqContextualEvidence.beq : ContextualEvidence → ContextualEvidence → Bool

Equations

• Core.Discourse.Commitment.instBEqContextualEvidence.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.Discourse.Commitment.instBEqContextualEvidence : BEq ContextualEvidence

Equations

• Core.Discourse.Commitment.instBEqContextualEvidence = { beq := Core.Discourse.Commitment.instBEqContextualEvidence.beq }

def Core.Discourse.Commitment.instReprContextualEvidence.repr : ContextualEvidence → ℕ → Std.Format

Equations

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

instance Core.Discourse.Commitment.instReprContextualEvidence : Repr ContextualEvidence

Equations

• Core.Discourse.Commitment.instReprContextualEvidence = { reprPrec := Core.Discourse.Commitment.instReprContextualEvidence.repr }