[RL23]: Conditionals, tense, and branching time — the settledness contrast

[RL23] [Kau05b] [Sch08e]

[RL23] (§2.1) observe that the eventive futurate present is felicitous only when the eventuality is settled — historically necessary, i.e. true on every possible future. Their minimal pair:

• (6a) The Red Sox play the Yankees tomorrow. — felicitous: the game is scheduled, so on every way the future might go, they play.
• (6b) #The Red Sox beat the Yankees tomorrow. — infelicitous out of the blue: the outcome is open, so that they win is not settled-true (felicitous only if the game is fixed for them).

We formalize the contrast against the BranchingTime substrate (the 𝔗 model). In a model where the game's outcome branches, play is IsInevitable (settled-true on every history through the utterance moment), while beat is not IsInevitable. Both members of the minimal pair are measured by the same unilateral notion (settled = historically necessary), which is R&L's actual constraint — a settled loss would not rescue (6b). (The bilateral IsSettledWhether/PresumedSettled in the substrate serves the [Phi21] apprehensional consumer, not R&L here.)

R&L (§4) reconstruct Kaufmann (2005) as an Ockhamist account and Schulz (2008) as a Peircean one. Both agree that the bare futurate present requires settledness; they differ in mechanism. The Ockhamism-vs-Peirceanism axis itself is the gap between history-relative future truth (oFut) and settledness (IsInevitable), which the same branching model exhibits.

A minimal branching model: the game's outcome branches

Three moments: now (game scheduled) below the two incomparable outcomes win / lose.

inductive RumbergLauer2023.Moment : Type

The moments of the Red Sox scenario.

• now : Moment
• win : Moment
• lose : Moment

@[implicit_reducible]

instance RumbergLauer2023.instDecidableEqMoment : DecidableEq Moment

Equations

• RumbergLauer2023.instDecidableEqMoment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance RumbergLauer2023.instFintypeMoment : Fintype Moment

Equations

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

def RumbergLauer2023.instReprMoment.repr : Moment → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RumbergLauer2023.instReprMoment : Repr Moment

Equations

• RumbergLauer2023.instReprMoment = { reprPrec := RumbergLauer2023.instReprMoment.repr }

@[implicit_reducible]

instance RumbergLauer2023.instLEMoment : LE Moment

now is below everything; otherwise the order is discrete, so win and lose are maximal and incomparable.

Equations

• RumbergLauer2023.instLEMoment = { le := fun (a b : RumbergLauer2023.Moment) => a = RumbergLauer2023.Moment.now ∨ a = b }

@[implicit_reducible]

instance RumbergLauer2023.instDecidableRelMomentLe : DecidableRel fun (x1 x2 : Moment) => x1 ≤ x2

Equations

• RumbergLauer2023.instDecidableRelMomentLe a b = instDecidableOr

@[implicit_reducible]

instance RumbergLauer2023.instPartialOrderMoment : PartialOrder Moment

Equations

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

@[implicit_reducible]

instance RumbergLauer2023.instDecidableLTMoment : DecidableLT Moment

Equations

• RumbergLauer2023.instDecidableLTMoment = decidableLTOfDecidableLE

instance RumbergLauer2023.instIsLeftLinearMoment : IsLeftLinear Moment

Left-linear: now is the only predecessor of anything, so any two predecessors of a moment are comparable.

instance RumbergLauer2023.instIsCodirectedOrderMoment : IsCodirectedOrder Moment

Historically connected: now is a global minimum, hence a common lower bound of any two moments.

instance RumbergLauer2023.instIsBranchingTimeMoment : BranchingTime.IsBranchingTime Moment

The outcome model is a genuine branching frame ([RL23] Def 1).

theorem RumbergLauer2023.now_lt_win : Moment.now < Moment.win

theorem RumbergLauer2023.now_lt_lose : Moment.now < Moment.lose

The two eventualities (minimal pair)

def RumbergLauer2023.played : BranchingTime.MProp Moment

The Red Sox play — true at both outcomes (the game is played either way).

Equations

• RumbergLauer2023.played m = (m = RumbergLauer2023.Moment.win ∨ m = RumbergLauer2023.Moment.lose)

def RumbergLauer2023.beat : BranchingTime.MProp Moment

The Red Sox beat the Yankees — true only at the win outcome.

Equations

• RumbergLauer2023.beat m = (m = RumbergLauer2023.Moment.win)

The contrast

theorem RumbergLauer2023.played_inevitable : BranchingTime.IsInevitable played Moment.now

(6a) is felicitous: play is inevitable. On every history through now, the game is played — because every history contains a future moment (exists_mem_gt_of_lt), and every successor of now is a playing moment.

theorem RumbergLauer2023.beat_not_inevitable : ¬BranchingTime.IsInevitable beat Moment.now

(6b) is infelicitous: beat is not inevitable. The lose-history passes through now but has no winning future, so winning is not settled-true (not historically necessary) — the same unilateral notion that makes (6a) felicitous.

theorem RumbergLauer2023.oFut_beat_but_not_inevitable : (∃ h ∈ BranchingTime.Hist Moment.now, BranchingTime.oFut (BranchingTime.oAtom beat) Moment.now h) ∧ ¬BranchingTime.IsInevitable beat Moment.now

The Ockhamism-vs-Peirceanism axis underlying R&L's two reconstructions ([RL23] §3.2, §4): on the win-history, beat is Ockhamist-future-true (oFut, history-relative), yet it is not settled (not IsInevitable/Peircean) — future truth and settledness come apart. Kaufmann's account is Ockhamist, Schulz's Peircean.

theorem RumbergLauer2023.beat_future_is_holds_after_but_not_inevitable : (∃ (h : Flag Moment) (hm : Moment.now ∈ h) (x : ↥h), Core.Order.holds Core.Order.after x ⟨Moment.now, hm⟩ ∧ beat ↑x) ∧ ¬BranchingTime.IsInevitable beat Moment.now

The Ockham side, grounded in the comparison kernel (BranchingTime.oFut_oAtom_holds_on_hist): beat's history-relative future truth is a Core.Order.holds Core.Order.after comparison along its witnessing history — win sits in the after cell relative to now (after = Tense.future), with the history's own chain order supplying the linear order holds needs. The Peircean contrast is deliberately preserved: beat is still ¬ IsInevitable, so the load-bearing felicity prediction remains settledness, not bare oFut.