Docs / Discourse / Commitment / Sincerity

Sincerity

import Linglib.Discourse.Commitment.Sincerity · namespace Commitment

A public commitment is sincere when the committer privately holds what it is committed to under the attitude of its force, belief for a doxastic commitment and preference for a preferential one. Sincerity relates a commitment state to an attitude for each holder, given as the propositions the holder holds at each world. Condoravdi and Lauer's sincerity condition on a directive use of an imperative is the preferential case, with effective preferences (Desire.Preferential.Want) as the attitude. Through the consistency of the effective preference structure it makes successive imperatives consistent (Studies/CondoravdiLauer2012.lean), and it excludes a force-augmenting particle from contexts in which the preference it expresses is unrealizable (Studies/Deo2025.lean). The doxastic case is the Sincerity of van der Leer's frames (Commitment.Frame.sincere_iff_forall_sincere_toState).

Main definitions

Commitment.Sincere M K w: every holder in K holds at w what it is committed to, under the attitude M gives the holder.
Commitment.effectivePreference P: effective preference as the attitude of preferential commitments, with doxastic commitments unconstrained.

References

Condoravdi & Lauer 2012, Imperatives: Meaning and Illocutionary Force formalized
Deo 2025, Take on This Commitment: The Particle bərə in Marathi (Indo-Aryan) formalized
van der Leer 2026, Commitments, beliefs and expectations in conversation: Understanding the effect of speech acts in logic formalized

Declarations

A commitment state is sincere at w relative to the attitudes M when every holder holds at w, under its attitude M k, each proposition it is committed to.

def Sincere L44–47

{κ : Type u_1} {W : Type u_3} (M : κ → W → Set (Set W)) (K : State κ W) (w : W) :

Prop

Sincere M K w = ∀ (k : κ) (p : Set W), (k, p) ∈ K → p ∈ M k w

Used by Sincere.mono, Sincere.mem, Sincere.want

Used in Discourse/Commitment/Frame, CondoravdiLauer2012, Deo2025

The attitudes of Condoravdi & Lauer 2012's sincerity condition hold a preferential commitment when its content is an effective preference and leave doxastic commitments unconstrained.

def effectivePreference L49–53

{A : Type u_2} {W : Type u_3} (P : A → W → PreferenceStructure W) :

A × Force → W → Set (Set W)

effectivePreference P (fst, Force.doxastic) = ⊤
effectivePreference P (a, Force.preferential) = fun (w : W) => {p : Set W | Desire.Preferential.Want P a p w}

Used by Sincere.want

Used in CondoravdiLauer2012, Deo2025

L57–58

L60–61

L63–66