Hacquard 2006: Aspects of Modality

[Hac06]: modals are relative to an event of evaluation, and the event fixes both the individual and the time the accessibility relation is keyed to — its holder and temporal trace. A high modal (above Asp) is bound by the speech event in matrix clauses and by the attitude event under attitude verbs; a low modal (below Asp) is bound by aspect to the VP event, whose time is the one provided by tense. Root modals under perfective yield actuality entailments ([Bha99]'s discovery, extended to French and Italian); epistemics, being above aspect, are immune.

Substrate note: the event-relative machinery (EventBinder, ModalPosition, EventProjection, content licensing) lives in Semantics/Modality/EventRelativity.lean, anchored to the journal version [Hac10]; this file uses those project-canonical types.

Main results

• positionPerspective, withAttitude_shifts_perspective — the temporal perspective ([Con02]) projected from the anchoring event, via ModalPosition.defaultBinder / withAttitude.
• epistemic_reading_possible, goal_reading_necessary — the two readings of "Jane a dû prendre le train" (201) from one modal entry.
• aspect_bound_epistemic_necessity — contentful complements license aspect-bound epistemics (246)–(248).
• data_matches_position_theory — the perfective/imperfective actuality split across Data/Examples/Hacquard2006.json rows matches the position × aspect prediction.

Position → temporal perspective

The anchoring event fixes the evaluation time: speech-bound modals sit at the utterance time, aspect-bound ones at the time provided by tense. The map factors through the substrate's binding maps, and its codomain has no future case. It agrees with [Con02]'s ModalReading.perspective classification — the "might (already/still) have won" ambiguity (176) recast positionally; the settledness consequences are proved in Studies/Condoravdi2002.lean (modal_over_perf_blocks_metaphysical, counterfactual_widens_domain).

def Hacquard2006.binderPerspective : Modality.EventBinder → Modality.TemporalPerspective

Perspective of the anchoring event in a past-tense clause: only the speech event sits at utterance time.

Equations

• Hacquard2006.binderPerspective Modality.EventBinder.speechAct = Modality.TemporalPerspective.present
• Hacquard2006.binderPerspective x✝ = Modality.TemporalPerspective.past

def Hacquard2006.positionPerspective (pos : Modality.ModalPosition) : Modality.TemporalPerspective

Perspective from modal position in a matrix clause.

Equations

• Hacquard2006.positionPerspective pos = Hacquard2006.binderPerspective pos.defaultBinder

theorem Hacquard2006.position_determines_perspective : positionPerspective Modality.ModalPosition.aboveAsp ≠ positionPerspective Modality.ModalPosition.belowAsp

The same modal (devoir, pouvoir) gets different temporal perspectives from different structural positions.

theorem Hacquard2006.withAttitude_shifts_perspective : binderPerspective Modality.ModalPosition.aboveAsp.withAttitude ≠ binderPerspective Modality.ModalPosition.aboveAsp.defaultBinder

Embedded under a past attitude, a high modal is keyed to the attitude time: the perspective tracks the binder, not the position.

Worked example: "Jane a dû prendre le train" (201)

Examples.ex201's two readings differ only in the anchoring event:

Reading	Event	holder(e)	τ(e)	Modal domain
Epistemic	speech act	speaker	now	speaker's evidence now
Goal-oriented	VP event	Jane	then	Jane's circumstances then

inductive Hacquard2006.TrainPerson : Type

Two individuals in the train scenario.

• speaker : TrainPerson
• jane : TrainPerson

@[instance_reducible]

instance Hacquard2006.instDecidableEqTrainPerson : DecidableEq TrainPerson

Equations

• Hacquard2006.instDecidableEqTrainPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hacquard2006.instReprTrainPerson.repr : TrainPerson → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Hacquard2006.instReprTrainPerson : Repr TrainPerson

Equations

• Hacquard2006.instReprTrainPerson = { reprPrec := Hacquard2006.instReprTrainPerson.repr }

inductive Hacquard2006.TrainTime : Type

Speech time and the past event time.

• now : TrainTime
• then : TrainTime

@[instance_reducible]

instance Hacquard2006.instDecidableEqTrainTime : DecidableEq TrainTime

Equations

• Hacquard2006.instDecidableEqTrainTime x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hacquard2006.instReprTrainTime.repr : TrainTime → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Hacquard2006.instReprTrainTime : Repr TrainTime

Equations

• Hacquard2006.instReprTrainTime = { reprPrec := Hacquard2006.instReprTrainTime.repr }

inductive Hacquard2006.TrainEvent : Type

The speech act and Jane's train-taking.

• speechAct : TrainEvent
• janesTaking : TrainEvent

@[instance_reducible]

instance Hacquard2006.instDecidableEqTrainEvent : DecidableEq TrainEvent

Equations

• Hacquard2006.instDecidableEqTrainEvent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hacquard2006.instReprTrainEvent : Repr TrainEvent

Equations

• Hacquard2006.instReprTrainEvent = { reprPrec := Hacquard2006.instReprTrainEvent.repr }

def Hacquard2006.instReprTrainEvent.repr : TrainEvent → ℕ → Std.Format

Equations

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

def Hacquard2006.trainProjection : Modality.EventProjection TrainEvent TrainPerson TrainTime

The event projection for the train scenario: the speech act projects to (speaker, now), the VP event to (Jane, then).

Equations

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

inductive Hacquard2006.TrainWorld : Type

One world where Jane took the train, one where she didn't.

• took : TrainWorld
• didnt : TrainWorld

@[instance_reducible]

instance Hacquard2006.instDecidableEqTrainWorld : DecidableEq TrainWorld

Equations

• Hacquard2006.instDecidableEqTrainWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hacquard2006.instReprTrainWorld : Repr TrainWorld

Equations

• Hacquard2006.instReprTrainWorld = { reprPrec := Hacquard2006.instReprTrainWorld.repr }

def Hacquard2006.instReprTrainWorld.repr : TrainWorld → ℕ → Std.Format

Equations

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

theorem Hacquard2006.epistemic_reading_possible : Modality.Kratzer.simplePossibility (Hacquard2006.trainAnchoring✝ TrainEvent.speechAct) (fun (x : TrainWorld) => x = TrainWorld.took) TrainWorld.took

took is possible when the modal is anchored to the speech event — the epistemic reading.

theorem Hacquard2006.goal_reading_necessary : Modality.Kratzer.simpleNecessity (Hacquard2006.trainAnchoring✝ TrainEvent.janesTaking) (fun (x : TrainWorld) => x = TrainWorld.took) TrainWorld.took

took is necessary when the modal is anchored to the VP event — the goal-oriented reading.

theorem Hacquard2006.same_modal_different_domains : Modality.Kratzer.kratzerR (Hacquard2006.trainAnchoring✝ TrainEvent.speechAct) TrainWorld.took TrainWorld.didnt ∧ ¬Modality.Kratzer.kratzerR (Hacquard2006.trainAnchoring✝ TrainEvent.janesTaking) TrainWorld.took TrainWorld.didnt

The didnt-world is accessible from the speech event but not from the VP event.

Aspect-bound epistemics (246)–(248)

Low modals lack epistemic readings because aspect's event has no content (the substrate's position_determines_epistemic) — unless the complement supplies a contentful attitude event: Examples.ex247b's aspect-bound LF reports Jane's past belief state, its speech-bound LF the speaker's evidence.

inductive Hacquard2006.DarcyWorld : Type

Two worlds for the (247b) scenario.

• loves : DarcyWorld
• lovesNot : DarcyWorld

@[instance_reducible]

instance Hacquard2006.instDecidableEqDarcyWorld : DecidableEq DarcyWorld

Equations

• Hacquard2006.instDecidableEqDarcyWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hacquard2006.instReprDarcyWorld.repr : DarcyWorld → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Hacquard2006.instReprDarcyWorld : Repr DarcyWorld

Equations

• Hacquard2006.instReprDarcyWorld = { reprPrec := Hacquard2006.instReprDarcyWorld.repr }

inductive Hacquard2006.PenserEvent : Type

Two candidate binders for the modal in (247b): the matrix speech act and Jane's thinking event.

• speech : PenserEvent
• thinking : PenserEvent

@[instance_reducible]

instance Hacquard2006.instDecidableEqPenserEvent : DecidableEq PenserEvent

Equations

• Hacquard2006.instDecidableEqPenserEvent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hacquard2006.instReprPenserEvent.repr : PenserEvent → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Hacquard2006.instReprPenserEvent : Repr PenserEvent

Equations

• Hacquard2006.instReprPenserEvent = { reprPrec := Hacquard2006.instReprPenserEvent.repr }

theorem Hacquard2006.aspect_bound_epistemic_necessity : Modality.Kratzer.simpleNecessity (Hacquard2006.fPenser✝ PenserEvent.thinking) (fun (x : DarcyWorld) => x = DarcyWorld.loves) DarcyWorld.lovesNot

Bound to Jane's thinking event, loves is necessary — an epistemic necessity for Jane.

theorem Hacquard2006.speech_bound_both_possible : Modality.Kratzer.simplePossibility (Hacquard2006.fPenser✝ PenserEvent.speech) (fun (x : DarcyWorld) => x = DarcyWorld.loves) DarcyWorld.lovesNot ∧ Modality.Kratzer.simplePossibility (Hacquard2006.fPenser✝ PenserEvent.speech) (fun (x : DarcyWorld) => x = DarcyWorld.lovesNot) DarcyWorld.lovesNot

Bound to the speech event, both worlds remain possible for the speaker.

theorem Hacquard2006.binding_determines_epistemic_domain : Modality.Kratzer.kratzerR (Hacquard2006.fPenser✝ PenserEvent.speech) DarcyWorld.lovesNot DarcyWorld.lovesNot ∧ ¬Modality.Kratzer.kratzerR (Hacquard2006.fPenser✝ PenserEvent.thinking) DarcyWorld.lovesNot DarcyWorld.lovesNot

The lovesNot-world is accessible from the speech event but not from Jane's thinking event.

Actuality entailments

Root modals entail their complement under perfective aspect but not imperfective ([Bha99]; French/Italian extensions in [Hac06]). No Hindi or Greek rows: the dissertation reproduces neither (fn. 7) and defers Greek's complement-internal aspect (318).

def Hacquard2006.aeDatum (e : Data.Examples.LinguisticExample) : Option (Semantics.Aspect.Perfectivity × Bool)

Aspect and observed actuality entailment of an example row, read off its paperFeatures; none for rows without the aspect contrast.

Equations

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

theorem Hacquard2006.ex22a_perfective_entails : aeDatum Examples.ex22a = some (Semantics.Aspect.Perfectivity.perfective, true)

Positive witness: the perfective French pair member carries the entailment.

theorem Hacquard2006.data_matches_position_theory : ((List.filterMap aeDatum Examples.all).all fun (d : Semantics.Aspect.Perfectivity × Bool) => d.2 == Modality.actualityEntailmentPredicted Modality.ModalPosition.belowAsp d.1) = true

Every datum's observed entailment matches the position × aspect prediction for root modals (all rows are root: below Asp, so perfective forces actualization).