Event-relative modality

This file defines the binders of a modal's event variable and quantification over the content of an event, the two ingredients of Hacquard's event-relative semantics for modals. In that semantics a modal's domain is projected from an event rather than fixed by the context of utterance. The modal's event variable is bound by the closest binder above it: aspect binds a modal below AspP to the event the verb phrase describes, and a modal above AspP is bound to the speech event in a matrix clause and to the attitude event in the complement of an attitude verb. Speech and attitude events have propositional content, the set of worlds compatible with what is asserted or believed, and a modal anchored to such an event can quantify over that content. Content is a property of the event and not of its binder: most verb phrases describe events without content, but an aspect-bound modal over an attitude predicate is anchored to a contentful event and again has a reading over its content.

Main definitions

• Modality.EventBinder: the three events a modal's event variable can be bound to.
• Modality.ModalPosition: the position of a modal relative to aspect, with the binders ModalPosition.matrixBinder and ModalPosition.embeddedBinder that position determines.
• Modality.contentNecessity, Modality.contentPossibility: quantification over the content of the anchoring event, undefined (false) when the event has none.

Main statements

• Modality.contentNecessity_const, Modality.contentPossibility_const: over a proposition that does not vary with the world, the quantifier contributes only the consistency of the content. A modal anchored to the event that embeds it is therefore vacuous.

Implementation notes

The content of an event is a function con : E → Option (Set W), the worlds compatible with the event's content where it has one. Ordering sources play no role in content licensing and are left to Semantics/Modality/Necessity, whose operators apply to a base f e projected from an event as they do to any other.

References

• [Hac06]
• [Hac10]

inductive Modality.EventBinder : Type

The events a modal's event variable can be bound to.

• speechAct : EventBinder

  The speech event, bound at the edge of a matrix clause.

• attitude : EventBinder

  The event of an attitude verb, bound at the edge of its complement.

• vpEvent : EventBinder

  The event the verb phrase describes, 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 }

inductive Modality.ModalPosition : Type

The position of a modal relative to aspect.

• aboveAsp : ModalPosition
• belowAsp : ModalPosition

@[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.matrixBinder : ModalPosition → EventBinder

The closest binder above a modal in a matrix clause is aspect below AspP and the speech act above it.

Equations

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

def Modality.ModalPosition.embeddedBinder : ModalPosition → EventBinder

The closest binder above a modal in the complement of an attitude verb is aspect below AspP and the attitude verb above it.

Equations

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

@[simp]

theorem Modality.ModalPosition.embeddedBinder_belowAsp : belowAsp.embeddedBinder = belowAsp.matrixBinder

Aspect intervenes between a low modal and any higher binder, so embedding leaves its binder unchanged.

theorem Modality.ModalPosition.matrixBinder_eq_vpEvent {pos : ModalPosition} : pos.matrixBinder = EventBinder.vpEvent ↔ pos = belowAsp

theorem Modality.ModalPosition.embeddedBinder_eq_vpEvent {pos : ModalPosition} : pos.embeddedBinder = EventBinder.vpEvent ↔ pos = belowAsp

Quantification over the content of an event

def Modality.contentNecessity {E : Type u_1} {W : Type u_2} (con : E → Option (Set W)) (q : W → Prop) (e : E) : Prop

Necessity over the content of the anchoring event holds when the event has content and the proposition holds throughout it.

Equations

• Modality.contentNecessity con q e = ∃ (C : Set W), C ∈ con e ∧ ∀ (w : W), w ∈ C → q w

def Modality.contentPossibility {E : Type u_1} {W : Type u_2} (con : E → Option (Set W)) (q : W → Prop) (e : E) : Prop

Possibility over the content of the anchoring event holds when the event has content and the proposition holds somewhere in it.

Equations

• Modality.contentPossibility con q e = ∃ (C : Set W), C ∈ con e ∧ ∃ (w : W), w ∈ C ∧ q w

theorem Modality.contentNecessity_iff_of_eq_some {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {q : W → Prop} {e : E} {C : Set W} (h : con e = some C) : contentNecessity con q e ↔ ∀ (w : W), w ∈ C → q w

theorem Modality.contentPossibility_iff_of_eq_some {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {q : W → Prop} {e : E} {C : Set W} (h : con e = some C) : contentPossibility con q e ↔ ∃ (w : W), w ∈ C ∧ q w

theorem Modality.isSome_of_contentNecessity {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {q : W → Prop} {e : E} (h : contentNecessity con q e) : (con e).isSome = true

theorem Modality.isSome_of_contentPossibility {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {q : W → Prop} {e : E} (h : contentPossibility con q e) : (con e).isSome = true

theorem Modality.not_contentNecessity_of_eq_none {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {q : W → Prop} {e : E} (h : con e = none) : ¬contentNecessity con q e

An event without content licenses no necessity over content.

theorem Modality.not_contentPossibility_of_eq_none {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {q : W → Prop} {e : E} (h : con e = none) : ¬contentPossibility con q e

An event without content licenses no possibility over content.

theorem Modality.contentNecessity.mono {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {p q : W → Prop} {e : E} (hpq : ∀ (w : W), p w → q w) (h : contentNecessity con p e) : contentNecessity con q e

theorem Modality.contentPossibility.mono {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {p q : W → Prop} {e : E} (hpq : ∀ (w : W), p w → q w) (h : contentPossibility con p e) : contentPossibility con q e

theorem Modality.contentNecessity.contentPossibility {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {q : W → Prop} {e : E} {C : Set W} (hC : con e = some C) (hne : C.Nonempty) (h : contentNecessity con q e) : Modality.contentPossibility con q e

Necessity over a consistent content entails possibility.

theorem Modality.contentPossibility_iff_not_contentNecessity_not {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {q : W → Prop} {e : E} {C : Set W} (hC : con e = some C) : contentPossibility con q e ↔ ¬contentNecessity con (fun (w : W) => ¬q w) e

The two quantifiers are dual wherever the event has content.

theorem Modality.contentNecessity_const {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {r : Prop} {e : E} {C : Set W} (hC : con e = some C) : contentNecessity con (fun (x : W) => r) e ↔ C.Nonempty → r

Necessity of a proposition that does not vary with the world holds when the content is inconsistent or the proposition is true.

theorem Modality.contentPossibility_const {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {r : Prop} {e : E} {C : Set W} (hC : con e = some C) : contentPossibility con (fun (x : W) => r) e ↔ C.Nonempty ∧ r

Possibility of a proposition that does not vary with the world holds when the content is consistent and the proposition is true.

theorem Modality.contentNecessity_contentNecessity {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {q : W → Prop} {e : E} : contentNecessity con (fun (x : W) => contentNecessity con q e) e ↔ contentNecessity con q e

A necessity modal anchored to the event that embeds it is vacuous, since necessity over a content of necessity over the same content is that necessity.

theorem Modality.contentPossibility_contentNecessity {E : Type u_1} {W : Type u_2} {con : E → Option (Set W)} {q : W → Prop} {e : E} : contentPossibility con (fun (x : W) => contentNecessity con q e) e ↔ ∃ (C : Set W), C ∈ con e ∧ C.Nonempty ∧ ∀ (w : W), w ∈ C → q w

A possibility modal over a necessity anchored to the same event is that necessity over a consistent content.