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 := World → List (BProp World). @cite{kratzer-2012} Ch. 4 argues that this should be World → Time → List (BProp World): 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 (Time : Type u_1) : Type u_1

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 Time = (Semantics.Attitudes.Intensional.World → Time → List (BProp Semantics.Attitudes.Intensional.World))

@[reducible, inline]

abbrev Semantics.Modality.Temporal.TemporalModalBase (Time : Type u_1) : Type u_1

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

Equations

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

@[reducible, inline]

abbrev Semantics.Modality.Temporal.TemporalOrderingSource (Time : Type u_1) : Type u_1

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

Equations

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

def Semantics.Modality.Temporal.TemporalConvBackground.atTime {Time : Type u_1} (f : TemporalConvBackground Time) (t : Time) : Kratzer.ConvBackground

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 {Time : Type u_1} (f : Kratzer.ConvBackground) : TemporalConvBackground 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 {Time : Type u_1} (f : Kratzer.ConvBackground) (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 {Time : Type u_1} (f : TemporalModalBase Time) (g : TemporalOrderingSource Time) (t : Time) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

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 {Time : Type u_1} (f : TemporalModalBase Time) (g : TemporalOrderingSource Time) (t : Time) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

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 {Time : Type u_1} (f : Kratzer.ModalBase) (g : Kratzer.OrderingSource) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (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 {Time : Type u_1} (f : TemporalModalBase Time) (g : TemporalOrderingSource Time) (t : Time) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : (temporalNecessity f g t p w == !temporalPossibility f g t (fun (w' : Attitudes.Intensional.World) => !p w') w) = true

Temporal duality: □ₜp ↔ ¬◇ₜ¬p.

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 {Time : Type u_1} (history : TemporalConvBackground Time) (t : Time) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

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 : Semantics.Attitudes.Intensional.World) (x_1 : Time) => []) t p w

theorem Semantics.Modality.Temporal.empty_history_universal {Time : Type u_1} (t : Time) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : historicalNecessity (fun (x : Attitudes.Intensional.World) (x_1 : Time) => []) t p w = Attitudes.Intensional.allWorlds.all p

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

Epistemic change over time

theorem Semantics.Modality.Temporal.evidence_monotone {Time : Type u_1} (f : TemporalModalBase Time) (t₁ t₂ : Time) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hSub : ∀ q ∈ f w t₁, q ∈ f w t₂) (hNec : temporalNecessity f (fun (x : Attitudes.Intensional.World) (x_1 : Time) => []) t₁ p w = true) : temporalNecessity f (fun (x : Attitudes.Intensional.World) (x_1 : Time) => []) t₂ p w = true

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 (circumstantial : Kratzer.ModalBase) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : Bool

"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 Semantics.Modality.Kratzer.emptyBackground p w

theorem Semantics.Modality.Temporal.future_eq_simple_necessity (circumstantial : Kratzer.ModalBase) (p : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : futureAsModal circumstantial p w = Kratzer.simpleNecessity circumstantial p w

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