The speech event and its content

[Hac06] (pp. 141–3) adopts [ST03]'s Speech Act Phrase — every matrix clause is headed by a SAP whose head introduces a speech event e* and encodes illocutionary force — and adds one assumption: the speech event has content, varying with the type of speech act. For a declarative, CON(e*) is the speaker's beliefs; for an imperative, the addressee's To-Do List ([Por04]). A modal bound by e* reads CON(e*) as its conversational background, so the speech act type determines the modal's flavor with no lexical ambiguity. Here CON(e*) enters the mood state through the force-targeted update — declarative content is asserted, imperative content promoted — and the licensed modal and flavor are read off the targeted component.

Main declarations

• SpeechEvent — a force together with CON(e*).
• SpeechEvent.toState, SpeechEvent.modal — the induced state and its licensed necessity modal.
• Component.flavor, Illocutionary.primaryFlavor — Hacquard's flavor assignment, derived from component targeting.
• HasTarget ModalFlavor — the third instance of [Por18]'s classification.

Implementation notes

[ST03] grammaticalize exactly four speech acts (declarative, interrogative, imperative, quotative). SpeechEvent uses the library-wide five-way Illocutionary — no quotative; promissive and exclamative are conjectural linglib extensions — and Hacquard gives content clauses only for declaratives and imperatives, so the inquisitive route induces the initial state. Binding height (which event a modal is bound by) is Semantics/Modality/EventRelativity's territory.

Speech events

structure Mood.SpeechEvent (W : Type u_2) : Type u_2

A speech act event e* with its content CON(e*) ([Hac06], her assumption 4, pp. 142–3).

• force : Illocutionary

  The illocutionary force the SAP head encodes.

• content : W → List (W → Prop)

  CON(e*): the propositional content of the speech event.

def Mood.SpeechEvent.declarative {W : Type u_1} (beliefs : W → List (W → Prop)) : SpeechEvent W

A declarative speech event: CON(e*) is the speaker's beliefs ([Hac06], her (222)).

Equations

• Mood.SpeechEvent.declarative beliefs = { force := Mood.Illocutionary.declarative, content := beliefs }

def Mood.SpeechEvent.imperative {W : Type u_1} (todo : W → List (W → Prop)) : SpeechEvent W

An imperative speech event: CON(e*) is the addressee's To-Do List ([Hac06] after [Por04]).

Equations

• Mood.SpeechEvent.imperative todo = { force := Mood.Illocutionary.imperative, content := todo }

The induced state

def Mood.SpeechEvent.toState {W : Type u_1} (sa : SpeechEvent W) (w₀ : W) : UpdateSemantics.Default.ExpState W

The state a speech event induces at anchor world w₀: fold CON(e*)(w₀) through the targeted component's update.

Equations

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

@[simp]

theorem Mood.SpeechEvent.toState_declarative {W : Type u_1} (beliefs : W → List (W → Prop)) (w₀ : W) : (declarative beliefs).toState w₀ = List.foldl UpdateSemantics.Default.ExpState.assert UpdateSemantics.Default.ExpState.init (beliefs w₀)

@[simp]

theorem Mood.SpeechEvent.toState_imperative {W : Type u_1} (todo : W → List (W → Prop)) (w₀ : W) : (imperative todo).toState w₀ = List.foldl UpdateSemantics.Default.ExpState.promote UpdateSemantics.Default.ExpState.init (todo w₀)

theorem Mood.SpeechEvent.mem_toState_declarative_info {W : Type u_1} (beliefs : W → List (W → Prop)) (w₀ v : W) : v ∈ ((declarative beliefs).toState w₀).info ↔ ∀ p ∈ beliefs w₀, p v

A declarative's information state is the worlds compatible with every belief in CON(e*).

theorem Mood.SpeechEvent.toState_imperative_le {W : Type u_1} (todo : W → List (W → Prop)) (w₀ w v : W) : w ≤ v ↔ ∀ p ∈ todo w₀, p v → p w

An imperative's ordering prefers TDL-compliant worlds — the [Kra81] ordering-source construction, arrived at by promotion.

theorem Mood.SpeechEvent.toState_imperative_info {W : Type u_1} (todo : W → List (W → Prop)) (w₀ : W) : ((imperative todo).toState w₀).info = Set.univ

The To-Do List ranks worlds; it does not eliminate them.

The licensed modal

def Mood.SpeechEvent.modal {W : Type u_1} (sa : SpeechEvent W) (w₀ : W) : (W → Prop) → Prop

The necessity modal a speech event licenses: the targeted component's modal on the induced state ([Hac06]'s epistemic and deontic readings).

Equations

• sa.modal w₀ = (Mood.HasTarget.target sa.force).boxOn (Mood.State.ofExpState (sa.toState w₀))

@[simp]

theorem Mood.SpeechEvent.modal_declarative {W : Type u_1} (beliefs : W → List (W → Prop)) (w₀ : W) (p : W → Prop) : (declarative beliefs).modal w₀ p = ((declarative beliefs).toState w₀).boxCs p

@[simp]

theorem Mood.SpeechEvent.modal_imperative {W : Type u_1} (todo : W → List (W → Prop)) (w₀ : W) (p : W → Prop) : (imperative todo).modal w₀ p = ((imperative todo).toState w₀).boxLe p

theorem Mood.SpeechEvent.modal_declarative_iff {W : Type u_1} (beliefs : W → List (W → Prop)) (w₀ : W) (p : W → Prop) : (declarative beliefs).modal w₀ p ↔ ∀ (v : W), (∀ q ∈ beliefs w₀, q v) → p v

The declarative modal quantifies over exactly the belief-compatible worlds.

Flavor factors through the component classification

@[implicit_reducible]

instance Mood.instHasTargetModalFlavor : HasTarget Semantics.Modality.ModalFlavor

Modal flavors target the component their Kratzer parameter feeds: modal-base flavors the informational, ordering-source flavors the preferential ([Kra81]'s parameter roles; [Por18], p. 233). The third instance of the one classification, beside sentence and verbal mood.

Equations

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

def Mood.Component.flavor : Component → Semantics.Modality.ModalFlavor

The flavor a component licenses on [Hac06]'s reading of CON(e*); the inquisitive component is routed to epistemic pending an interrogative-content story.

Equations

• Mood.Component.informational.flavor = Semantics.Modality.ModalFlavor.epistemic
• Mood.Component.preferential.flavor = Semantics.Modality.ModalFlavor.deontic
• Mood.Component.inquisitive.flavor = Semantics.Modality.ModalFlavor.epistemic

def Mood.Illocutionary.primaryFlavor (f : Illocutionary) : Semantics.Modality.ModalFlavor

The primary flavor a speech act licenses ([Hac06]): the targeted component's flavor.

Equations

• f.primaryFlavor = (Mood.HasTarget.target f).flavor

theorem Mood.target_flavor (c : Component) (h : c ≠ Component.inquisitive) : HasTarget.target c.flavor = c

Component.flavor is a section of the modal-flavor targeting on the two POSW components: the representative flavor of a component targets that component back.

@[simp]

theorem Mood.primaryFlavor_declarative : Illocutionary.declarative.primaryFlavor = Semantics.Modality.ModalFlavor.epistemic

@[simp]

theorem Mood.primaryFlavor_imperative : Illocutionary.imperative.primaryFlavor = Semantics.Modality.ModalFlavor.deontic

theorem Mood.speech_act_determines_flavor : Illocutionary.declarative.primaryFlavor ≠ Illocutionary.imperative.primaryFlavor

Different speech acts, different flavors — the "must" ambiguity without lexical ambiguity.

Worked example: "You can leave"

Same modal, same proposition, different speech events: the force, routed through its targeted component, determines the modal domain.

inductive Mood.LeaveWorld : Type

Two outcomes: leave or stay.

• leave : LeaveWorld
• stay : LeaveWorld

@[implicit_reducible]

instance Mood.instDecidableEqLeaveWorld : DecidableEq LeaveWorld

Equations

• Mood.instDecidableEqLeaveWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Mood.instReprLeaveWorld : Repr LeaveWorld

Equations

• Mood.instReprLeaveWorld = { reprPrec := Mood.instReprLeaveWorld.repr }

def Mood.instReprLeaveWorld.repr : LeaveWorld → ℕ → Std.Format

Equations

• Mood.instReprLeaveWorld.repr Mood.LeaveWorld.leave prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mood.LeaveWorld.leave")).group prec✝
• Mood.instReprLeaveWorld.repr Mood.LeaveWorld.stay prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mood.LeaveWorld.stay")).group prec✝

@[implicit_reducible]

instance Mood.instInhabitedLeaveWorld : Inhabited LeaveWorld

Equations

• Mood.instInhabitedLeaveWorld = { default := Mood.instInhabitedLeaveWorld.default }

def Mood.declarativeEvidence : SpeechEvent LeaveWorld

Declarative context: the speaker's evidence is compatible with both outcomes.

Equations

• Mood.declarativeEvidence = Mood.SpeechEvent.declarative fun (x : Mood.LeaveWorld) => []

def Mood.imperativePermission : SpeechEvent LeaveWorld

Imperative context: leave is on the addressee's To-Do List.

Equations

• Mood.imperativePermission = Mood.SpeechEvent.imperative fun (x : Mood.LeaveWorld) => [fun (x : Mood.LeaveWorld) => x = Mood.LeaveWorld.leave]

theorem Mood.declarative_leave_not_necessary : ¬declarativeEvidence.modal LeaveWorld.leave fun (x : LeaveWorld) => x = LeaveWorld.leave

Under the declarative, the speaker's evidence leaves staying open.

theorem Mood.imperative_leave_required : imperativePermission.modal LeaveWorld.leave fun (x : LeaveWorld) => x = LeaveWorld.leave

Under the imperative, every TDL-best world is a leave-world.

Participant projection

inductive Mood.Interlocutor : Type

Speaker and addressee for the projection example.

• speaker : Interlocutor
• addressee : Interlocutor

@[implicit_reducible]

instance Mood.instDecidableEqInterlocutor : DecidableEq Interlocutor

Equations

• Mood.instDecidableEqInterlocutor x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Mood.instReprInterlocutor : Repr Interlocutor

Equations

• Mood.instReprInterlocutor = { reprPrec := Mood.instReprInterlocutor.repr }

def Mood.instReprInterlocutor.repr : Interlocutor → ℕ → Std.Format

Equations

• Mood.instReprInterlocutor.repr Mood.Interlocutor.speaker prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mood.Interlocutor.speaker")).group prec✝
• Mood.instReprInterlocutor.repr Mood.Interlocutor.addressee prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mood.Interlocutor.addressee")).group prec✝

@[implicit_reducible]

instance Mood.instInhabitedInterlocutor : Inhabited Interlocutor

Equations

• Mood.instInhabitedInterlocutor = { default := Mood.instInhabitedInterlocutor.default }

inductive Mood.SpeechTime : Type

Speech time.

• now : SpeechTime

@[implicit_reducible]

instance Mood.instDecidableEqSpeechTime : DecidableEq SpeechTime

Equations

• Mood.instDecidableEqSpeechTime x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Mood.instReprSpeechTime.repr : SpeechTime → ℕ → Std.Format

Equations

• Mood.instReprSpeechTime.repr Mood.SpeechTime.now prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Mood.SpeechTime.now")).group prec✝

@[implicit_reducible]

instance Mood.instReprSpeechTime : Repr SpeechTime

Equations

• Mood.instReprSpeechTime = { reprPrec := Mood.instReprSpeechTime.repr }

@[implicit_reducible]

instance Mood.instInhabitedSpeechTime : Inhabited SpeechTime

Equations

• Mood.instInhabitedSpeechTime = { default := Mood.instInhabitedSpeechTime.default }

def Mood.speechActProjection : Semantics.Modality.EventRelativity.EventProjection Illocutionary Interlocutor SpeechTime

Whose attitudes provide CON(e*), at speech time ([ST03]'s participant structure; distinct from the seat of knowledge, tracked per-force by Illocutionary.authority).

Equations

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