Discourse Commitments

[Ham70] [Kri15a] [Bra94] [Gun01]

Commitment slates, source × force tagging, and the speaker-indexed S⊢φ constructor. The per-agent commitment store originates with [Ham70]'s formal dialectic.

Commitment Slates

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

An agent's public discourse commitments ([Kri15a], [Bra94]): a list of propositions the agent has publicly committed to.

• commitments : List (W → Prop)

  The propositions the agent is publicly committed to.

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

The empty commitment slate.

Equations

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

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

Add a commitment to the slate.

Equations

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

def Discourse.Commitment.CommitmentSlate.toContextSet {W : Type u_1} (s : CommitmentSlate W) : W → Prop

Worlds compatible with every committed proposition.

Equations

• s.toContextSet w = ∀ p ∈ s.commitments, p w

def Discourse.Commitment.CommitmentSlate.entails {W : Type u_1} (s : CommitmentSlate W) (p : W → Prop) : Prop

The slate entails p iff every compatible world satisfies p.

Equations

• s.entails p = ∀ (w : W), (∀ q ∈ s.commitments, q w) → p w

theorem Discourse.Commitment.CommitmentSlate.empty_trivial {W : Type u_1} (w : W) : empty.toContextSet w

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

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

Source-Marked Commitments

inductive Discourse.Commitment.CommitmentSource : Type

The source of a discourse commitment: self-generated commitments can be challenged by the addressee; other-generated commitments can be challenged by the speaker.

• selfGenerated : CommitmentSource
• otherGenerated : CommitmentSource

@[implicit_reducible]

instance Discourse.Commitment.instDecidableEqCommitmentSource : DecidableEq CommitmentSource

Equations

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

@[implicit_reducible]

instance Discourse.Commitment.instReprCommitmentSource : Repr CommitmentSource

Equations

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

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

Equations

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

@[implicit_reducible]

instance Discourse.Commitment.instInhabitedCommitmentSource : Inhabited CommitmentSource

Equations

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

inductive Discourse.Commitment.CommitmentForce : Type

The modal force of a commitment: doxastic (act-as-if-believe) or preferential (act-as-if-effectively-prefer, [CL12], [Lau13]).

• doxastic : CommitmentForce
• preferential : CommitmentForce

@[implicit_reducible]

instance Discourse.Commitment.instDecidableEqCommitmentForce : DecidableEq CommitmentForce

Equations

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

@[implicit_reducible]

instance Discourse.Commitment.instReprCommitmentForce : Repr CommitmentForce

Equations

• Discourse.Commitment.instReprCommitmentForce = { reprPrec := Discourse.Commitment.instReprCommitmentForce.repr }

def Discourse.Commitment.instReprCommitmentForce.repr : CommitmentForce → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Discourse.Commitment.instInhabitedCommitmentForce : Inhabited CommitmentForce

Equations

• Discourse.Commitment.instInhabitedCommitmentForce = { default := Discourse.Commitment.instInhabitedCommitmentForce.default }

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

A commitment tagged with epistemic source and modal force. source × force is [Deo25]'s 2×2 cross.

• content : W → Prop
• source : CommitmentSource
• commitmentForce : CommitmentForce

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

A source-tagged commitment slate.

• commitments : List (TaggedCommitment W)

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

The empty tagged slate.

Equations

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

def Discourse.Commitment.TaggedSlate.add {W : Type u_1} (s : TaggedSlate W) (p : W → Prop) (src : CommitmentSource) (force : CommitmentForce := CommitmentForce.doxastic) : TaggedSlate W

Add a tagged commitment.

Equations

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

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

Self-generated commitments (any force).

Equations

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

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

Other-generated commitments (any force).

Equations

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

def Discourse.Commitment.TaggedSlate.doxasticContents {W : Type u_1} (s : TaggedSlate W) : List (W → Prop)

Doxastic commitments (any source).

Equations

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

def Discourse.Commitment.TaggedSlate.preferentialContents {W : Type u_1} (s : TaggedSlate W) : List (W → Prop)

Preferential commitments (any source). The input to a joint-preferences set when intersected across agents ([Deo25]).

Equations

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

def 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 : Discourse.Commitment.TaggedCommitment W) => x.content) s.commitments }

def Discourse.Commitment.TaggedSlate.toContextSet {W : Type u_1} (s : TaggedSlate W) : W → Prop

Convert to context set (ignoring source tags).

Equations

• s.toContextSet = s.toSlate.toContextSet

Projection reductions

Simp-normal forms so a consumer reading an agent's plain commitments (doxasticContents, selfGenerated, …) gets rfl-grade reductions under add, instead of unfolding the filter ∘ map.

@[simp]

theorem Discourse.Commitment.TaggedSlate.doxasticContents_empty {W : Type u_1} : empty.doxasticContents = []

@[simp]

theorem Discourse.Commitment.TaggedSlate.doxasticContents_add_doxastic {W : Type u_1} (s : TaggedSlate W) (p : W → Prop) (src : CommitmentSource) : (s.add p src).doxasticContents = p :: s.doxasticContents

@[simp]

theorem Discourse.Commitment.TaggedSlate.doxasticContents_add_preferential {W : Type u_1} (s : TaggedSlate W) (p : W → Prop) (src : CommitmentSource) : (s.add p src CommitmentForce.preferential).doxasticContents = s.doxasticContents

@[simp]

theorem Discourse.Commitment.TaggedSlate.selfGenerated_empty {W : Type u_1} : empty.selfGenerated = []

@[simp]

theorem Discourse.Commitment.TaggedSlate.selfGenerated_add_self {W : Type u_1} (s : TaggedSlate W) (p : W → Prop) (force : CommitmentForce) : (s.add p CommitmentSource.selfGenerated force).selfGenerated = p :: s.selfGenerated

@[simp]

theorem Discourse.Commitment.TaggedSlate.selfGenerated_add_other {W : Type u_1} (s : TaggedSlate W) (p : W → Prop) (force : CommitmentForce) : (s.add p CommitmentSource.otherGenerated force).selfGenerated = s.selfGenerated

@[simp]

theorem Discourse.Commitment.TaggedSlate.otherGenerated_empty {W : Type u_1} : empty.otherGenerated = []

@[simp]

theorem Discourse.Commitment.TaggedSlate.otherGenerated_add_other {W : Type u_1} (s : TaggedSlate W) (p : W → Prop) (force : CommitmentForce) : (s.add p CommitmentSource.otherGenerated force).otherGenerated = p :: s.otherGenerated

@[simp]

theorem Discourse.Commitment.TaggedSlate.otherGenerated_add_self {W : Type u_1} (s : TaggedSlate W) (p : W → Prop) (force : CommitmentForce) : (s.add p CommitmentSource.selfGenerated force).otherGenerated = s.otherGenerated

@[simp]

theorem Discourse.Commitment.TaggedSlate.toSlate_empty {W : Type u_1} : empty.toSlate = CommitmentSlate.empty

@[simp]

theorem Discourse.Commitment.TaggedSlate.toSlate_add_commitments {W : Type u_1} (s : TaggedSlate W) (p : W → Prop) (src : CommitmentSource) (force : CommitmentForce) : (s.add p src force).toSlate.commitments = p :: s.toSlate.commitments

Grade typeclasses

class Discourse.Commitment.HasSupport (G : Type u_1) : Type u_1

The support predicate of a commitment grade G: which grades count as "actively committing". For Prop: identity. For Bool: · = true. For ℝ_≥0: · > 0.

• support : G → Prop

class Discourse.Commitment.CommitmentGrade (G : Type u_1) extends Discourse.Commitment.HasSupport G : Type u_1

A commitment grade with a complement operation. Used to construct the "no" branch of bipolar questions.

• support : G → Prop
• complement : G → G

@[implicit_reducible]

instance Discourse.Commitment.instHasSupportProp : HasSupport Prop

Equations

• Discourse.Commitment.instHasSupportProp = { support := id }

@[implicit_reducible]

instance Discourse.Commitment.instCommitmentGradeProp : CommitmentGrade Prop

Equations

• Discourse.Commitment.instCommitmentGradeProp = { toHasSupport := Discourse.Commitment.instHasSupportProp, complement := Not }

Speaker-Indexed Commitments

IndexedWeightedCommitment W G is the polymorphic commitment type. Three axes:

• committer : DiscourseRole — who is committing.
• force : CommitmentForce — doxastic vs preferential.
• weight : W → G (commit) or content : W → Prop (refuse).

The G = Prop specialisation is IndexedCommitment W.

inductive Discourse.Commitment.IndexedWeightedCommitment (W : Type u_1) (G : Type u_2) : Type (max u_1 u_2)

A polymorphic indexed commitment.

• commit {W : Type u_1} {G : Type u_2} (committer : DiscourseRole) (force : CommitmentForce) (weight : W → G) : IndexedWeightedCommitment W G

  S⊢φ with per-world grade in G.

• refuse {W : Type u_1} {G : Type u_2} (committer : DiscourseRole) (force : CommitmentForce) (content : W → Prop) : IndexedWeightedCommitment W G

  ¬S⊢φ: agent explicitly NOT committed to φ.

def Discourse.Commitment.IndexedWeightedCommitment.committer {W : Type u_1} {G : Type u_2} : IndexedWeightedCommitment W G → DiscourseRole

The committing agent.

Equations

• (Discourse.Commitment.IndexedWeightedCommitment.commit c force weight).committer = c
• (Discourse.Commitment.IndexedWeightedCommitment.refuse c force content).committer = c

def Discourse.Commitment.IndexedWeightedCommitment.force {W : Type u_1} {G : Type u_2} : IndexedWeightedCommitment W G → CommitmentForce

The commitment force.

Equations

• (Discourse.Commitment.IndexedWeightedCommitment.commit c force weight).force = force
• (Discourse.Commitment.IndexedWeightedCommitment.refuse c force content).force = force

def Discourse.Commitment.IndexedWeightedCommitment.IsCommit {W : Type u_1} {G : Type u_2} : IndexedWeightedCommitment W G → Prop

True for commit, false for refuse.

Equations

• (Discourse.Commitment.IndexedWeightedCommitment.commit c force weight).IsCommit = True
• (Discourse.Commitment.IndexedWeightedCommitment.refuse c force content).IsCommit = False

@[implicit_reducible]

instance Discourse.Commitment.IndexedWeightedCommitment.instDecidablePredIsCommit {W : Type u_1} {G : Type u_2} : DecidablePred IsCommit

Equations

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

def Discourse.Commitment.IndexedWeightedCommitment.toCommitment {W : Type u_1} {G : Type u_2} [HasSupport G] : IndexedWeightedCommitment W G → W → Prop

Project to the context-set constraint: a commit excludes worlds where support (weight w) fails; a refuse imposes no exclusion.

Equations

• (Discourse.Commitment.IndexedWeightedCommitment.commit c force weight).toCommitment = fun (w : W) => Discourse.Commitment.HasSupport.support (weight w)
• (Discourse.Commitment.IndexedWeightedCommitment.refuse c force content).toCommitment = fun (x : W) => True

@[simp]

theorem Discourse.Commitment.IndexedWeightedCommitment.toCommitment_commit {W : Type u_1} {G : Type u_2} [HasSupport G] (c : DiscourseRole) (f : CommitmentForce) (weight : W → G) (w : W) : (commit c f weight).toCommitment w = HasSupport.support (weight w)

@[simp]

theorem Discourse.Commitment.IndexedWeightedCommitment.toCommitment_refuse {W : Type u_1} {G : Type u_2} [HasSupport G] (c : DiscourseRole) (f : CommitmentForce) (φ : W → Prop) (w : W) : (refuse c f φ).toCommitment w = True

@[reducible, inline]

abbrev Discourse.Commitment.IndexedCommitment (W : Type u_1) : Type u_1

Binary speaker-indexed commitment (Krifka 2015 default).

Equations

• Discourse.Commitment.IndexedCommitment W = Discourse.Commitment.IndexedWeightedCommitment W Prop

@[reducible, inline]

abbrev Discourse.Commitment.IndexedCommitment.commit {W : Type u_1} (committer : DiscourseRole) (content : W → Prop) : IndexedCommitment W

Smart constructor for the doxastic binary commit case.

Equations

• Discourse.Commitment.IndexedCommitment.commit committer content = Discourse.Commitment.IndexedWeightedCommitment.commit committer Discourse.Commitment.CommitmentForce.doxastic content

@[reducible, inline]

abbrev Discourse.Commitment.IndexedCommitment.refuse {W : Type u_1} (committer : DiscourseRole) (content : W → Prop) : IndexedCommitment W

Smart constructor for the doxastic binary refuse case.

Equations

• Discourse.Commitment.IndexedCommitment.refuse committer content = Discourse.Commitment.IndexedWeightedCommitment.refuse committer Discourse.Commitment.CommitmentForce.doxastic content

def Discourse.Commitment.IndexedCommitment.content {W : Type u_1} : IndexedCommitment W → W → Prop

Propositional content of the commitment.

Equations

• Discourse.Commitment.IndexedCommitment.content (Discourse.Commitment.IndexedWeightedCommitment.commit committer force φ) = φ
• Discourse.Commitment.IndexedCommitment.content (Discourse.Commitment.IndexedWeightedCommitment.refuse committer force φ) = φ

def Discourse.Commitment.IndexedCommitment.toCommitment {W : Type u_1} : IndexedCommitment W → W → Prop

Project to the world-level context-set constraint. commit projects to its content; refuse projects to True — because ¬S⊢φ imposes no constraint on the facts of the world. The constraint refuse does impose is second-order (on the committer's commitment state); see holdsIn.

Equations

• Discourse.Commitment.IndexedCommitment.toCommitment (Discourse.Commitment.IndexedWeightedCommitment.commit committer force φ) = φ
• Discourse.Commitment.IndexedCommitment.toCommitment (Discourse.Commitment.IndexedWeightedCommitment.refuse committer force φ) = fun (x : W) => True

def Discourse.Commitment.IndexedCommitment.holdsIn {W : Type u_1} : IndexedCommitment W → CommitmentSlate W → Prop

Commitment-level meaning of an entry as a constraint on the committer's resulting commitment state t (Krifka's S⊢_, [Kri15a] §4): commit r φ requires t to entail φ (r⊢φ); refuse r φ requires t NOT to entail φ (¬ r⊢φ). The refuse case is the second-order constraint that the world-level toCommitment (sending refuse to True) deliberately cannot express.

Equations

• Discourse.Commitment.IndexedCommitment.holdsIn (Discourse.Commitment.IndexedWeightedCommitment.commit committer force φ) x✝ = x✝.entails φ
• Discourse.Commitment.IndexedCommitment.holdsIn (Discourse.Commitment.IndexedWeightedCommitment.refuse committer force φ) x✝ = ¬x✝.entails φ

@[simp]

theorem Discourse.Commitment.IndexedCommitment.holdsIn_commit {W : Type u_1} (r : DiscourseRole) (φ : W → Prop) (t : CommitmentSlate W) : (commit r φ).holdsIn t = t.entails φ

@[simp]

theorem Discourse.Commitment.IndexedCommitment.holdsIn_refuse {W : Type u_1} (r : DiscourseRole) (φ : W → Prop) (t : CommitmentSlate W) : (refuse r φ).holdsIn t = ¬t.entails φ

HasContextSet Instance

@[implicit_reducible]

instance Discourse.instHasContextSetCommitmentSlate {W : Type u_1} : CommonGround.HasContextSet (Commitment.CommitmentSlate W) W

A commitment slate projects to a context set.

Equations

• Discourse.instHasContextSetCommitmentSlate = { toContextSet := fun (s : Discourse.Commitment.CommitmentSlate W) (w : W) => s.toContextSet w }