@cite{gunlogson-2004}: Source-Marked Commitments

@cite{gunlogson-2004} @cite{gunlogson-2001} @cite{gunlogson-2003}Models the distinction between falling and rising declaratives via @cite{bring-gunlogson-2000} source-marked discourse commitments. The key innovation: commitments carry a tag indicating whether they are self-generated (from the speaker's own evidence) or other-generated (attributed to the addressee).

Falling vs Rising Declaratives

Intonation	Example	Source	Speaker committed?
Falling ↓	"It's raining."	self-generated	Yes
Rising ↑	"It's raining?"	other-generated	No

A falling declarative commits the speaker to the content (self-generated). A rising declarative attributes the content to the addressee (other-generated) without speaker commitment. This explains why rising declaratives can be used to check or confirm information.

Challengeability

Source determines who can challenge:

• Self-generated commitments can be challenged by the addressee ("Why do you think that?")
• Other-generated commitments can be challenged by the speaker ("Is that really what you think?")

structure Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState (W : Type u_1) : Type u_1

Gunlogson's discourse state: source-tagged commitment slates for speaker and addressee.

Unlike Stalnaker (single CG) or Farkas & Bruce (dcS + dcL + cg), Gunlogson tracks the SOURCE of each commitment, not just which participant holds it.

• speakerSlate : Core.Discourse.Commitment.TaggedSlate W

  Speaker's source-tagged commitments

• addresseeSlate : Core.Discourse.Commitment.TaggedSlate W

  Addressee's source-tagged commitments

def Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.empty {W : Type u_1} : GunlogsonState W

Initial state: no commitments for either participant.

Equations

• Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.empty = { speakerSlate := Core.Discourse.Commitment.TaggedSlate.empty, addresseeSlate := Core.Discourse.Commitment.TaggedSlate.empty }

def Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.fallingDeclarative {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : GunlogsonState W

Falling declarative: speaker commits self to p.

The speaker adds p to their own slate with source = .selfGenerated. This is the standard declarative assertion: "It's raining."

Equations

• s.fallingDeclarative p = { speakerSlate := s.speakerSlate.add p Core.Discourse.Commitment.CommitmentSource.selfGenerated, addresseeSlate := s.addresseeSlate }

def Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.risingDeclarative {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : GunlogsonState W

Rising declarative: speaker attributes p to addressee.

The speaker adds p to the addressee's slate with source = .otherGenerated. No commitment is added to the speaker's own slate. This is the rising declarative: "It's raining?"

Equations

• s.risingDeclarative p = { speakerSlate := s.speakerSlate, addresseeSlate := s.addresseeSlate.add p Core.Discourse.Commitment.CommitmentSource.otherGenerated }

def Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.assert {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : GunlogsonState W

Assert: defaults to falling declarative (standard assertion).

Equations

• s.assert p = s.fallingDeclarative p

def Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.contextSet {W : Type u_1} (s : GunlogsonState W) : Core.CommonGround.ContextSet W

Context set: intersection of both participants' commitment contexts. Only propositions that both participants are committed to (regardless of source) contribute to the shared context.

Equations

• s.contextSet w = (s.speakerSlate.toContextSet w = true ∧ s.addresseeSlate.toContextSet w = true)

def Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.isStable {W : Type u_1} (s : GunlogsonState W) : Bool

Stability: stable when neither participant has unresolved other-generated commitments.

Equations

• s.isStable = (s.speakerSlate.otherGenerated.isEmpty && s.addresseeSlate.otherGenerated.isEmpty)

def Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.canChallenge (src : Core.Discourse.Commitment.CommitmentSource) (role : Core.Discourse.DiscourseRole) : Bool

Can the given role challenge a commitment?

Source determines challengeability:

• Self-generated → challengeable by the OTHER participant
• Other-generated → challengeable by the SAME participant

Equations

• Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.canChallenge Core.Discourse.Commitment.CommitmentSource.selfGenerated Core.Discourse.DiscourseRole.addressee = true
• Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.canChallenge Core.Discourse.Commitment.CommitmentSource.otherGenerated Core.Discourse.DiscourseRole.speaker = true
• Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.canChallenge src role = false

def Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.cbcMet {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : Prop

The Contextual Bias Condition (@cite{gunlogson-2001}, Ch. 4 §4.2).

A rising declarative about p is felicitous only when the addressee's existing commitments already entail p. This is NOT a free parameter — it's a condition derivable from the discourse state.

The CBC follows from the uninformativeness requirement on questions: a rising declarative can serve as a question only if it's uninformative for the addressee, which holds iff the addressee is already committed to p (see cbc_from_uninformativeness below).

Equations

• s.cbcMet p = ∀ (w : W), s.addresseeSlate.toContextSet w = true → p w = true

def Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.risingDeclarativeFelicitous {W : Type u_1} (s : GunlogsonState W) (p : BProp W) (evidence : Core.Discourse.Commitment.ContextualEvidence) : Option (GunlogsonState W)

Rising declarative guarded by the CBC.

Returns the updated state when the CBC is met, none otherwise. Also accepts a coarser ContextualEvidence tag for compatibility with the polar question bias framework.

Equations

• s.risingDeclarativeFelicitous p Core.Discourse.Commitment.ContextualEvidence.forP = some (s.risingDeclarative p)
• s.risingDeclarativeFelicitous p evidence = none

def Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.uninformativeForAddressee {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : Prop

A move is uninformative for a participant if their commitment context set doesn't change.

This is the key notion connecting rising declaratives to questions: questioning requires uninformativeness for the addressee (the addressee isn't learning anything new — they're being asked to make their existing commitment public).

Equations

• s.uninformativeForAddressee p = ((s.risingDeclarative p).addresseeSlate.toContextSet = s.addresseeSlate.toContextSet)

theorem Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.rising_uninformative_for_speaker {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : (s.risingDeclarative p).speakerSlate.toContextSet = s.speakerSlate.toContextSet

Rising declaratives are ALWAYS uninformative for the speaker.

The speaker's slate is untouched, so their commitment context is trivially unchanged. This is Generalization (9) from Ch. 2.

theorem Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.cbc_from_uninformativeness {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : s.cbcMet p → s.uninformativeForAddressee p

The CBC is the uninformativeness condition for the addressee.

A rising declarative about p is uninformative for the addressee iff the addressee's commitment set already entails p. This is Gunlogson's central result: the CBC is derived, not stipulated. It follows from the definition of uninformativeness applied to the commitment-set update semantics of rising declaratives.

def Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.confirm {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : GunlogsonState W

Confirm: addressee endorses content of a rising declarative.

Adds p as self-generated on the addressee's slate, signaling acceptance. Both participants now have p (speaker via falling assertion or prior commitment, addressee via confirmation), moving p toward the effective common ground.

Equations

• s.confirm p = { speakerSlate := s.speakerSlate, addresseeSlate := s.addresseeSlate.add p Core.Discourse.Commitment.CommitmentSource.selfGenerated }

def Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.reject {W : Type u_1} (s : GunlogsonState W) : GunlogsonState W

Reject: addressee declines to endorse a rising declarative.

Does NOT commit the addressee to ¬p — rejection is weaker than denial. The addressee simply doesn't add p as self-generated, leaving the other-generated commitment unresolved.

Formally, rejection is the identity on the state: no new commitment is added. The discourse remains unstable (the other-generated commitment is still pending).

Equations

• s.reject = s

def Theories.Pragmatics.Assertion.Gunlogson.GunlogsonState.strongDeny {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : GunlogsonState W

Strong denial: addressee asserts ¬p (stronger than rejection).

Only appropriate when the addressee actively disagrees, not merely declines to confirm. Adds ¬p as self-generated.

Equations

• s.strongDeny p = { speakerSlate := s.speakerSlate, addresseeSlate := s.addresseeSlate.add (fun (w : W) => !p w) Core.Discourse.Commitment.CommitmentSource.selfGenerated }

theorem Theories.Pragmatics.Assertion.Gunlogson.falling_is_self_generated {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : Option.map (fun (x : Core.Discourse.Commitment.TaggedCommitment W) => x.source) (s.fallingDeclarative p).speakerSlate.commitments.head? = some Core.Discourse.Commitment.CommitmentSource.selfGenerated

Falling declaratives add self-generated commitments to the speaker.

theorem Theories.Pragmatics.Assertion.Gunlogson.rising_is_other_generated {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : Option.map (fun (x : Core.Discourse.Commitment.TaggedCommitment W) => x.source) (s.risingDeclarative p).addresseeSlate.commitments.head? = some Core.Discourse.Commitment.CommitmentSource.otherGenerated

Rising declaratives add other-generated commitments to the addressee.

theorem Theories.Pragmatics.Assertion.Gunlogson.rising_no_speaker_commitment {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : (s.risingDeclarative p).speakerSlate = s.speakerSlate

Rising declaratives do NOT commit the speaker.

The speaker's slate is unchanged by a rising declarative — only the addressee's slate gets an other-generated commitment.

theorem Theories.Pragmatics.Assertion.Gunlogson.falling_vs_rising_source {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : Option.map (fun (x : Core.Discourse.Commitment.TaggedCommitment W) => x.source) (s.fallingDeclarative p).speakerSlate.commitments.head? = some Core.Discourse.Commitment.CommitmentSource.selfGenerated ∧ Option.map (fun (x : Core.Discourse.Commitment.TaggedCommitment W) => x.source) (s.risingDeclarative p).addresseeSlate.commitments.head? = some Core.Discourse.Commitment.CommitmentSource.otherGenerated

Falling and rising declaratives differ in source.

theorem Theories.Pragmatics.Assertion.Gunlogson.rising_infelicitous_neutral {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : s.risingDeclarativeFelicitous p Core.Discourse.Commitment.ContextualEvidence.neutral = none

Rising declaratives are infelicitous in neutral contexts.

theorem Theories.Pragmatics.Assertion.Gunlogson.rising_infelicitous_againstP {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : s.risingDeclarativeFelicitous p Core.Discourse.Commitment.ContextualEvidence.againstP = none

Rising declaratives are infelicitous when evidence is against p.

theorem Theories.Pragmatics.Assertion.Gunlogson.rising_felicitous_forP {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : (s.risingDeclarativeFelicitous p Core.Discourse.Commitment.ContextualEvidence.forP).isSome = true

Rising declaratives are felicitous when evidence supports p.

theorem Theories.Pragmatics.Assertion.Gunlogson.confirm_adds_self_generated {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : Option.map (fun (x : Core.Discourse.Commitment.TaggedCommitment W) => x.source) (s.confirm p).addresseeSlate.commitments.head? = some Core.Discourse.Commitment.CommitmentSource.selfGenerated

Confirmation adds a self-generated commitment to the addressee.

theorem Theories.Pragmatics.Assertion.Gunlogson.strongDeny_adds_self_generated {W : Type u_1} (s : GunlogsonState W) (p : BProp W) : Option.map (fun (x : Core.Discourse.Commitment.TaggedCommitment W) => x.source) (s.strongDeny p).addresseeSlate.commitments.head? = some Core.Discourse.Commitment.CommitmentSource.selfGenerated

Strong denial adds a self-generated commitment to the addressee.

theorem Theories.Pragmatics.Assertion.Gunlogson.reject_identity {W : Type u_1} (s : GunlogsonState W) : s.reject = s

Rejection is the identity: no new commitment.

theorem Theories.Pragmatics.Assertion.Gunlogson.rising_confirm_has_both {W : Type u_1} (p : BProp W) : have s := GunlogsonState.empty.risingDeclarative p; have s' := s.confirm p; s'.addresseeSlate.selfGenerated.length = 1 ∧ s'.addresseeSlate.otherGenerated.length = 1

Rising then confirm: the addressee ends up with both an other-generated and a self-generated commitment. The self-generated endorsement is what moves p toward the common ground.

theorem Theories.Pragmatics.Assertion.Gunlogson.rising_from_empty_unstable {W : Type u_1} (p : BProp W) : (GunlogsonState.empty.risingDeclarative p).isStable = false

A rising declarative from the empty state breaks stability: the other-generated commitment on the addressee's slate is unresolved.

theorem Theories.Pragmatics.Assertion.Gunlogson.confirm_still_unstable {W : Type u_1} (p : BProp W) : have s := GunlogsonState.empty.risingDeclarative p; (s.confirm p).isStable = false

Confirm does NOT restore stability: the other-generated commitment remains alongside the new self-generated one. Full resolution would require removing the other-generated entry.