Imperatives as Preferential Commitment

@cite{condoravdi-lauer-2012} @cite{lauer-2013}

Worked examples exercising the substrate's force = .preferential axis, which had no consumer prior to this file. Anchored on @cite{condoravdi-lauer-2012} ("Imperatives: meaning and illocutionary force", Empirical Issues in Syntax and Semantics 9, pp. 37–58).

Paper's central distinction (§§3.2–3.3)

@cite{condoravdi-lauer-2012} argue that declarative and imperative utterances create commitments of different attitudinal types:

• Declarative utterance (e.g., "It's raining"): adds PB_w(Sp, ⟦φ⟧) — public commitment to ACT AS THOUGH BELIEVING φ.
• Imperative utterance (e.g., "Sit down!"): adds PEP_w(Sp, ⟦φ⟧) — public commitment to ACT AS THOUGH PREFERRING φ to be a maximal element of the speaker's effective preference structure.

Both kinds are commitments to act (paper §3.2). They differ in the attitude the speaker is committed to act under: doxastic vs preferential. This is the substrate's CommitmentForce axis.

Coverage

• §1 — World fixture and propositions
• §2 — Declarative-as-doxastic baseline (Krifka 2015 default)
• §3 — Imperative-as-preferential (the paper's central claim)
• §4 — Doxastic vs preferential CG divergence (the two projections see different things)
• §5 — vs Krifka 2015: same substrate, different force; Krifka's framework was purely doxastic

Out of scope

• The paper's "four challenges" (§2: contextual inconsistency, speaker endorsement, automatic sincerity, interlocutors' role) — these are arguments that any imperative theory must meet; Condoravdi-Lauer's apparatus passes them via PEP/PB closure properties (Lauer 2013 Ch. 5). The substrate doesn't yet model time-indexed PB/PEP closure (per CommitmentSpace.lean substrate scope note); these challenges are deferred.
• The paper's typology of imperative uses (§1: directives, wishes, permissions, disinterested advice, four groups) — formalized via varying the contextual conditions on the SAME PEP commitment; worked examples for each group would multiply the file. Single-case worked example here.
• Comparison with @cite{kaufmann-2012} and @cite{portner-2007} (paper §6) — separate study files would cover these; the @cite{roberts-2023} study at sibling Studies/Roberts2023.lean already engages the Kaufmann-Portner debate.

inductive Phenomena.Directives.Studies.CondoravdiLauer2012.AddrPosture : Type

A 2-world model: addressee sits / doesn't sit.

• sitting : AddrPosture
• standing : AddrPosture

@[implicit_reducible]

instance Phenomena.Directives.Studies.CondoravdiLauer2012.instDecidableEqAddrPosture : DecidableEq AddrPosture

Equations

• Phenomena.Directives.Studies.CondoravdiLauer2012.instDecidableEqAddrPosture x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Directives.Studies.CondoravdiLauer2012.instReprAddrPosture.repr : AddrPosture → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Directives.Studies.CondoravdiLauer2012.instReprAddrPosture : Repr AddrPosture

Equations

• Phenomena.Directives.Studies.CondoravdiLauer2012.instReprAddrPosture = { reprPrec := Phenomena.Directives.Studies.CondoravdiLauer2012.instReprAddrPosture.repr }

def Phenomena.Directives.Studies.CondoravdiLauer2012.isSitting : AddrPosture → Prop

Proposition: the addressee is sitting.

Equations

• Phenomena.Directives.Studies.CondoravdiLauer2012.isSitting Phenomena.Directives.Studies.CondoravdiLauer2012.AddrPosture.sitting = True
• Phenomena.Directives.Studies.CondoravdiLauer2012.isSitting Phenomena.Directives.Studies.CondoravdiLauer2012.AddrPosture.standing = False

def Phenomena.Directives.Studies.CondoravdiLauer2012.declarativeState : Dialogue.Krifka.KrifkaState AddrPosture

Speaker utters the declarative "The addressee is sitting". Creates a doxastic commitment (Krifka 2015 default; @cite{condoravdi-lauer-2012} paper §3.3 Convention applied to assertions).

Equations

• Phenomena.Directives.Studies.CondoravdiLauer2012.declarativeState = Dialogue.Krifka.KrifkaState.empty.assert Phenomena.Directives.Studies.CondoravdiLauer2012.isSitting

theorem Phenomena.Directives.Studies.CondoravdiLauer2012.declarative_root_eq : declarativeState.space.root = [Core.Discourse.Commitment.IndexedCommitment.commit Core.Discourse.DiscourseRole.speaker isSitting]

The declarative state has speaker doxastically committed to isSitting.

theorem Phenomena.Directives.Studies.CondoravdiLauer2012.declarative_doxastic_narrows (w : AddrPosture) : declarativeState.space.toDoxasticContextSet w ↔ isSitting w

Therefore the doxastic context set narrows to sitting-worlds.

theorem Phenomena.Directives.Studies.CondoravdiLauer2012.declarative_preferential_unchanged (w : AddrPosture) : declarativeState.space.toPreferentialContextSet w

The preferential context set is unaffected by the declarative (no preferential commitments in root).

def Phenomena.Directives.Studies.CondoravdiLauer2012.imperativeState : Dialogue.Krifka.KrifkaState AddrPosture

Speaker utters the imperative "Sit down!". The substrate's assert operator with force := .preferential models the paper's PEP_w(Sp, ⟦sit_down⟧) commitment.

Per @cite{condoravdi-lauer-2012} §3.3: the convention for imperatives parallels the convention for declaratives, but commits the speaker to a PREFERENCE rather than a BELIEF.

Equations

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

theorem Phenomena.Directives.Studies.CondoravdiLauer2012.imperative_root_eq : imperativeState.space.root = [Core.Discourse.Commitment.IndexedWeightedCommitment.commit Core.Discourse.DiscourseRole.speaker Core.Discourse.Commitment.CommitmentForce.preferential isSitting]

The imperative state has speaker preferentially committed to isSitting. Same IndexedCommitment.commit constructor as the declarative — only the force field differs.

theorem Phenomena.Directives.Studies.CondoravdiLauer2012.imperative_doxastic_unchanged (w : AddrPosture) : imperativeState.space.toDoxasticContextSet w

The doxastic context set is unaffected by the imperative — the speaker has not committed to BELIEVE the addressee is sitting, only to prefer it.

theorem Phenomena.Directives.Studies.CondoravdiLauer2012.imperative_preferential_narrows (w : AddrPosture) : imperativeState.space.toPreferentialContextSet w ↔ isSitting w

The preferential context set narrows to sitting-worlds — the speaker IS committed to act as though preferring isSitting.

The two projections see different things

Paper §3.2: PB and PEP are independent attitudinal commitments. A declarative engages only PB; an imperative engages only PEP. The substrate's toDoxasticContextSet / toPreferentialContextSet projections make this independence Lean-checkable.

theorem Phenomena.Directives.Studies.CondoravdiLauer2012.dox_pref_dual (w : AddrPosture) : (declarativeState.space.toDoxasticContextSet w ↔ isSitting w) ∧ declarativeState.space.toPreferentialContextSet w ∧ imperativeState.space.toDoxasticContextSet w ∧ (imperativeState.space.toPreferentialContextSet w ↔ isSitting w)

Headline: declarative narrows doxastic but not preferential; imperative narrows preferential but not doxastic.

theorem Phenomena.Directives.Studies.CondoravdiLauer2012.imperative_conflated_loses_distinction (w : AddrPosture) : imperativeState.space.toContextSet w ↔ isSitting w

The conflated toContextSet is the conjunction of both projections (substrate-level theorem toContextSet_eq_doxastic_and_preferential). Specialised to imperativeState: the conflated CG narrows to sitting-worlds even though only the preferential-CG component is really committed. The conflated view loses information.

Krifka 2015 was purely doxastic; CL2012 adds preferential

Per the chronological-dependency rule, this 2012 paper PRECEDES Krifka 2015 — but Krifka 2015's framework, as formalised in Phenomena/Assertion/Studies/Krifka2015.lean, only exercises force = .doxastic (the substrate's default). Condoravdi-Lauer 2012 provides the missing imperative case via force = .preferential, exercising the same substrate machinery on the same IndexedCommitment constructor.

The interesting cross-framework observation: both Krifka 2015's declarative-assertion and Condoravdi-Lauer 2012's imperative-assertion produce a single-element root. They differ ONLY in the force field.

theorem Phenomena.Directives.Studies.CondoravdiLauer2012.declarative_imperative_share_content_differ_in_force : declarativeState.space.root = [Core.Discourse.Commitment.IndexedWeightedCommitment.commit Core.Discourse.DiscourseRole.speaker Core.Discourse.Commitment.CommitmentForce.doxastic isSitting] ∧ imperativeState.space.root = [Core.Discourse.Commitment.IndexedWeightedCommitment.commit Core.Discourse.DiscourseRole.speaker Core.Discourse.Commitment.CommitmentForce.preferential isSitting] ∧ Option.map (fun (x : Core.Discourse.Commitment.IndexedWeightedCommitment AddrPosture Prop) => x.force) declarativeState.space.root.head? ≠ Option.map (fun (x : Core.Discourse.Commitment.IndexedWeightedCommitment AddrPosture Prop) => x.force) imperativeState.space.root.head?

Both Krifka 2015's declarative and CL2012's imperative produce a single-element root with the SAME IndexedCommitment.commit constructor and the SAME content (isSitting). They differ only in the force field.