Documentation

Linglib.Theories.Semantics.Modality.EventRelativity

Event-Relative Modality #

@cite{hacquard-2006} @cite{hacquard-2009} @cite{hacquard-2010} @cite{alonso-ovalle-royer-2024} @cite{kratzer-1981}

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 (World → List (BProp World)) gives the modal base for a world. Hacquard adds a layer: modal bases are not context-global but event-local. An anchoring function f : Ev → W → List (BProp W) first selects the event, then produces a Kratzer background.

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:

BinderEventContent?Epistemic?
ASSERTspeech act (e₀)
Attitude verbattitude (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 Semantics.Modality.EventRelativity.AnchoringFn (Ev : Type u_1) (W : Type u_2) :
Type (max u_1 u_2)

An anchoring function maps events to conversational backgrounds.

This is @cite{hacquard-2006}'s central innovation: modal bases are not global context parameters but projected from event arguments.

The type AnchoringFn Ev W = Ev → W → List (BProp W) specializes to Kratzer's ConvBackground = World → List (BProp World) when applied to a specific event.

Equations
Instances For
    def Semantics.Modality.EventRelativity.anchor {Ev : Type u_1} {W : Type u_2} (f : AnchoringFn Ev W) (e : Ev) :
    WList (BProp W)

    An anchoring function applied to a specific event yields a Kratzer-style conversational background.

    Equations
    Instances For

      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.

      @cite{hacquard-2006}: the speech event projects epistemic modality; the described event projects circumstantial/root modality. @cite{alonso-ovalle-royer-2024} 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

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

          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 @cite{kratzer-1981}).

          Equations
          Instances For
            def Semantics.Modality.EventRelativity.accessible {Ev : Type u_1} {W : Type u_2} (f : AnchoringFn Ev W) (e : Ev) (allW : List W) (w : W) :

            Accessibility: world w' is accessible from w given anchoring function f applied to event e.

            NB: This omits Kratzer's ordering source g (cf. @cite{hacquard-2010}, (29): max_g(e)(∩f(e))). The ordering source is orthogonal to the content-licensing analysis and not needed for the MI application.

            Equations
            Instances For
              def Semantics.Modality.EventRelativity.possibility {Ev : Type u_1} {W : Type u_2} (f : AnchoringFn Ev W) (e : Ev) (allW : List W) (p : BProp W) (w : W) :

              Existential modal: ◇_{f(e)} p at world w. True iff some world accessible via f(e) satisfies p.

              Equations
              Instances For
                def Semantics.Modality.EventRelativity.necessity {Ev : Type u_1} {W : Type u_2} (f : AnchoringFn Ev W) (e : Ev) (allW : List W) (p : BProp W) (w : W) :

                Universal modal: □_{f(e)} p at world w. True iff all worlds accessible via f(e) satisfy p.

                Equations
                Instances For
                  theorem Semantics.Modality.EventRelativity.duality {Ev : Type u_1} {W : Type u_2} (f : AnchoringFn Ev W) (e : Ev) (allW : List W) (p : BProp W) (w : W) :
                  (necessity f e allW p w == !possibility f e allW (fun (w' : W) => !p w') w) = true

                  The modal indefinite denotation (A-@cite{alonso-ovalle-royer-2024}), upper-boundedness, non-maximality, and harmonic interpretation types have been extracted to Theories/Semantics/Modality/ModalIndefinites.lean. That file imports this one for AnchoringFn and possibility.

                  @cite{hacquard-2010} 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:

                  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.

                  The three event binders (@cite{hacquard-2010}, (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)

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

                      @cite{hacquard-2010} (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 Semantics.Modality.EventRelativity.ContentFn (Ev : 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
                      Instances For
                        def Semantics.Modality.EventRelativity.epistemicFromContent {Ev : Type u_1} {W : Type u_2} (con : ContentFn Ev W) (e : Ev) :
                        Option (WList (BProp W))

                        Derive the epistemic modal base from event content.

                        @cite{hacquard-2010}, (51): ∩f_epis(e) = {w' : w' compatible with CON(e)}. The epistemic base IS the content — this is identity, not a bridge.

                        Equations
                        Instances For
                          def Semantics.Modality.EventRelativity.contentDefined {Ev : Type u_1} {W : Type u_2} (con : ContentFn Ev W) (e : Ev) :

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

                          Equations
                          Instances For

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

                            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
                            Instances For

                              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
                              Instances For

                                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.

                                Epistemic modal bases require contentful events.

                                Equations
                                Instances For

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

                                  Equations
                                  Instances For

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

                                    Deontic accessibility relations (@cite{hacquard-2006}, (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
                                    Instances For

                                      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 (@cite{hacquard-2006}, (235c)) — not on content. See hasAddressee and fullAvailableFlavors for the complete picture.

                                      Equations
                                      Instances For

                                        Full available flavors including deontic (@cite{hacquard-2006}, (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
                                        Instances For

                                          Content licensing: epistemic availability ↔ content.

                                          Speech acts license all three accessibility types (@cite{hacquard-2006}, (235)): epistemic (content), circumstantial (circumstances), and deontic (addressee).

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

                                          The three licensing conditions (@cite{hacquard-2006}, (235)):

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

                                          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.

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

                                          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).

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

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

                                          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.

                                          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).

                                          The six binder × flavor combinations (@cite{hacquard-2010}, (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 @cite{hacquard-2006}): -- 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 Theories/Syntax/Minimalism/Core/Voice.lean and the aspect operators in Theories/Semantics/Lexical/Verb/ViewpointAspect.lean to the event-relative framework.

                                          Position of a modal relative to Aspect in the clause. @cite{hacquard-2010}: this is the structural correlate of the @cite{cinque-1999} 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[...])

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

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

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

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

                                              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.

                                              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.

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

                                                  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.

                                                  An anchoring function applied to a specific event yields a function W → List (BProp W) — structurally identical to Kratzer's ConvBackground = World → List (BProp World) (in Theories/Semantics/Modality/Kratzer.lean).

                                                  anchor f e : W → List (BProp W) ≡ ConvBackground
                                                  

                                                  This is definitional: anchor f e = f e. Event-relative modality IS Kratzer modality with the conversational background projected from an event argument rather than stipulated as a context parameter. No bridge theorem is needed — the types unify by construction.

                                                  theorem Semantics.Modality.EventRelativity.anchor_reduces {Ev : Type u_1} {W : Type u_2} (f : AnchoringFn Ev W) (e : Ev) :
                                                  anchor f e = f e

                                                  anchor f e reduces to the anchoring function applied to the event. This makes explicit that the result is a conversational background (world → set of propositions) in Kratzer's sense.

                                                  theorem Semantics.Modality.EventRelativity.accessible_is_background_filter {Ev : Type u_1} {W : Type u_2} (f : AnchoringFn Ev W) (e : Ev) (allW : List W) (w : W) :
                                                  accessible f e allW w = List.filter (fun (w' : W) => (f e w).all fun (x : BProp W) => x w') allW

                                                  Event-relative accessibility reduces to Kratzer-style accessibility: filtering worlds by the propositions in the background projected from event e. The implementation parallels Kratzer.accessibleWorlds (which computes allWorlds.filter (λ w' => (f w).all (· w'))).

                                                  The modal evaluation in §2 omits Kratzer's ordering source g. The full @cite{hacquard-2010} semantics (29) is:

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

                                                  where max_{g(e)(w)} selects the BEST worlds among the accessible worlds, ranked by the ordering source projected from event e.

                                                  An event-relative ordering source maps events to ordering functions, parallel to how the anchoring function maps events to modal bases. Different events can yield different orderings — e.g., a speech event might project the speaker's normative standards, while a VP event might project stereotypical ordering (inertia).

                                                  @[reducible, inline]
                                                  abbrev Semantics.Modality.EventRelativity.OrderingFn (Ev : Type u_1) (W : Type u_2) :
                                                  Type (max u_1 u_2)

                                                  An event-relative ordering source: maps events to world-orderings. The ordering source determines how accessible worlds are ranked. Applied to event e and world w, it yields the set of propositions characterizing the ideal (norms, stereotypes, goals).

                                                  Equations
                                                  Instances For
                                                    def Semantics.Modality.EventRelativity.bestAccessible {Ev : Type u_1} {W : Type u_2} [DecidableEq W] (f : AnchoringFn Ev W) (g : OrderingFn Ev W) (e : Ev) (allW : List W) (w : W) :

                                                    The best worlds among the accessible set, ranked by the event-relative ordering source. Combines the anchoring function (modal base) with the ordering function to select the maximally ideal accessible worlds.

                                                    This implements Hacquard's (29): max_{g(e)}(∩f(e)).

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      def Semantics.Modality.EventRelativity.orderedNecessity {Ev : Type u_1} {W : Type u_2} [DecidableEq W] (f : AnchoringFn Ev W) (g : OrderingFn Ev W) (e : Ev) (allW : List W) (p : BProp W) (w : W) :

                                                      Event-relative necessity with ordering source: □_{f(e),g(e)} p at world w = ∀w' ∈ Best(f(e),g(e),w). p(w').

                                                      Equations
                                                      Instances For
                                                        def Semantics.Modality.EventRelativity.orderedPossibility {Ev : Type u_1} {W : Type u_2} [DecidableEq W] (f : AnchoringFn Ev W) (g : OrderingFn Ev W) (e : Ev) (allW : List W) (p : BProp W) (w : W) :

                                                        Event-relative possibility with ordering source: ◇_{f(e),g(e)} p at world w = ∃w' ∈ Best(f(e),g(e),w). p(w').

                                                        Equations
                                                        Instances For
                                                          theorem Semantics.Modality.EventRelativity.empty_ordering_reduces {Ev : Type u_1} {W : Type u_2} [DecidableEq W] (f : AnchoringFn Ev W) (e : Ev) (allW : List W) (p : BProp W) (w : W) :
                                                          orderedNecessity f (fun (x : Ev) (x_1 : W) => []) e allW p w = necessity f e allW p w

                                                          Empty ordering source: all accessible worlds are best (no ranking). Reduces to the unordered evaluation in §2.

                                                          @cite{hacquard-2010} 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.

                                                          @cite{hacquard-2010}, (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 Semantics.Modality.EventRelativity.doxasticAnchoring {Ev : Type u_1} {W : Type u_2} {E : Type u_3} (R : Core.ModalLogic.AgentAccessRel W E) (holder : EvE) :

                                                          Construct an anchoring function from a doxastic accessibility relation.

                                                          Given R : E → W → W → Bool (agent → eval world → accessible world → Bool) and holder : Ev → E (event → agent), the anchoring function f(e)(w) = [R(holder(e), w, ·)] — a singleton background whose sole proposition encodes the doxastic accessibility from world w.

                                                          This implements @cite{hacquard-2010}'s insight that CON(e) for an attitude event e IS the set of doxastic alternatives of holder(e).

                                                          Equations
                                                          Instances For
                                                            theorem Semantics.Modality.EventRelativity.doxastic_necessity_eq {Ev : Type u_1} {W : Type u_2} {E : Type u_3} (R : Core.ModalLogic.AgentAccessRel W E) (holder : EvE) (e : Ev) (allW : List W) (p : BProp W) (w : W) :
                                                            necessity (doxasticAnchoring R holder) e allW p w = allW.all fun (w' : W) => !R (holder e) w w' || p w'

                                                            Event-relative necessity with doxastic anchoring equals Hintikka-style universal quantification over doxastic alternatives.

                                                            necessity (doxasticAnchoring R holder) e allW p w = (allW.filter (R (holder e) w)).all p -- event-relative = allW.all (λw'. ¬R(holder(e),w,w') ∨ p(w')) -- Hintikka's □

                                                            This is the core bridge theorem: attitude verbs and modals share the same quantificational structure. Embedded epistemics under believe quantify over the SAME set of worlds as the attitude verb itself (@cite{hacquard-2010}, §6.1.3).

                                                            theorem Semantics.Modality.EventRelativity.doxastic_possibility_eq {Ev : Type u_1} {W : Type u_2} {E : Type u_3} (R : Core.ModalLogic.AgentAccessRel W E) (holder : EvE) (e : Ev) (allW : List W) (p : BProp W) (w : W) :
                                                            possibility (doxasticAnchoring R holder) e allW p w = allW.any fun (w' : W) => R (holder e) w w' && p w'

                                                            Doxastic possibility dually: ◇_{DOX(holder(e))} p at w iff some doxastic alternative of holder(e) satisfies p.

                                                            @cite{hacquard-2006} 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:

                                                            This makes individual-time pairs (the traditional modal parameter per @cite{kratzer-1981}; @cite{von-fintel-1999} 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 Semantics.Modality.EventRelativity.IndTimePair (Individual : Type u_1) (TimePoint : Type u_2) :
                                                            Type (max u_1 u_2)

                                                            An individual-time pair: the traditional modal parameter.

                                                            @cite{kratzer-1981} relativizes accessibility to circumstances at a world. @cite{von-fintel-1999} §3.2 generalizes to (individual, world) pairs for attitude predicates. Hacquard derives (individual, time) from events, making stipulated parameters redundant.

                                                            • individual : Individual
                                                            • time : TimePoint
                                                            Instances For
                                                              def Semantics.Modality.EventRelativity.instDecidableEqIndTimePair.decEq {Individual✝ : Type u_1} {TimePoint✝ : Type u_2} [DecidableEq Individual✝] [DecidableEq TimePoint✝] (x✝ x✝¹ : IndTimePair Individual✝ TimePoint✝) :
                                                              Decidable (x✝ = x✝¹)
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                instance Semantics.Modality.EventRelativity.instBEqIndTimePair {Individual✝ : Type u_1} {TimePoint✝ : Type u_2} [BEq Individual✝] [BEq TimePoint✝] :
                                                                BEq (IndTimePair Individual✝ TimePoint✝)
                                                                Equations
                                                                def Semantics.Modality.EventRelativity.instBEqIndTimePair.beq {Individual✝ : Type u_1} {TimePoint✝ : Type u_2} [BEq Individual✝] [BEq TimePoint✝] :
                                                                IndTimePair Individual✝ TimePoint✝IndTimePair Individual✝ TimePoint✝Bool
                                                                Equations
                                                                Instances For
                                                                  instance Semantics.Modality.EventRelativity.instReprIndTimePair {Individual✝ : Type u_1} {TimePoint✝ : Type u_2} [Repr Individual✝] [Repr TimePoint✝] :
                                                                  Repr (IndTimePair Individual✝ TimePoint✝)
                                                                  Equations
                                                                  def Semantics.Modality.EventRelativity.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.
                                                                  Instances For
                                                                    structure Semantics.Modality.EventRelativity.EventProjection (Ev : 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 : EvIndividual
                                                                    • time : EvTimePoint
                                                                    Instances For
                                                                      def Semantics.Modality.EventRelativity.EventProjection.toPair {Ev : Type u_1} {Individual : Type u_2} {TimePoint : Type u_3} (proj : EventProjection Ev Individual TimePoint) (e : Ev) :
                                                                      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
                                                                      Instances For
                                                                        def Semantics.Modality.EventRelativity.factoredAnchoring {Ev : Type u_1} {W : Type u_2} {Individual : Type u_3} {TimePoint : Type u_4} (proj : EventProjection Ev Individual TimePoint) (g : IndividualTimePointWList (BProp 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
                                                                        Instances For
                                                                          theorem Semantics.Modality.EventRelativity.factored_reduces {Ev : Type u_1} {W : Type u_2} {Individual : Type u_3} {TimePoint : Type u_4} (proj : EventProjection Ev Individual TimePoint) (g : IndividualTimePointWList (BProp W)) (e : Ev) (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.

                                                                          (201) "Jane a dû prendre le train." Jane must-PST-PFV take the train. a. Given MY evidence NOW, Jane must have taken the train. [epistemic] b. Given JANE'S circumstances THEN, Jane had to take the train. [root]

                                                                          The sentence is ambiguous between an epistemic and a goal-oriented reading. The two readings differ in the event that anchors the modal:

                                                                          ReadingEventholder(e)τ(e)Modal domain
                                                                          Epistemicspeech act e₀speakernowspeaker's evidence NOW
                                                                          RootVP event e₂JanethenJane's circumstances THEN

                                                                          The same modal devoir gets different parameters from different event bindings. No lexical ambiguity is needed.

                                                                          Two individuals in the train scenario.

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

                                                                              Two time points: speech time and the past event time.

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

                                                                                  Two events: the speech act and Jane's train-taking.

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

                                                                                      The event projection for the train scenario.

                                                                                      Speech act event: holder = speaker, τ = speech time (now). VP event (Jane's taking): holder = Jane, τ = past time (then).

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

                                                                                        The same modal (devoir) gets different individual-time pairs from different event bindings. This is (201): the epistemic reading relativizes to the speaker's evidence NOW; the root reading relativizes to Jane's circumstances THEN.

                                                                                        Two worlds: one where Jane took the train, one where she didn't.

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

                                                                                            Epistemic reading: modal anchored to speech event. The speaker's evidence is compatible with Jane taking the train. ◇_{f(e₀)} (took) holds because the speaker considers took possible.

                                                                                            Root reading: modal anchored to VP event. Given Jane's circumstances, she HAD to take the train. □_{f(e₂)} (took) holds because only took is accessible.

                                                                                            The root anchoring via VP event restricts the accessible worlds more than the epistemic anchoring via speech event. Both readings use the SAME modal; the different accessible worlds come entirely from the different event bindings → different (individual, time) projections → different conversational backgrounds.

                                                                                            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.

                                                                                            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.

                                                                                            (248c) "Jane thinks Mary might be pregnant."

                                                                                            Might is a high modal (above the embedded AspP) bound to the attitude event e₁ of think. Since thinking is contentful — CON(e₁) = Jane's beliefs — epistemic R is available. The modal domain is Jane's belief worlds, not the speaker's.

                                                                                            This contrasts with the matrix case (§12): in "Mary might be pregnant" (no embedding), might binds to the speech event e₀ and the modal domain is the speaker's evidence.

                                                                                            ContextBinding eventCON(e)Epistemic domain
                                                                                            Matrixe₀ (speech act)speaker's evidencewhat speaker considers possible
                                                                                            Embeddede₁ (attitude)Jane's beliefswhat Jane considers possible

                                                                                            The embedded case demonstrates that attitude events, like speech acts, are contentful (§8) — this is why attitudes_pattern_with_speech holds.

                                                                                            Two worlds for the pregnancy scenario.

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

                                                                                                Two events: the matrix speech act and Jane's embedded thinking.

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

                                                                                                    Embedded epistemic: might bound to Jane's thinking event. Jane's beliefs restrict to the pregnant-world only. Under Jane's beliefs, Mary's being pregnant is necessary (Jane is certain).

                                                                                                    Same modal (might), different event bindings, different epistemic domains. Under Jane's beliefs, only the pregnant-world is accessible. Under the speaker's evidence, both worlds are accessible.

                                                                                                    This demonstrates that attitude events are contentful (§8): the thinking event provides CON(e₁) = Jane's beliefs, licensing epistemic R for the embedded modal.