@cite{condoravdi-2002}: Temporal Interpretation of Modals

Condoravdi, C. (2002). Temporal Interpretation of Modals: Modals for the Present and for the Past. In D. Beaver, S. Kaufmann, B. Clark, & L. Casillas (Eds.), The Construction of Meaning. CSLI Publications.

Core claims

1. Uniform modal semantics: modals for the present and modals for the past share a single meaning. No implicit tense under the modal.
2. Decompositional analysis: "might have" parses as MAY(PERF(φ)), not as a single lexical item MIGHT-HAVE.
3. Temporal expansion: modals expand evaluation to a forward interval rather than shifting it. Forward orientation follows from this for eventive predicates; present-or-future for stative predicates.
4. Scope–modality correlation: MODAL > PERF yields the epistemic reading; PERF > MODAL yields the counterfactual (metaphysical) reading. This follows from the diversity condition: metaphysical modal bases require non-settledness, which the past cannot provide.

Architecture

• The AT and atForward primitives live in Theories/Semantics/Tense/AT.lean.
• Branching-time, settledness, and diversity live in Core/Modality/HistoricalAlternatives.lean.
• This file composes them into Condoravdi's specific operators and derives the paper's predictions.

Operators

def Condoravdi2002.pres {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (sort : Features.Dynamicity) (P : Semantics.Events.EventPred W Time) (t : Time) (w : W) : Prop

Present tense: instantiates a property at the utterance time. The temporal anchor is a single point.

Equations

• Condoravdi2002.pres sort P t w = Semantics.Tense.Modal.AtOperator.at' sort P w (Core.Time.Interval.point t)

def Condoravdi2002.perf {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (sort : Features.Dynamicity) (P : Semantics.Events.EventPred W Time) (w : W) (t : Time) : Prop

Perfect: shifts evaluation to a prior time. There is some t' < t at which the property holds.

Equations

• Condoravdi2002.perf sort P w t = ∃ t' < t, Semantics.Tense.Modal.AtOperator.at' sort P w (Core.Time.Interval.point t')

Modal cores vs. prospective modals

The temporal evaluator is factored out: mayCore/wollCore quantify over the modal base and check the prejacent at the perspective point, while may/woll apply forward temporal expansion. Condoravdi's English might/would use the prospective versions (futurity is lexicalized in the modal). Languages whose modals are not inherently future-oriented — @cite{matthewson-2013} argues Gitksan ima('a) is one — should be modeled with mayCore/wollCore, with prospective aspect supplied by a separate operator (Gitksan dim).

This is the structural expression of @cite{matthewson-2013}'s central anti-Condoravdi claim: the prospective component is a separable combinator, not part of the modal lexical entry.

def Condoravdi2002.mayCore {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (MB : W → Time → Set W) (sort : Features.Dynamicity) (P : Semantics.Events.EventPred W Time) (w : W) (t : Time) : Prop

Modal possibility core: ∃ w' ∈ MB(w,t), the prejacent holds at the point t in w'. No forward expansion.

Equations

• Condoravdi2002.mayCore MB sort P w t = ∃ w' ∈ MB w t, Semantics.Tense.Modal.AtOperator.at' sort P w' (Core.Time.Interval.point t)

def Condoravdi2002.may {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (MB : W → Time → Set W) (sort : Features.Dynamicity) (P : Semantics.Events.EventPred W Time) (w : W) (t : Time) : Prop

MAY/MIGHT: existential quantification over the modal base, with forward temporal expansion. The English modal lexicalizes the prospective choice (@cite{condoravdi-2002}).

Equations

• Condoravdi2002.may MB sort P w t = ∃ w' ∈ MB w t, Semantics.Tense.Modal.AtOperator.atForward sort P w' t

def Condoravdi2002.wollCore {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (MB : W → Time → Set W) (sort : Features.Dynamicity) (P : Semantics.Events.EventPred W Time) (w : W) (t : Time) : Prop

Modal necessity core: ∀ w' ∈ MB(w,t), the prejacent holds at the point t in w'. No forward expansion.

Equations

• Condoravdi2002.wollCore MB sort P w t = ∀ w' ∈ MB w t, Semantics.Tense.Modal.AtOperator.at' sort P w' (Core.Time.Interval.point t)

def Condoravdi2002.woll {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (MB : W → Time → Set W) (sort : Features.Dynamicity) (P : Semantics.Events.EventPred W Time) (w : W) (t : Time) : Prop

WOLL: universal quantification over the modal base, with forward temporal expansion. The untensed modal underlying will / would; contrasts with @cite{cariani-santorio-2018}'s atemporal-propositional willSem.

Equations

• Condoravdi2002.woll MB sort P w t = ∀ w' ∈ MB w t, Semantics.Tense.Modal.AtOperator.atForward sort P w' t

theorem Condoravdi2002.may_of_mayCore_dynamic {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (MB : W → Time → Set W) (P : Semantics.Events.EventPred W Time) (w : W) (t : Time) (h : mayCore MB Features.Dynamicity.dynamic P w t) : may MB Features.Dynamicity.dynamic P w t

For dynamic predicates, mayCore implies may: forward expansion is a weakening when the prejacent is checked at a point. The pointwise instantiation gives an event whose start lies at or after t, which is exactly what atEventForward requires.

theorem Condoravdi2002.may_of_mayCore_stative {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (MB : W → Time → Set W) (P : Semantics.Events.EventPred W Time) (w : W) (t : Time) (h : mayCore MB Features.Dynamicity.stative P w t) : may MB Features.Dynamicity.stative P w t

For stative predicates, mayCore implies may: pointwise state overlap entails forward state persistence at the point.

Composed scope readings

The two scope orderings of MAY and PERF that derive epistemic vs. counterfactual modality. The trivial single-operator examples ("He might run", "He might be here") are inlined as docstrings on may rather than given separate names.

def Condoravdi2002.mayEpistemic {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (MB : W → Time → Set W) (P : Semantics.Events.EventPred W Time) (t : Time) (w : W) : Prop

"He may have won" — epistemic reading. The modal scopes over the perfect (PRES > MAY > PERF). Modal base evaluated at t; the perfect back-shifts inside the modal's scope.

Equations

• Condoravdi2002.mayEpistemic MB P t w = ∃ w' ∈ MB w t, Condoravdi2002.perf Features.Dynamicity.dynamic P w' t

def Condoravdi2002.mightCounterfactual {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (MB : W → Time → Set W) (P : Semantics.Events.EventPred W Time) (t : Time) (w : W) : Prop

"He might have won" — counterfactual reading. The perfect scopes over the modal (PRES > PERF > MAY). The perfect shifts the modal base's evaluation point to a past t'; the modal then quantifies over worlds compatible with the past, with the property in [t', _).

Equations

• Condoravdi2002.mightCounterfactual MB P t w = ∃ t' < t, Condoravdi2002.may MB Features.Dynamicity.dynamic P w t'

Reading classification

inductive Condoravdi2002.Perspective : Type

Temporal perspective: the time at which the modal base is evaluated.

• present : Perspective

  Modal base evaluated at the utterance time.

• past : Perspective

  Modal base evaluated at a prior time (via PERF > MODAL).

@[implicit_reducible]

instance Condoravdi2002.instDecidableEqPerspective : DecidableEq Perspective

Equations

• Condoravdi2002.instDecidableEqPerspective x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Condoravdi2002.instReprPerspective : Repr Perspective

Equations

• Condoravdi2002.instReprPerspective = { reprPrec := Condoravdi2002.instReprPerspective.repr }

def Condoravdi2002.instReprPerspective.repr : Perspective → ℕ → Std.Format

Equations

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

inductive Condoravdi2002.Orientation : Type

Temporal orientation: the direction of temporal reference for the property in the modal's scope.

• future : Orientation

  Property instantiated at or after the perspective time.

• past : Orientation

  Property instantiated before the perspective time.

@[implicit_reducible]

instance Condoravdi2002.instDecidableEqOrientation : DecidableEq Orientation

Equations

• Condoravdi2002.instDecidableEqOrientation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Condoravdi2002.instReprOrientation : Repr Orientation

Equations

• Condoravdi2002.instReprOrientation = { reprPrec := Condoravdi2002.instReprOrientation.repr }

def Condoravdi2002.instReprOrientation.repr : Orientation → ℕ → Std.Format

Equations

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

inductive Condoravdi2002.ModalReading : Type

The three attested readings of an English modal-perfect string. The fourth combination (past perspective + past orientation) is unattested and excluded by construction.

• present : ModalReading

  "He might win." Future-oriented from a present perspective.

• epistemic : ModalReading

  "He may have already won." Past-oriented from a present perspective (PRES > MAY > PERF).

• counterfactual : ModalReading

  "He might still have won." Future-oriented from a past perspective (PRES > PERF > MAY).

@[implicit_reducible]

instance Condoravdi2002.instDecidableEqModalReading : DecidableEq ModalReading

Equations

• Condoravdi2002.instDecidableEqModalReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Condoravdi2002.instReprModalReading.repr : ModalReading → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Condoravdi2002.instReprModalReading : Repr ModalReading

Equations

• Condoravdi2002.instReprModalReading = { reprPrec := Condoravdi2002.instReprModalReading.repr }

def Condoravdi2002.ModalReading.perspective : ModalReading → Perspective

Modal-base evaluation time of a reading.

Equations

• Condoravdi2002.ModalReading.present.perspective = Condoravdi2002.Perspective.present
• Condoravdi2002.ModalReading.epistemic.perspective = Condoravdi2002.Perspective.present
• Condoravdi2002.ModalReading.counterfactual.perspective = Condoravdi2002.Perspective.past

def Condoravdi2002.ModalReading.orientation : ModalReading → Orientation

Direction of temporal reference of a reading.

Equations

• Condoravdi2002.ModalReading.present.orientation = Condoravdi2002.Orientation.future
• Condoravdi2002.ModalReading.counterfactual.orientation = Condoravdi2002.Orientation.future
• Condoravdi2002.ModalReading.epistemic.orientation = Condoravdi2002.Orientation.past

Bridge to Klein's PERF

theorem Condoravdi2002.perf_eventive_implies_perfSimple {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Semantics.Events.EventPred W Time) (w : W) (t : Time) (h : perf Features.Dynamicity.dynamic P w t) : Semantics.Aspect.Core.perfSimple P { world := w, time := t }

Condoravdi's eventive perf entails Klein's perfSimple: a prior point of instantiation gives a degenerate PTS [t', t'] right-bounded at t.

Scope–modality correlation

The relative scope of MODAL and PERF correlates with the kind of modality expressed:

• MODAL > PERF (epistemic): the modal's perspective is present; the property under it is back-shifted past. Past properties are settled, so the diversity condition blocks a metaphysical base — only epistemic modality remains available.
• PERF > MODAL (counterfactual): the modal's perspective is a past time; the property is in that past's future. Future properties are not settled, so a metaphysical base is available.

theorem Condoravdi2002.modal_over_perf_blocks_metaphysical {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (MB : W → Time → Set W) (cg : Set W) (now : Time) (P : Semantics.Events.EventPred W Time) (hMB : ∀ w ∈ cg, ∀ w' ∈ MB w now, Core.Modality.HistoricalAlternatives.histEquiv history now w w') (hSettled : Core.Modality.HistoricalAlternatives.settled history cg now fun (w : W) => perf Features.Dynamicity.dynamic P w now) : ¬Core.Modality.HistoricalAlternatives.diverse MB cg now fun (w : W) => perf Features.Dynamicity.dynamic P w now

When MAY scopes over PERF, the property under the modal is back- shifted past. If this property is settled in the common ground (as past properties are), then a metaphysical modal base cannot satisfy diversity — restricting MODAL > PERF to epistemic modality.

theorem Condoravdi2002.counterfactual_widens_domain {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (hBC : history.backwardsClosed) (w : W) {t' now : Time} (hle : t' ≤ now) : Core.Modality.HistoricalAlternatives.metaphysicalBase history w now ⊆ Core.Modality.HistoricalAlternatives.metaphysicalBase history w t'

When PERF scopes over MAY (counterfactual reading), the metaphysical base at the past perspective t' ≤ now is a superset of the one at now: backwards-closure of historical equivalence makes the past base wider. This is the structural source of the counterfactual reading's "could have been otherwise" force.

Adverb compatibility

Frame adverbials are intersective predicate modifiers: they restrict temporal reference to a period relative to the reference time. A frame adverb is compatible with a modal reading exactly when its selected period intersects the temporal region the modal projects. The eight (in)compat theorems below follow from lt_irrefl/lt_of_lt_of_le/ le_refl rather than a lookup table.

structure Condoravdi2002.FrameAdverb (Time : Type u_2) : Type u_2

A frame adverb selects a period of times relative to a reference time.

• name : String
• period : Time → Set Time

def Condoravdi2002.FrameAdverb.yesterday {Time : Type u_1} [LinearOrder Time] : FrameAdverb Time

Strictly before the reference time.

Equations

• Condoravdi2002.FrameAdverb.yesterday = { name := "yesterday", period := fun (now : Time) => {t : Time | t < now} }

def Condoravdi2002.FrameAdverb.now_ {Time : Type u_1} : FrameAdverb Time

The reference time itself.

Equations

• Condoravdi2002.FrameAdverb.now_ = { name := "now", period := fun (now : Time) => {now} }

def Condoravdi2002.FrameAdverb.tomorrow {Time : Type u_1} [LinearOrder Time] : FrameAdverb Time

Strictly after the reference time.

Equations

• Condoravdi2002.FrameAdverb.tomorrow = { name := "tomorrow", period := fun (now : Time) => {t : Time | now < t} }

def Condoravdi2002.projectedRegion {Time : Type u_1} [LinearOrder Time] (orient : Orientation) (now : Time) : Set Time

The temporal region in which a modal evaluates its scope, read off the AT relation:

• Future orientation: atForward requires the property's temporal anchor to lie at or after the reference time. Projected region: [now, ∞).
• Past orientation: perf requires a strictly earlier instantiation time. Projected region: (-∞, now).

Note: the eventive/stative distinction is not recorded here. The AT relation permits now = e.start for atEventForward, so the table-style "now is incompatible with eventive future" prediction of the original paper is a pragmatic event-duration fact that compatible does not formally exclude.

Equations

• Condoravdi2002.projectedRegion Condoravdi2002.Orientation.future now = {t : Time | now ≤ t}
• Condoravdi2002.projectedRegion Condoravdi2002.Orientation.past now = {t : Time | t < now}

def Condoravdi2002.compatible {Time : Type u_1} [LinearOrder Time] (adv : FrameAdverb Time) (reading : ModalReading) (now : Time) : Prop

Compatibility: the adverb's selected period overlaps the modal's projected region.

Equations

• Condoravdi2002.compatible adv reading now = ∃ t ∈ adv.period now, t ∈ Condoravdi2002.projectedRegion reading.orientation now

theorem Condoravdi2002.tomorrow_present_compat {Time : Type u_1} [LinearOrder Time] [NoMaxOrder Time] (now : Time) : compatible FrameAdverb.tomorrow ModalReading.present now

"He may get sick tomorrow." Future-oriented modal accepts a future adverb (witnessed via NoMaxOrder).

theorem Condoravdi2002.yesterday_present_incompat {Time : Type u_1} [LinearOrder Time] (now : Time) : ¬compatible FrameAdverb.yesterday ModalReading.present now

"*He may get sick yesterday." Future-oriented modal rejects a past adverb: any witness would satisfy t < now ∧ now ≤ t, contradicting lt_irrefl.

theorem Condoravdi2002.now_present_compat {Time : Type u_1} [LinearOrder Time] (now : Time) : compatible FrameAdverb.now_ ModalReading.present now

"He may be sick now." The reference time witnesses overlap of {now} with [now, ∞) via le_refl. The eventive variant ("??He may get sick now") is marginal in the paper for pragmatic event-duration reasons; see the projectedRegion docstring.

theorem Condoravdi2002.yesterday_epistemic_compat {Time : Type u_1} [LinearOrder Time] [NoMinOrder Time] (now : Time) : compatible FrameAdverb.yesterday ModalReading.epistemic now

"He may have gotten sick yesterday." Past-oriented modal accepts a past adverb (witnessed via NoMinOrder).

theorem Condoravdi2002.tomorrow_epistemic_incompat {Time : Type u_1} [LinearOrder Time] (now : Time) : ¬compatible FrameAdverb.tomorrow ModalReading.epistemic now

"*He may have gotten sick tomorrow." Past-oriented modal rejects a future adverb: now < t ∧ t < now contradicts lt_irrefl via lt_trans.

Fragment binding

theorem Condoravdi2002.might_have_distinct_aux_types : Fragments.English.Auxiliaries.might.auxType ≠ Fragments.English.Auxiliaries.have_.auxType

Might and perfect have are distinct aux heads in the English Fragment. The decomposition "might have" = MAY(PERF(...)) and the scope permutation deriving the epistemic vs counterfactual reading both require the Fragment to classify them under different auxTypes — if they ever fused (e.g., a single might-have modal entry), the analysis would not apply at the surface-form level.

Co-binders of these entries (e.g., @cite{cariani-santorio-2018} on will/would) are discoverable by greping Fragments.English.Auxiliaries.<entry> across Phenomena/.