Docs / Discourse / Commitment / Proposition

Commitment propositions

import Linglib.Discourse.Commitment.Proposition · namespace Commitment

Source

In Krifka's account a commitment is itself a proposition, so k⊢φ holds at the worlds where k vouches for φ. Over an accessibility O k for each holder k it is the core of φ, the worlds all of whose O k-successors are φ-worlds. It is closed under consequence and conjunction, its complement is the refusal ¬k⊢φ, and a common ground can contain it without containing φ. Asserting φ is the performative update that makes k⊢φ hold everywhere. Public commitment sets give the accessibilities that do not depend on the world, and a commitment state of Commitment.Basic projects onto them. Indices that pair a fact with every holder's commitment set are the canonical model in which commitments vary from world to world.

Main definitions

Main results

References

Declarations

The proposition k⊢φ holds at the worlds all of whose O k-successors are φ-worlds, where k is committed to φ.

def committedL56–58
{κ : Type u_1} {W : Type u_2} (O : κ → SetRel W W) (k : κ) (φ : Set W) :
Set W

Used by mem_committed, committed_mono, committed_inter, committed_univ, committed_iInter, disjoint_committed_compl, committed_perform_self, perform_eq_self_iff, committed_ofSets, Index.committed_access_preimage

Used in Discourse/Commitment/Frame, Discourse/Commitment/Space, Discourse/SpeechAct, CohenKrifka2014, Krifka2015

The performative update by k's commitment to φ keeps the φ-successors of O k and leaves every other accessibility unchanged (van der Leer 2026 Definition 4).

def performL60–62
{κ : Type u_1} {W : Type u_2} (O : κ → SetRel W W) (k : κ) (φ : Set W) :
κ → SetRel W W
  • perform O k φ k' = {p : W × W | p ∈ O k' ∧ (k' = k → p.2 ∈ φ)}

Used by mem_perform, perform_subset, perform_of_ne, committed_perform_self, perform_mono, perform_perform, perform_eq_self_iff, instIsK45FramePerform, perform_ofSets, ofSets_commitmentSet_insert

Used in Discourse/Commitment/Frame

L66
L68–69
L74
L88–89
L91
L93–94
L99–100
L107–112

Public commitment sets

L132–133

Indices