The ASSERT Operator and Speech Act Phrase

@cite{hacquard-2006}

Formalizes the Speech Act Phrase (SAP) from @cite{hacquard-2006}. Every matrix clause is headed by a SAP that introduces a speech event e* with propositional CONTENT. The type of speech act determines the content:

• Declarative: CON(e*) = speaker's beliefs → epistemic R
• Imperative: CON(e*) = addressee's to-do list → deontic R
• Interrogative: CON(e*) = question content

Architectural Significance

EventBinder.speechAct.hasContent = true is currently stipulated in EventRelativity §8. This file DERIVES that fact: ASSERT introduces a speech event, and all speech events carry propositional content (that is what makes them speech acts). Content licensing then follows: the speech event is contentful → epistemic R can project from it.

Connection to EventRelativity

The speech event's content IS the conversational background that a modal bound to e* accesses. In the AnchoringFn framework:

anchor f e* = CON(e*)

Different speech act types give different CON(e*), hence different modal flavors — without lexical ambiguity in the modal.

@[reducible, inline]

abbrev Semantics.Modality.Assert.SpeechActType : Type

The type of speech act heading the Speech Act Phrase.

@cite{hacquard-2006}: "The content of the speech event is different depending on the type of speech act."

Now unified with IllocutionaryMood from Core.Discourse. The five constructors — declarative, interrogative, imperative, promissive, exclamative — classify the pragmatic act performed.

Equations

• Semantics.Modality.Assert.SpeechActType = Core.Discourse.IllocutionaryMood

def Semantics.Modality.Assert.hasContent : SpeechActType → Bool

All speech acts are contentful events. This is definitional: a speech act IS the performance of propositional content.

This derives EventBinder.speechAct.hasContent = true: the speech event introduced by SAP always carries content, hence it can always project epistemic R (content licensing, EventRelativity §8).

Equations

• Semantics.Modality.Assert.hasContent x✝ = true

def Semantics.Modality.Assert.primaryFlavor : SpeechActType → Core.Modality.ModalFlavor

The primary modal flavor licensed by each speech act type.

• Declarative → epistemic: the content is the speaker's beliefs, so R accesses what the speaker considers possible.
• Imperative → deontic: the content is the addressee's obligations, so R accesses what is permitted/required.
• Promissive → deontic: the content is the speaker's commitments, paralleling imperative.

Equations

• Semantics.Modality.Assert.primaryFlavor Core.Discourse.IllocutionaryMood.declarative = Core.Modality.ModalFlavor.epistemic
• Semantics.Modality.Assert.primaryFlavor Core.Discourse.IllocutionaryMood.imperative = Core.Modality.ModalFlavor.deontic
• Semantics.Modality.Assert.primaryFlavor Core.Discourse.IllocutionaryMood.promissive = Core.Modality.ModalFlavor.deontic
• Semantics.Modality.Assert.primaryFlavor Core.Discourse.IllocutionaryMood.interrogative = Core.Modality.ModalFlavor.epistemic
• Semantics.Modality.Assert.primaryFlavor Core.Discourse.IllocutionaryMood.exclamative = Core.Modality.ModalFlavor.epistemic

structure Semantics.Modality.Assert.SpeechActEvent (W : Type u_1) : Type u_1

A speech act event e* with its content CON(e*).

This is what the Speech Act Phrase introduces at the top of every matrix clause. The content field is the conversational background that modals in the clause can bind to (@cite{hacquard-2006}, (219)–(222)).

• actType : SpeechActType

  The type of speech act

• content : W → List (BProp W)

  CON(e*): the propositional content of the speech event. Maps each world to the set of propositions encoding the content.

def Semantics.Modality.Assert.ASSERT {W : Type u_1} (beliefs : W → List (BProp W)) : SpeechActEvent W

ASSERT: introduce a declarative speech event.

(222) SPEECH ACT_DECLARATIVE(e*): The content encodes the speaker's beliefs — worlds compatible with what the speaker takes to be true.

Equations

• Semantics.Modality.Assert.ASSERT beliefs = { actType := Core.Discourse.IllocutionaryMood.declarative, content := beliefs }

def Semantics.Modality.Assert.DIRECT {W : Type u_1} (obligations : W → List (BProp W)) : SpeechActEvent W

DIRECT: introduce an imperative speech event.

The content encodes the addressee's to-do list — worlds compatible with the addressee fulfilling their obligations.

Equations

• Semantics.Modality.Assert.DIRECT obligations = { actType := Core.Discourse.IllocutionaryMood.imperative, content := obligations }

def Semantics.Modality.Assert.SpeechActEvent.toBackground {W : Type u_1} (sa : SpeechActEvent W) : W → List (BProp W)

A speech act event's content IS a conversational background.

SpeechActEvent.content : W → List (BProp W) has the same type as a Kratzer ConvBackground and as anchor f e from EventRelativity §10. The speech event's content is the background that modals in its scope access when they bind to e*.

Equations

• sa.toBackground = sa.content

def Semantics.Modality.Assert.speechActAnchoring {Ev : Type u_1} {W : Type u_2} (sa : SpeechActEvent W) (describedBg : Ev → W → List (BProp W)) : EventRelativity.AnchoringFn (Unit ⊕ Ev) W

Lift a speech act event into an anchoring function.

Given a speech act event sa, we construct an AnchoringFn where:

• The speech event (.inl ) maps to sa's content
• Any described event (.inr ev) maps to the described event's own background.

This models the clause structure: the speech event anchoring is provided by ASSERT at the top; the described event anchoring comes from the verb's event structure lower in the clause.

Equations

• Semantics.Modality.Assert.speechActAnchoring sa describedBg (Sum.inl PUnit.unit) x✝ = sa.content x✝
• Semantics.Modality.Assert.speechActAnchoring sa describedBg (Sum.inr ev) x✝ = describedBg ev x✝

theorem Semantics.Modality.Assert.speech_slot_is_content {Ev : Type u_1} {W : Type u_2} (sa : SpeechActEvent W) (bg : Ev → W → List (BProp W)) (w : W) : speechActAnchoring sa bg (Sum.inl ()) w = sa.content w

The speech event slot of speechActAnchoring reduces to the speech act's content.

theorem Semantics.Modality.Assert.described_slot_passthrough {Ev : Type u_1} {W : Type u_2} (sa : SpeechActEvent W) (bg : Ev → W → List (BProp W)) (ev : Ev) (w : W) : speechActAnchoring sa bg (Sum.inr ev) w = bg ev w

The described event slot passes through to the verb's background.

EventRelativity §8 stipulates EventBinder.speechAct.hasContent = true. With the SAP formalization, this becomes derivable:

1. Every matrix clause has a SAP.
2. SAP introduces a speech event e*.
3. e* carries CON(e*) (the speech act's propositional content).
4. Therefore e* is contentful.
5. Therefore epistemic R can project from e* (content licensing).

The bridge theorems below make this derivation explicit.

theorem Semantics.Modality.Assert.all_speech_acts_contentful (t : SpeechActType) : hasContent t = true

All speech act types are contentful — by definition, performing a speech act involves producing propositional content.

theorem Semantics.Modality.Assert.assert_contentful {W : Type u_1} (beliefs : W → List (BProp W)) : hasContent (ASSERT beliefs).actType = true

ASSERT produces a contentful event.

theorem Semantics.Modality.Assert.direct_contentful {W : Type u_1} (obligations : W → List (BProp W)) : hasContent (DIRECT obligations).actType = true

DIRECT produces a contentful event.

theorem Semantics.Modality.Assert.sap_justifies_binder_content : (∀ (t : SpeechActType), hasContent t = true) ∧ EventRelativity.EventBinder.speechAct.hasContent = true

Speech act contentfulness agrees with EventBinder.speechAct.hasContent.

This is the key bridge: the stipulated fact in EventRelativity §8 (EventBinder.speechAct.hasContent = true) is justified by the SAP analysis — ASSERT always introduces a contentful event.

theorem Semantics.Modality.Assert.declarative_epistemic : primaryFlavor Core.Discourse.IllocutionaryMood.declarative = Core.Modality.ModalFlavor.epistemic

Declarative speech acts license epistemic modals.

theorem Semantics.Modality.Assert.imperative_deontic : primaryFlavor Core.Discourse.IllocutionaryMood.imperative = Core.Modality.ModalFlavor.deontic

Imperative speech acts license deontic modals.

theorem Semantics.Modality.Assert.speech_act_determines_flavor : primaryFlavor Core.Discourse.IllocutionaryMood.declarative ≠ primaryFlavor Core.Discourse.IllocutionaryMood.imperative

Different speech act types yield different primary flavors for the same modal. This derives the "must" ambiguity:

• "John must be home" (declarative) → epistemic necessity (CON(e*) = speaker's beliefs → must = "given my evidence")
• "Go home!" (imperative) → deontic necessity (CON(e*) = to-do list → must = "you are required to")

Same modal, different speech acts, different readings. No lexical ambiguity needed.

Two contexts for "You can leave":

1. Declarative (informing): "Based on what I know, it's possible you'll leave." ASSERT introduces e* with content = speaker's evidence. The modal accesses epistemic R. Staying is also possible.

2. Imperative (permitting): "You have permission to leave." DIRECT introduces e* with content = addressee's permissions. The modal accesses deontic R. Staying is NOT permitted.

The difference: same modal "can" (◇), but different speech events yield different accessible worlds.

inductive Semantics.Modality.Assert.LeaveWorld : Type

Two outcomes: leave or stay.

• leave : LeaveWorld
• stay : LeaveWorld

instance Semantics.Modality.Assert.instDecidableEqLeaveWorld : DecidableEq LeaveWorld

Equations

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

instance Semantics.Modality.Assert.instBEqLeaveWorld : BEq LeaveWorld

Equations

• Semantics.Modality.Assert.instBEqLeaveWorld = { beq := Semantics.Modality.Assert.instBEqLeaveWorld.beq }

def Semantics.Modality.Assert.instBEqLeaveWorld.beq : LeaveWorld → LeaveWorld → Bool

Equations

• Semantics.Modality.Assert.instBEqLeaveWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Modality.Assert.instReprLeaveWorld : Repr LeaveWorld

Equations

• Semantics.Modality.Assert.instReprLeaveWorld = { reprPrec := Semantics.Modality.Assert.instReprLeaveWorld.repr }

def Semantics.Modality.Assert.instReprLeaveWorld.repr : LeaveWorld → ℕ → Std.Format

Equations

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

instance Semantics.Modality.Assert.instInhabitedLeaveWorld : Inhabited LeaveWorld

Equations

• Semantics.Modality.Assert.instInhabitedLeaveWorld = { default := Semantics.Modality.Assert.instInhabitedLeaveWorld.default }

def Semantics.Modality.Assert.instInhabitedLeaveWorld.default : LeaveWorld

Equations

• Semantics.Modality.Assert.instInhabitedLeaveWorld.default = Semantics.Modality.Assert.LeaveWorld.leave

def Semantics.Modality.Assert.declarativeEvidence : SpeechActEvent LeaveWorld

Declarative context: speaker's evidence is compatible with both outcomes (speaker doesn't know whether the addressee will leave).

Equations

• Semantics.Modality.Assert.declarativeEvidence = Semantics.Modality.Assert.ASSERT fun (x : Semantics.Modality.Assert.LeaveWorld) => []

def Semantics.Modality.Assert.imperativePermission : SpeechActEvent LeaveWorld

Imperative context: permission to leave — only leave-world is compatible with the addressee's permissions.

Equations

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

theorem Semantics.Modality.Assert.different_speech_acts : declarativeEvidence.actType = Core.Discourse.IllocutionaryMood.declarative ∧ imperativePermission.actType = Core.Discourse.IllocutionaryMood.imperative

The two speech acts have different types.

theorem Semantics.Modality.Assert.declarative_leave_possible : EventRelativity.possibility Semantics.Modality.Assert.fDecl✝ () Semantics.Modality.Assert.allLW✝ (fun (x : LeaveWorld) => x == LeaveWorld.leave) LeaveWorld.leave = true

Under the declarative, both leaving and staying are possible (speaker is uncertain).

theorem Semantics.Modality.Assert.declarative_stay_possible : EventRelativity.possibility Semantics.Modality.Assert.fDecl✝ () Semantics.Modality.Assert.allLW✝ (fun (x : LeaveWorld) => x == LeaveWorld.stay) LeaveWorld.leave = true

theorem Semantics.Modality.Assert.imperative_leave_permitted : EventRelativity.possibility Semantics.Modality.Assert.fImpr✝ () Semantics.Modality.Assert.allLW✝ (fun (x : LeaveWorld) => x == LeaveWorld.leave) LeaveWorld.leave = true

Under the imperative, leaving is permitted but staying is NOT.

theorem Semantics.Modality.Assert.imperative_stay_not_permitted : EventRelativity.possibility Semantics.Modality.Assert.fImpr✝ () Semantics.Modality.Assert.allLW✝ (fun (x : LeaveWorld) => x == LeaveWorld.stay) LeaveWorld.leave = false

theorem Semantics.Modality.Assert.speech_act_modulates_domain : EventRelativity.possibility Semantics.Modality.Assert.fDecl✝ () Semantics.Modality.Assert.allLW✝ (fun (x : LeaveWorld) => x == LeaveWorld.stay) LeaveWorld.leave = true ∧ EventRelativity.possibility Semantics.Modality.Assert.fImpr✝ () Semantics.Modality.Assert.allLW✝¹ (fun (x : LeaveWorld) => x == LeaveWorld.stay) LeaveWorld.leave = false

The core contrast: same modal (◇), same proposition (stay), same evaluation world — but different speech acts yield different truth values. The speech act type, mediated through CON(e*), determines the modal domain.

The speech event projects to an individual-time pair via EventProjection (EventRelativity §11):

Speech act	holder(e*)	τ(e*)
Declarative	speaker	speech time
Imperative	addressee	speech time

The holder determines WHOSE propositional attitudes are relevant:

• Declarative: speaker's beliefs (epistemic = "what I know")
• Imperative: addressee's obligations (deontic = "what you must do")

Both share the same time (speech time = now), but the different holders yield different content types.

inductive Semantics.Modality.Assert.Interlocutor : Type

Speaker and addressee for the projection example.

• speaker : Interlocutor
• addressee : Interlocutor

instance Semantics.Modality.Assert.instDecidableEqInterlocutor : DecidableEq Interlocutor

Equations

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

def Semantics.Modality.Assert.instBEqInterlocutor.beq : Interlocutor → Interlocutor → Bool

Equations

• Semantics.Modality.Assert.instBEqInterlocutor.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Modality.Assert.instBEqInterlocutor : BEq Interlocutor

Equations

• Semantics.Modality.Assert.instBEqInterlocutor = { beq := Semantics.Modality.Assert.instBEqInterlocutor.beq }

instance Semantics.Modality.Assert.instReprInterlocutor : Repr Interlocutor

Equations

• Semantics.Modality.Assert.instReprInterlocutor = { reprPrec := Semantics.Modality.Assert.instReprInterlocutor.repr }

def Semantics.Modality.Assert.instReprInterlocutor.repr : Interlocutor → ℕ → Std.Format

Equations

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

def Semantics.Modality.Assert.instInhabitedInterlocutor.default : Interlocutor

Equations

• Semantics.Modality.Assert.instInhabitedInterlocutor.default = Semantics.Modality.Assert.Interlocutor.speaker

instance Semantics.Modality.Assert.instInhabitedInterlocutor : Inhabited Interlocutor

Equations

• Semantics.Modality.Assert.instInhabitedInterlocutor = { default := Semantics.Modality.Assert.instInhabitedInterlocutor.default }

inductive Semantics.Modality.Assert.SpeechTime : Type

Speech time.

• now : SpeechTime

instance Semantics.Modality.Assert.instDecidableEqSpeechTime : DecidableEq SpeechTime

Equations

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

instance Semantics.Modality.Assert.instBEqSpeechTime : BEq SpeechTime

Equations

• Semantics.Modality.Assert.instBEqSpeechTime = { beq := Semantics.Modality.Assert.instBEqSpeechTime.beq }

def Semantics.Modality.Assert.instBEqSpeechTime.beq : SpeechTime → SpeechTime → Bool

Equations

• Semantics.Modality.Assert.instBEqSpeechTime.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Modality.Assert.instReprSpeechTime.repr : SpeechTime → ℕ → Std.Format

Equations

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

instance Semantics.Modality.Assert.instReprSpeechTime : Repr SpeechTime

Equations

• Semantics.Modality.Assert.instReprSpeechTime = { reprPrec := Semantics.Modality.Assert.instReprSpeechTime.repr }

def Semantics.Modality.Assert.instInhabitedSpeechTime.default : SpeechTime

Equations

• Semantics.Modality.Assert.instInhabitedSpeechTime.default = Semantics.Modality.Assert.SpeechTime.now

instance Semantics.Modality.Assert.instInhabitedSpeechTime : Inhabited SpeechTime

Equations

• Semantics.Modality.Assert.instInhabitedSpeechTime = { default := Semantics.Modality.Assert.instInhabitedSpeechTime.default }

def Semantics.Modality.Assert.speechActProjection : EventRelativity.EventProjection SpeechActType Interlocutor SpeechTime

The event projection for speech act events.

Declarative: holder = speaker (it's the speaker's beliefs). Imperative: holder = addressee (it's the addressee's obligations).

NB: .interrogative =>.speaker because the holder is who PERFORMS the speech act (always the speaker in Hacquard's framework). This is distinct from the SEAT OF KNOWLEDGE, which is the hearer for interrogatives — that notion captures who has epistemic authority over the content, not who initiates the speech event. The bridge between these is in SpeechActs.lean: seat_of_knowledge_agrees_with_epistemic_authority.

Equations

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

theorem Semantics.Modality.Assert.declarative_projects_to_speaker : speechActProjection.toPair Core.Discourse.IllocutionaryMood.declarative = { individual := Interlocutor.speaker, time := SpeechTime.now }

Declarative projects to (speaker, now).

theorem Semantics.Modality.Assert.imperative_projects_to_addressee : speechActProjection.toPair Core.Discourse.IllocutionaryMood.imperative = { individual := Interlocutor.addressee, time := SpeechTime.now }

Imperative projects to (addressee, now).

theorem Semantics.Modality.Assert.different_holders : speechActProjection.toPair Core.Discourse.IllocutionaryMood.declarative ≠ speechActProjection.toPair Core.Discourse.IllocutionaryMood.imperative

Different speech act types project to different holders. The holder determines whose attitudes provide the modal content: speaker's beliefs (epistemic) vs addressee's obligations (deontic).