[Con02]: 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 relation (at'/atForward) and its forward-expansion variants are defined in the AT relation section below; the eventive case reuses Klein's perfective viewpoint (Aspect.PRFV).
• Branching-time, settledness, and diversity live in Semantics/Modality/HistoricalAlternatives.lean.
• This file composes them into Condoravdi's specific operators and derives the paper's predictions.
• The mayCore/may split (point-evaluation vs forward-expansion; see Modal cores vs. prospective modals) is the hook downstream studies consume to model modals whose prospectivity is not lexicalized — the locus of this account's cross-linguistic contrasts.

The AT relation

[Con02]'s temporal-instantiation relation AT(t, w, P), dispatching on eventuality sort (after [KR83], [Par84]): events require temporal inclusion τ(e) ⊆ t, states temporal overlap τ(e) ∘ t. The eventive case is definitionally Klein's perfective viewpoint (Aspect.PRFV) and is reused rather than re-stipulated; the forward-expansion variants are Condoravdi's modal apparatus (evaluation expanded to the half-open [t, _)), consumed by the modal operators below.

def Condoravdi2002.atEvent {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) : Semantics.Aspect.IntervalPred W Time

Eventive AT, AT(t, w, P) for eventive P: an event of P whose runtime is included in t. Definitionally Klein's perfective Aspect.PRFV; Condoravdi writes the conjuncts predicate-first, PRFV relation-first.

Equations

• Condoravdi2002.atEvent P = Semantics.Aspect.PRFV P

def Condoravdi2002.atState {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) : Semantics.Aspect.IntervalPred W Time

Stative AT, AT(t, w, P) for stative P: an event of P whose runtime merely overlaps t. Weaker than Aspect.IMPF (proper inclusion), so it has no Aspect counterpart and stays a local definition.

Equations

• Condoravdi2002.atState P w t = ∃ (e : Event Time), e.τ.overlaps t ∧ P w e

def Condoravdi2002.at' {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (sort : Features.Dynamicity) (P : W → Event Time → Prop) (w : W) (t : NonemptyInterval Time) : Prop

The AT relation, dispatching on eventuality sort. The paper's third case (properties of times) is vacuous here: the event predicate is eventuality-valued.

Equations

• Condoravdi2002.at' Features.Dynamicity.dynamic P w t = Condoravdi2002.atEvent P w t
• Condoravdi2002.at' Features.Dynamicity.stative P w t = Condoravdi2002.atState P w t

theorem Condoravdi2002.atState_of_atEvent {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (t : NonemptyInterval Time) (h : atEvent P w t) : atState P w t

Eventive instantiation is stronger than stative: an event included in the interval certainly overlaps it.

theorem Condoravdi2002.atEvent_mono {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {t₁ t₂ : NonemptyInterval Time} (P : W → Event Time → Prop) (w : W) (hSub : t₁ ≤ t₂) (h : atEvent P w t₁) : atEvent P w t₂

atEvent is monotone in the reference interval.

theorem Condoravdi2002.atState_mono {W : Type u_1} {Time : Type u_2} [LinearOrder Time] {t₁ t₂ : NonemptyInterval Time} (P : W → Event Time → Prop) (w : W) (hSub : t₁ ≤ t₂) (h : atState P w t₁) : atState P w t₂

atState is monotone in the reference interval: overlap with a subinterval entails overlap with the containing interval.

Forward expansion

[Con02]: modals expand the evaluation time forward to [t, _) rather than shifting it. Since NonemptyInterval requires finite bounds, the constraints are expressed directly: for events the runtime starts at or after t; for states it persists at or past t.

def Condoravdi2002.atEventForward {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (t : Time) : Prop

Event instantiated in the future of t — AT([t, _), w, P) for eventive P: the event starts at or after t.

Equations

• Condoravdi2002.atEventForward P w t = ∃ (e : Event Time), t ≤ e.τ.toProd.1 ∧ P w e

def Condoravdi2002.atStateForward {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (t : Time) : Prop

State instantiated through t — AT([t, _), w, P) for stative P: the state persists at or past t.

Equations

• Condoravdi2002.atStateForward P w t = ∃ (e : Event Time), t ≤ e.τ.toProd.2 ∧ P w e

def Condoravdi2002.atForward {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (sort : Features.Dynamicity) (P : W → Event Time → Prop) (w : W) (t : Time) : Prop

Forward AT, dispatching on eventuality sort.

Equations

• Condoravdi2002.atForward Features.Dynamicity.dynamic P w t = Condoravdi2002.atEventForward P w t
• Condoravdi2002.atForward Features.Dynamicity.stative P w t = Condoravdi2002.atStateForward P w t

theorem Condoravdi2002.atStateForward_of_atEventForward {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (t : Time) (h : atEventForward P w t) : atStateForward P w t

Forward stative is weaker than forward eventive: if the event starts at or after t, its finish is also at or after t.

theorem Condoravdi2002.atEventForward_of_atEvent_point {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (t : Time) (h : atEvent P w (NonemptyInterval.pure t)) : atEventForward P w t

atEvent at a point [t, t] implies atEventForward at t.

theorem Condoravdi2002.atStateForward_of_atState_point {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (t : Time) (h : atState P w (NonemptyInterval.pure t)) : atStateForward P w t

atState at a point [t, t] implies atStateForward at t.

Operators

def Condoravdi2002.pres {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (sort : Features.Dynamicity) (P : W → Event Time → Prop) (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 = Condoravdi2002.at' sort P w (NonemptyInterval.pure t)

def Condoravdi2002.perf {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (sort : Features.Dynamicity) (P : W → Event Time → Prop) (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, Condoravdi2002.at' sort P w (NonemptyInterval.pure 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. The point-evaluation cores are the hook for modals whose futurity is not lexicalized but supplied by a separate prospective operator; may_of_mayCore_dynamic relates the two.

def Condoravdi2002.mayCore {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (MB : W → Time → Set W) (sort : Features.Dynamicity) (P : W → Event Time → Prop) (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, Condoravdi2002.at' sort P w' (NonemptyInterval.pure t)

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

MAY/MIGHT: existential quantification over the modal base, with forward temporal expansion. The English modal lexicalizes the prospective choice ([Con02]).

Equations

• Condoravdi2002.may MB sort P w t = ∃ w' ∈ MB w t, Condoravdi2002.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 : W → Event Time → Prop) (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, Condoravdi2002.at' sort P w' (NonemptyInterval.pure t)

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

WOLL: universal quantification over the modal base, with forward temporal expansion. The untensed modal underlying will / would.

Equations

• Condoravdi2002.woll MB sort P w t = ∀ w' ∈ MB w t, Condoravdi2002.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 : W → Event Time → Prop) (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 : W → Event Time → Prop) (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 : W → Event Time → Prop) (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 : W → Event Time → Prop) (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

Readings are classified along the canonical modal-temporal axes (Semantics/Modality/TemporalAxes.lean): TemporalPerspective (present/past evaluation of the modal base) and TemporalOrientation (direction from the perspective to the prejacent). Condoravdi's typology uses only the future and past orientations; the present-orientation cell of TemporalOrientation goes unused.

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 ⋯

@[implicit_reducible]

instance Condoravdi2002.instReprModalReading : Repr ModalReading

Equations

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

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

Equations

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

def Condoravdi2002.ModalReading.perspective : ModalReading → Semantics.Modality.TemporalPerspective

Modal-base evaluation time of a reading.

Equations

• Condoravdi2002.ModalReading.present.perspective = Semantics.Modality.TemporalPerspective.present
• Condoravdi2002.ModalReading.epistemic.perspective = Semantics.Modality.TemporalPerspective.present
• Condoravdi2002.ModalReading.counterfactual.perspective = Semantics.Modality.TemporalPerspective.past

def Condoravdi2002.ModalReading.orientation : ModalReading → Semantics.Modality.TemporalOrientation

Direction of temporal reference of a reading.

Equations

• Condoravdi2002.ModalReading.present.orientation = Semantics.Modality.TemporalOrientation.future
• Condoravdi2002.ModalReading.counterfactual.orientation = Semantics.Modality.TemporalOrientation.future
• Condoravdi2002.ModalReading.epistemic.orientation = Semantics.Modality.TemporalOrientation.past

Bridge to Klein's viewpoint operators

theorem Condoravdi2002.perf_eventive_implies_perfSimple {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (t : Time) (h : perf Features.Dynamicity.dynamic P w t) : Semantics.Aspect.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.

theorem Condoravdi2002.atState_of_impf {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (t : NonemptyInterval Time) (h : Semantics.Aspect.IMPF P w t) : atState P w t

[Kle94]'s imperfective entails Condoravdi's stative AT: proper inclusion of the reference interval in the event runtime implies overlap.

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 : HistoricalAlternatives W Time) (MB : W → Time → Set W) (cg : Set W) (now : Time) (P : W → Event Time → Prop) (hMB : ∀ w ∈ cg, ∀ w' ∈ MB w now, history.histEquiv now w w') (hSettled : history.settled cg now fun (w : W) => perf Features.Dynamicity.dynamic P w now) : ¬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 : HistoricalAlternatives W Time) (hBC : history.backwardsClosed) (w : W) {t' now : Time} (hle : t' ≤ now) : history.metaphysicalBase w now ⊆ history.metaphysicalBase 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.

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

"Yesterday": strictly before the reference time.

Equations

• Condoravdi2002.yesterday now = {t : Time | t < now}

def Condoravdi2002.nowAdv {Time : Type u_1} (now : Time) : Set Time

"Now": the reference time itself.

Equations

• Condoravdi2002.nowAdv now = {now}

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

"Tomorrow": strictly after the reference time.

Equations

• Condoravdi2002.tomorrow now = {t : Time | now < t}

def Condoravdi2002.projectedRegion {Time : Type u_1} [LinearOrder Time] (orient : Semantics.Modality.TemporalOrientation) (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, ∞).
• Present orientation: coincident with the reference time (unused by Condoravdi's typology). 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.fst 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 Semantics.Modality.TemporalOrientation.future now = {t : Time | now ≤ t}
• Condoravdi2002.projectedRegion Semantics.Modality.TemporalOrientation.present now = {now}
• Condoravdi2002.projectedRegion Semantics.Modality.TemporalOrientation.past now = {t : Time | t < now}

def Condoravdi2002.compatible {Time : Type u_1} [LinearOrder Time] (period : Time → Set Time) (reading : ModalReading) (now : Time) : Prop

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

Equations

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

theorem Condoravdi2002.tomorrow_present_compat {Time : Type u_1} [LinearOrder Time] [NoMaxOrder Time] (now : Time) : compatible 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 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 nowAdv 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 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 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 : English.Auxiliaries.might.auxType ≠ 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.

Other studies binding these Fragment entries are discoverable by greping English.Auxiliaries.<entry> across Studies/.