Branching Time and Temporal Propositions

@cite{condoravdi-2002} @cite{thomason-1984}

Theory-specific temporal infrastructure that commits to truth-conditional evaluation at situation indices.

The framework-agnostic layer (intervals, situations, temporal relations, Reichenbach frames) lives in Core.Time and Core.Reichenbach.

Key Concepts

1. Historical modal base for future branching
2. Temporal propositions evaluated at situations

def Semantics.Tense.BranchingTime.WorldHistory (W : Type u_1) (Time : Type u_2) : Type (max u_2 u_1)

World history function: given a world and time, returns worlds that agree with that world up to that time.

This is the basis for the "historical" or "open future" modal base used in future-oriented modality.

Intuition: At time t in world w, multiple futures are possible. The historical alternatives are all worlds that share the same past with w up to t.

Equations

• Semantics.Tense.BranchingTime.WorldHistory W Time = (Situation W Time → Set W)

def Semantics.Tense.BranchingTime.historicalBase {W : Type u_1} {Time : Type u_2} [LE Time] (history : WorldHistory W Time) (s : Situation W Time) : Set (Situation W Time)

Historical modal base: situations whose worlds agree with s up to τ(s), and whose times are at or after τ(s).

Following @cite{thomason-1984} and @cite{condoravdi-2002}:

• Past is fixed (determined)
• Future branches (open)

hist(s) = {s' : w_{s'} ∈ H(wₛ, τ(s)) ∧ τ(s') ≥ τ(s)}

Equations

• Semantics.Tense.BranchingTime.historicalBase history s = {s' : Situation W Time | s'.world ∈ history s ∧ s'.time ≥ s.time}

def Semantics.Tense.BranchingTime.WorldHistory.reflexive {W : Type u_1} {Time : Type u_2} (h : WorldHistory W Time) : Prop

A world history is reflexive if every world agrees with itself.

Equations

• h.reflexive = ∀ (s : Situation W Time), s.world ∈ h s

def Semantics.Tense.BranchingTime.WorldHistory.backwardsClosed {W : Type u_1} {Time : Type u_2} [LE Time] (h : WorldHistory W Time) : Prop

A world history is backwards-closed: if w' agrees with w up to t, and t' ≤ t, then w' agrees with w up to t'.

"If two worlds agree up to time t, they also agree up to any earlier time."

Equations

• h.backwardsClosed = ∀ (w w' : W) (t t' : Time), t' ≤ t → w' ∈ h { world := w, time := t } → w' ∈ h { world := w, time := t' }

structure Semantics.Tense.BranchingTime.HistoricalProperties {W : Type u_1} {Time : Type u_2} [LE Time] (h : WorldHistory W Time) : Prop

Standard historical modal base properties.

• refl : h.reflexive

  Every world agrees with itself

• backwards : h.backwardsClosed

  Agreement is preserved for earlier times

@[reducible, inline]

abbrev Semantics.Tense.BranchingTime.TProp (W : Type u_1) (Time : Type u_2) : Type (max u_2 u_1)

A temporal proposition: true or false at each situation.

This is the situation-semantic analog of Prop' W.

Equations

• Semantics.Tense.BranchingTime.TProp W Time = (Situation W Time → Prop)

@[reducible, inline]

abbrev Semantics.Tense.BranchingTime.TBProp (W : Type u_1) (Time : Type u_2) : Type (max u_2 u_1)

Decidable temporal proposition (for computation).

Equations

• Semantics.Tense.BranchingTime.TBProp W Time = (Situation W Time → Bool)

def Semantics.Tense.BranchingTime.liftProp {W : Type u_1} {Time : Type u_2} (p : W → Prop) : TProp W Time

Lift a world proposition to a temporal proposition.

The lifted proposition is true at situation s iff the original proposition is true at s.world.

Equations

• Semantics.Tense.BranchingTime.liftProp p s = p s.world

def Semantics.Tense.BranchingTime.holdsAt {W : Type u_1} {Time : Type u_2} (p : TProp W Time) (w : W) (t : Time) : Prop

A proposition holds at time t in world w.

Equations

• Semantics.Tense.BranchingTime.holdsAt p w t = p { world := w, time := t }