Hacquard (2010): On the Event Relativity of Modal Auxiliaries

This file formalizes [Hac10]'s event-relative semantics for modal auxiliaries. A modal's modal base is a function of an event rather than a world (29), must and can, and its event variable is bound by the closest binder (37), (38): the speech event for a high modal in a matrix clause, the attitude event for a high modal in a complement, and the VP event for a low modal (48), the binders of Modality.ModalPosition. Speech and attitude events carry propositional content and embed a proposition under universal quantification over it (41), (44), attitude; the epistemic modal base is the content of the event the modal is anchored to (51), Modality.contentNecessity and Modality.contentPossibility, so it is undefined where a low modal is anchored to a contentless VP event (49e), (59), Modality.not_contentPossibility_of_eq_none, and defined again when the complement is itself an attitude (60). Anchored to the event that embeds it, an epistemic modal quantifies over the same worlds as that event, so the outer layer of quantification is vacuous, (53) to (57), attitude_can_iff and attitude_must_iff, the possibility case once the information state is consistent; and Yalcin's supposition (58) is incoherent because the modal quantifies over the supposition's own content, not_attitude_suppose. Cinque's puzzle (section 3) is that [Cin99]'s hierarchy fixes the epistemic head above tense and the root head below aspect, CinqueHead, where a single flavor-neutral entry should suffice; the paper derives the same matrix correlation from the content of the binding event, epistemic_high_iff. The paper's examples are the rows of Data.Examples.Hacquard2010.

Implementation notes

The content of an event is its set of compatible worlds, ⋂CON(e), an Option undefined for contentless events; the descriptive part of an attitude or asserting event, Exp(e, x) and belief'(e, w) or Assert'(e₀, w), is an abstract predicate. Ordering sources are omitted, as in the paper's derivations, and the circumstantial modal base (61), whose event dependence the paper leaves open, is not defined. The individual and time a modal is keyed to (section 4) enter only through the binding event; the Italian restructuring evidence belongs to [Hac06].

References

• [Hac10]
• [Cin99]
• [Yal07]

Event-relative modals, section 5

def Hacquard2010.must {E : Type u_1} {W : Type u_2} (f : E → Set W) (q : W → Prop) (e : E) : Prop

A necessity modal (29) quantifies over the worlds its event-relative modal base returns.

Equations

• Hacquard2010.must f q e = ∀ w' ∈ f e, q w'

def Hacquard2010.can {E : Type u_1} {W : Type u_2} (f : E → Set W) (q : W → Prop) (e : E) : Prop

A possibility modal (29) quantifies existentially over the same worlds.

Equations

• Hacquard2010.can f q e = ∃ w' ∈ f e, q w'

def Hacquard2010.attitude {E : Type u_1} {W : Type u_2} (con : E → Option (Set W)) (holds : E → W → Prop) (e : E) (p : W → Prop) (w : W) : Prop

A contentful event, an attitude or the speech event, embeds a proposition under universal quantification over its content (41), (44); holds e w is the event's descriptive part.

Equations

• Hacquard2010.attitude con holds e p w = (holds e w ∧ Modality.contentNecessity con p e)

theorem Hacquard2010.must_iff_contentNecessity {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {f : E → Set W} {e : E} {q : W → Prop} (h : con e = some (f e)) : must f q e ↔ Modality.contentNecessity con q e

The epistemic modal base is the content of the event the modal is anchored to (51).

theorem Hacquard2010.can_iff_contentPossibility {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {f : E → Set W} {e : E} {q : W → Prop} (h : con e = some (f e)) : can f q e ↔ Modality.contentPossibility con q e

Content licensing, section 6.1

theorem Hacquard2010.attitude_can_iff {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {holds : E → W → Prop} {e : E} {q : W → Prop} {w : W} {C : Set W} (hC : con e = some C) : attitude con holds e (fun (x : W) => Modality.contentPossibility con q e) w ↔ holds e w ∧ (C.Nonempty → ∃ w' ∈ C, q w')

A possibility modal anchored to the event that embeds it quantifies over the same worlds as that event (53), (57), so the outer universal layer is vacuous whenever the content is consistent.

theorem Hacquard2010.attitude_can_iff_of_nonempty {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {holds : E → W → Prop} {e : E} {q : W → Prop} {w : W} {C : Set W} (hC : con e = some C) (hne : C.Nonempty) : attitude con holds e (fun (x : W) => Modality.contentPossibility con q e) w ↔ holds e w ∧ ∃ w' ∈ C, q w'

With a consistent content, an embedded epistemic possibility says that q is compatible with the content of the embedding event, the speaker's beliefs under ASSERT or the attitude holder's under believe (54).

theorem Hacquard2010.attitude_must_iff {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {holds : E → W → Prop} {e : E} {q : W → Prop} {w : W} : attitude con holds e (fun (x : W) => Modality.contentNecessity con q e) w ↔ holds e w ∧ Modality.contentNecessity con q e

An embedded epistemic necessity is necessity over the embedding event's content, the outer layer again vacuous (55), (57).

theorem Hacquard2010.not_attitude_suppose {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {holds : E → W → Prop} {e : E} {w : W} {C : Set W} {rain : W → Prop} (hC : con e = some C) (hne : C.Nonempty) : ¬attitude con holds e (fun (w' : W) => rain w' ∧ Modality.contentPossibility con (fun (w'' : W) => ¬rain w'') e) w

(58), [Yal07]'s puzzle: supposing that it is raining and that it might not be raining is incoherent, since the epistemic quantifies over the supposition's own content and no consistent content satisfies both.

Cinque's puzzle, section 3

inductive Hacquard2010.CinqueHead : Type

[Cin99]'s hierarchy at the granularity the paper uses: an epistemic head above tense, a root head below aspect.

• modEpistemic : CinqueHead
• tense : CinqueHead
• aspect : CinqueHead
• modRoot : CinqueHead

@[instance_reducible]

instance Hacquard2010.instDecidableEqCinqueHead : DecidableEq CinqueHead

Equations

• Hacquard2010.instDecidableEqCinqueHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hacquard2010.CinqueHead.height : CinqueHead → ℕ

Height in the hierarchy, the topmost head highest.

Equations

• Hacquard2010.CinqueHead.modEpistemic.height = 3
• Hacquard2010.CinqueHead.tense.height = 2
• Hacquard2010.CinqueHead.aspect.height = 1
• Hacquard2010.CinqueHead.modRoot.height = 0

def Hacquard2010.CinqueHead.Above (h h' : CinqueHead) : Prop

h sits above h' in the hierarchy.

Equations

• h.Above h' = (h'.height < h.height)

@[instance_reducible]

instance Hacquard2010.CinqueHead.instDecidableRelAbove : DecidableRel Above

Equations

• h.instDecidableRelAbove h' = { decide := h'.height.succ.ble h.height, reflects_decide := ⋯ }

def Hacquard2010.CinqueHead.IsHigh (h : CinqueHead) : Prop

A high head sits above tense.

Equations

• h.IsHigh = h.Above Hacquard2010.CinqueHead.tense

@[instance_reducible]

instance Hacquard2010.CinqueHead.instDecidablePredIsHigh : DecidablePred IsHigh

Equations

• h.instDecidablePredIsHigh = { decide := Hacquard2010.CinqueHead.tense.height.succ.ble h.height, reflects_decide := ⋯ }

def Hacquard2010.CinqueHead.flavor : CinqueHead → Option Modality.ModalFlavor

The flavor the hierarchy stipulates for each modal head.

Equations

• Hacquard2010.CinqueHead.modEpistemic.flavor = some Modality.ModalFlavor.epistemic
• Hacquard2010.CinqueHead.modRoot.flavor = some Modality.ModalFlavor.circumstantial
• x✝.flavor = none

theorem Hacquard2010.CinqueHead.isHigh_iff (h : CinqueHead) : h.IsHigh ↔ h.flavor = some Modality.ModalFlavor.epistemic

In the hierarchy the correlation of height and flavor is built in, since the high modal head is the epistemic one and the root head is below aspect.

theorem Hacquard2010.CinqueHead.aspect_above_modRoot : aspect.Above modRoot

theorem Hacquard2010.epistemic_high_iff {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {ev : Modality.EventBinder → E} (hs : (con (ev Modality.EventBinder.speechAct)).isSome = true) (hv : con (ev Modality.EventBinder.vpEvent) = none) (pos : Modality.ModalPosition) : (con (ev pos.matrixBinder)).isSome = true ↔ pos = Modality.ModalPosition.aboveAsp

The same matrix correlation follows from one flavor-neutral entry (section 6.3). A modal above tense is bound by the speech event, which has content, and a modal below aspect by the VP event, which in (59) has none, so an epistemic modal base is available exactly in the high position.