Temporal Modal Evaluation

@cite{abusch-1997} @cite{condoravdi-2002} @cite{kratzer-2012} @cite{werner-2006}

Modal bases and ordering sources are functions of both world and time (@cite{kratzer-2012} Ch. 4, @cite{condoravdi-2002}). This module extends Kratzer.lean with time-indexed conversational backgrounds and derives the static (time-independent) versions as a special case.

Core Extension

Kratzer.lean defines ConvBackground W := W → List (W → Prop). @cite{kratzer-2012} Ch. 4 argues that this should be W → Time → List (W → Prop): the modal base and ordering source can vary with the temporal perspective.

This distinction matters for:

• Temporal orientation: whether "must p" is about the past, present, or future depends on when the modal base is evaluated.
• Historical accessibility: worlds that share history up to time t may diverge afterward ("branching futures").
• Epistemic change: the speaker's evidence base changes over time; "at t, it was necessary that p" ≠ "at t', it is necessary that p".

Key Result

temporal_eq_static: temporal modal evaluation reduces to standard Kratzer evaluation when the conversational backgrounds are time-independent.

Time-indexed conversational backgrounds

@[reducible, inline]

abbrev Semantics.Modality.Temporal.TemporalConvBackground (W : Type u_2) (Time : Type u_3) : Type (max u_2 u_3)

A time-indexed conversational background maps (world, time) pairs to sets of propositions. This is the book's core extension: f(w,t) and g(w,t).

At different times, the same world may yield different sets of relevant facts (modal base) or normative standards (ordering source).

Equations

• Semantics.Modality.Temporal.TemporalConvBackground W Time = (W → Time → List (W → Prop))

@[reducible, inline]

abbrev Semantics.Modality.Temporal.TemporalModalBase (W : Type u_2) (Time : Type u_3) : Type (max u_2 u_3)

Time-indexed modal base: what facts are relevant at (w, t).

Equations

• Semantics.Modality.Temporal.TemporalModalBase W Time = Semantics.Modality.Temporal.TemporalConvBackground W Time

@[reducible, inline]

abbrev Semantics.Modality.Temporal.TemporalOrderingSource (W : Type u_2) (Time : Type u_3) : Type (max u_2 u_3)

Time-indexed ordering source: what standards apply at (w, t).

Equations

• Semantics.Modality.Temporal.TemporalOrderingSource W Time = Semantics.Modality.Temporal.TemporalConvBackground W Time

def Semantics.Modality.Temporal.TemporalConvBackground.atTime {W : Type u_1} {Time : Type u_2} (f : TemporalConvBackground W Time) (t : Time) : Core.Logic.Intensional.ConvBackground W

Fix a time t to obtain a standard (time-independent) conversational background. This is the "temporal perspective" operation: evaluating the modal at a specific time.

Equations

• f.atTime t w = f w t

def Semantics.Modality.Temporal.ConvBackground.liftTemporal {W : Type u_1} {Time : Type u_2} (f : Core.Logic.Intensional.ConvBackground W) : TemporalConvBackground W Time

Lift a time-independent background to a trivially temporal one (constant across time).

Equations

• Semantics.Modality.Temporal.ConvBackground.liftTemporal f w x✝ = f w

theorem Semantics.Modality.Temporal.lift_atTime_id {W : Type u_1} {Time : Type u_2} (f : Core.Logic.Intensional.ConvBackground W) (t : Time) : (ConvBackground.liftTemporal f).atTime t = f

Lifting then fixing at any time recovers the original background.

Temporal modal evaluation

def Semantics.Modality.Temporal.temporalNecessity {W : Type u_1} {Time : Type u_2} (f : TemporalModalBase W Time) (g : TemporalOrderingSource W Time) (t : Time) (p : W → Prop) (w : W) : Prop

Modal necessity evaluated at a world-time pair.

⟦must p⟧(w, t) = ∀w' ∈ Best(f(w,t), g(w,t), w). p(w')

Equations

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

def Semantics.Modality.Temporal.temporalPossibility {W : Type u_1} {Time : Type u_2} (f : TemporalModalBase W Time) (g : TemporalOrderingSource W Time) (t : Time) (p : W → Prop) (w : W) : Prop

Modal possibility evaluated at a world-time pair.

⟦might p⟧(w, t) = ∃w' ∈ Best(f(w,t), g(w,t), w). p(w')

Equations

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

theorem Semantics.Modality.Temporal.temporal_eq_static {W : Type u_1} {Time : Type u_2} (f : Core.Logic.Intensional.ModalBase W) (g : Core.Logic.Intensional.OrderingSource W) (p : W → Prop) (w : W) (t : Time) : temporalNecessity (ConvBackground.liftTemporal f) (ConvBackground.liftTemporal g) t p w ↔ Kratzer.necessity f g p w

Temporal ↔ Static bridge: temporal modal evaluation reduces to standard Kratzer when the backgrounds are time-independent.

theorem Semantics.Modality.Temporal.temporal_duality {W : Type u_1} {Time : Type u_2} (f : TemporalModalBase W Time) (g : TemporalOrderingSource W Time) (t : Time) (p : W → Prop) (w : W) : temporalNecessity f g t p w ↔ ¬temporalPossibility f g t (fun (w' : W) => ¬p w') w

Temporal duality: □ₜp ↔ ¬◇ₜ¬p. One of five sibling theorem dualitys (see Modality/Kratzer/Operators.lean::duality for the unification opportunity via Core.Logic.Opposition.Square.fromBox).

Historical accessibility

Worlds share history up to time t: they agree on all facts prior to t. This gives the "branching futures" model: the past is settled, the future is open.

def Semantics.Modality.Temporal.historicalNecessity {W : Type u_1} {Time : Type u_2} (history : TemporalConvBackground W Time) (t : Time) (p : W → Prop) (w : W) : Prop

Historical necessity: p holds at all worlds sharing w's history up to t.

The history function (a TemporalConvBackground) serves as the modal base; the ordering source is empty (pure accessibility, no ranking).

Equations

• Semantics.Modality.Temporal.historicalNecessity history t p w = Semantics.Modality.Temporal.temporalNecessity history (fun (x : W) (x_1 : Time) => []) t p w

theorem Semantics.Modality.Temporal.empty_history_universal {W : Type u_1} {Time : Type u_2} (t : Time) (p : W → Prop) (w : W) : historicalNecessity (fun (x : W) (x_1 : Time) => []) t p w ↔ ∀ (w' : W), p w'

With empty history (no shared past), all worlds are accessible: historical necessity collapses to necessity over the universal set.

Epistemic change over time

theorem Semantics.Modality.Temporal.evidence_monotone {W : Type u_1} {Time : Type u_2} (f : TemporalModalBase W Time) (t₁ t₂ : Time) (p : W → Prop) (w : W) (hSub : ∀ q ∈ f w t₁, q ∈ f w t₂) (hNec : temporalNecessity f (fun (x : W) (x_1 : Time) => []) t₁ p w) : temporalNecessity f (fun (x : W) (x_1 : Time) => []) t₂ p w

Evidence monotonicity: if the evidence at t₁ is a subset of the evidence at t₂ (more evidence was gathered), then what was necessary at t₁ (less evidence) is still necessary at t₂ (more evidence).

More evidence → fewer accessible worlds → at least as many necessities.

Future-as-modal (Ch 4 bridge)

def Semantics.Modality.Temporal.futureAsModal {W : Type u_1} (circumstantial : Core.Logic.Intensional.ModalBase W) (p : W → Prop) (w : W) : Prop

"Will" as a circumstantial modal with empty ordering source. The future marker contributes modal force (necessity over a circumstantial base) without adding normative/stereotypical ranking.

This captures the unitary modal analysis: "will" does not decompose cleanly into force × flavor.

Equations

• Semantics.Modality.Temporal.futureAsModal circumstantial p w = Semantics.Modality.Kratzer.necessity circumstantial Core.Logic.Intensional.emptyBackground p w

theorem Semantics.Modality.Temporal.future_eq_simple_necessity {W : Type u_1} (circumstantial : Core.Logic.Intensional.ModalBase W) (p : W → Prop) (w : W) : futureAsModal circumstantial p w ↔ Kratzer.simpleNecessity circumstantial p w

Future-as-modal with empty ordering = simple necessity over the circumstantial base.