Commitments

A public commitment is a participant's undertaking to act as if a proposition holds, in the tradition of Hamblin and Brandom: committer is committed to content. Three further coordinates distinguish the frameworks built on commitments: whether the commitment is undertaken or refused (Krifka's S⊢φ against ¬S⊢φ), the attitude it is a commitment to, belief or preference (Condoravdi and Lauer), and whether it was generated by the committer or attributed by the other party (Gunlogson). A discourse state records a set of such commitments; the propositions it entails form the filter generated by the undertaken contents, and the worlds it leaves open are that filter's kernel, so a commitment set projects onto the Stalnakerian common ground of Discourse/CommonGround.lean by Commitment.slate.

Main definitions

• Commitment A W: the atom, with Commitment.Stance, Commitment.Force, Commitment.Source.
• Commitment.State: a commitment state, the set of commitments accumulated so far.
• Commitment.contents, Commitment.slate, Commitment.contextSet: what a state undertakes, entails, and leaves open.

Main results

• Commitment.ker_slate: the context set is the kernel of the slate.
• Commitment.contextSet_insert_of_commit: a new commitment intersects the context set with its content.
• Commitment.contextSet_ofForce_insert_of_eq_of_commit, Commitment.contextSet_ofForce_insert_of_ne: a new commitment narrows the context set of its own attitude and no other.

References

• C. L. Hamblin, Fallacies (1970)
• R. Brandom, Making It Explicit (1994)
• A. Cohen and M. Krifka, Superlative quantifiers and meta-speech acts (2014)
• M. Krifka, Bias in Commitment Space Semantics: Declarative Questions, Negated Questions, and Question Tags (2015)
• C. Condoravdi and S. Lauer, Imperatives: Meaning and illocutionary force (2012)
• C. Gunlogson, A Question of Commitment (2008)

inductive Commitment.Stance : Type

Whether a commitment is undertaken or refused.

• commit : Stance

  The participant undertakes the commitment, [Kri15a]'s S⊢φ.

• refuse : Stance

  The participant refuses it, ¬S⊢φ, a denegation and not a commitment to the negation.

@[instance_reducible]

instance Commitment.instDecidableEqStance : DecidableEq Stance

Equations

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

@[instance_reducible]

instance Commitment.instReprStance : Repr Stance

Equations

• Commitment.instReprStance = { reprPrec := Commitment.instReprStance.repr }

def Commitment.instReprStance.repr : Stance → ℕ → Std.Format

Equations

• Commitment.instReprStance.repr Commitment.Stance.commit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Commitment.Stance.commit")).group prec✝
• Commitment.instReprStance.repr Commitment.Stance.refuse prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Commitment.Stance.refuse")).group prec✝

inductive Commitment.Force : Type

The attitude a commitment is to, belief or preference.

• doxastic : Force
• preferential : Force

@[instance_reducible]

instance Commitment.instDecidableEqForce : DecidableEq Force

Equations

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

@[instance_reducible]

instance Commitment.instReprForce : Repr Force

Equations

• Commitment.instReprForce = { reprPrec := Commitment.instReprForce.repr }

def Commitment.instReprForce.repr : Force → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Commitment.instReprForce.repr Commitment.Force.doxastic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Commitment.Force.doxastic")).group prec✝

inductive Commitment.Source : Type

Who generated the commitment, the committer or the other party attributing it.

• selfGenerated : Source
• otherGenerated : Source

@[instance_reducible]

instance Commitment.instDecidableEqSource : DecidableEq Source

Equations

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

def Commitment.instReprSource.repr : Source → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Commitment.instReprSource : Repr Source

Equations

• Commitment.instReprSource = { reprPrec := Commitment.instReprSource.repr }

structure Commitment (A : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

A public commitment, by which committer is committed to content.

• committer : A
• content : Set W
• stance : Stance
• force : Force
• source : Source

theorem Commitment.ext_iff {A : Type u_1} {W : Type u_2} {x y : Commitment A W} : x = y ↔ x.committer = y.committer ∧ x.content = y.content ∧ x.stance = y.stance ∧ x.force = y.force ∧ x.source = y.source

theorem Commitment.ext {A : Type u_1} {W : Type u_2} {x y : Commitment A W} (committer : x.committer = y.committer) (content : x.content = y.content) (stance : x.stance = y.stance) (force : x.force = y.force) (source : x.source = y.source) : x = y

theorem Filter.generate_insert {W : Type u_1} (φ : Set W) (S : Set (Set W)) : generate (insert φ S) = generate S ⊓ principal φ

@[reducible, inline]

abbrev Commitment.State (A : Type u_1) (W : Type u_2) : Type (max u_2 u_1)

A commitment state is the set of public commitments the interlocutors have accumulated up to a point in conversation ([CK14] §2.1, [Kri15a]).

Equations

• Commitment.State A W = Set (Commitment A W)

def Commitment.commit {A : Type u_1} {W : Type u_2} (a : A) (p : Set W) (force : Force := Force.doxastic) (source : Source := Source.selfGenerated) : Commitment A W

a commits to p.

Equations

• Commitment.commit a p force source = { committer := a, content := p, force := force, source := source }

def Commitment.refuse {A : Type u_1} {W : Type u_2} (a : A) (p : Set W) (force : Force := Force.doxastic) (source : Source := Source.selfGenerated) : Commitment A W

a refuses to commit to p.

Equations

• Commitment.refuse a p force source = { committer := a, content := p, stance := Commitment.Stance.refuse, force := force, source := source }

@[simp]

theorem Commitment.commit_stance {A : Type u_1} {W : Type u_2} (a : A) (p : Set W) (f : Force) (s : Source) : (commit a p f s).stance = Stance.commit

@[simp]

theorem Commitment.refuse_stance {A : Type u_1} {W : Type u_2} (a : A) (p : Set W) (f : Force) (s : Source) : (refuse a p f s).stance = Stance.refuse

@[simp]

theorem Commitment.commit_content {A : Type u_1} {W : Type u_2} (a : A) (p : Set W) (f : Force) (s : Source) : (commit a p f s).content = p

@[simp]

theorem Commitment.refuse_content {A : Type u_1} {W : Type u_2} (a : A) (p : Set W) (f : Force) (s : Source) : (refuse a p f s).content = p

@[simp]

theorem Commitment.commit_committer {A : Type u_1} {W : Type u_2} (a : A) (p : Set W) (f : Force) (s : Source) : (commit a p f s).committer = a

@[simp]

theorem Commitment.commit_force {A : Type u_1} {W : Type u_2} (a : A) (p : Set W) (f : Force) (s : Source) : (commit a p f s).force = f

@[simp]

theorem Commitment.commit_source {A : Type u_1} {W : Type u_2} (a : A) (p : Set W) (f : Force) (s : Source) : (commit a p f s).source = s

def Commitment.contents {A : Type u_1} {W : Type u_2} (K : State A W) : Set (Set W)

The contents of the undertaken commitments in K.

Equations

• Commitment.contents K = Commitment.content '' {c : Commitment A W | c ∈ K ∧ c.stance = Commitment.Stance.commit}

def Commitment.ofCommitter {A : Type u_1} {W : Type u_2} (K : State A W) (a : A) : State A W

The commitments of a in K.

Equations

• Commitment.ofCommitter K a = {c : Commitment A W | c ∈ K ∧ c.committer = a}

theorem Commitment.ofCommitter_insert_of_eq {A : Type u_1} {W : Type u_2} (K : State A W) (a : A) (c : Commitment A W) (h : c.committer = a) : ofCommitter (insert c K) a = insert c (ofCommitter K a)

theorem Commitment.ofCommitter_insert_of_ne {A : Type u_1} {W : Type u_2} (K : State A W) (a : A) (c : Commitment A W) (h : c.committer ≠ a) : ofCommitter (insert c K) a = ofCommitter K a

def Commitment.ofForce {A : Type u_1} {W : Type u_2} (K : State A W) (f : Force) : State A W

The commitments in K to the attitude f, PB for belief and PEP for preference ([CL12]).

Equations

• Commitment.ofForce K f = {c : Commitment A W | c ∈ K ∧ c.force = f}

def Commitment.slate {A : Type u_1} {W : Type u_2} (K : State A W) : Filter W

The filter generated by the undertaken commitments in K, which is what K entails.

Equations

• Commitment.slate K = Filter.generate (Commitment.contents K)

def Commitment.contextSet {A : Type u_1} {W : Type u_2} (K : State A W) : Set W

The worlds compatible with the undertaken commitments in K.

Equations

• Commitment.contextSet K = ⋂₀ Commitment.contents K

@[instance_reducible]

instance Commitment.instHasCommonGroundState {A : Type u_1} {W : Type u_2} : HasCommonGround (State A W) W

A commitment set's common ground is what it entails.

Equations

• Commitment.instHasCommonGroundState = { commonGround := Commitment.slate }

theorem Commitment.ker_slate {A : Type u_1} {W : Type u_2} (K : State A W) : (slate K).ker = contextSet K

theorem Commitment.mem_slate_of_mem {A : Type u_1} {W : Type u_2} (K : State A W) {φ : Set W} (h : φ ∈ contents K) : φ ∈ slate K

theorem Commitment.contextSet_subset_of_mem_contents {A : Type u_1} {W : Type u_2} (K : State A W) {φ : Set W} (h : φ ∈ contents K) : contextSet K ⊆ φ

theorem Commitment.contextSet_subset_of_mem_slate {A : Type u_1} {W : Type u_2} (K : State A W) {φ : Set W} (h : φ ∈ slate K) : contextSet K ⊆ φ

theorem Commitment.not_mem_slate_of_compl_mem {A : Type u_1} {W : Type u_2} (K : State A W) {φ : Set W} (h : φᶜ ∈ contents K) (hne : (contextSet K).Nonempty) : φ ∉ slate K

A consistent commitment set committed to ¬φ does not entail φ.

theorem Commitment.contents_mono {A : Type u_1} {W : Type u_2} {K L : State A W} (h : K ⊆ L) : contents K ⊆ contents L

theorem Commitment.slate_mono {A : Type u_1} {W : Type u_2} {K L : State A W} (h : K ⊆ L) : slate L ≤ slate K

@[simp]

theorem Commitment.contents_empty {A : Type u_1} {W : Type u_2} : contents ∅ = ∅

@[simp]

theorem Commitment.slate_empty {A : Type u_1} {W : Type u_2} : slate ∅ = ⊤

theorem Commitment.contents_insert_of_commit {A : Type u_1} {W : Type u_2} {K : State A W} {c : Commitment A W} (h : c.stance = Stance.commit) : contents (insert c K) = insert c.content (contents K)

theorem Commitment.contents_insert_of_refuse {A : Type u_1} {W : Type u_2} {K : State A W} {c : Commitment A W} (h : c.stance = Stance.refuse) : contents (insert c K) = contents K

theorem Commitment.slate_insert_of_commit {A : Type u_1} {W : Type u_2} {K : State A W} {c : Commitment A W} (h : c.stance = Stance.commit) : slate (insert c K) = slate K ⊓ Filter.principal c.content

A new commitment adds its content to the slate.

theorem Commitment.contextSet_insert_of_commit {A : Type u_1} {W : Type u_2} {K : State A W} {c : Commitment A W} (h : c.stance = Stance.commit) : contextSet (insert c K) = c.content ∩ contextSet K

A new commitment intersects the context set with its content.

theorem Commitment.ofForce_insert_of_eq {A : Type u_1} {W : Type u_2} {K : State A W} {c : Commitment A W} {f : Force} (h : c.force = f) : ofForce (insert c K) f = insert c (ofForce K f)

theorem Commitment.ofForce_insert_of_ne {A : Type u_1} {W : Type u_2} {K : State A W} {c : Commitment A W} {f : Force} (h : c.force ≠ f) : ofForce (insert c K) f = ofForce K f

theorem Commitment.contextSet_ofForce_insert_of_eq_of_commit {A : Type u_1} {W : Type u_2} {K : State A W} {c : Commitment A W} {f : Force} (hf : c.force = f) (hp : c.stance = Stance.commit) : contextSet (ofForce (insert c K) f) = c.content ∩ contextSet (ofForce K f)

A new commitment to the attitude f intersects the f-context set with its content.

theorem Commitment.contextSet_ofForce_insert_of_ne {A : Type u_1} {W : Type u_2} {K : State A W} {c : Commitment A W} {f : Force} (h : c.force ≠ f) : contextSet (ofForce (insert c K) f) = contextSet (ofForce K f)

A new commitment to another attitude leaves the f-context set alone.

@[simp]

theorem Commitment.contextSet_empty {A : Type u_1} {W : Type u_2} : contextSet ∅ = Set.univ

theorem Commitment.contents_union {A : Type u_1} {W : Type u_2} (K L : State A W) : contents (K ∪ L) = contents K ∪ contents L

theorem Commitment.contextSet_union {A : Type u_1} {W : Type u_2} (K L : State A W) : contextSet (K ∪ L) = contextSet K ∩ contextSet L

Context sets intersect across a union of commitment sets.

theorem Commitment.contextSet_eq_inter_ofForce {A : Type u_1} {W : Type u_2} {K : State A W} : contextSet K = contextSet (ofForce K Force.doxastic) ∩ contextSet (ofForce K Force.preferential)

The context set is the meet of the doxastic and the preferential context sets.

theorem Commitment.contents_image_commit {A : Type u_1} {W : Type u_2} {ι : Type u_3} (a : A) (p : ι → Set W) (s : Set ι) : contents ((fun (i : ι) => commit a (p i)) '' s) = p '' s

The contents of a family of commitments by a are the family's contents.

theorem Commitment.contextSet_insert_of_refuse {A : Type u_1} {W : Type u_2} {K : State A W} {c : Commitment A W} (h : c.stance = Stance.refuse) : contextSet (insert c K) = contextSet K

A refusal leaves the context set alone.