Commitment spaces

A commitment space is a set of discourse states with a least member, its root: the current state together with the continuations it projects. Speech acts transform spaces in two ways. A basic act keeps the projected states that carry its commitments, and the least of them is the new root. A meta-speech act keeps the root and prunes the continuations: a question restricts them to the answers it proposes, a denegation removes the states an act would reach. Conjunction and disjunction of acts are intersection and union of the sets of states they reach, which need not be rooted, so the laws relating the acts are stated on those sets.

Commitment Space Semantics is the instance over commitment states, sets of Commitments ordered by inclusion, where a basic act adds a set of commitments and an assertion adds the speaker's commitment to a proposition.

Main definitions

• Commitment.Space S: rooted sets of states, ordered by inclusion, with the free space Space.Ici.
• Space.restrict, Space.denegate: the meta-speech acts.
• Space.update: the basic act adding k.
• Space.assert: assertion in Commitment Space Semantics.

Main results

• Space.root_update_mem_iff, Space.coe_update_of_root_mem: a space admits an update iff its states above k have a least member, and the update is then the restriction {c ∈ C | √C + A ⊆ c}.
• Space.coe_update_sSup: the update by a join is the conjunction of the updates.
• Space.sdiff_coe_denegate, Space.coe_denegate_inter: two denegations cancel, and de Morgan's laws hold for them.

Implementation notes

• The operations are total. restrict and denegate always keep the root, and update roots at the meet of the states above k, adjoining it when it is not one of them. The space admits the update when that root is one of its states, (C.update k).root ∈ C; this and "not redundant", ¬ k ≤ C.root, are hypotheses of the theorems, not arguments of the operations.
• The root of an update is k ⊔ C.root only when the space projects that state (Space.root_update_of_mem). After a question it carries the proposal as well, so an assertion on a space need not add exactly its content to the common ground.
• The root is a field; it is determined by the states, which makes Space S a SetLike.

References

• 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)
• T. van der Leer, Commitments, beliefs and expectations in conversation (2026)

structure Commitment.Space (S : Type u_1) [LE S] : Type u_1

A commitment space is a set of states with a least member, its root.

• carrier : Set S

  The states the space projects.

• root : S

  The current state.

• isLeast' : IsLeast self.carrier self.root

  The root is the least state.

@[instance_reducible]

instance Commitment.Space.instSetLike {S : Type u_1} [PartialOrder S] : SetLike (Space S) S

Equations

• Commitment.Space.instSetLike = { coe := Commitment.Space.carrier, coe_injective := ⋯ }

@[instance_reducible]

instance Commitment.Space.instPartialOrder {S : Type u_1} [PartialOrder S] : PartialOrder (Space S)

Spaces are ordered by inclusion, and the smaller space is the stronger act.

Equations

• Commitment.Space.instPartialOrder = PartialOrder.ofSetLike (Commitment.Space S)

theorem Commitment.Space.ext {S : Type u_1} [PartialOrder S] {C D : Space S} (h : ∀ (c : S), c ∈ C ↔ c ∈ D) : C = D

theorem Commitment.Space.ext_iff {S : Type u_1} [PartialOrder S] {C D : Space S} : C = D ↔ ∀ (c : S), c ∈ C ↔ c ∈ D

@[simp]

theorem Commitment.Space.mem_carrier {S : Type u_1} [PartialOrder S] (C : Space S) {c : S} : c ∈ C.carrier ↔ c ∈ C

@[simp]

theorem Commitment.Space.mem_mk {S : Type u_1} [PartialOrder S] {c : S} {s : Set S} {r : S} (h : IsLeast s r) : c ∈ { carrier := s, root := r, isLeast' := h } ↔ c ∈ s

@[simp]

theorem Commitment.Space.coe_mk {S : Type u_1} [PartialOrder S] {s : Set S} {r : S} (h : IsLeast s r) : ↑{ carrier := s, root := r, isLeast' := h } = s

theorem Commitment.Space.isLeast {S : Type u_1} [PartialOrder S] (C : Space S) : IsLeast (↑C) C.root

theorem Commitment.Space.root_mem {S : Type u_1} [PartialOrder S] (C : Space S) : C.root ∈ C

theorem Commitment.Space.root_le {S : Type u_1} [PartialOrder S] (C : Space S) {c : S} (hc : c ∈ C) : C.root ≤ c

@[instance_reducible]

instance Commitment.Space.instSingleton {S : Type u_1} [PartialOrder S] : Singleton S (Space S)

The space with only its root.

Equations

• Commitment.Space.instSingleton = { singleton := fun (c : S) => { carrier := {c}, root := c, isLeast' := ⋯ } }

@[simp]

theorem Commitment.Space.coe_singleton {S : Type u_1} [PartialOrder S] (c : S) : ↑{c} = {c}

@[simp]

theorem Commitment.Space.mem_singleton {S : Type u_1} [PartialOrder S] {c d : S} : d ∈ {c} ↔ d = c

@[simp]

theorem Commitment.Space.root_singleton {S : Type u_1} [PartialOrder S] (c : S) : {c}.root = c

def Commitment.Space.Ici {S : Type u_1} [PartialOrder S] (c : S) : Space S

The free space on c has every state above c.

Equations

• Commitment.Space.Ici c = { carrier := Set.Ici c, root := c, isLeast' := ⋯ }

@[simp]

theorem Commitment.Space.coe_Ici {S : Type u_1} [PartialOrder S] (c : S) : ↑(Space.Ici c) = Set.Ici c

@[simp]

theorem Commitment.Space.mem_Ici {S : Type u_1} [PartialOrder S] {c d : S} : d ∈ Space.Ici c ↔ c ≤ d

@[simp]

theorem Commitment.Space.root_Ici {S : Type u_1} [PartialOrder S] (c : S) : (Space.Ici c).root = c

Meta-speech acts

def Commitment.Space.restrict {S : Type u_1} [PartialOrder S] (C : Space S) (D : Set S) : Space S

C.restrict D has the root and the members of C in D. A meta-speech act is such a restriction, which keeps the root and prunes the continuations.

Equations

• C.restrict D = { carrier := insert C.root (↑C ∩ D), root := C.root, isLeast' := ⋯ }

@[simp]

theorem Commitment.Space.root_restrict {S : Type u_1} [PartialOrder S] (C : Space S) (D : Set S) : (C.restrict D).root = C.root

@[simp]

theorem Commitment.Space.coe_restrict {S : Type u_1} [PartialOrder S] (C : Space S) (D : Set S) : ↑(C.restrict D) = insert C.root (↑C ∩ D)

@[simp]

theorem Commitment.Space.mem_restrict {S : Type u_1} [PartialOrder S] (C : Space S) {D : Set S} {d : S} : d ∈ C.restrict D ↔ d = C.root ∨ d ∈ C ∧ d ∈ D

theorem Commitment.Space.coe_restrict_of_root_mem {S : Type u_1} [PartialOrder S] (C : Space S) {D : Set S} (h : C.root ∈ D) : ↑(C.restrict D) = ↑C ∩ D

theorem Commitment.Space.coe_restrict_union {S : Type u_1} [PartialOrder S] (C : Space S) (D E : Set S) : ↑(C.restrict (D ∪ E)) = ↑(C.restrict D) ∪ ↑(C.restrict E)

Restricting to a union is the disjunction of the restrictions.

theorem Commitment.Space.coe_restrict_inter {S : Type u_1} [PartialOrder S] (C : Space S) (D E : Set S) : ↑(C.restrict (D ∩ E)) = ↑(C.restrict D) ∩ ↑(C.restrict E)

Restricting to an intersection is the conjunction of the restrictions.

def Commitment.Space.denegate {S : Type u_1} [PartialOrder S] (C : Space S) (D : Set S) : Space S

The denegation C − D has the root and the members of C outside D ([CK14] (26), [Kri15a] (5), [vdL26] Definition 22).

Equations

• C.denegate D = C.restrict Dᶜ

@[simp]

theorem Commitment.Space.root_denegate {S : Type u_1} [PartialOrder S] (C : Space S) (D : Set S) : (C.denegate D).root = C.root

@[simp]

theorem Commitment.Space.mem_denegate {S : Type u_1} [PartialOrder S] (C : Space S) {D : Set S} {d : S} : d ∈ C.denegate D ↔ d = C.root ∨ d ∈ C ∧ d ∉ D

theorem Commitment.Space.coe_denegate_of_root_notMem {S : Type u_1} [PartialOrder S] (C : Space S) {D : Set S} (h : C.root ∉ D) : ↑(C.denegate D) = ↑C \ D

Denegating an act that moves the root leaves the relative complement.

theorem Commitment.Space.sdiff_coe_denegate {S : Type u_1} [PartialOrder S] (C : Space S) {D : Set S} (hD : D ⊆ ↑C) (h : C.root ∉ D) : ↑C \ ↑(C.denegate D) = D

Two denegations cancel ([CK14] (28)).

theorem Commitment.Space.coe_denegate_inter {S : Type u_1} [PartialOrder S] (C : Space S) (D E : Set S) : ↑(C.denegate (D ∩ E)) = ↑(C.denegate D) ∪ ↑(C.denegate E)

De Morgan's law ∼[A & B] = ∼A ∨ ∼B for denegations ([CK14] (34)).

theorem Commitment.Space.coe_denegate_union {S : Type u_1} [PartialOrder S] (C : Space S) (D E : Set S) : ↑(C.denegate (D ∪ E)) = ↑(C.denegate D) ∩ ↑(C.denegate E)

De Morgan's law ∼[A ∨ B] = ∼A & ∼B for denegations ([CK14] (35)), whose two sides are rooted though the disjunction is not.

Basic speech acts

def Commitment.Space.update {S : Type u_1} [CompleteLattice S] (C : Space S) (k : S) : Space S

The update C + k has the states of C above k, rooted at their meet ([CK14] (23), [Kri15a] (2), (3)).

Equations

• C.update k = { carrier := insert (sInf (↑C ∩ Set.Ici k)) (↑C ∩ Set.Ici k), root := sInf (↑C ∩ Set.Ici k), isLeast' := ⋯ }

theorem Commitment.Space.root_update {S : Type u_1} [CompleteLattice S] (C : Space S) (k : S) : (C.update k).root = sInf (↑C ∩ Set.Ici k)

@[simp]

theorem Commitment.Space.mem_update {S : Type u_1} [CompleteLattice S] (C : Space S) {k d : S} : d ∈ C.update k ↔ d = (C.update k).root ∨ d ∈ C ∧ k ≤ d

theorem Commitment.Space.le_root_update {S : Type u_1} [CompleteLattice S] (C : Space S) (k : S) : k ≤ (C.update k).root

theorem Commitment.Space.root_le_root_update {S : Type u_1} [CompleteLattice S] (C : Space S) (k : S) : C.root ≤ (C.update k).root

theorem Commitment.Space.root_update_mem_iff {S : Type u_1} [CompleteLattice S] (C : Space S) {k : S} : (C.update k).root ∈ C ↔ ∃ (r : S), IsLeast (↑C ∩ Set.Ici k) r

The space admits an update, in that the new root is one of its states, iff its states above k have a least member.

theorem Commitment.Space.root_update_of_mem {S : Type u_1} [CompleteLattice S] (C : Space S) {k : S} (h : k ⊔ C.root ∈ C) : (C.update k).root = k ⊔ C.root

When the space projects the root joined with k, that state is the root of the update.

theorem Commitment.Space.coe_update_of_root_mem {S : Type u_1} [CompleteLattice S] (C : Space S) {k : S} (h : (C.update k).root ∈ C) : ↑(C.update k) = ↑C ∩ Set.Ici k

An update the space admits is its restriction to the states above k.

theorem Commitment.Space.update_le {S : Type u_1} [CompleteLattice S] (C : Space S) {k : S} (h : (C.update k).root ∈ C) : C.update k ≤ C

theorem Commitment.Space.root_mem_update_iff {S : Type u_1} [CompleteLattice S] (C : Space S) {k : S} : C.root ∈ C.update k ↔ k ≤ C.root

The root survives an update iff the update is redundant.

theorem Commitment.Space.update_le_update {S : Type u_1} [CompleteLattice S] (C : Space S) {k l : S} (hkl : k ≤ l) (h : (C.update l).root ∈ C) : C.update l ≤ C.update k

Adding more is the stronger act ([CK14] (86)).

theorem Commitment.Space.update_congr {S : Type u_1} [CompleteLattice S] (C : Space S) {k l : S} {C' : Space S} (h : ↑C ∩ Set.Ici k = ↑C' ∩ Set.Ici l) : C.update k = C'.update l

Updates agree when the same states carry them.

theorem Commitment.Space.update_update {S : Type u_1} [CompleteLattice S] (C : Space S) {k : S} (h : (C.update k).root ∈ C) (l : S) : (C.update k).update l = C.update (l ⊔ k)

Consecutive updates are the update by the join, when the space admits the first.

theorem Commitment.Space.update_comm {S : Type u_1} [CompleteLattice S] (C : Space S) {k l : S} (hk : (C.update k).root ∈ C) (hl : (C.update l).root ∈ C) : (C.update k).update l = (C.update l).update k

Admitted updates commute ([CK14] (31), [Kri15a] (6)).

theorem Commitment.Space.restrict_coe_update {S : Type u_1} [CompleteLattice S] (C : Space S) (k : S) : C.restrict ↑(C.update k) = C.restrict (Set.Ici k)

Restricting to an update keeps the members above k, admitted or not.

theorem Commitment.Space.update_restrict_of_subset {S : Type u_1} [CompleteLattice S] (C : Space S) {D : Set S} {k : S} (h : ↑C ∩ Set.Ici k ⊆ D) : (C.restrict D).update k = C.update k

A restriction that keeps the states above k leaves the update by k as it was.

theorem Commitment.Space.coe_update_sSup {S : Type u_1} [CompleteLattice S] (C : Space S) {K : Set S} (hK : K.Nonempty) (h : (C.update (sSup K)).root ∈ C) : ↑(C.update (sSup K)) = ⋂ k ∈ K, ↑(C.update k)

The update by a join is the conjunction of the updates ([CK14] (31)), when the space admits it.

Commitment space semantics

def Commitment.Space.assert {A : Type u_1} {W : Type u_2} (C : Space (State A W)) (a : A) (φ : Set W) (force : Force := Force.doxastic) : Space (State A W)

In the assertion C + S⊢φ, a commits to φ ([CK14] (37), [Kri15a] (14)).

Equations

• C.assert a φ force = C.update {Commitment.commit a φ force}

theorem Commitment.Space.mem_assert {A : Type u_1} {W : Type u_2} (C : Space (State A W)) (a : A) (φ : Set W) (force : Force) {d : State A W} : d ∈ C.assert a φ force ↔ d = (C.assert a φ force).root ∨ d ∈ C ∧ commit a φ force ∈ d

theorem Commitment.Space.commit_mem_root_assert {A : Type u_1} {W : Type u_2} (C : Space (State A W)) (a : A) (φ : Set W) (force : Force) : commit a φ force ∈ (C.assert a φ force).root

theorem Commitment.Space.root_assert_of_mem {A : Type u_1} {W : Type u_2} (C : Space (State A W)) (a : A) (φ : Set W) (force : Force) (h : insert (commit a φ force) C.root ∈ C) : (C.assert a φ force).root = insert (commit a φ force) C.root

When the space projects the root with the new commitment, that state is the root of the assertion.

theorem Commitment.Space.root_mem_assert_iff {A : Type u_1} {W : Type u_2} (C : Space (State A W)) (a : A) (φ : Set W) (force : Force) : C.root ∈ C.assert a φ force ↔ commit a φ force ∈ C.root

The root survives an assertion iff the assertion is redundant.