Condoravdi and Lauer 2012: imperatives as preferential commitments

Condoravdi and Lauer give declaratives and imperatives one kind of conventional effect, a public commitment of the speaker, differing in the attitude committed to: a declarative commits the speaker to act as though believing its content, an imperative to act as though the content were a maximal element of the speaker's effective preference structure, the consistent ranking of propositions that guides action. The range of uses, from commands to wishes, permissions and disinterested advice, comes from the context, while the constraints on every use come from the commitment: successive imperatives are consistent because the maximal elements of a consistent structure are jointly realizable, the speaker cannot be insincere because the commitment is self-verifying, and a preference against the content survives a concession but not disinterested advice, since the addressee's goal enters the adviser's structure at the bottom by cooperation by default. The paper's formal points against ordering-source affirmation and, in its discussion of To-Do Lists, against a secondary update of the ordering source are checked as well.

Implementation notes

The information state of a preference structure is its world type, so the paper's consistency is PreferenceStructure.Consistent Set.univ; the theorems take an information state B, since the paper's incompatibility is relative to what the speaker believes. A public effective preference is a commitment of force .preferential; the doxastic reduction of a commitment to one's own preferential commitment, which the paper takes over from the authors' earlier work, is a hypothesis on the world-indexed commitment state. Disinterested advice identifies the content with the adopted goal, which the paper reaches through a means-end inference, and quantifies over the effective structure alone where cooperation by default ranges over all of the adviser's structures.

TODO

• Informal in the paper and not formalized: the two preconditions and the re-ranking of a permission, the second meaning component (36) that limits speaker involvement and excludes promises, the two conditions on wish uses behind (37), the conditional preferences of offers (41), and the practical reasoning step by which the preliminary semantics (32) is recovered from the final (34).

References

• C. Condoravdi and S. Lauer, Imperatives: Meaning and illocutionary force (2012)
• C. Condoravdi and S. Lauer, Performative verbs and performative acts (2011)
• S. Schmerling, How imperatives are special, and how they aren't (1982)
• M. Schwager, Interpreting Imperatives (2006)
• S. Kaufmann and M. Schwager, A unified analysis of conditional imperatives (2009)
• M. Kaufmann, Interpreting Imperatives (2012)
• P. Portner, Imperatives and modals (2007)

Effective preferences and public commitments

Want P a p w is the effective preference EP_w(a, p): p is a maximal element of a's effective preference structure P a w, the distinguished consistent structure that determines a's action choices, (28) and (29). The public commitments of §3.2 are Commitments: commit a p is PB(a, p), to act as though believing p, and commit a p .preferential is PEP(a, p), to act as though p were a maximal effective preference; a speaker commits to an effective preference only when holding it, condition (iii) of §3.4, Commitment.Sincere.

The conventions

theorem CondoravdiLauer2012.declarative_contextSets {A : Type u_1} {W : Type u_2} (a : A) (p : Set W) (K : Commitment.State A W) : Commitment.contextSet (Commitment.ofForce (insert (Commitment.commit a p) K) Commitment.Force.doxastic) = p ∩ Commitment.contextSet (Commitment.ofForce K Commitment.Force.doxastic) ∧ Commitment.contextSet (Commitment.ofForce (insert (Commitment.commit a p) K) Commitment.Force.preferential) = Commitment.contextSet (Commitment.ofForce K Commitment.Force.preferential)

Uttering a declarative, whose propositional denotation falls under the convention (30), narrows the doxastic context set by the content and leaves the preferential one as it was.

theorem CondoravdiLauer2012.imperative_contextSets {A : Type u_1} {W : Type u_2} (a : A) (p : Set W) (K : Commitment.State A W) : Commitment.contextSet (Commitment.ofForce (insert (Commitment.commit a p Commitment.Force.preferential) K) Commitment.Force.preferential) = p ∩ Commitment.contextSet (Commitment.ofForce K Commitment.Force.preferential) ∧ Commitment.contextSet (Commitment.ofForce (insert (Commitment.commit a p Commitment.Force.preferential) K) Commitment.Force.doxastic) = Commitment.contextSet (Commitment.ofForce K Commitment.Force.doxastic)

Uttering an imperative under the imperative convention (47) narrows the preferential context set by the content and leaves the doxastic one as it was, so an imperative never claims its content, (10).

Self-verification

def CondoravdiLauer2012.imp {A : Type u_1} {W : Type u_2} (K : W → Commitment.State A W) (a : A) (p : Set W) : Set W

The denotation (34) of IMP(p) over a world-indexed commitment state is the set of worlds at which the speaker is publicly committed to an effective preference for p.

Equations

• CondoravdiLauer2012.imp K a p = {w : W | Commitment.commit a p Commitment.Force.preferential ∈ K w}

def CondoravdiLauer2012.DoxasticReduction {A : Type u_1} {W : Type u_2} (K : W → Commitment.State A W) : Prop

Doxastic reduction for preference commitment, after [CL11], identifies a doxastic commitment to one's own preferential commitment with that preferential commitment.

Equations

• CondoravdiLauer2012.DoxasticReduction K = ∀ (w : W) (c : Commitment A W), c.force = Commitment.Force.preferential → Commitment.commit c.committer {v : W | c ∈ K v} ∈ K w → c ∈ K w

theorem CondoravdiLauer2012.imp_self_verifying {A : Type u_1} {W : Type u_2} {a : A} {p : Set W} {w : W} {K : W → Commitment.State A W} (hK : DoxasticReduction K) (h : Commitment.commit a (imp K a p) ∈ K w) : w ∈ imp K a p

An imperative is self-verifying, §3.3: the doxastic commitment to IMP(p) that (30) assigns to its utterance is true at the world of utterance, so the utterance cannot be insincere and is not open to the challenges of (23) to (25). The operator implementation of §6 thereby ends in the commitment the imperative convention (47) assigns to the denotation p directly.

Directive uses

theorem CondoravdiLauer2012.directive_want_addressee {A : Type u_1} {W : Type u_2} {P : A → W → PreferenceStructure W} {a : A} {p : Set W} {w : W} {K : Commitment.State A W} {ad : A} (hs : Commitment.Sincere P K w) (hp : Commitment.commit a p Commitment.Force.preferential ∈ K) (hii : p ⊆ {v : W | Desire.Preferential.Want P ad p v}) : Desire.Preferential.WantNecessary P a {v : W | Desire.Preferential.Want P ad p v} w

In a directive context the final semantics (34) makes a preferential commitment to p an effective preference satisfied only if the addressee effectively prefers p, §3.4, given that the speaker commits sincerely, (iii), and believes the addressee's effective preference for p a precondition of p, (ii) under (i). The paper reaches the exact-match effective preference for the addressee's preference, the private counterpart of the preliminary (32), by a step of practical reasoning it leaves informal; without it, the only-if reading is what follows.

Consistency

theorem CondoravdiLauer2012.imperatives_consistent {A : Type u_1} {W : Type u_2} {P : A → W → PreferenceStructure W} {a : A} {w : W} {K : Commitment.State A W} {B : Set W} (hC : (P a w).Consistent B) (hs : Commitment.Sincere P K w) : (B ∩ Commitment.contextSet (Commitment.ofForce (Commitment.ofCommitter K a) Commitment.Force.preferential)).Nonempty

The preferential commitments of a sincere speaker with consistent effective preferences are jointly realizable in the information state: successive imperatives are consistent, §2.1.

theorem CondoravdiLauer2012.imperatives_revise {A : Type u_1} {W : Type u_2} {P : A → W → PreferenceStructure W} {a : A} {p q : Set W} {w : W} {K : Commitment.State A W} {B : Set W} (hC : (P a w).Consistent B) (hp : Commitment.commit a p Commitment.Force.preferential ∈ K) (hq : Commitment.commit a q Commitment.Force.preferential ∈ K) (h : B ∩ (p ∩ q) = ∅) : ¬Commitment.Sincere P K w

Two imperatives with incompatible contents are not both sincere at one time, (11) and (15): the second revises the speaker's effective preferences, (12) to (14).

Endorsement: advice, permission, concession

theorem CondoravdiLauer2012.advice_compatible {W : Type u_2} {q : Set W} {S : PreferenceStructure W} {B g : Set W} (hC : S.Consistent B) (hb : ∀ r ∈ S.prefs, ¬S.prec r g) (hg : g ∈ S.maxElts) (hq : q ∈ S.prefs) : (B ∩ (g ∩ q)).Nonempty

In disinterested advice, (39) and (40), a goal adopted by cooperation by default, with nothing ranked below it in the effective structure, is an effective preference only if no preference of the agent, effective or not, conflicts with it, so the follow-ups but I don't want you to and but I wish you would not are both out.

theorem CondoravdiLauer2012.concession_not_want {W : Type u_2} {p q : Set W} {S : PreferenceStructure W} {B : Set W} (hC : S.Consistent B) (hp : p ∈ S.maxElts) (hq : q ∈ S.prefs) (h : B ∩ (p ∩ q) = ∅) : q ∉ S.maxElts

In a concession, (21) and (22), a retained preference against an effective one is ranked strictly below it, so it survives as a wish but not as an effective preference. The follow-up but I don't want you to is out and but I wish you would not is fine.

inductive CondoravdiLauer2012.Use : Type

The utterances whose follow-ups the paper contrasts.

• assertion : Use
• directive : Use
• advice : Use
• concession : Use

@[instance_reducible]

instance CondoravdiLauer2012.instDecidableEqUse : DecidableEq Use

Equations

• CondoravdiLauer2012.instDecidableEqUse x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CondoravdiLauer2012.Use.Holds {W : Type u_2} (u : Use) (S : PreferenceStructure W) (p : Set W) : Prop

An utterance requires of the speaker's effective preference structure an effective preference for the content unless it is an assertion, which incurs no preferential commitment, declarative_contextSets, and for advice also nothing ranked below the content, (39).

Equations

• u.Holds S p = ((u ≠ CondoravdiLauer2012.Use.assertion → p ∈ S.maxElts) ∧ (u = CondoravdiLauer2012.Use.advice → ∀ r ∈ S.prefs, ¬S.prec r p))

inductive CondoravdiLauer2012.Denial : Type

A follow-up's present preference against the content is effective for I don't want you to, mere for I wish you would not, and absent for a deontic statement or a past desire.

• want : Denial
• wish : Denial
• none : Denial

@[instance_reducible]

instance CondoravdiLauer2012.instDecidableEqDenial : DecidableEq Denial

Equations

• CondoravdiLauer2012.instDecidableEqDenial x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CondoravdiLauer2012.Denial.Against {W : Type u_2} (d : Denial) (S : PreferenceStructure W) (q : Set W) : Prop

A denial carries a preference against the content unless it has none, and an effective one for a want.

Equations

• d.Against S q = ((d ≠ CondoravdiLauer2012.Denial.none → q ∈ S.prefs) ∧ (d = CondoravdiLauer2012.Denial.want → q ∈ S.maxElts))

def CondoravdiLauer2012.Coherent (W : Type u_2) (u : Use) (d : Denial) : Prop

A follow-up is coherent when some consistent effective preference structure meets the utterance's requirement on the content and carries the denial's preference against it.

Equations

• CondoravdiLauer2012.Coherent W u d = ∃ (S : PreferenceStructure W) (p : Set W) (q : Set W), S.Consistent Set.univ ∧ u.Holds S p ∧ p ∩ q = ∅ ∧ d.Against S q

theorem CondoravdiLauer2012.coherent_iff {W : Type u_2} [Nontrivial W] {u : Use} {d : Denial} : Coherent W u d ↔ d = Denial.none ∨ u = Use.assertion ∨ d ≠ Denial.want ∧ u ≠ Use.advice

A follow-up is coherent unless it denies an effective preference the utterance incurred, concession_not_want, or denies the content of disinterested advice at all, advice_compatible. A directive followed by a wish against its content is thereby predicted coherent, a case the paper does not discuss.

Ordering-source affirmation

theorem CondoravdiLauer2012.affirmation_consistent {W : Type u_2} {p q : Set W} {w : W} {f g : Modality.Background W} (hne : (Modality.bestWorlds f g w).Nonempty) (hp : Modality.necessity f g (fun (x : W) => x ∈ p) w) (hq : Modality.necessity f g (fun (x : W) => x ∈ q) w) : (p ∩ q).Nonempty

[Sch06a]'s ordering-source affirmation, (19), read as a bouletic necessity of the content, predicts the consistency requirement: two affirmed contents share a best world.

theorem CondoravdiLauer2012.weak_affirmation_compl {W : Type u_2} {p : Set W} {w : W} {f g : Modality.Background W} (hp : ∃ u ∈ Modality.bestWorlds f g w, u ∈ p) (hq : ∃ u ∈ Modality.bestWorlds f g w, u ∉ p) : Modality.possibility f g (fun (x : W) => x ∈ p) w ∧ Modality.possibility f g (fun (x : W) => x ∈ pᶜ) w

The weaker affirmation of [KS09], (20), that the negation of the content not follow from what is optimal, does not: whenever the speaker's wishes leave the content open, a content and its negation are both weakly affirmed, so (20) admits the incompatible imperatives of (15).

To-Do Lists

theorem CondoravdiLauer2012.todo_not_must {W : Type u_2} {w : W} {f g : Modality.Background W} {φ ψ : W → Prop} {u : W} (hψ : ψ ∈ g w) (hφψ : ∀ (v : W), ψ v → ¬φ v) (hu : u ∈ Modality.bestWorlds f g w) (huψ : ψ u) : ¬Modality.necessity f (fun (v : W) => insert φ (g v)) φ w

[Por07]'s secondary update adds the content to the modal ordering source; when the source already holds a proposition incompatible with the content, a best world verifying it stays best, so the common ground does not come to entail must p, §5.2.

The rows

The uses of (6) to (9), after [Sch82]'s inventory, and the exclusions of (10) are data; the sequences, follow-ups and challenges instantiate the theorems above.

inductive CondoravdiLauer2012.Second : Type

The second utterance of a sequence.

• imperative : Second
• assertion : Second

@[instance_reducible]

instance CondoravdiLauer2012.instDecidableEqSecond : DecidableEq Second

Equations

• CondoravdiLauer2012.instDecidableEqSecond x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive CondoravdiLauer2012.Continuation : Type

Whether the context lets the second utterance revise the first.

• revising : Continuation
• conflicting : Continuation

@[instance_reducible]

instance CondoravdiLauer2012.instDecidableEqContinuation : DecidableEq Continuation

Equations

• CondoravdiLauer2012.instDecidableEqContinuation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure CondoravdiLauer2012.Sequence : Type

A sequence row of two utterances with incompatible contents.

• second : Second

  The second utterance.

• continuation : Continuation

  Whether the context lets it revise the first.

def CondoravdiLauer2012.Sequence.ofRow (row : Datum) : Option Sequence

The configuration a sequence row records.

Equations

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

theorem CondoravdiLauer2012.sequence_rows (row : Datum) : row ∈ Examples.all → row.feature? "construction" = some "sequence" → ∃ s ∈ Sequence.ofRow row, row.JudgedFelicitous ↔ s.second = Second.assertion ∨ s.continuation = Continuation.revising

In the sequences of (11) to (16) incompatible imperatives are coherent only as a revision, imperatives_revise, while an assertion of incompatible desires reports underlying preferences, which need not be consistent.

structure CondoravdiLauer2012.FollowUp : Type

A follow-up row of an utterance and a denial.

• use : Use

  The utterance.

• denial : Denial

  The denial that follows.

def CondoravdiLauer2012.FollowUp.ofRow (row : Datum) : Option FollowUp

The configuration a follow-up row records.

Equations

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

theorem CondoravdiLauer2012.followUp_rows (row : Datum) : row ∈ Examples.all → row.feature? "construction" = some "followUp" → ∃ c ∈ FollowUp.ofRow row, row.judgment = Judgment.acceptable ↔ Coherent Bool c.use c.denial

The follow-ups of (17), (18), (21), (22) and (40) are acceptable exactly when coherent, coherent_iff.

inductive CondoravdiLauer2012.Form : Type

The form of an utterance challenged as a lie or disbelieved.

• imperative : Form
• performative : Form
• assertion : Form

@[instance_reducible]

instance CondoravdiLauer2012.instDecidableEqForm : DecidableEq Form

Equations

• CondoravdiLauer2012.instDecidableEqForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CondoravdiLauer2012.Form.ofRow (row : Datum) : Option Form

The form a challenge row records.

Equations

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

theorem CondoravdiLauer2012.challenge_rows (row : Datum) : row ∈ Examples.all → row.feature? "construction" = some "challenge" → ∃ f ∈ Form.ofRow row, row.judgment = Judgment.acceptable ↔ f = Form.assertion

Of the challenges of (23) to (25), only the assertion of a desire can be called a lie or disbelieved; imperatives and explicit performatives are self-verifying, imp_self_verifying.