Event-level mood operators

This file defines the event-level dimension of grammatical mood, following [Gra24]: mood morphemes operate on the eventuality argument of the complement clause. Indicative existentially closes it, yielding a proposition; subjunctive leaves it open, as required by causatives, intention reports, aspectual predicates, and memory/perception reports.

def Mood.INDev {Event : Type u_1} (P : Event → Prop) : Prop

The indicative existentially closes the complement's event argument, yielding a proposition ([Gra24], (87)).

Equations

• Mood.INDev P = ∃ (e : Event), P e

def Mood.SBJVev₁ {Event : Type u_1} (P : Event → Prop) : Event → Prop

The subjunctive leaves the complement's event argument open for abstraction ([Gra24], (88a)).

Equations

• Mood.SBJVev₁ P = P

def Mood.SBJVev₂ {Event : Type u_1} {W : Type u_2} (causeStar : Event → Event → W → Prop) (content : Event → W → Prop) (P : W → Event → Prop) (e : Event) : Prop

The intend subjunctive: the attitude state must causally bring about the described event ([Gra24], (134); [Sea83]).

Equations

• Mood.SBJVev₂ causeStar content P e = ∀ (w : W), content e w → ∃ (e' : Event), causeStar e e' w ∧ P w e'

Mood as event closure, by constructor

inductive Mood.EventDenotation (Event : Type u_2) : Type u_2

The result of a mood's event-level denotation: the event argument closed to a proposition, or still open for abstraction.

• closed {Event : Type u_2} (p : Prop) : EventDenotation Event

  The event argument has been existentially closed.

• abstracted {Event : Type u_2} (p : Event → Prop) : EventDenotation Event

  The event argument remains open for abstraction.

def Mood.Grammatical.eventDenotation {Event : Type u_1} (P : Event → Prop) : Grammatical → EventDenotation Event

The event-level denotation of a complement under each grammatical mood ([Gra24]).

Equations

• Mood.Grammatical.eventDenotation P Mood.Grammatical.indicative = Mood.EventDenotation.closed (Mood.INDev P)
• Mood.Grammatical.eventDenotation P Mood.Grammatical.subjunctive = Mood.EventDenotation.abstracted (Mood.SBJVev₁ P)

@[simp]

theorem Mood.eventDenotation_indicative {Event : Type u_1} (P : Event → Prop) : Grammatical.eventDenotation P Grammatical.indicative = EventDenotation.closed (∃ (e : Event), P e)

Indicative closes the event argument — why indicative complements cannot feed CAUSE* or aspectual operators ([Gra24]).

@[simp]

theorem Mood.eventDenotation_subjunctive {Event : Type u_1} (P : Event → Prop) : Grammatical.eventDenotation P Grammatical.subjunctive = EventDenotation.abstracted P

Subjunctive leaves the event argument open — why subjunctive complements feed eventuality abstraction ([Gra24]).