Event-Relative Modality

[Hac06] [Hac09] [Hac10] [AOR24] [Kra81]

Modal domains are projected from event arguments, not stipulated at the clause level. An anchoring function maps events to conversational backgrounds: the event type determines the modal flavor.

Core Architecture

Kratzer's ConvBackground W (W → List (W → Prop)) gives the modal base for a world. Hacquard adds a layer: modal bases are not context-global but event-local. An anchoring function f : Event → ConvBackground W first selects the event, then produces a Kratzer background — the Semantics/Modality/Kratzer operators apply to f e directly.

Content Licensing (§8–9)

The position → flavor correlation is DERIVED from a single predicate: content licensing. Epistemic modal bases require a contentful event — one with propositional content. Three event binders:

Binder	Event	Content?	Epistemic?
ASSERT	speech act (e₀)	✓	✓
Attitude verb	attitude (e₁)	✓	✓
Aspect (IMPF/PRFV)	VP event (e₂)	✗	✗

High modals (above AspP) are bound to contentful events → epistemic available. Low modals (below AspP) are bound by aspect to the VP event → circumstantial only. The binary AnchorType (§1) captures the A-O&R application; EventBinder (§8) captures the full three-way distinction needed for embedded contexts.

Application: Modal Indefinites (§3–7)

Modal indefinites are existential quantifiers carrying a modal component whose domain is projected from an event argument via an anchoring function.

@[reducible, inline]

abbrev Modality.AnchoringFn (Event : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

An anchoring function maps events to conversational backgrounds.

This is [Hac06]'s central innovation: modal bases are not global context parameters but projected from event arguments. Applied to a specific event it is exactly a Kratzer ConvBackground, so the Semantics/Modality/Kratzer operators apply to f e directly.

Equations

• Modality.AnchoringFn Event W = (Event → Modality.Kratzer.ConvBackground W)

inductive Modality.AnchorType : Type

The type of modal anchor: a binary coarsening of EventBinder (§8) that collapses the contentful cases (speech act, attitude) into speechEvent and the contentless case (VP event) into describedEvent.

This captures the matrix-clause application where only two anchor types matter. For the full three-way distinction needed for embedded contexts, use EventBinder directly.

[Hac06]: the speech event projects epistemic modality; the described event projects circumstantial/root modality. [AOR24] refine circumstantial to include random choice as a subtype.

• speechEvent : AnchorType

  Anchored to a contentful event (speech act or attitude) → epistemic available

• describedEvent : AnchorType

  Anchored to the VP event → circumstantial modal base

@[instance_reducible]

instance Modality.instDecidableEqAnchorType : DecidableEq AnchorType

Equations

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

def Modality.instReprAnchorType.repr : AnchorType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Modality.instReprAnchorType : Repr AnchorType

Equations

• Modality.instReprAnchorType = { reprPrec := Modality.instReprAnchorType.repr }

@[instance_reducible]

instance Modality.instInhabitedAnchorType : Inhabited AnchorType

Equations

• Modality.instInhabitedAnchorType = { default := Modality.instInhabitedAnchorType.default }

def Modality.AnchorType.toFlavor : AnchorType → ModalFlavor

Map anchor type to modal flavor.

Speech event anchoring yields epistemic modality; described event anchoring yields circumstantial modality (which subsumes random choice, teleological, ability, etc. per [Kra81]).

Equations

• Modality.AnchorType.speechEvent.toFlavor = Modality.ModalFlavor.epistemic
• Modality.AnchorType.describedEvent.toFlavor = Modality.ModalFlavor.circumstantial

theorem Modality.speech_is_epistemic : AnchorType.speechEvent.toFlavor = ModalFlavor.epistemic

theorem Modality.described_is_circumstantial : AnchorType.describedEvent.toFlavor = ModalFlavor.circumstantial

The modal indefinite denotation ([AOR24]), upper-boundedness, non-maximality, and harmonic interpretation types live in Studies/AlonsoOvalleRoyer2024.lean, which imports this file for AnchoringFn and applies the Semantics/Modality/Kratzer operators to the anchored backgrounds.

[Hac10] identifies THREE event binders that can supply a modal's event argument. The closest c-commanding binder determines which event the modal is relative to:

• e₀: the speech act event (bound by ASSERT / illocutionary force)
• e₁: an attitude event (bound by attitude verbs: believe, want,...)
• e₂: the VP event (bound by aspect: IMPF/PRFV)

The binary AnchorType (§1) omits e₁ (irrelevant in A-O&R's matrix-clause data), keeping only the speech event (e₀) / VP event (e₂) distinction. EventBinder adds e₁, which matters because attitude events are contentful (like speech events), not contentless (like VP events).

The key insight: epistemic modal bases require a contentful event — one with propositional content CON(e). Speech acts and attitudes have content; VP events (running, screaming) do not. This single predicate derives the position → flavor correlation.

inductive Modality.EventBinder : Type

The three event binders ([Hac10], (38), (48)).

• speechAct : EventBinder

  e₀: the utterance event (bound by ASSERT)

• attitude : EventBinder

  e₁: an attitude verb's event (believe, want, think,...)

• vpEvent : EventBinder

  e₂: the VP's described event (bound by aspect)

@[instance_reducible]

instance Modality.instDecidableEqEventBinder : DecidableEq EventBinder

Equations

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

def Modality.instReprEventBinder.repr : EventBinder → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Modality.instReprEventBinder : Repr EventBinder

Equations

• Modality.instReprEventBinder = { reprPrec := Modality.instReprEventBinder.repr }

[Hac10] (51) recasts the epistemic modal base as a function of propositional content:

∩f_epis(e) = {w' : w' is compatible with CON(e)}

CON(e) is the propositional content of event e — the set of propositions that constitute the "information state" of the event. For speech acts, CON(e₀) = the speaker's doxastic alternatives. For attitudes, CON(e₁) = the attitude holder's doxastic alternatives. For VP events, CON(e₂) is undefined: running, screaming, and swimming carry no propositional content.

ContentFn makes CON(e) a first-class function. The epistemic modal base is DERIVED from it, and hasContent (below) is derivable from whether CON(e) is defined — not stipulated as a lookup table.

@[reducible, inline]

abbrev Modality.ContentFn (Event : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

CON(e): the propositional content of an event.

Returns some bg when the event carries propositional content (speech acts, attitudes), where bg is the conversational background (propositions accessible from each world). Returns none when the event lacks content (VP events).

Equations

• Modality.ContentFn Event W = (Event → Option (Modality.Kratzer.ConvBackground W))

def Modality.epistemicFromContent {Event : Type u_1} {W : Type u_2} (con : ContentFn Event W) (e : Event) : Option (Kratzer.ConvBackground W)

Derive the epistemic modal base from event content.

[Hac10], (51): ∩f_epis(e) = {w' : w' compatible with CON(e)}. The epistemic base IS the content — this is identity, not a bridge.

Equations

• Modality.epistemicFromContent con e = con e

def Modality.contentDefined {Event : Type u_1} {W : Type u_2} (con : ContentFn Event W) (e : Event) : Bool

Whether CON(e) is defined for a given event. Derived from the content function, not stipulated.

Equations

• Modality.contentDefined con e = (con e).isSome

theorem Modality.epistemic_available_iff_content_defined {Event : Type u_1} {W : Type u_2} (con : ContentFn Event W) (e : Event) : (epistemicFromContent con e).isSome = contentDefined con e

Epistemic modal base available iff CON(e) is defined. This is definitional — not a bridge theorem but an architectural fact.

def Modality.binderContent {W : Type u_1} : EventBinder → Option (Kratzer.ConvBackground W)

Concrete CON for the three event binder types.

Speech acts: CON(e₀) provides the speaker's doxastic alternatives. Attitudes: CON(e₁) provides the holder's doxastic alternatives. VP events: CON(e₂) is undefined — no propositional content.

The actual propositions depend on the specific event instance; binderContent captures only definedness (some vs none).

Equations

• Modality.binderContent Modality.EventBinder.speechAct = some fun (x : W) => []
• Modality.binderContent Modality.EventBinder.attitude = some fun (x : W) => []
• Modality.binderContent Modality.EventBinder.vpEvent = none

def Modality.EventBinder.hasContent : EventBinder → Bool

Whether an event has propositional content.

⟦f_epis(e)⟧ = {w' : w' compatible with CON(e)} — but CON(e) is only defined for events with propositional content. Speech acts carry assertive content; attitudes carry doxastic/bouletic content; VP events (running, screaming, swimming) carry none.

Equations

• Modality.EventBinder.speechAct.hasContent = true
• Modality.EventBinder.attitude.hasContent = true
• Modality.EventBinder.vpEvent.hasContent = false

theorem Modality.hasContent_from_contentFn (b : EventBinder) : b.hasContent = (binderContent b).isSome

hasContent is derivable from binderContent: a binder has content iff CON(e) is defined (returns some). This shows that the Boolean predicate is a consequence of the deeper structure, not a stipulation.

def Modality.EventBinder.canProjectEpistemic (b : EventBinder) : Bool

Epistemic modal bases require contentful events.

Equations

• b.canProjectEpistemic = b.hasContent

def Modality.EventBinder.canProjectCircumstantial : EventBinder → Bool

Circumstantial modal bases need only the event's surrounding circumstances — available for any event type.

Equations

• x✝.canProjectCircumstantial = true

def Modality.EventBinder.hasAddressee : EventBinder → Bool

Whether an event has an addressee with a to-do list.

Deontic accessibility relations ([Hac06], (235c)) require the binding event to have an addressee: f_deontic(e) = λw. {w' : w' compatible with TO-DO-LIST(ADDR(e))}. Speech acts are directed at an addressee; VP events are not.

NB: Whether an attitude event has an addressee depends on the verb: order, tell, permit do; think, believe do not. This field captures the default case (non-directive attitude).

Equations

• Modality.EventBinder.speechAct.hasAddressee = true
• Modality.EventBinder.attitude.hasAddressee = false
• Modality.EventBinder.vpEvent.hasAddressee = false

def Modality.EventBinder.availableFlavors (b : EventBinder) : List ModalFlavor

Available modal flavors DERIVED from content licensing.

Contentful events (speech acts, attitudes): epistemic + circumstantial. Contentless events (VP events): circumstantial only.

NB: This captures the epistemic/non-epistemic divide from content licensing but omits deontic. Deontic licensing depends on a separate predicate — addressee availability ([Hac06], (235c)) — not on content. See hasAddressee and fullAvailableFlavors for the complete picture.

Equations

• b.availableFlavors = if b.hasContent = true then [Modality.ModalFlavor.epistemic, Modality.ModalFlavor.circumstantial] else [Modality.ModalFlavor.circumstantial]

def Modality.EventBinder.fullAvailableFlavors (b : EventBinder) : List ModalFlavor

Full available flavors including deontic ([Hac06], (235)).

Three accessibility relation types, each with different licensing:

• Epistemic f_epis(e): worlds compatible with CON(e). Requires content.
• Circumstantial f_circ(e): worlds compatible with CIRC(e). Any event.
• Deontic f_deontic(e): worlds compatible with TO-DO-LIST(ADDR(e)). Requires an addressee.

This extends availableFlavors with the deontic dimension.

Equations

• b.fullAvailableFlavors = if b.hasAddressee = true then b.availableFlavors ++ [Modality.ModalFlavor.deontic] else b.availableFlavors

theorem Modality.speechAct_has_content : EventBinder.speechAct.hasContent = true

theorem Modality.attitude_has_content : EventBinder.attitude.hasContent = true

theorem Modality.vpEvent_lacks_content : EventBinder.vpEvent.hasContent = false

theorem Modality.epistemic_iff_content (b : EventBinder) : b.canProjectEpistemic = b.hasContent

Content licensing: epistemic availability ↔ content.

theorem Modality.speechAct_has_addressee : EventBinder.speechAct.hasAddressee = true

theorem Modality.vpEvent_no_addressee : EventBinder.vpEvent.hasAddressee = false

theorem Modality.speechAct_full_flavors : EventBinder.speechAct.fullAvailableFlavors = [ModalFlavor.epistemic, ModalFlavor.circumstantial, ModalFlavor.deontic]

Speech acts license all three accessibility types ([Hac06], (235)): epistemic (content), circumstantial (circumstances), and deontic (addressee).

theorem Modality.vpEvent_full_flavors : EventBinder.vpEvent.fullAvailableFlavors = [ModalFlavor.circumstantial]

VP events license only circumstantial: no content (→ no epistemic), no addressee (→ no deontic).

theorem Modality.three_accessibility_types : EventBinder.speechAct.canProjectEpistemic = true ∧ EventBinder.vpEvent.canProjectEpistemic = false ∧ EventBinder.speechAct.canProjectCircumstantial = true ∧ EventBinder.vpEvent.canProjectCircumstantial = true ∧ EventBinder.speechAct.hasAddressee = true ∧ EventBinder.vpEvent.hasAddressee = false

The three licensing conditions ([Hac06], (235)):

• Epistemic needs content (CON(e))
• Circumstantial needs nothing (CIRC(e) is always available)
• Deontic needs an addressee (TO-DO-LIST(ADDR(e)))

theorem Modality.high_modal_epistemic : EventBinder.speechAct.canProjectEpistemic = true ∧ EventBinder.attitude.canProjectEpistemic = true

High modals (bound to speech act or attitude event) can be epistemic.

theorem Modality.low_modal_not_epistemic : EventBinder.vpEvent.canProjectEpistemic = false

Low modals (bound to VP event by aspect) cannot be epistemic. This is the core prediction: Italian restructuring forces modals low (below Asp), blocking epistemic readings.

theorem Modality.content_determines_flavors : EventBinder.speechAct.availableFlavors = [ModalFlavor.epistemic, ModalFlavor.circumstantial] ∧ EventBinder.attitude.availableFlavors = [ModalFlavor.epistemic, ModalFlavor.circumstantial] ∧ EventBinder.vpEvent.availableFlavors = [ModalFlavor.circumstantial]

Contentful events yield both flavors; contentless events yield only circumstantial. Derives the pattern in [Hac10]'s (49a–f).

theorem Modality.attitudes_pattern_with_speech : EventBinder.attitude.availableFlavors = EventBinder.speechAct.availableFlavors

Attitude verbs pattern with speech acts, not VP events — both are contentful. "John believes Mary might be pregnant" ([Hac10], (48b)): the embedded epistemic might is bound to the attitude event e₁ of believe, which has content, licensing epistemic.

theorem Modality.vpEvent_differs_from_contentful : EventBinder.vpEvent.availableFlavors ≠ EventBinder.speechAct.availableFlavors ∧ EventBinder.vpEvent.availableFlavors ≠ EventBinder.attitude.availableFlavors

VP events differ from both contentful event types. The three-way distinction is invisible to the binary AnchorType but crucial for embedded contexts (attitude verbs license epistemic; VP events do not).

def Modality.AnchorType.toEventBinder : AnchorType → EventBinder

Map the binary anchor type to the corresponding event binder. speechEvent → speechAct (matrix clause default). describedEvent → vpEvent (VP event bound by aspect).

Equations

• Modality.AnchorType.speechEvent.toEventBinder = Modality.EventBinder.speechAct
• Modality.AnchorType.describedEvent.toEventBinder = Modality.EventBinder.vpEvent

def Modality.EventBinder.toAnchorType : EventBinder → AnchorType

Project an event binder to the binary anchor type.

This collapses the three-way EventBinder to the two-way AnchorType by grouping contentful events (speech act, attitude) together as speechEvent and contentless events (VP) as describedEvent.

The grouping is principled: it follows hasContent. Contentful binders project to speechEvent; contentless to describedEvent.

Equations

• Modality.EventBinder.speechAct.toAnchorType = Modality.AnchorType.speechEvent
• Modality.EventBinder.attitude.toAnchorType = Modality.AnchorType.speechEvent
• Modality.EventBinder.vpEvent.toAnchorType = Modality.AnchorType.describedEvent

theorem Modality.toAnchorType_groups_by_content (b : EventBinder) : (b.toAnchorType == AnchorType.speechEvent) = b.hasContent

The projection groups by contentfulness: all contentful binders map to speechEvent, the contentless binder maps to describedEvent.

theorem Modality.toEventBinder_section (a : AnchorType) : a.toEventBinder.toAnchorType = a

toEventBinder is a section of toAnchorType: round-tripping through EventBinder and back recovers the original AnchorType.

theorem Modality.toFlavor_derived (a : AnchorType) : a.toEventBinder.availableFlavors.head? = some a.toFlavor

AnchorType.toFlavor is derivable from content licensing: the primary flavor for each anchor type is the head of the corresponding event binder's available flavor list. This replaces a stipulation with a derivation through hasContent.

theorem Modality.toFlavor_via_projection (b : EventBinder) : b.hasContent = true → b.toAnchorType.toFlavor = ModalFlavor.epistemic

AnchorType.toFlavor is also derivable via toAnchorType: the primary flavor of any binder's anchor type equals the head of that binder's available flavors (for binders that have a primary flavor).

theorem Modality.unattested_49e_explained : EventBinder.vpEvent.canProjectEpistemic = false ∧ EventBinder.speechAct.canProjectEpistemic = true ∧ EventBinder.attitude.canProjectEpistemic = true ∧ EventBinder.vpEvent.canProjectCircumstantial = true ∧ EventBinder.speechAct.canProjectCircumstantial = true ∧ EventBinder.attitude.canProjectCircumstantial = true

The six binder × flavor combinations ([Hac10], (49a–f)). Content licensing explains (49e): VP events lack content → no epistemic. The remaining unattested combinations (49b: speech act + circumstantial, 49d: attitude + circumstantial) are semantically possible but pragmatically blocked — circumstantial readings of high modals are pre-empted by the more informative epistemic reading.

Syntactic position determines which event binder is closest to the modal. Aspect (IMPF/PRFV) existentially quantifies over VP events and binds the event variable of any modal in its scope. A modal ABOVE AspP is bound by the speech act or attitude event (whichever is closest); a modal BELOW AspP is bound by aspect's event quantifier.

The full clausal ordering derived in [Hac06]): -- UNVERIFIED: p.160

Mod_epis > T > CF > Asp > Mod_circ

Epistemic modals are above Tense and counterfactual morphology; circumstantial/root modals are below Aspect. Our ModalPosition captures the binary above/below Asp distinction, which is sufficient for content licensing and actuality entailments. The finer-grained ordering relative to T and CF would require syntactic tree structure.

This connects the clause structure formalized in Syntax/Minimalism/Voice.lean and the viewpoint-aspect operators in Semantics/Aspect/Basic.lean to the event-relative framework.

inductive Modality.ModalPosition : Type

Position of a modal relative to Aspect in the clause. [Hac10]: this is the structural correlate of the [Cin99] high/low modal distinction.

• aboveAsp : ModalPosition

  Above AspP: bound by ASSERT (matrix) or attitude verb (embedded)

• belowAsp : ModalPosition

  Below AspP: bound by aspect's event quantifier (∃e[...])

@[instance_reducible]

instance Modality.instDecidableEqModalPosition : DecidableEq ModalPosition

Equations

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

@[instance_reducible]

instance Modality.instReprModalPosition : Repr ModalPosition

Equations

• Modality.instReprModalPosition = { reprPrec := Modality.instReprModalPosition.repr }

def Modality.instReprModalPosition.repr : ModalPosition → ℕ → Std.Format

Equations

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

def Modality.ModalPosition.defaultBinder : ModalPosition → EventBinder

Default event binder for a modal in each position. High modals default to the speech act (matrix) or attitude event (embedded — see withAttitude). Low modals are bound to the VP event by aspect.

Equations

• Modality.ModalPosition.aboveAsp.defaultBinder = Modality.EventBinder.speechAct
• Modality.ModalPosition.belowAsp.defaultBinder = Modality.EventBinder.vpEvent

def Modality.ModalPosition.withAttitude : ModalPosition → EventBinder

In an embedded context under an attitude verb, a high modal's event is bound by the attitude event rather than the speech act.

Equations

• Modality.ModalPosition.aboveAsp.withAttitude = Modality.EventBinder.attitude
• Modality.ModalPosition.belowAsp.withAttitude = Modality.EventBinder.vpEvent

theorem Modality.position_determines_epistemic : ModalPosition.aboveAsp.defaultBinder.canProjectEpistemic = true ∧ ModalPosition.belowAsp.defaultBinder.canProjectEpistemic = false

High modals can be epistemic; low modals cannot. DERIVED from defaultBinder + content licensing — not stipulated.

theorem Modality.embedded_high_still_epistemic : ModalPosition.aboveAsp.withAttitude.canProjectEpistemic = true

Embedded high modals under attitude verbs can still be epistemic, because attitude events are contentful.

theorem Modality.embedded_low_still_root : ModalPosition.belowAsp.withAttitude.canProjectEpistemic = false

Low modals remain circumstantial-only even under attitude verbs: aspect binds them to the VP event regardless of embedding.

theorem Modality.full_position_flavor_table : ModalPosition.aboveAsp.defaultBinder.availableFlavors = [ModalFlavor.epistemic, ModalFlavor.circumstantial] ∧ ModalPosition.aboveAsp.withAttitude.availableFlavors = [ModalFlavor.epistemic, ModalFlavor.circumstantial] ∧ ModalPosition.belowAsp.defaultBinder.availableFlavors = [ModalFlavor.circumstantial]

Full flavor availability by position and embedding context. Matrix high: epistemic + circumstantial (speech act). Embedded high: epistemic + circumstantial (attitude event). Low (either context): circumstantial only (VP event).

Aspect is the event binder for low modals. Perfective and imperfective both existentially quantify over events:

⟦PRFV⟧ = λP.λt.∃e[τ(e) ⊆ t ∧ P(e)]
⟦IMPF⟧ = λP.λt.∃e[t ⊂ τ(e) ∧ P(e)]

This ∃e binds the free event variable in the modal's restriction, anchoring it to the VP event. Both perfective and imperfective bind to VP events — they differ in temporal containment, not in which event they bind.

This makes aspect the structural MECHANISM behind ModalPosition.belowAsp.defaultBinder = .vpEvent: it is aspect's existential quantification that performs the binding.

inductive Modality.Perfectivity' : Type

Aspect binds the modal to the VP event regardless of viewpoint (perfective or imperfective). The two viewpoints differ in temporal containment (τ(e) ⊆ t vs t ⊂ τ(e)) but both bind the same event variable — the VP event.

• perfective : Perfectivity'
• imperfective : Perfectivity'

@[instance_reducible]

instance Modality.instDecidableEqPerfectivity' : DecidableEq Perfectivity'

Equations

• Modality.instDecidableEqPerfectivity' x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Modality.instReprPerfectivity'.repr : Perfectivity' → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Modality.instReprPerfectivity' : Repr Perfectivity'

Equations

• Modality.instReprPerfectivity' = { reprPrec := Modality.instReprPerfectivity'.repr }

def Modality.Perfectivity'.bindsTo : Perfectivity' → EventBinder

Aspect always binds the modal's event variable to the VP event. This is WHY low modals have defaultBinder = .vpEvent: the structural source of that binding is aspect's ∃e quantification.

Equations

• Modality.Perfectivity'.perfective.bindsTo = Modality.EventBinder.vpEvent
• Modality.Perfectivity'.imperfective.bindsTo = Modality.EventBinder.vpEvent

theorem Modality.aspect_always_binds_vp (asp : Perfectivity') : asp.bindsTo = EventBinder.vpEvent

theorem Modality.aspect_bound_no_epistemic (asp : Perfectivity') : asp.bindsTo.canProjectEpistemic = false

Aspect binding entails the low-modal flavor restriction: since aspect binds to VP events, and VP events lack content, aspect-bound modals cannot be epistemic.

The full [Hac10] semantics (29) is

⟦modal⟧(p)(e)(w) = ∀/∃ w' ∈ max_{g(e)(w)}(∩f(e)(w)). p(w')

— Kratzer's ordered operators applied to the anchored base and ordering: Kratzer.necessity (f e) (g e) and Kratzer.possibility (f e) (g e). The only event-relative ingredient is the ordering source projected from the event.

@[reducible, inline]

abbrev Modality.OrderingFn (Event : Type u_1) (W : Type u_2) : Type (max u_1 u_2)

An event-relative ordering source: applied to an event it is a Kratzer OrderingSource.

Equations

• Modality.OrderingFn Event W = (Event → Modality.Kratzer.OrderingSource W)

[Hac10] unifies attitude semantics with modal semantics: the epistemic modal base under an attitude verb IS the content of the attitude event. Hintikka-style doxastic quantification — ∀w' ∈ DOX(x,w). p(w') — is a special case of event-relative necessity where the anchoring function encodes the agent's doxastic alternatives.

[Hac10], (41):

⟦believe⟧ = λe. λp. λx. λw. Exp(e,x) & belief'(e,w) &
            ∀w'∈ ∩CON(e): p(w') = 1
  where ∩CON(e) = DOX(ιx Holder(x,e), w)

The bridge: given an agent-indexed accessibility relation R and a holder function extracting the agent from an event, we construct an anchoring function whose event-relative necessity IS Hintikka's □.

def Modality.doxasticAnchoring {Event : Type u_1} {W : Type u_2} {E : Type u_3} (R : E → W → W → Prop) (holder : Event → E) : AnchoringFn Event W

Construct an anchoring function from a doxastic accessibility relation.

Given R : E → W → W → Prop (agent → eval world → accessible world) and holder : Event → E, the anchoring function f(e)(w) = [R(holder(e), w, ·)] — a singleton background whose sole premise is doxastic accessibility from w.

This implements [Hac10]'s insight that CON(e) for an attitude event e IS the set of doxastic alternatives of holder(e).

Equations

• Modality.doxasticAnchoring R holder e w = [R (holder e) w]

theorem Modality.doxastic_necessity_eq {Event : Type u_1} {W : Type u_2} {E : Type u_3} (R : E → W → W → Prop) (holder : Event → E) (e : Event) (p : W → Prop) (w : W) : Kratzer.simpleNecessity (doxasticAnchoring R holder e) p w ↔ ∀ (w' : W), R (holder e) w w' → p w'

Necessity over a doxastic anchoring is Hintikka-style universal quantification over the holder's doxastic alternatives — attitude verbs and modals share the same quantificational structure ([Hac10], §6.1.3).

theorem Modality.doxastic_possibility_eq {Event : Type u_1} {W : Type u_2} {E : Type u_3} (R : E → W → W → Prop) (holder : Event → E) (e : Event) (p : W → Prop) (w : W) : Kratzer.simplePossibility (doxasticAnchoring R holder e) p w ↔ ∃ (w' : W), R (holder e) w w' ∧ p w'

Possibility dually: some doxastic alternative of the holder satisfies p.

[Hac06] proposes that accessibility relations take EVENT arguments (193): R_f := λe.λw. w is compatible with f(e). Events project to (individual, time) pairs via two functions:

• holder(e): the thematic participant — Agent, Experiencer, or speaker — determined by the event's thematic structure.
• τ(e): the temporal trace — the time of the event.

This makes individual-time pairs (the traditional modal parameter per [Kra81]; [vF99a] generalizes to (individual, world) pairs) DERIVED from events, not primitive. Three advantages:

1. Unification: The same mechanism (event projection) applies to all three event types, deriving the right individual and time.
2. Additional structure: Events carry propositional content (§8), aspectual structure (ActualityEntailments.lean), and thematic structure. Individual-time pairs carry none of this.
3. No stipulated parameters: The modal doesn't need to be specified for a particular individual or time. These are projected from whichever event binds the modal (200): the closest binder.

structure Modality.IndTimePair (Individual : Type u_1) (TimePoint : Type u_2) : Type (max u_1 u_2)

An individual-time pair: the traditional modal parameter.

[Kra81] relativizes accessibility to circumstances at a world. [vF99a] §3.2 generalizes to (individual, world) pairs for attitude predicates. Hacquard derives (individual, time) from events, making stipulated parameters redundant.

• individual : Individual
• time : TimePoint

@[instance_reducible]

instance Modality.instDecidableEqIndTimePair {Individual✝ : Type u_1} {TimePoint✝ : Type u_2} [DecidableEq Individual✝] [DecidableEq TimePoint✝] : DecidableEq (IndTimePair Individual✝ TimePoint✝)

Equations

• Modality.instDecidableEqIndTimePair = Modality.instDecidableEqIndTimePair.decEq

def Modality.instDecidableEqIndTimePair.decEq {Individual✝ : Type u_1} {TimePoint✝ : Type u_2} [DecidableEq Individual✝] [DecidableEq TimePoint✝] (x✝ x✝¹ : IndTimePair Individual✝ TimePoint✝) : Decidable (x✝ = x✝¹)

Equations

• Modality.instDecidableEqIndTimePair.decEq { individual := a, time := a_1 } { individual := b, time := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Modality.instReprIndTimePair.repr {Individual✝ : Type u_1} {TimePoint✝ : Type u_2} [Repr Individual✝] [Repr TimePoint✝] : IndTimePair Individual✝ TimePoint✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Modality.instReprIndTimePair {Individual✝ : Type u_1} {TimePoint✝ : Type u_2} [Repr Individual✝] [Repr TimePoint✝] : Repr (IndTimePair Individual✝ TimePoint✝)

Equations

• Modality.instReprIndTimePair = { reprPrec := Modality.instReprIndTimePair.repr }

structure Modality.EventProjection (Event : Type u_1) (Individual : Type u_2) (TimePoint : Type u_3) : Type (max (max u_1 u_2) u_3)

Event projection: how events map to individuals and times.

holder extracts the thematic participant: "the agent and temporal trace of the event quantified by Aspect." For speech events: the speaker. For attitudes: the experiencer. For VP events: the agent or experiencer.

time extracts the temporal trace τ: the time at which the event occurs, hence the time at which the accessibility relation is evaluated.

• holder : Event → Individual
• time : Event → TimePoint

def Modality.EventProjection.toPair {Event : Type u_1} {Individual : Type u_2} {TimePoint : Type u_3} (proj : EventProjection Event Individual TimePoint) (e : Event) : IndTimePair Individual TimePoint

Derive the individual-time pair from an event.

This is the core of §4.1: individual-time pairs are not stipulated but projected from events. toPair proj e = (holder(e), τ(e)).

Equations

• proj.toPair e = { individual := proj.holder e, time := proj.time e }

def Modality.factoredAnchoring {Event : Type u_1} {W : Type u_2} {Individual : Type u_3} {TimePoint : Type u_4} (proj : EventProjection Event Individual TimePoint) (g : Individual → TimePoint → Kratzer.ConvBackground W) : AnchoringFn Event W

An anchoring function that factors through event projection.

If g is an accessibility relation parameterized by (individual, time), then factoredAnchoring proj g is the event-relative version: f(e)(w) = g(holder(e), τ(e))(w).

This shows that event-relative anchoring SUBSUMES individual-time anchoring: any (individual, time)-parameterized R can be recovered by composing with event projection.

Equations

• Modality.factoredAnchoring proj g e w = g (proj.holder e) (proj.time e) w

theorem Modality.factored_reduces {Event : Type u_1} {W : Type u_2} {Individual : Type u_3} {TimePoint : Type u_4} (proj : EventProjection Event Individual TimePoint) (g : Individual → TimePoint → Kratzer.ConvBackground W) (e : Event) (w : W) : factoredAnchoring proj g e w = g (proj.holder e) (proj.time e) w

Factored anchoring reduces to the (individual, time)-parameterized function applied to the event's projected pair.

Individual-time pairs capture WHO and WHEN, but events additionally carry WHETHER-CONTENT. This extra dimension is what content licensing (§8) exploits: epistemic R requires CON(e), which is a property of events (speech acts and attitudes have content; VP events don't), not a property of (individual, time) pairs.

Two events can project to the SAME individual-time pair yet differ in content licensing. For instance, imagine a speech event and an attitude event where the speaker = the attitude holder and the times coincide. Both project to (speaker, now), but they are different events with (potentially) different content. The event level is strictly richer.

theorem Modality.events_richer_than_pairs : EventBinder.speechAct.hasContent = true ∧ EventBinder.attitude.hasContent = true ∧ EventBinder.vpEvent.hasContent = false ∧ EventBinder.speechAct.availableFlavors = EventBinder.attitude.availableFlavors

Events carry content information (§8) that individual-time pairs do not. This theorem shows that hasContent discriminates events even though pairs cannot: speech acts and attitudes are both contentful, VP events are not.

An (individual, time) pair has no hasContent field. If we collapsed events to pairs, we would LOSE the ability to derive content licensing. This is why events, not pairs, are the right primitive.