Event Projection → Temporal Orientation

@cite{hacquard-2006} @cite{hacquard-2010} @cite{condoravdi-2002} @cite{kratzer-2012}Derives the temporal orientation of modals from event projection. High modals get the speech time (present perspective); low modals get the event time (past perspective).

The Pattern

Position	Event binder	holder(e)	τ(e)	Temporal orientation
High (above Asp)	speech act e₀	speaker	speech time (now)	Present
Low (below Asp)	VP event e₂	agent	event time (then)	Past/event-local

Hacquard's Derivation

Individual-time pairs are DERIVED from events via projection functions holder(e) and τ(e). Since high modals bind to the speech event and low modals bind to the VP event, their temporal parameters differ:

• "Jane a dû prendre le train" (@cite{hacquard-2006}, (201)):
  • Epistemic (high): τ(e₀) = now → "Given my evidence NOW,..."
  • Root (low): τ(e₂) = then → "Given Jane's circumstances THEN,..."

This connects EventProjection (EventRelativity §11) to the temporal modal evaluation framework in Temporal.lean.

inductive Phenomena.Modality.Studies.Hacquard2006.TemporalOrientation : Type

The temporal orientation of a modal: what time the modal's conversational background is evaluated at.

• present : TemporalOrientation

  Present: evaluated at the speech time

• past : TemporalOrientation

  past: evaluated at a past event time

instance Phenomena.Modality.Studies.Hacquard2006.instDecidableEqTemporalOrientation : DecidableEq TemporalOrientation

Equations

• Phenomena.Modality.Studies.Hacquard2006.instDecidableEqTemporalOrientation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Modality.Studies.Hacquard2006.instBEqTemporalOrientation : BEq TemporalOrientation

Equations

• Phenomena.Modality.Studies.Hacquard2006.instBEqTemporalOrientation = { beq := Phenomena.Modality.Studies.Hacquard2006.instBEqTemporalOrientation.beq }

def Phenomena.Modality.Studies.Hacquard2006.instBEqTemporalOrientation.beq : TemporalOrientation → TemporalOrientation → Bool

Equations

• Phenomena.Modality.Studies.Hacquard2006.instBEqTemporalOrientation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Modality.Studies.Hacquard2006.instReprTemporalOrientation.repr : TemporalOrientation → ℕ → Std.Format

Equations

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

instance Phenomena.Modality.Studies.Hacquard2006.instReprTemporalOrientation : Repr TemporalOrientation

Equations

• Phenomena.Modality.Studies.Hacquard2006.instReprTemporalOrientation = { reprPrec := Phenomena.Modality.Studies.Hacquard2006.instReprTemporalOrientation.repr }

inductive Phenomena.Modality.Studies.Hacquard2006.OTime : Type

A time type for the orientation examples.

• now : OTime

  Speech time (= utterance time)

• then_ : OTime

  Past event time

instance Phenomena.Modality.Studies.Hacquard2006.instDecidableEqOTime : DecidableEq OTime

Equations

• Phenomena.Modality.Studies.Hacquard2006.instDecidableEqOTime x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Modality.Studies.Hacquard2006.instBEqOTime : BEq OTime

Equations

• Phenomena.Modality.Studies.Hacquard2006.instBEqOTime = { beq := Phenomena.Modality.Studies.Hacquard2006.instBEqOTime.beq }

def Phenomena.Modality.Studies.Hacquard2006.instBEqOTime.beq : OTime → OTime → Bool

Equations

• Phenomena.Modality.Studies.Hacquard2006.instBEqOTime.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Modality.Studies.Hacquard2006.instReprOTime.repr : OTime → ℕ → Std.Format

Equations

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

instance Phenomena.Modality.Studies.Hacquard2006.instReprOTime : Repr OTime

Equations

• Phenomena.Modality.Studies.Hacquard2006.instReprOTime = { reprPrec := Phenomena.Modality.Studies.Hacquard2006.instReprOTime.repr }

inductive Phenomena.Modality.Studies.Hacquard2006.OrientationEvent : Type

Two events: speech act and VP event.

• speech : OrientationEvent

  The speech event (e₀)

• vpEvent : OrientationEvent

  The VP event (e₂)

instance Phenomena.Modality.Studies.Hacquard2006.instDecidableEqOrientationEvent : DecidableEq OrientationEvent

Equations

• Phenomena.Modality.Studies.Hacquard2006.instDecidableEqOrientationEvent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Modality.Studies.Hacquard2006.instBEqOrientationEvent.beq : OrientationEvent → OrientationEvent → Bool

Equations

• Phenomena.Modality.Studies.Hacquard2006.instBEqOrientationEvent.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Modality.Studies.Hacquard2006.instBEqOrientationEvent : BEq OrientationEvent

Equations

• Phenomena.Modality.Studies.Hacquard2006.instBEqOrientationEvent = { beq := Phenomena.Modality.Studies.Hacquard2006.instBEqOrientationEvent.beq }

instance Phenomena.Modality.Studies.Hacquard2006.instReprOrientationEvent : Repr OrientationEvent

Equations

• Phenomena.Modality.Studies.Hacquard2006.instReprOrientationEvent = { reprPrec := Phenomena.Modality.Studies.Hacquard2006.instReprOrientationEvent.repr }

def Phenomena.Modality.Studies.Hacquard2006.instReprOrientationEvent.repr : OrientationEvent → ℕ → Std.Format

Equations

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

inductive Phenomena.Modality.Studies.Hacquard2006.OrientationPerson : Type

Individuals: speaker and the described event's agent.

• speaker : OrientationPerson
• agent : OrientationPerson

instance Phenomena.Modality.Studies.Hacquard2006.instDecidableEqOrientationPerson : DecidableEq OrientationPerson

Equations

• Phenomena.Modality.Studies.Hacquard2006.instDecidableEqOrientationPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Modality.Studies.Hacquard2006.instBEqOrientationPerson : BEq OrientationPerson

Equations

• Phenomena.Modality.Studies.Hacquard2006.instBEqOrientationPerson = { beq := Phenomena.Modality.Studies.Hacquard2006.instBEqOrientationPerson.beq }

def Phenomena.Modality.Studies.Hacquard2006.instBEqOrientationPerson.beq : OrientationPerson → OrientationPerson → Bool

Equations

• Phenomena.Modality.Studies.Hacquard2006.instBEqOrientationPerson.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Modality.Studies.Hacquard2006.instReprOrientationPerson : Repr OrientationPerson

Equations

• Phenomena.Modality.Studies.Hacquard2006.instReprOrientationPerson = { reprPrec := Phenomena.Modality.Studies.Hacquard2006.instReprOrientationPerson.repr }

def Phenomena.Modality.Studies.Hacquard2006.instReprOrientationPerson.repr : OrientationPerson → ℕ → Std.Format

Equations

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

def Phenomena.Modality.Studies.Hacquard2006.orientationProjection : Semantics.Modality.EventRelativity.EventProjection OrientationEvent OrientationPerson OTime

Event projection for the temporal orientation scenario. Speech events project to (speaker, now); VP events project to (agent, then).

Equations

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

theorem Phenomena.Modality.Studies.Hacquard2006.speech_projects_to_now : orientationProjection.time OrientationEvent.speech = OTime.now

Speech event projects to speech time (now).

theorem Phenomena.Modality.Studies.Hacquard2006.vp_projects_to_then : orientationProjection.time OrientationEvent.vpEvent = OTime.then_

VP event projects to event time (then).

def Phenomena.Modality.Studies.Hacquard2006.positionToOrientation (pos : Semantics.Modality.EventRelativity.ModalPosition) : TemporalOrientation

Derive temporal orientation from modal position, via event binding.

High modals (above Asp) bind to the speech event → τ(e₀) = now → present. Low modals (below Asp) bind to the VP event → τ(e₂) = then → past.

Equations

• Phenomena.Modality.Studies.Hacquard2006.positionToOrientation Semantics.Modality.EventRelativity.ModalPosition.aboveAsp = Phenomena.Modality.Studies.Hacquard2006.TemporalOrientation.present
• Phenomena.Modality.Studies.Hacquard2006.positionToOrientation Semantics.Modality.EventRelativity.ModalPosition.belowAsp = Phenomena.Modality.Studies.Hacquard2006.TemporalOrientation.past

theorem Phenomena.Modality.Studies.Hacquard2006.high_present : positionToOrientation Semantics.Modality.EventRelativity.ModalPosition.aboveAsp = TemporalOrientation.present

High modals have present temporal orientation.

theorem Phenomena.Modality.Studies.Hacquard2006.low_past : positionToOrientation Semantics.Modality.EventRelativity.ModalPosition.belowAsp = TemporalOrientation.past

Low modals have past temporal orientation.

theorem Phenomena.Modality.Studies.Hacquard2006.position_determines_orientation : positionToOrientation Semantics.Modality.EventRelativity.ModalPosition.aboveAsp ≠ positionToOrientation Semantics.Modality.EventRelativity.ModalPosition.belowAsp

The same modal (devoir, pouvoir) has different temporal perspectives depending on its structural position — derived from event projection, not stipulated.

theorem Phenomena.Modality.Studies.Hacquard2006.event_projection_subsumes_temporal : orientationProjection.time OrientationEvent.speech = OTime.now ∧ orientationProjection.time OrientationEvent.vpEvent = OTime.then_ ∧ orientationProjection.time OrientationEvent.speech ≠ orientationProjection.time OrientationEvent.vpEvent

The temporal orientation derived from event projection connects to Temporal.lean's time-indexed conversational backgrounds.

When the modal binds to event e with τ(e) = t, the conversational background is evaluated at time t: f(w,t). The time IS the event's temporal trace. Event projection subsumes time-indexing: rather than stipulating which time to evaluate at, the time is projected from whichever event binds the modal.

(@cite{hacquard-2006}, (201)): two readings of the same sentence with different temporal perspectives, derived from event binding.

Epistemic (high): "Given MY evidence NOW, Jane must have taken the train." → modal bound to speech event → τ(e₀) = speech time = now → background evaluated at speech time

Root (low): "Given JANE'S circumstances THEN, Jane had to take the train." → modal bound to VP event → τ(e₂) = event time = then → background evaluated at event time

theorem Phenomena.Modality.Studies.Hacquard2006.jane_train_orientation : orientationProjection.time OrientationEvent.speech = OTime.now ∧ positionToOrientation Semantics.Modality.EventRelativity.ModalPosition.aboveAsp = TemporalOrientation.present ∧ orientationProjection.time OrientationEvent.vpEvent = OTime.then_ ∧ positionToOrientation Semantics.Modality.EventRelativity.ModalPosition.belowAsp = TemporalOrientation.past

The full derivation chain for "Jane a dû prendre le train": event binding → event projection → temporal orientation.

This is the payoff of event-relative modality: the same modal gets different temporal perspectives from different event bindings, without any stipulation about temporal orientation.

Bridge content (merged from ActualityInferencesBridge.lean)

Actuality Inference Data (Cross-Linguistic)

@cite{bhatt-1999} @cite{hacquard-2006} @cite{nadathur-2023}

Cross-linguistic empirical data on actuality inferences with ability modals, following the pattern of Phenomena/Causation/Data.lean.

Key Generalization (@cite{nadathur-2023}, Chapter 1)

Across languages, ability modals with perfective aspect entail the complement, while those with imperfective aspect do not.

Language	Modal	PFV entails?	IMPF entails?
Greek	boro	Yes	No
Hindi	saknaa	Yes	No
French	pouvoir	Yes	No
English	be able	Yes (episodic)	No (habitual)

structure Phenomena.Modality.ActualityInferencesBridge.ActualityDatum : Type

A single cross-linguistic data point for actuality inferences.

• language : String

  Language name

• modalForm : String

  The modal form in that language

• aspect : Semantics.Tense.Aspect.Core.ViewpointAspectB

  Viewpoint aspect of the sentence

• complementEntailed : Bool

  Does the complement entailment hold?

• gloss : String

  Example sentence gloss

def Phenomena.Modality.ActualityInferencesBridge.instReprActualityDatum.repr : ActualityDatum → ℕ → Std.Format

Equations

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

instance Phenomena.Modality.ActualityInferencesBridge.instReprActualityDatum : Repr ActualityDatum

Equations

• Phenomena.Modality.ActualityInferencesBridge.instReprActualityDatum = { reprPrec := Phenomena.Modality.ActualityInferencesBridge.instReprActualityDatum.repr }

instance Phenomena.Modality.ActualityInferencesBridge.instDecidableEqActualityDatum : DecidableEq ActualityDatum

Equations

• Phenomena.Modality.ActualityInferencesBridge.instDecidableEqActualityDatum = Phenomena.Modality.ActualityInferencesBridge.instDecidableEqActualityDatum.decEq

def Phenomena.Modality.ActualityInferencesBridge.instDecidableEqActualityDatum.decEq (x✝ x✝¹ : ActualityDatum) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Modality.ActualityInferencesBridge.instBEqActualityDatum : BEq ActualityDatum

Equations

• Phenomena.Modality.ActualityInferencesBridge.instBEqActualityDatum = { beq := Phenomena.Modality.ActualityInferencesBridge.instBEqActualityDatum.beq }

def Phenomena.Modality.ActualityInferencesBridge.instBEqActualityDatum.beq : ActualityDatum → ActualityDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Modality.ActualityInferencesBridge.instBEqActualityDatum.beq x✝¹ x✝ = false

def Phenomena.Modality.ActualityInferencesBridge.greek_pfv : ActualityDatum

Greek boro + perfective (aorist): "She was-able.PFV to swim across" → She swam across.

Equations

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

def Phenomena.Modality.ActualityInferencesBridge.greek_impf : ActualityDatum

Greek boro + imperfective: "She was-able.IMPF to swim across" ↛ She swam across.

Equations

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

def Phenomena.Modality.ActualityInferencesBridge.hindi_pfv : ActualityDatum

Hindi saknaa + perfective: "She was-able.PFV to swim across" → She swam across.

Equations

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

def Phenomena.Modality.ActualityInferencesBridge.hindi_impf : ActualityDatum

Hindi saknaa + imperfective: "She was-able.IMPF to swim across" ↛ She swam across.

Equations

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

def Phenomena.Modality.ActualityInferencesBridge.french_pfv : ActualityDatum

French pouvoir + passé composé (perfective): "She was-able.PFV to swim across" → She swam across.

Equations

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

def Phenomena.Modality.ActualityInferencesBridge.french_impf : ActualityDatum

French pouvoir + imparfait (imperfective): "She was-able.IMPF to swim across" ↛ She swam across.

Equations

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

def Phenomena.Modality.ActualityInferencesBridge.english_pfv : ActualityDatum

English be able + episodic (perfective-like): "She was able to swim across" → She swam across.

Equations

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

def Phenomena.Modality.ActualityInferencesBridge.english_impf : ActualityDatum

English be able + habitual (imperfective-like): "She was able to swim across" ↛ She swam across on that occasion.

Equations

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

def Phenomena.Modality.ActualityInferencesBridge.allData : List ActualityDatum

All actuality inference data points.

Equations

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

def Phenomena.Modality.ActualityInferencesBridge.perfData : List ActualityDatum

The perfective subset.

Equations

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

def Phenomena.Modality.ActualityInferencesBridge.impfData : List ActualityDatum

The imperfective subset.

Equations

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

theorem Phenomena.Modality.ActualityInferencesBridge.perfective_entails : (perfData.all fun (x : ActualityDatum) => x.complementEntailed) = true

All 4 perfective data points have complementEntailed = true.

theorem Phenomena.Modality.ActualityInferencesBridge.imperfective_no_entailment : (impfData.all fun (x : ActualityDatum) => x.complementEntailed == false) = true

All 4 imperfective data points have complementEntailed = false.

theorem Phenomena.Modality.ActualityInferencesBridge.empirical_matches_theory : (allData.all fun (d : ActualityDatum) => (d.aspect == Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective) == d.complementEntailed) = true

Central empirical generalization: across all 8 data points, complementEntailed tracks aspect ==.perfective exactly.

This is the empirical observation that @cite{nadathur-2023} explains via the causal sufficiency + aspect interaction.

theorem Phenomena.Modality.ActualityInferencesBridge.four_languages : (List.map (fun (x : ActualityDatum) => x.language) allData).dedup.length = 4

We have data from 4 distinct languages.

theorem Phenomena.Modality.ActualityInferencesBridge.balanced_design : perfData.length = 4 ∧ impfData.length = 4

Each language contributes exactly one perfective and one imperfective datum.

theorem Phenomena.Modality.ActualityInferencesBridge.data_matches_position_theory : (allData.all fun (d : ActualityDatum) => d.complementEntailed == Semantics.Modality.ActualityEntailments.actualityEntailmentPredicted Semantics.Modality.EventRelativity.ModalPosition.belowAsp d.aspect) = true

Every datum's complementEntailed field matches the position × aspect prediction for root modals. All data involves root/ability modals (below AspP), so the prediction is actualityEntailmentPredicted.belowAsp d.aspect.

This connects the theory-neutral empirical data (§§ above) to @cite{hacquard-2006}'s structural explanation: root modals are below Asp, so perfective forces actualization.

theorem Phenomena.Modality.ActualityInferencesBridge.greek_matches_theory : greek_pfv.complementEntailed = Semantics.Modality.ActualityEntailments.actualityEntailmentPredicted Semantics.Modality.EventRelativity.ModalPosition.belowAsp Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective ∧ greek_impf.complementEntailed = Semantics.Modality.ActualityEntailments.actualityEntailmentPredicted Semantics.Modality.EventRelativity.ModalPosition.belowAsp Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective

Per-language bridge: Greek data matches position theory.

theorem Phenomena.Modality.ActualityInferencesBridge.hindi_matches_theory : hindi_pfv.complementEntailed = Semantics.Modality.ActualityEntailments.actualityEntailmentPredicted Semantics.Modality.EventRelativity.ModalPosition.belowAsp Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective ∧ hindi_impf.complementEntailed = Semantics.Modality.ActualityEntailments.actualityEntailmentPredicted Semantics.Modality.EventRelativity.ModalPosition.belowAsp Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective

Per-language bridge: Hindi data matches position theory.

theorem Phenomena.Modality.ActualityInferencesBridge.french_matches_theory : french_pfv.complementEntailed = Semantics.Modality.ActualityEntailments.actualityEntailmentPredicted Semantics.Modality.EventRelativity.ModalPosition.belowAsp Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective ∧ french_impf.complementEntailed = Semantics.Modality.ActualityEntailments.actualityEntailmentPredicted Semantics.Modality.EventRelativity.ModalPosition.belowAsp Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective

Per-language bridge: French data matches position theory.

theorem Phenomena.Modality.ActualityInferencesBridge.english_matches_theory : english_pfv.complementEntailed = Semantics.Modality.ActualityEntailments.actualityEntailmentPredicted Semantics.Modality.EventRelativity.ModalPosition.belowAsp Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective ∧ english_impf.complementEntailed = Semantics.Modality.ActualityEntailments.actualityEntailmentPredicted Semantics.Modality.EventRelativity.ModalPosition.belowAsp Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective

Per-language bridge: English data matches position theory.