Roberts (2023): Imperatives in Dynamic Pragmatics

[Rob23]

Imperatives in dynamic pragmatics. Semantics & Pragmatics 16, Article 7: 1–55.

Core Contribution

A semantics and dynamic pragmatics for imperative mood that combines the best features of [Kau12] and [Por04]:

1. Semantic type: Imperatives denote de se properties indexed to the addressee — following [Por04].
2. Modal in semantic content: The content includes a futurate circumstantial modal with Kratzerian modal base f and goal-based ordering source g — following [Kau12]. But the modal is not deontic.
3. Pragmatic deontic flavor: The perceived deontic force arises entirely from the pragmatics of accepting a direction — updating the addressee's preference structure (the goals component G of the discourse scoreboard) — not from the LF.

Substrate hookup

This file is a configuration of existing infrastructure, not a standalone formalization of an imperative mood ontology:

• The futurate modal base reuses HistoricalAlternatives.futureHistoryBase.
• The goal-based ordering and circumstantial modal base are Kratzer.OrderingSource / ModalBase, packaged as TeleologicalFlavor (no parallel types).
• The architectural commitment "imperative force targets the preferential POSW component, not the informational" is Semantics.Mood.POSWTarget's HasPOSWTarget IllocutionaryMood instance — Roberts agrees with [Por18] on the POSW component, disagrees with [Kau12] only on the prejacent's modal flavor.
• The scoreboard updates are Discourse.Scoreboard's assertion/interrogation/direction; the derivation that directionUpdate factors as POSW.star lives in Scoreboard.lean (toPOSW_direction_eq_star).

Equation citations

All equation numbers verified against the published PDF: (45) circumstance, (47) SameHistory, (48) FUT, (49) goal-based ordering source, (50) timely future, (51) futurate circumstantial modal base, (53) APPLIC, (54)/(67) imperative character ¡, (57) assertion, (58) interrogation, (59) direction, (65) conservativity. Example "Have a cookie" is (60) in §2.2 (not §3).

Discourse Move

[Rob23] [Lew79b]

An illocutionary move: speaker performs mood F(p) for some content p, addressed to an interlocutor, possibly accepted.

[Rob23] §2.1.1: M is the set of moves on the scoreboard, with distinguished subsets A (assertions), Q (questions), D (directions), Acc (accepted).

Main definitions

• Move W — ⟨mood, content, agent, accepted⟩.

structure Discourse.Move (W : Type u_1) : Type u_1

An illocutionary move: a speech act performed by an agent.

• mood : Semantics.Mood.IllocutionaryMood

  Which kind of speech act.

• content : W → Prop

  Propositional content (for assertions and questions; for directions, the propositional closure of the targeted property).

• agent : ℕ

  Who made the move (agent index into interlocutors).

• accepted : Prop

  Whether this move has been accepted by the interlocutors.

@[implicit_reducible]

instance Discourse.instInhabitedMove {a✝ : Type u_1} : Inhabited (Move a✝)

Equations

• Discourse.instInhabitedMove = { default := Discourse.instInhabitedMove.default }

Scoreboard: Unified Discourse State

[Rob23] [Rob12] [Lew79b] [Por04]

The scoreboard K for a language game at time t is a tuple ⟨I, M, ≺, CommonGround, QUD, G⟩ ([Rob23]), tracking:

• I: the set of interlocutors
• M: illocutionary moves made so far (with subsets A, Q, D, Acc)
• ≺: temporal order on moves
• CommonGround: the common ground (propositions treated as mutually believed)
• QUD: the ordered set of questions under discussion
• G: the interlocutors' publicly evident goals, plans, and priorities

The three central elements — CommonGround, QUD, G — are updated by assertion, interrogation, and direction respectively, via the Illocutionary Force Linking Principle ([Rob23]).

Goals (the G component)

structure Discourse.Goal (W : Type u_2) : Type u_2

A single goal: a proposition the agent is committed to realizing, conditional on certain circumstances obtaining ([Rob23]).

• content : W → Prop

  The content: what the agent aims to bring about.

• condition : W → Prop

  Circumstances under which this goal is active. λ _ => True for unconditional goals.

• priority : ℕ

  Priority level: 0 = highest priority.

@[implicit_reducible]

instance Discourse.instInhabitedGoal {a✝ : Type u_2} : Inhabited (Goal a✝)

Equations

• Discourse.instInhabitedGoal = { default := Discourse.instInhabitedGoal.default }

structure Discourse.GoalSet (W : Type u_2) : Type u_2

An agent's goal set: publicly evident goals, plans, and priorities.

• goals : List (Goal W)

@[implicit_reducible]

instance Discourse.instInhabitedGoalSet {a✝ : Type u_2} : Inhabited (GoalSet a✝)

Equations

• Discourse.instInhabitedGoalSet = { default := Discourse.instInhabitedGoalSet.default }

def Discourse.GoalSet.empty {W : Type u_1} : GoalSet W

The empty goal set.

Equations

• Discourse.GoalSet.empty = { }

@[simp]

theorem Discourse.GoalSet.empty_goals {W : Type u_1} : empty.goals = []

def Discourse.GoalSet.add {W : Type u_1} (gs : GoalSet W) (g : Goal W) : GoalSet W

Add a goal to the set.

Equations

• gs.add g = { goals := g :: gs.goals }

@[simp]

theorem Discourse.GoalSet.add_goals {W : Type u_1} (gs : GoalSet W) (g : Goal W) : (gs.add g).goals = g :: gs.goals

def Discourse.GoalSet.toPropertyList {W : Type u_1} (gs : GoalSet W) : List (W → Prop)

Project to a flat list of contents ([Por04] ToDo list interface).

Equations

• gs.toPropertyList = List.map Discourse.Goal.content gs.goals

@[simp]

theorem Discourse.GoalSet.toPropertyList_empty {W : Type u_1} : empty.toPropertyList = []

@[simp]

theorem Discourse.GoalSet.toPropertyList_add {W : Type u_1} (gs : GoalSet W) (g : Goal W) : (gs.add g).toPropertyList = g.content :: gs.toPropertyList

inductive Discourse.SemanticType : Type

The semantic type of a clause, determining its default illocutionary force.

[Rob23]: propositions → assertion, sets of propositions → interrogation, indexed properties → direction.

• proposition : SemanticType

  Type ⟨s, t⟩: a proposition (set of worlds)

• setOfPropositions : SemanticType

  Type ⟨⟨s, t⟩, t⟩: a set of propositions (Hamblin question denotation)

• indexedProperty : SemanticType

  Type ⟨s, ⟨e, t⟩⟩: a property indexed to the addressee

@[implicit_reducible]

instance Discourse.instDecidableEqSemanticType : DecidableEq SemanticType

Equations

• Discourse.instDecidableEqSemanticType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Discourse.instReprSemanticType : Repr SemanticType

Equations

• Discourse.instReprSemanticType = { reprPrec := Discourse.instReprSemanticType.repr }

def Discourse.instReprSemanticType.repr : SemanticType → ℕ → Std.Format

Equations

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

def Discourse.forceLinkingPrinciple : SemanticType → Semantics.Mood.IllocutionaryMood

Illocutionary Force Linking Principle: the default illocutionary force of a root sentence is determined by its semantic type.

Equations

• Discourse.forceLinkingPrinciple Discourse.SemanticType.proposition = Semantics.Mood.IllocutionaryMood.declarative
• Discourse.forceLinkingPrinciple Discourse.SemanticType.setOfPropositions = Semantics.Mood.IllocutionaryMood.interrogative
• Discourse.forceLinkingPrinciple Discourse.SemanticType.indexedProperty = Semantics.Mood.IllocutionaryMood.imperative

@[simp]

theorem Discourse.forceLinkingPrinciple_proposition : forceLinkingPrinciple SemanticType.proposition = Semantics.Mood.IllocutionaryMood.declarative

@[simp]

theorem Discourse.forceLinkingPrinciple_setOfPropositions : forceLinkingPrinciple SemanticType.setOfPropositions = Semantics.Mood.IllocutionaryMood.interrogative

@[simp]

theorem Discourse.forceLinkingPrinciple_indexedProperty : forceLinkingPrinciple SemanticType.indexedProperty = Semantics.Mood.IllocutionaryMood.imperative

def Discourse.defaultSemanticType : Semantics.Mood.IllocutionaryMood → SemanticType

The default semantic type for each illocutionary mood (inverse of IFLP).

Equations

• Discourse.defaultSemanticType Semantics.Mood.IllocutionaryMood.declarative = Discourse.SemanticType.proposition
• Discourse.defaultSemanticType Semantics.Mood.IllocutionaryMood.interrogative = Discourse.SemanticType.setOfPropositions
• Discourse.defaultSemanticType Semantics.Mood.IllocutionaryMood.imperative = Discourse.SemanticType.indexedProperty
• Discourse.defaultSemanticType Semantics.Mood.IllocutionaryMood.promissive = Discourse.SemanticType.indexedProperty
• Discourse.defaultSemanticType Semantics.Mood.IllocutionaryMood.exclamative = Discourse.SemanticType.proposition

@[simp]

theorem Discourse.defaultSemanticType_declarative : defaultSemanticType Semantics.Mood.IllocutionaryMood.declarative = SemanticType.proposition

@[simp]

theorem Discourse.defaultSemanticType_interrogative : defaultSemanticType Semantics.Mood.IllocutionaryMood.interrogative = SemanticType.setOfPropositions

@[simp]

theorem Discourse.defaultSemanticType_imperative : defaultSemanticType Semantics.Mood.IllocutionaryMood.imperative = SemanticType.indexedProperty

theorem Discourse.iflp_roundtrip_decl : forceLinkingPrinciple (defaultSemanticType Semantics.Mood.IllocutionaryMood.declarative) = Semantics.Mood.IllocutionaryMood.declarative

IFLP round-trips for the three core moods.

theorem Discourse.iflp_roundtrip_interrog : forceLinkingPrinciple (defaultSemanticType Semantics.Mood.IllocutionaryMood.interrogative) = Semantics.Mood.IllocutionaryMood.interrogative

theorem Discourse.iflp_roundtrip_imp : forceLinkingPrinciple (defaultSemanticType Semantics.Mood.IllocutionaryMood.imperative) = Semantics.Mood.IllocutionaryMood.imperative

The Scoreboard

structure Discourse.Scoreboard (W : Type u_2) : Type u_2

The scoreboard K = ⟨I, M, ≺, CommonGround, QUD, G⟩. The temporal order ≺ is implicit in list position of moves. qud is specialised to polar-question content (W → Prop); the richer Discourse.QUDStack over Semantics.Questions.Basic.Question W is consumed by other files. Bridging the two is an open API-coherence item.

• numInterlocutors : ℕ
• moves : List (Move W)
• cg : List (W → Prop)
• qud : List (W → Prop)
• goals : List (GoalSet W)

@[implicit_reducible]

instance Discourse.instInhabitedScoreboard {a✝ : Type u_2} : Inhabited (Scoreboard a✝)

Equations

• Discourse.instInhabitedScoreboard = { default := Discourse.instInhabitedScoreboard.default }

def Discourse.Scoreboard.contextSet {W : Type u_1} (K : Scoreboard W) : W → Prop

The context set: worlds compatible with all CommonGround propositions.

Equations

• K.contextSet w = ∀ p ∈ K.cg, p w

def Discourse.Scoreboard.agentGoals {W : Type u_1} (K : Scoreboard W) (i : ℕ) : GoalSet W

An agent's goal set. Returns empty if index out of bounds.

Equations

• K.agentGoals i = K.goals.getD i Discourse.GoalSet.empty

def Discourse.Scoreboard.assertionUpdate {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (agent : ℕ) : Scoreboard W

Assertion update: accepted assertion of p adds p to CommonGround.

Equations

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

def Discourse.Scoreboard.interrogationUpdate {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (agent : ℕ) : Scoreboard W

Interrogation update: accepted question q adds q to QUD.

Equations

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

def Discourse.Scoreboard.addGoalAt {W : Type u_1} : List (GoalSet W) → ℕ → ℕ → Goal W → List (GoalSet W)

Add goal g to the agent at target index in xs (walking from i). Identity when target is out of range.

Equations

• Discourse.Scoreboard.addGoalAt [] x✝² x✝¹ x✝ = []
• Discourse.Scoreboard.addGoalAt (gs :: rest) x✝² x✝¹ x✝ = (if (x✝¹ == x✝²) = true then gs.add x✝ else gs) :: Discourse.Scoreboard.addGoalAt rest x✝² (x✝¹ + 1) x✝

theorem Discourse.Scoreboard.addGoalAt_out_of_range {W : Type u_1} (xs : List (GoalSet W)) (target i : ℕ) (g : Goal W) (h : target < i) : addGoalAt xs target i g = xs

If the walk is past target, addGoalAt is the identity.

def Discourse.Scoreboard.directionUpdate {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (speaker target : ℕ) (priority : ℕ := 0) : Scoreboard W

Direction update: targeted property issued to addressee target and accepted; revises G_target to include the property's realization.

Equations

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

@[simp]

theorem Discourse.Scoreboard.assertion_adds_to_cg {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (a : ℕ) : (K.assertionUpdate p a).cg = p :: K.cg

Assertion update adds to CommonGround.

@[simp]

theorem Discourse.Scoreboard.assertion_preserves_qud {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (a : ℕ) : (K.assertionUpdate p a).qud = K.qud

Assertion update preserves QUD.

@[simp]

theorem Discourse.Scoreboard.assertion_preserves_goals {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (a : ℕ) : (K.assertionUpdate p a).goals = K.goals

Assertion update preserves G.

@[simp]

theorem Discourse.Scoreboard.interrogation_adds_to_qud {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (a : ℕ) : (K.interrogationUpdate q a).qud = q :: K.qud

Interrogation update adds to QUD.

@[simp]

theorem Discourse.Scoreboard.interrogation_preserves_cg {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (a : ℕ) : (K.interrogationUpdate q a).cg = K.cg

Interrogation update preserves CommonGround.

@[simp]

theorem Discourse.Scoreboard.interrogation_preserves_goals {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (a : ℕ) : (K.interrogationUpdate q a).goals = K.goals

Interrogation update preserves G.

@[simp]

theorem Discourse.Scoreboard.direction_preserves_cg {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (s t pr : ℕ) : (K.directionUpdate p s t pr).cg = K.cg

Direction update preserves CommonGround.

@[simp]

theorem Discourse.Scoreboard.direction_preserves_qud {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (s t pr : ℕ) : (K.directionUpdate p s t pr).qud = K.qud

Direction update preserves QUD.

POSW substrate bridge

The scoreboard's CommonGround and G components project jointly into a Semantics.Mood.POSW: CommonGround via contextSet, G via the goal-induced preference ordering. Assertion ↔ plus, direction ↔ star.

def Discourse.Scoreboard.goalContents {W : Type u_1} (K : Scoreboard W) : List (W → Prop)

Flat list of goal contents across all agents.

Equations

• K.goalContents = List.flatMap Discourse.GoalSet.toPropertyList K.goals

@[simp]

theorem Discourse.Scoreboard.assertion_preserves_goalContents {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (a : ℕ) : (K.assertionUpdate p a).goalContents = K.goalContents

Assertion update preserves goal contents (since it doesn't touch G).

theorem Discourse.Scoreboard.mem_addGoalAt_flatMap {W : Type u_1} (xs : List (GoalSet W)) (target i : ℕ) (g : Goal W) (hin : i ≤ target) (hbd : target < i + xs.length) (q : W → Prop) : q ∈ List.flatMap GoalSet.toPropertyList (addGoalAt xs target i g) ↔ q = g.content ∨ q ∈ List.flatMap GoalSet.toPropertyList xs

After a directionUpdate, the new directive's content joins the flat goal-content list. Requires target in bounds.

theorem Discourse.Scoreboard.mem_directionUpdate_goalContents {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (s t pr : ℕ) (hin : t < K.goals.length) (q : W → Prop) : q ∈ (K.directionUpdate p s t pr).goalContents ↔ q = p ∨ q ∈ K.goalContents

Membership in the flat goal-content list after directionUpdate: the new directive's content joins the existing goal contents.

def Discourse.Scoreboard.toPOSW {W : Type u_1} (K : Scoreboard W) : Semantics.Mood.POSW W

Project the scoreboard into a POSW: cs from CommonGround, le from goal-induced preference.

Equations

• K.toPOSW = { cs := K.contextSet, le := fun (w v : W) => ∀ p ∈ K.goalContents, p v → p w, le_refl := ⋯, le_trans := ⋯ }

@[simp]

theorem Discourse.Scoreboard.toPOSW_cs {W : Type u_1} (K : Scoreboard W) : K.toPOSW.cs = K.contextSet

@[simp]

theorem Discourse.Scoreboard.toPOSW_le {W : Type u_1} (K : Scoreboard W) (w v : W) : K.toPOSW.le w v ↔ ∀ p ∈ K.goalContents, p v → p w

theorem Discourse.Scoreboard.toPOSW_assertion_eq_plus {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (a : ℕ) (w : W) : (K.assertionUpdate p a).toPOSW.cs w ↔ (K.toPOSW.plus p).cs w

Assertion-as-+-update bridge: assertionUpdate refines the projected POSW's cs exactly as POSW.plus does.

theorem Discourse.Scoreboard.boxCs_after_assertion {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (a : ℕ) : (K.assertionUpdate p a).toPOSW.boxCs p

After asserting p, p is informationally necessary on the projected POSW (Stalnakerian assertion principle).

theorem Discourse.Scoreboard.toPOSW_direction_eq_star {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (s t pr : ℕ) (hin : t < K.goals.length) (w v : W) : (K.directionUpdate p s t pr).toPOSW.le w v ↔ (K.toPOSW.star p).le w v

Direction-as-⋆-update bridge: directionUpdate refines the projected POSW's le exactly as POSW.star does (modulo target-in-bounds).

theorem Discourse.Scoreboard.direction_demotes_violators {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (s t pr : ℕ) (hin : t < K.goals.length) (w v : W) (hpv : p v) (hpw : ¬p w) : ¬(K.directionUpdate p s t pr).toPOSW.le w v

After directionUpdate p, no p-violator dominates a p-satisfier.

POSWQ inquiry-partition bridge

QUD projects into POSWQ's inquiry partition: meet of polar Setoids over the QUD stack. Interrogation ↔ inquire.

def Discourse.Scoreboard.qudInquiry {W : Type u_1} (K : Scoreboard W) : Setoid W

Inquiry partition from the QUD stack: meet of polar Setoids (⊤ as identity). Cons-right convention so that consing reduces definitionally to inquire.

Equations

• K.qudInquiry = List.foldr (fun (q : W → Prop) (s : Setoid W) => s ⊓ Semantics.Mood.POSWQ.polarSetoid q) ⊤ K.qud

@[simp]

theorem Discourse.Scoreboard.qudInquiry_nil {W : Type u_1} (K : Scoreboard W) (h : K.qud = []) : K.qudInquiry = ⊤

@[simp]

theorem Discourse.Scoreboard.qudInquiry_cons {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (rest : List (W → Prop)) (h : K.qud = q :: rest) : K.qudInquiry = List.foldr (fun (q : W → Prop) (s : Setoid W) => s ⊓ Semantics.Mood.POSWQ.polarSetoid q) ⊤ rest ⊓ Semantics.Mood.POSWQ.polarSetoid q

@[simp]

theorem Discourse.Scoreboard.interrogation_preserves_goalContents {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (a : ℕ) : (K.interrogationUpdate q a).goalContents = K.goalContents

Interrogation update preserves goal contents (doesn't touch G).

def Discourse.Scoreboard.toPOSWQ {W : Type u_1} (K : Scoreboard W) : Semantics.Mood.POSWQ W

Project the scoreboard into a POSWQ: underlying POSW + QUD inquiry.

Equations

• K.toPOSWQ = { toPOSW := K.toPOSW, inquiry := K.qudInquiry }

@[simp]

theorem Discourse.Scoreboard.toPOSWQ_toPOSW {W : Type u_1} (K : Scoreboard W) : K.toPOSWQ.toPOSW = K.toPOSW

@[simp]

theorem Discourse.Scoreboard.toPOSWQ_inquiry {W : Type u_1} (K : Scoreboard W) : K.toPOSWQ.inquiry = K.qudInquiry

theorem Discourse.Scoreboard.toPOSWQ_interrogation_eq_inquire {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (a : ℕ) : (K.interrogationUpdate q a).toPOSWQ.inquiry = (K.toPOSWQ.inquire (Semantics.Mood.POSWQ.polarSetoid q)).inquiry

Interrogation-as-?-update bridge: interrogationUpdate refines the projected POSWQ's inquiry exactly as POSWQ.inquire does.

theorem Discourse.Scoreboard.boxAns_polar_after_interrogation {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (a : ℕ) : (K.interrogationUpdate q a).toPOSWQ.boxAns q

After posing q, the polar partition of q is settled by the new POSWQ (inquiry analogue of boxCs_after_assertion).

@[reducible, inline]

abbrev Roberts2023.World : Type

Equations

• Roberts2023.World = Fin 4

§2.1.2 Basic Ontology

Roberts's "circumstance" ⟨w, t⟩ (eq. 45), SameHistory (47), and FUT (48) all instantiate the canonical world-time substrate in Intensional.WorldTimeIndex and HistoricalAlternatives:

Roberts Linglib substrate ──────────────────────────── ──────────────────────────── ⟨w, t⟩ circumstance WorldTimeIndex W T SameHistory(w', w, t) HistoricalAlternatives W T predicate FUT(⟨w, t⟩) futureHistoryBase history s

No new types are introduced for these.

§2.1.2 The Imperative Character

Roberts's ¡ (eq. 54/67) bundles the addressee, the prejacent, and the modal parameters. The modal flavor is teleological — facts plus goals — represented directly by Kratzer.TeleologicalFlavor. The "futurate" property of the modal base is enforced separately as the predicate IsFuturate below, which uses futureHistoryBase.

structure Roberts2023.ImperativeCharacter (W : Type u_1) : Type u_1

Roberts's imperative character ¡ ([Rob23] (54)/(67)). Bundles the addressee, the prejacent property, and the teleological-flavor parameters.

• addressee : ℕ

  The addressee (target of the directive).

• prejacent : W → Prop

  The prejacent: VP denotation.

• flavor : Semantics.Modality.Kratzer.TeleologicalFlavor W

  Modal parameters: futurate circumstantial modal base + goal-based ordering source, packaged as a TeleologicalFlavor.

def Roberts2023.ImperativeCharacter.realize {W : Type u_1} (ic : ImperativeCharacter W) (w : W) : Prop

Necessity reading of the imperative character: the prejacent holds at every applicable circumstance (= every best world under the teleological flavor). Eq. (54)/(67) flattened to a world index.

Equations

• ic.realize w = ic.flavor.toKratzerParams.necessity ic.prejacent w

§4 Conservativity Presupposition

Eq. (65), after [Kau12]: an imperative subject NP must live on the addressee set. Stated as a property of the bundle.

def Roberts2023.ImperativeCharacter.conservativeOn {W : Type u_1} (_ic : ImperativeCharacter W) (domain addressees : List ℕ) : Prop

Conservativity presupposition: the subject's quantificational domain is a subset of the addressee set.

Equations

• _ic.conservativeOn domain addressees = ∀ e ∈ domain, e ∈ addressees

§3 Architectural commitments

Roberts's central architectural claim is that the deontic flavor of imperatives is pragmatic — it lives in the preferential POSW component (the addressee's goals/plans), not in the LF as a deontic modal. This is precisely the [Por18] POSWTarget assignment for IllocutionaryMood.imperative, derived (not restipulated) here.

theorem Roberts2023.imperative_targets_preferential : Semantics.Mood.target Semantics.Mood.IllocutionaryMood.imperative = Semantics.Mood.POSWTarget.preferential

Roberts's architectural commitment, derived from [Por18]'s HasPOSWTarget IllocutionaryMood instance: the imperative targets the preferential POSW component (= the addressee's preference structure), not the informational component (= CommonGround).

This is the type-level shadow of "deontic force is pragmatic, not LF": deontic-style content lives where the preference component does, and the imperative refines that component (via POSW.star / Scoreboard.directionUpdate) rather than the informational one.

theorem Roberts2023.pragmatic_deontic_routing {W : Type u_1} (K : Discourse.Scoreboard W) (p : W → Prop) (s t pr : ℕ) (hin : t < K.goals.length) {w v : W} (hpv : p v) (hpw : ¬p w) : ¬(K.directionUpdate p s t pr).toPOSW.le w v

Pragmatic-deontic routing ([Rob23] §3, headline claim).

Directing p to addressee t routes the deontic content through the preferential component of the projected POSW: every prejacent-violator w (¬ p w) is demoted relative to every prejacent-satisfier v (p v) in the preference order (¬ (· ).toPOSW.le w v).

The dual negative claim — that the informational component (CommonGround) is untouched — is Scoreboard.direction_preserves_cg (a @[simp] lemma). The two together discharge Roberts's claim that deontic content arises pragmatically via the preference structure rather than via assertion to common ground.

The hypothesis hin : t < K.goals.length is the substrate counterpart of Roberts's conservativity presupposition (eq. (65)): the addressee must be a real participant for the directive to have its preferential effect. Composes Scoreboard.direction_demotes_violators (the substrate theorem that does the work) with the POSWTarget assignment imperative_targets_preferential (the architectural commitment that this preference-side change is the deontic content).

§1 Desideratum (h): Futurate Flavor

Restated against futureHistoryBase (the canonical Condoravdi/CIR substrate in HistoricalAlternatives) rather than a local FUT enumeration.

theorem Roberts2023.futurate {W : Type u_1} {T : Type u_2} [LT T] (history : HistoricalAlternatives W T) (s s' : Intensional.WorldTimeIndex W T) (h : s' ∈ history.futureHistoryBase s) : s.time < s'.time

(h) Futurate flavor ([Rob23] Table 1, §1, exx. 33–35). Every circumstance in the future-history base of ⟨w, t⟩ has a strictly later time than t. Direct consequence of futureHistoryBase's definition.

§2.2 Force Linking — integration tests

These are smoke tests that the IllocutionaryMood infrastructure agrees with Roberts's IFLP and her sincerity-condition triad. Each rfl is a structural check that the Scoreboard enum assignment matches the paper.

theorem Roberts2023.iflp_roundtrip : Discourse.forceLinkingPrinciple (Discourse.defaultSemanticType Semantics.Mood.IllocutionaryMood.declarative) = Semantics.Mood.IllocutionaryMood.declarative ∧ Discourse.forceLinkingPrinciple (Discourse.defaultSemanticType Semantics.Mood.IllocutionaryMood.interrogative) = Semantics.Mood.IllocutionaryMood.interrogative ∧ Discourse.forceLinkingPrinciple (Discourse.defaultSemanticType Semantics.Mood.IllocutionaryMood.imperative) = Semantics.Mood.IllocutionaryMood.imperative

The IFLP round-trips for all three core moods.

theorem Roberts2023.sincerity_triad : Semantics.Mood.IllocutionaryMood.declarative.sincerityCondition = PsychMode.belief ∧ Semantics.Mood.IllocutionaryMood.interrogative.sincerityCondition = PsychMode.desire ∧ Semantics.Mood.IllocutionaryMood.imperative.sincerityCondition = PsychMode.desire

Sincerity conditions: assertion expresses belief; interrogation and direction both express desire.

theorem Roberts2023.direction_of_fit_triad : Semantics.Mood.IllocutionaryMood.declarative.sincerityCondition.directionOfFit = DirectionOfFit.mindToWorld ∧ Semantics.Mood.IllocutionaryMood.interrogative.sincerityCondition.directionOfFit = DirectionOfFit.worldToMind ∧ Semantics.Mood.IllocutionaryMood.imperative.sincerityCondition.directionOfFit = DirectionOfFit.worldToMind

Direction-of-fit triad: assertion is mind-to-world, interrogation and direction are world-to-mind.

§5 Comparison with [Kau12] / [ROK17]

Roberts's central disagreement with [Kau12]: the imperative's prejacent-internal modal flavor is teleological (circumstantial + goals), not deontic. [ROK17] adopt Kaufmann's position: their SentType.imperative.modalFlavor = some .deontic (RuytenbeekEtAl2017.lean line 102) and their directiveCompatible test fires only on .deontic flavor. This is a substantive disagreement, not a naming dispute: the two accounts make opposite predictions about whether circumstantial declaratives ("Il est possible de VP" with goal-relevance) should pattern with imperatives in directive force.

def Roberts2023.robertsImperativeFlavor : Semantics.Modality.ModalFlavor

The flavor Roberts assigns to the imperative's prejacent-internal modal: teleological/circumstantial.

Equations

• Roberts2023.robertsImperativeFlavor = Semantics.Modality.Kratzer.TeleologicalFlavor.flavorTag

theorem Roberts2023.disagrees_with_ruytenbeek_imperative_flavor : some robertsImperativeFlavor ≠ RuytenbeekEtAl2017.SentType.imperative.modalFlavor

Cross-paper disagreement — [ROK17] Study 2 encodes the [Kau12] position by stipulating SentType.imperative.modalFlavor = some .deontic. Roberts's account predicts .circumstantial. The two prejacent-internal flavors are distinct.

theorem Roberts2023.disagrees_with_assert : robertsImperativeFlavor ≠ Semantics.Modality.Assert.primaryFlavor Semantics.Mood.IllocutionaryMood.imperative

[Kau12]'s position is exposed in Semantics/Modality/Assert.lean as primaryFlavor .imperative = .deontic. Roberts disagrees.

This subsumes a previous roberts_fails_ruytenbeek_mechanism_one theorem (deleted after Ruytenbeek's directiveCompatible wrapper was inlined): under Roberts, an imperative is directive despite not having deontic flavor in its prejacent — the directive force comes from the POSW.star update on the addressee's preference structure (see pragmatic_deontic_routing), not from the prejacent's flavor matching the imperative's.

theorem Roberts2023.empirical_wedge_possible_declarative : RuytenbeekEtAl2017.SentType.possibleDecl.modalFlavor = some robertsImperativeFlavor ∧ ¬RuytenbeekEtAl2017.SentType.possibleDecl.deonticMatch ∧ ¬RuytenbeekEtAl2017.SentType.possibleDecl.prepConditionQueried

Mechanism wedge (post-2026-05-13: empirical wedge collapsed). possibleDecl ("Il est possible de VP") was previously the lone construction where Roberts and Ruytenbeek made opposite predictions about directive force: Roberts predicted directive (prejacent flavor matches imperative under teleological account), while RuytenbeekEtAl2017.lean's mechanisms 1 and 2 alone did not fire on possibleDecl. The 2026-05-13 PDF re-audit found the paper's §4 General Discussion (p. 61) explicitly groups all four ability/possibility constructions — including Il est possible de VP — as encoding force-dynamic enablement (Talmy 2000, Sweetser 1990, Johnson 1987), and the corresponding Fig. 6 shows possibleDecl does receive directive interpretations. Ruytenbeek now formalises this as mechanism 3 (enablementEncoded), which fires on possibleDecl.

The two accounts therefore agree on the prediction (possibleDecl is directive) but route through different mechanisms: Roberts via prejacent-flavor matching (teleological), Ruytenbeek via mechanism 3 (force-dynamic enablement).

The conjuncts below remain literally true and document the mechanism difference: under Ruytenbeek's original two mechanisms (1 = deontic match, 2 = preparatory-condition questioning) — the only ones the chronologically-prior [Kau12] and [Cla79] sources support — possibleDecl would not be licensed. The substantive Roberts-vs-Ruytenbeek wedge has migrated to the imperative's prejacent flavor (see disagrees_with_ruytenbeek_imperative_flavor above).

Worked Examples

These instantiate ImperativeCharacter with the local 4-world toy type World := Fin 4 defined above.

def Roberts2023.moveExample : ImperativeCharacter World

Example: "Move!" ([Rob23] (55), worked derivation). Trivial case — empty modal base and ordering, prejacent always holds.

Equations

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

theorem Roberts2023.move_trivial (w : World) : moveExample.realize w

def Roberts2023.nobodyMoveExample : ImperativeCharacter World

Example: "Nobody move!" ([Rob23] (42), attributed to [Vel18]). Negation is internal (predicate-term negation ¬MOVE), not external (¬□) — propositional negation cannot scope over a property.

Equations

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

theorem Roberts2023.nobody_move_total_prohibition (w : World) : ¬nobodyMoveExample.realize w

§1 (38) Weak imperatives — suggestions and advice

Suggestions like "Hire an attorney" carry weaker modal force than commands. The mood and semantic type are unchanged; the force difference lives in the ordering source, where the prejacent itself serves as a secondary ordering criterion (yielding weak necessity in the sense of [vFI08], which linglib formalizes in Semantics/Modality/Directive.lean).

def Roberts2023.ImperativeCharacter.weakRealize {W : Type u_1} (ic : ImperativeCharacter W) (secondaryGoals : Semantics.Modality.Kratzer.OrderingSource W) (w : W) : Prop

Weak (suggestion/advice) reading of an imperative character: weak necessity under the primary teleological ordering plus a secondary ordering favoring the prejacent.

Equations

• ic.weakRealize secondaryGoals w = Semantics.Modality.Directive.weakNecessity ic.flavor.circumstances ic.flavor.goals secondaryGoals ic.prejacent w

theorem Roberts2023.strong_imperative_entails_suggestion {W : Type u_1} (ic : ImperativeCharacter W) (secondaryGoals : Semantics.Modality.Kratzer.OrderingSource W) (w : W) (h : ic.realize w) : ic.weakRealize secondaryGoals w

Commands entail suggestions: strong necessity entails weak necessity (Directive.strong_entails_weak), so a command-strength imperative a fortiori realizes the suggestion.

def Roberts2023.haveCookieExample : ImperativeCharacter World

Example: "Have a cookie." ([Rob23] §2.2, (60)). Invitation, not command — the hostess proposes the goal of eating a cookie; the guest may decline. Modeled as weak necessity over an empty primary ordering, with a secondary ordering favoring cookie-eating worlds.

Equations

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

theorem Roberts2023.cookie_not_command : ¬haveCookieExample.realize 1

theorem Roberts2023.cookie_is_suggestion : haveCookieExample.weakRealize (fun (x : World) => [fun (w : World) => w = 0]) 0