Preferential commitments and effective preferences

A commitment of force .preferential is [CL12]'s PEP(a, p), a's public commitment to act as though p were a maximal element of a's effective preference structure, the consistent ranking of propositions that guides a's actions. A commitment state is sincere at a world when each of its preferential commitments is an effective preference there, Desire.Preferential.Want: the sincerity condition on a directive use of an imperative. Through the consistency of the effective preference structure, sincerity is what makes successive imperatives consistent (Studies/CondoravdiLauer2012.lean) and what excludes a force-augmenting particle from contexts in which the preference it expresses is unrealizable (Studies/Deo2025.lean).

References

• [CL12]
• [Deo25]

def Commitment.Sincere {A : Type u_1} {W : Type u_2} (P : A → W → PreferenceStructure W) (K : State A W) (w : W) : Prop

The preferential commitments in K are effective preferences at w.

Equations

• Commitment.Sincere P K w = ∀ c ∈ K, c.force = Commitment.Force.preferential → c.stance = Commitment.Stance.commit → Desire.Preferential.Want P c.committer c.content w

theorem Commitment.Sincere.mono {A : Type u_1} {W : Type u_2} {P : A → W → PreferenceStructure W} {K L : State A W} {w : W} (hL : Sincere P L w) (h : K ⊆ L) : Sincere P K w

theorem Commitment.Sincere.want {A : Type u_1} {W : Type u_2} {P : A → W → PreferenceStructure W} {K : State A W} {w : W} (hs : Sincere P K w) {a : A} {p : Set W} (h : commit a p Force.preferential ∈ K) : Desire.Preferential.Want P a p w