Discourse Commitments

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

The public trace of speech acts: commitment slates, source-tagged commitments, and contextual evidence bias. Pairs with Core/Discourse/IllocutionaryForce.lean (F in F(p)) and Core/Discourse/Intentionality.lean (S in S(r)).

Where Intentional states are private, commitments are public — the publicly-tracked obligations created by performing speech acts. Asserting p creates a mind-to-world commitment; promising p creates a world-to-mind one.

Organization

• § 1. Commitment Slates (@cite{krifka-2015}, @cite{brandom-1994})
• § 2. Source-Marked Commitments (@cite{gunlogson-2001})
• § 3. Contextual Evidence (@cite{bring-gunlogson-2000})
• § 4. Speaker-Indexed Commitments (@cite{krifka-2015} S⊢φ notation)
• § 5. HasContextSet Instance

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).

In @cite{searle-1983}'s terms: commitment is the public direction-of-fit obligation created by performing a speech act. Asserting p creates a mind-to-world commitment (the speaker is responsible if p is false); promising p creates a world-to-mind commitment (the speaker is responsible if p is unfulfilled).

• commitments : List (W → Prop)

  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 : W → Prop) : CommitmentSlate W

Add a commitment to the slate.

Equations

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

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

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

Equations

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

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

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

Equations

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

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

Empty slate is trivial: all worlds are compatible.

theorem Core.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

Adding a commitment restricts the context set.

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

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. 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

@[implicit_reducible]

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.

@[implicit_reducible]

instance Core.Discourse.Commitment.instReprCommitmentSource : Repr CommitmentSource

Equations

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

@[implicit_reducible]

instance Core.Discourse.Commitment.instInhabitedCommitmentSource : Inhabited CommitmentSource

Equations

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

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

Equations

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

inductive Core.Discourse.Commitment.CommitmentForce : Type

The modal force of a discourse commitment: doxastic (act-as-if-believe) vs preferential (act-as-if-effectively-prefer).

@cite{condoravdi-lauer-2012} @cite{lauer-2013} introduce the preferential side; @cite{portner-2018} (commitments to priorities) and @cite{rudin-2018} (teleological common ground) develop the doxastic/preferential parallel in scoreboard models; @cite{deo-2025-bara} lifts the existing CommitmentSource source/dependent distinction to apply to both forces.

Default .doxastic matches the historical assumption that bare TaggedCommitment means doxastic — preserves all existing call sites.

• doxastic : CommitmentForce

  Doxastic commitment: speaker publicly commits to acting as though they believe the content. The standard assertion case.

• preferential : CommitmentForce

  Preferential commitment: speaker publicly commits to acting as though the content is among their effective preferences (@cite{condoravdi-lauer-2012}). The standard imperative-as-PEP / C&L analysis case.

@[implicit_reducible]

instance Core.Discourse.Commitment.instDecidableEqCommitmentForce : DecidableEq CommitmentForce

Equations

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

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

Equations

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

@[implicit_reducible]

instance Core.Discourse.Commitment.instReprCommitmentForce : Repr CommitmentForce

Equations

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

def Core.Discourse.Commitment.instInhabitedCommitmentForce.default : CommitmentForce

Equations

• Core.Discourse.Commitment.instInhabitedCommitmentForce.default = Core.Discourse.Commitment.CommitmentForce.doxastic

@[implicit_reducible]

instance Core.Discourse.Commitment.instInhabitedCommitmentForce : Inhabited CommitmentForce

Equations

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

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

A commitment tagged with its epistemic source and modal force.

Two orthogonal axes:

• source (selfGenerated / otherGenerated): whose evidence supports it (@cite{gunlogson-2001}).
• commitmentForce (doxastic / preferential): whether it is a belief-like or preference-like commitment (@cite{condoravdi-lauer-2012}, @cite{lauer-2013}, lifted across source by @cite{deo-2025-bara}).

commitmentForce defaults to .doxastic so existing two-argument anonymous-constructor calls (⟨content, source⟩) and existing TaggedSlate.add s p src invocations continue to type-check.

• content : W → Prop

  The propositional content

• source : CommitmentSource

  How the commitment was generated

• commitmentForce : CommitmentForce

  Whether the commitment is doxastic (default) or preferential.

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 : W → Prop) (src : CommitmentSource) (force : CommitmentForce := CommitmentForce.doxastic) : TaggedSlate W

Add a tagged commitment. The optional force parameter defaults to .doxastic for backward compatibility with the pre-CommitmentForce API; pass .preferential for C&L-style preferential commitments.

Equations

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

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

Get all self-generated commitments (any force).

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 (W → Prop)

Get all other-generated commitments (any force).

Equations

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

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

Get all doxastic commitments (any source). The contribution to an agent's belief-like commitments — the input to a Stalnakerian common ground when intersected across agents.

Equations

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

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

Get all preferential commitments (any source). The contribution to an agent's preference-like commitments — the input to a "joint preferences" set (@cite{deo-2025-bara} eq. 17c) when intersected across agents.

Equations

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

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

Dependent commitments (any force) — DC_x_dep in @cite{deo-2025-bara}'s notation. The Set-typed counterpart of the legacy otherGenerated (List-typed); use this for new code and proofs.

Equations

• s.dependent = {p : W → Prop | ∃ c ∈ s.commitments, c.source = Core.Discourse.Commitment.CommitmentSource.otherGenerated ∧ c.content = p}

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

Independent (self-sourced) commitments (any force) — DC_x_ind.

Equations

• s.independent = {p : W → Prop | ∃ c ∈ s.commitments, c.source = Core.Discourse.Commitment.CommitmentSource.selfGenerated ∧ c.content = p}

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

Dependent doxastic commitments — the (source = .otherGenerated, commitmentForce = .doxastic) cell of the 2×2 cross. The agent's DC_x_dep_dox in @cite{deo-2025-bara}'s notation.

Equations

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

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

Dependent preferential commitments — DC_x_dep_pref. The 2×2 cell targeted by @cite{deo-2025-bara}'s bərə convention (eq. 20).

Equations

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

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

Independent doxastic commitments — DC_x_ind_dox. The standard Stalnakerian assertion-driven cell.

Equations

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

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

Independent preferential commitments — DC_x_ind_pref. The @cite{condoravdi-lauer-2012} imperative-as-PEP cell.

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) : W → Prop

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 (@cite{bring-gunlogson-2000}). Used as:

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

• forP : ContextualEvidence

  Current context provides evidence for p.

• neutral : ContextualEvidence

  No contextual evidence either way.

• againstP : ContextualEvidence

  Current context provides evidence against p.

@[implicit_reducible]

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.instReprContextualEvidence.repr : ContextualEvidence → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Discourse.Commitment.instReprContextualEvidence : Repr ContextualEvidence

Equations

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

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

A commitment grade is the value type for a graded commitment. The typeclass exposes the operations the substrate needs to lift binary-only operators (bipolarQuestion, negatedQuestionLow, toContextSet) to arbitrary graded weights.

Instances:

• G = Prop: binary commitment (Krifka, F&B, Brandom, Stalnaker). complement := Not, support := id.
• G = Bool: Bool-valued commitment (Cohen-Krifka 2014 worked example with denegation markers). complement := !, support := (· = true).
• G = ℚ or G = ℝ: probabilistic / distributional (deferred until a study consumer; would set complement := (1 - ·), support := (· > 0) or threshold-based).

The typeclass is small on purpose — only complement and support are required, both per-grade-value (not per-weight-function). The per-weight projection follows by composition.

• support : G → Prop

  Support predicate: which grades count as "actively committing". For Prop: identity. For Bool: · = true. For ℝ_≥0: · > 0. For ℚ: · > 0 (or threshold). Used to project a weighted commitment to a binary context-set constraint.

  The minimal axiom-free typeclass for context-set projection. toContextSet and toCommitment consume only this.

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

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

  Negation/complement of a grade. For Prop: Not; for Bool: !; for ℚ ∈ [0,1]: 1 - ·. Used to construct the "no" branch of bipolar questions and the negated content of low-negation questions.

• support_complement_iff_not_support (g : G) : HasSupport.support (complement g) ↔ ¬HasSupport.support g

  Complement is the propositional dual of support: a grade's complement is supportable iff the grade itself is not. Holds for Prop (LEM-classically) and Bool (definitionally). Does NOT hold for ℝ in general (e.g., 0 < 1 - 1/2 = 1/2 AND 0 < 1/2); the law restricts CommitmentGrade instances to "Bool-shaped" grades. Anderson 2021's ℝ-distributional CG provides only HasSupport ℝ, not CommitmentGrade ℝ.

@[implicit_reducible]

instance Core.Discourse.Commitment.instHasSupportProp : HasSupport Prop

Equations

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

@[implicit_reducible]

instance Core.Discourse.Commitment.instCommitmentGradeProp : CommitmentGrade Prop

Equations

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

No Bool instance — by design

A CommitmentGrade Bool / HasSupport Bool instance was provided in the original typeclass landing (0.230.658). We removed it because no consumer needed it post-CohenKrifka2014's migration from G = Bool (decide-style) to G = Prop (structural-theorem style).

The Bool instance invited a "decide-and-done" worked-example shape that the user explicitly steered away from: linglib's thesis is structural theorems quantifying over content, not concrete-fixture decide-reduces-to-this units. Removing the instance signals that the typeclass is for formal grades (Prop, NNReal, lattice elements with laws), not for computational ones. Consumers that genuinely need Bool (e.g., for explicit decide-based smoke tests) can declare a local instance with full responsibility for its consequences.

Other potential grades (ℚ, ℝ, NNReal, lattices) provide instances at the consumer's site (e.g., Anderson 2021's HasSupport ℝ for distributional CG; Anderson does NOT provide CommitmentGrade ℝ because the involution law fails for unrestricted real-valued weights).

Polymorphic indexed commitments

IndexedWeightedCommitment W G is the substrate's polymorphic commitment type. Three orthogonal axes:

• committer : DiscourseRole — who is committing (Krifka 2015's S₁/S₂).
• force : CommitmentForce — doxastic (belief, declarative) vs preferential (Lauer 2013, Condoravdi-Lauer 2011). The doxastic case covers Krifka/Farkas-Bruce/Brandom assertion; the preferential case covers Lauer's imperative-as-PEP analysis.
• weight : W → G (commit) or content : W → Prop (refuse) — per-world grade in G. The G parameter selects framework granularity:
  • G = Prop: binary commitment (Krifka, Farkas-Bruce, Brandom, Stalnaker).
  • G = ℝ: distributional CG (@cite{anderson-2021}).
  • G = ℚ: credence-bounded (Lauer simplification).

The Krifka 2015 default is the binary doxastic case, exposed via the IndexedCommitment W abbreviation and smart constructors that hide the force and (via G = Prop) weight-vs-content asymmetry.

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

A polymorphic indexed commitment: who commits, with what force, with what per-world weight (or, for refusal, what content).

The commit constructor models S⊢φ — agent publicly commits to φ with weight weight : W → G per world. The refuse constructor models ¬S⊢φ — agent explicitly does NOT commit to content φ, distinct from committing to ¬φ. The refuse-content stays at W → Prop because refusal is a meta-fact about the agent's commitment slate, not about the world.

The force field has no current consumer that explicitly passes .preferential (every binary call site defaults to .doxastic via the smart constructors). The next demand for the .preferential branch is @cite{condoravdi-lauer-2012}'s imperative-as-PEP analysis; a study file using force := .preferential would be the first consumer to exercise this axis.

• 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: agent committed to φ at weight weight.

• 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 φ. Pragmatically weaker than commit committer .doxastic (fun w => ¬ φ w).

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

The agent who committed (or refused to commit).

Equations

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

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

The commitment force (doxastic / preferential).

Equations

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

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

Holds for commit, fails for refuse.

Equations

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

@[implicit_reducible]

instance Core.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 Core.Discourse.Commitment.IndexedWeightedCommitment.toCommitment {W : Type u_1} {G : Type u_2} [HasSupport G] : IndexedWeightedCommitment W G → W → Prop

Project to the propositional constraint imposed on the context set, polymorphic in G via [CommitmentGrade G].

A commit excludes worlds where the per-world weight is NOT in support (i.e., where support (weight w) is false). A refuse imposes no exclusion (it's a meta-fact about the agent, not about the world).

For G = Prop: support := id, so commit committer force φ projects to φ itself — recovering the binary toCommitment. For G = Bool: support := (· = true), so commit ... weight projects to fun w => weight w = true. For other G (ℚ, ℝ), the typeclass's support predicate determines the projection.

Equations

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

@[simp]

theorem Core.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)

toCommitment of a commit reduces to support of the per-world weight. The @[simp] form makes downstream proofs robust to reformulation of HasSupport.support (e.g. if the Prop instance changed from support := id to something else, proofs that rely on rfl-reducing through support would break silently; proofs that rewrite via this lemma keep working).

@[simp]

theorem Core.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

toCommitment of a refuse is trivially true.

@[reducible, inline]

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

Binary speaker-indexed commitment — the G = Prop specialisation. This is the Krifka 2015 default, used throughout the binary commitment-space substrate. The general type is IndexedWeightedCommitment W G.

Equations

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

@[reducible, inline]

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

Smart constructor for the doxastic binary commit case. Equivalent to IndexedWeightedCommitment.commit committer .doxastic content. Existing call sites that don't need preferential force or non-Prop grade use this. The @[match_pattern] attribute lets pattern-position use of IndexedCommitment.commit c φ resolve through the abbrev to the underlying 3-arg constructor.

Equations

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

@[reducible, inline]

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

Smart constructor for the doxastic binary refuse case.

Equations

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

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

The propositional content of the commitment (binary case). For commit, the weight W → Prop IS the content; for refuse, it's the refused content.

Equations

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

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

Project to the propositional constraint imposed on the context set. A commit excludes worlds incompatible with the weight; a refuse imposes no exclusion (it's a meta-fact about the agent, not about the world). For the CG-as-set view, only commit-cases narrow.

This is what makes refuse pragmatically weaker than commit (¬φ): refuse projects to True (no narrowing), while commit (¬φ) projects to ¬φ (narrows out φ-worlds).

Equations

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

@[implicit_reducible]

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

A commitment slate projects to a context set: the worlds compatible with all committed propositions.

Equations

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