Branching time (the 𝔗 model)

The branching-times model of Prior–Thomason: an order-theoretic tree of moments, whose maximal chains are the histories. This is the sibling of the T×W parallel-worlds model in Semantics/Modality/HistoricalAlternatives.lean; the two are inter-translatable by quotienting the historical-equivalence relation ([RL23] §4.1.3, deferred).

A branching-time structure is a left-linear (Core.Order.IsLeftLinear: no backward branching) and downward-directed (IsCodirectedOrder: historically connected) partial order ([RL23] Def 1). Histories are mathlib Flags (maximal chains).

Temporal-modal formulas are evaluated in one of two postsemantics ([RL23] §3.2): Peircean at a moment (future truth requires settledness) and Ockhamist at a moment/history pair (future truth is history-relative). Settledness oSettled (□_O) quantifies over the histories through a moment.

The conceptual heart ([RL23] pp. 541, 546): the Ockhamist history parameter is not fixed by a context of utterance ("there is no actual future") — only the moment is. oSettled is precisely the operator that quantifies the unfixed parameter away, which is why the felicity facts (eventive futurate present, apprehensionals) turn on it.

Main definitions

• IsBranchingTime, IsBranchingMeetTree — the frame ([RL23] Def 1; the meet-tree form adds branching points as ⊓, R&L Def 1(ii) / fn. 9).
• Hist — the histories through a moment.
• pPast; oAtom/oPast/oFut/oSettled/oSupervaluation — the Peircean/Ockhamist operators.
• IsInevitable, PresumedSettled, IsSettledWhether — settledness (context-relative).
• kaufmannPresent, kaufmannPast — [Kau05b]'s non-deictic tenses, reconstructed in Ockhamist branching time by [RL23] §4.1.3 (NOT framework-neutral primitives).

Main results

• oSettled_oAtom — atomic propositions are settled ([RL23] fn. 10).
• isInevitable_iff_oSupervaluation_oFut — Peircean future = Ockhamist settled future.
• Iic_subset_of_mem — the past sits inside every history through a moment (the past is history-independent), the payoff of left-linearity.

The frame

class BranchingTime.IsBranchingTime (M : Type u_2) [PartialOrder M] extends IsLeftLinear M, IsDirected M fun (x1 x2 : M) => x2 ≤ x1 : Prop

A branching-time structure ([RL23] Def 1): a left-linear, downward-directed partial order. Left-linearity (IsLeftLinear) is no backward branching; downward-directedness (IsCodirectedOrder) is historical connectedness. Weaker than R&L Def 1(ii), which asks for a greatest common lower bound (fn. 9) — that strengthening is IsBranchingMeetTree.

• comparable_of_le_common ⦃a b c : M⦄ : a ≤ c → b ≤ c → a ≤ b ∨ b ≤ a
• directed (a b : M) : ∃ c ≤ a, c ≤ b

class BranchingTime.IsBranchingMeetTree (M : Type u_2) [SemilatticeInf M] extends IsLeftLinear M : Prop

The meet-tree form ([RL23] Def 1(ii) + fn. 9): branching points exist as meets, m₁ ⊓ m₂ being the moment where the histories of m₁ and m₂ diverge. (The same ⊓ that Core.Order.Branching.Positions uses for syntactic least common ancestors.)

• comparable_of_le_common ⦃a b c : M⦄ : a ≤ c → b ≤ c → a ≤ b ∨ b ≤ a

Histories

def BranchingTime.Hist {M : Type u_1} [PartialOrder M] (m : M) : Set (Flag M)

The histories through a moment: the maximal ≤-chains (mathlib Flag) containing m ([RL23] Def 2).

Equations

• BranchingTime.Hist m = {h : Flag M | m ∈ h}

theorem BranchingTime.hist_nonempty {M : Type u_1} [PartialOrder M] (m : M) : (Hist m).Nonempty

Every moment lies on a history.

theorem BranchingTime.Iic_subset_of_mem {M : Type u_1} [PartialOrder M] [IsLeftLinear M] {m : M} {h : Flag M} (hm : m ∈ h) : Set.Iic m ⊆ ↑h

The past of a moment sits inside every history through it — the past is history-independent. The payoff of left-linearity: Iic m is a chain (IsLeftLinear.isChain_Iic), so (h : Set M) ∪ Iic m is a chain extending the maximal chain h, forcing Iic m ⊆ h.

theorem BranchingTime.exists_mem_gt_of_lt {M : Type u_1} [PartialOrder M] {m x : M} {h : Flag M} (hm : m ∈ h) (hx : m < x) : ∃ y ∈ h, m < y

A history through a non-maximal moment contains a future moment: if m ∈ h and m < x for some x, then h contains some y > m. (Otherwise insert x h would be a strictly larger chain, contradicting h's maximality.) The engine of inevitability reasoning: a history cannot stop at a moment that still has a future.

Postsemantics

MProp = truth at a moment (Peircean); OProp = truth at a moment/history pair (Ockhamist; intended m ∈ h). Atomic propositions depend only on the moment ([RL23] Def 3).

@[reducible, inline]

abbrev BranchingTime.MProp (M : Type u_2) : Type u_2

A Peircean proposition: truth at a moment.

Equations

• BranchingTime.MProp M = (M → Prop)

@[reducible, inline]

abbrev BranchingTime.OProp (M : Type u_2) [PartialOrder M] : Type u_2

An Ockhamist proposition: truth at a moment/history pair.

Equations

• BranchingTime.OProp M = (M → Flag M → Prop)

def BranchingTime.pPast {M : Type u_1} [PartialOrder M] (φ : MProp M) : MProp M

Peircean past: φ held at some earlier moment ([RL23] §3.2.1).

Equations

• BranchingTime.pPast φ m = ∃ m' < m, φ m'

def BranchingTime.oAtom {M : Type u_1} [PartialOrder M] (φ : MProp M) : OProp M

Lift a moment-proposition to an Ockhamist one, ignoring the history (atoms depend only on the moment).

Equations

• BranchingTime.oAtom φ m _h = φ m

def BranchingTime.oPast {M : Type u_1} [PartialOrder M] (φ : OProp M) : OProp M

Ockhamist past: φ held at some earlier moment, along the same history.

Equations

• BranchingTime.oPast φ m h = ∃ m' < m, φ m' h

def BranchingTime.oFut {M : Type u_1} [PartialOrder M] (φ : OProp M) : OProp M

Ockhamist future (F_O): φ holds at some later moment on the fixed history h ([RL23] §3.2.2).

Equations

• BranchingTime.oFut φ m h = ∃ m' ∈ h, m < m' ∧ φ m' h

def BranchingTime.oSettled {M : Type u_1} [PartialOrder M] (φ : OProp M) : OProp M

Ockhamist settledness (□_O): φ holds at m on every history through m ([RL23] §3.2.2). The history argument is ignored — settledness quantifies the (contextually unfixed) history parameter away.

Equations

• BranchingTime.oSettled φ m _h = ∀ h' ∈ BranchingTime.Hist m, φ m h'

def BranchingTime.oSupervaluation {M : Type u_1} [PartialOrder M] (φ : OProp M) : MProp M

Supervaluationist truth at a moment (Thomason 1970): □_O read off the moment. The third classic postsemantics; makes the settledness connection explicit.

Equations

• BranchingTime.oSupervaluation φ m = ∀ h ∈ BranchingTime.Hist m, φ m h

Settledness (context-relative)

The objective "all histories through m agree" is the special case of agreement over the histories compatible with a context/common ground ([Phi21]'s "presumed settled" is over ∩cg, not all histories; the T×W sibling carries the same cg parameter).

def BranchingTime.IsInevitable {M : Type u_1} [PartialOrder M] (φ : MProp M) (m : M) : Prop

A future-directed claim φ is inevitable at m: on every history through m, φ eventually holds. This is the Peircean future.

Equations

• BranchingTime.IsInevitable φ m = ∀ h ∈ BranchingTime.Hist m, ∃ m' ∈ h, m < m' ∧ φ m'

def BranchingTime.PresumedSettled {M : Type u_1} [PartialOrder M] (C : Set (Flag M)) (φ : MProp M) (m : M) : Prop

Presumed settled-whether relative to a context set C of histories: all C-histories agree on whether φ will hold ([Phi21]'s "(not) presumed settled").

Equations

• BranchingTime.PresumedSettled C φ m = ((∀ h ∈ C, ∃ m' ∈ h, m < m' ∧ φ m') ∨ ∀ h ∈ C, ¬∃ m' ∈ h, m < m' ∧ φ m')

@[reducible, inline]

abbrev BranchingTime.IsSettledWhether {M : Type u_1} [PartialOrder M] (φ : MProp M) (m : M) : Prop

Objective settledness = presumed-settled relative to the maximal context (all histories).

Equations

• BranchingTime.IsSettledWhether φ m = BranchingTime.PresumedSettled (BranchingTime.Hist m) φ m

Tense translations ([Kau05b] via [RL23] §4.1.3)

PRESENT Q := Q ∨ F_O Q, PAST Q := P_O Q. These encode [Kau05b]'s non-deictic-present analysis (morphological present = non-pastness) reconstructed in Ockhamism — not neutral branching primitives ([Sch08e]'s Peircean reconstruction gives the same surface forms).

def BranchingTime.kaufmannPresent {M : Type u_1} [PartialOrder M] (φ : OProp M) : OProp M

[Kau05b]'s present (non-deictic), Ockhamist reconstruction.

Equations

• BranchingTime.kaufmannPresent φ m h = (φ m h ∨ BranchingTime.oFut φ m h)

def BranchingTime.kaufmannPast {M : Type u_1} [PartialOrder M] (φ : OProp M) : OProp M

[Kau05b]'s past, Ockhamist reconstruction.

Equations

• BranchingTime.kaufmannPast φ = BranchingTime.oPast φ

Theorems

@[simp]

theorem BranchingTime.oSettled_oAtom {M : Type u_1} [PartialOrder M] (φ : MProp M) (m : M) (h : Flag M) : oSettled (oAtom φ) m h ↔ φ m

Atomic propositions are settled ([RL23] fn. 10): the valuation depends only on the moment, so □_O Q ↔ Q. Uses history-nonemptiness.

theorem BranchingTime.isInevitable_iff_oSupervaluation_oFut {M : Type u_1} [PartialOrder M] (φ : MProp M) (m : M) : IsInevitable φ m ↔ oSupervaluation (oFut (oAtom φ)) m

Peircean future = Ockhamist settled future ([RL23] §3.2): inevitability of φ is □_O F_O φ read off the moment. Holds by construction — the two postsemantics' notions of "settled that φ will happen" coincide.

Grounding in the Core.Order comparison kernel

The Ockhamist past/future operators reuse the shared point-comparison kernel (Core.Order.holds over Finset Ordering) rather than re-stipulating "earlier"/"later": oPast's witness sits before the evaluation moment, oFut's sits after it. Since Core.Order.before = Tense.past and Core.Order.after = Tense.future, branching-time tense and the rest of the library's tense are the same comparison. These are the linear-frame reductions (no branching, so the comparison is total on all of M); for a genuinely branching frame the comparison lives on each history's chain order (Flag's LinearOrder), oFut_oAtom_holds_on_hist.

@[simp]

theorem BranchingTime.oPast_oAtom_iff_holds {M : Type u_2} [LinearOrder M] (φ : MProp M) (m : M) (h : Flag M) : oPast (oAtom φ) m h ↔ ∃ (m' : M), Core.Order.holds Core.Order.before m' m ∧ φ m'

@[simp]

theorem BranchingTime.oFut_oAtom_iff_holds {M : Type u_2} [LinearOrder M] (φ : MProp M) (m : M) (h : Flag M) : oFut (oAtom φ) m h ↔ ∃ m' ∈ h, Core.Order.holds Core.Order.after m' m ∧ φ m'

theorem BranchingTime.oFut_oAtom_holds_on_hist {M : Type u_2} [PartialOrder M] [DecidableEq M] [DecidableRel fun (x1 x2 : M) => x1 ≤ x2] [DecidableLT M] (φ : MProp M) {m : M} {h : Flag M} (hm : m ∈ h) : oFut (oAtom φ) m h ↔ ∃ (x : ↥h), Core.Order.holds Core.Order.after x ⟨m, hm⟩ ∧ φ ↑x

Genuine-branching grounding (oFut on any branching frame): the future witness comparison is Core.Order.holds after over the history's own chain order (mathlib's LinearOrder ↥h for a maximal chain h). So the Ockhamist future along a history is literally the comparison-kernel future, with the chain supplying the linear order Core.Order.holds requires.