Rumberg and Lauer (2023): What if, and when? Conditionals, tense, and branching time

An isolated present tense sentence can talk about the future only when the eventuality is settled: the game the Red Sox play tomorrow is scheduled, their winning it is not. In the antecedent of an indicative conditional the constraint disappears, the consequent can be read at a later moment than the utterance ([Cro93]'s if I smile when I get out, the interview went well), and a past tense antecedent never shifts this way. The paper reconstructs the accounts of [Kau05b] and [Sch08g] in branching time and measures them, and its own proposal, against these facts.

Both rivals instantiate Kratzer's recipe, the conditional as a universal quantifier over a domain of antecedent possibilities, which this file renders with the library's conditional operators. Kaufmann's conditional is the strict conditional over the forward extension of historical accessibility, with the antecedent settled (kaufmannCond); Schulz's is the ordering conditional over the later moments, preferring the earliest by time (schulzCond). Both can place the antecedent at a future moment, so both wrongly shift past tense antecedents. The paper's own account uses the transition semantics of [Rum16]: truth is relative to a moment and a course of events, the future operator quantifies only over the histories the course admits (Transition.future), and the conditional reads its consequent at the first moment of decidedness of each minimal course making the antecedent true (Transition.cond). At the actual past the future operator is settledness; a present antecedent can be true relative to a longer course without being settled; and a past antecedent's only minimal course is the actual past, so its consequent never shifts.

Main statements

• Transition.future_atom_self, Transition.present_atom_self: at the actual past, future truth is settledness, so the isolated futurate present requires it.
• Transition.future_atom_of_lt: relative to a course leading to a witness, a future claim is true without being settled, which frees the antecedent.
• Transition.cond_past_atom: a past antecedent's consequent is read at the utterance moment, so past antecedents never shift.
• Transition.cond_eq_orderingImp: the paper's conditional is Kratzer's recipe over the extensions of the actual past, except that the consequent is read at the first moment of decidedness.
• Transition.future_atom_subset_stable: future truth persists under extensions of the course, the stability behind the covert necessity operator.
• Game.settledness_contrast, Game.antecedent_true_without_settledness: the Red Sox minimal pair.
• Trains.schulz_validates_arrival_at_two, Trains.kaufmann_rejects_both_arrivals, Trains.transition_rejects_both_arrivals: on the two-trains scenario Schulz's minimality wrongly validates the early arrival, while Kaufmann with a permissive context and the transition account reject both.
• Interview.smile_conditional_shifts_consequent: Crouch's shifted reading, with the consequent read after the interview.
• Interview.rivals_shift_past_antecedents, Interview.no_shifted_antecedent_moment: the rivals shift a past tense antecedent where the transition account cannot.

Implementation notes

The paper's transition sets with a last transition are represented by their first moment of decidedness, as licensed by its Definition 18, where extending a course is moving up the order and the actual past at a moment is the moment itself; the identification of course extension with the order relies on the existence of branching points, the connectedness the paper imposes for this purpose. Kaufmann's contextual parameter is carried as a set of moments, following the paper's note that it is in effect a property of times. The clock time of a moment in the finite scenarios is its depth in the tree of Gorn addresses. Claims on the finite models are decided through the reduction of histories to maximal moments.

References

• [RL23]
• [Rum16]
• [Kau05b]
• [Sch08g]
• [Cro93]
• [Pri67]

The present tense as non-pastness

All three accounts read the morphological present as non-pastness: truth now or in the future, with the future operator of the respective postsemantics.

def RumbergLauer2023.peirceanPresent {M : Type u_1} [PartialOrder M] (φ : Set M) : Set M

The present tense under the Peircean future holds now or in the settled future.

Equations

• RumbergLauer2023.peirceanPresent φ = φ ∪ BranchingTime.Peircean.future φ

def RumbergLauer2023.ockhamistPresent {M : Type u_1} [PartialOrder M] (φ : Set (M × Flag M)) : Set (M × Flag M)

The present tense under the Ockhamist future holds now or later on the history.

Equations

• RumbergLauer2023.ockhamistPresent φ = φ ∪ BranchingTime.Ockhamist.future φ

@[simp]

theorem RumbergLauer2023.mem_peirceanPresent {M : Type u_1} [PartialOrder M] {φ : Set M} {m : M} : m ∈ peirceanPresent φ ↔ m ∈ φ ∨ m ∈ BranchingTime.Peircean.future φ

@[simp]

theorem RumbergLauer2023.mem_ockhamistPresent {M : Type u_1} [PartialOrder M] {φ : Set (M × Flag M)} {p : M × Flag M} : p ∈ ockhamistPresent φ ↔ p ∈ φ ∨ p ∈ BranchingTime.Ockhamist.future φ

@[instance_reducible]

instance RumbergLauer2023.instDecidableMemSetPeirceanPresentOfDecidablePredFuture {M : Type u_1} [PartialOrder M] {φ : Set M} [DecidablePred fun (x : M) => x ∈ φ] [DecidablePred fun (x : M) => x ∈ BranchingTime.Peircean.future φ] (m : M) : Decidable (m ∈ peirceanPresent φ)

Equations

• RumbergLauer2023.instDecidableMemSetPeirceanPresentOfDecidablePredFuture m = { decide := decide (m ∈ φ) || decide (m ∈ BranchingTime.Peircean.future φ), reflects_decide := ⋯ }

theorem RumbergLauer2023.settled_ockhamistPresent_atom {M : Type u_1} [PartialOrder M] (φ : Set M) : BranchingTime.Ockhamist.settled (ockhamistPresent (BranchingTime.Ockhamist.atom φ)) = BranchingTime.Ockhamist.atom (peirceanPresent φ)

A settled present-tensed atom is the Peircean present read off the moment, since settledness commutes with the history-independent disjunct.

Transition semantics

Truth is relative to a moment and a course of events, represented by the moment whose past the course is: the actual past at m is the pair (m, m), and extending the course is moving up the order. The future operator quantifies over the histories through the moment that the course admits.

def RumbergLauer2023.Transition.atom {M : Type u_1} (φ : Set M) : Set (M × M)

A proposition of moments read relative to any course.

Equations

• RumbergLauer2023.Transition.atom φ = Prod.fst ⁻¹' φ

def RumbergLauer2023.Transition.past {M : Type u_1} [PartialOrder M] (φ : Set (M × M)) : Set (M × M)

The transition past of a proposition holds where it held at an earlier moment, relative to the same course.

Equations

• RumbergLauer2023.Transition.past φ = {p : M × M | ∃ m' < p.1, (m', p.2) ∈ φ}

def RumbergLauer2023.Transition.future {M : Type u_1} [PartialOrder M] (φ : Set (M × M)) : Set (M × M)

The transition future of a proposition holds where every history through the moment that the course admits has a later witness.

Equations

• RumbergLauer2023.Transition.future φ = {p : M × M | ∀ h ∈ BranchingTime.histories p.1 ∩ BranchingTime.histories p.2, ∃ m' ∈ h, p.1 < m' ∧ (m', p.2) ∈ φ}

def RumbergLauer2023.Transition.stable {M : Type u_1} [PartialOrder M] (φ : Set (M × M)) : Set (M × M)

A proposition is stable where it holds under every extension of the course compatible with the moment.

Equations

• RumbergLauer2023.Transition.stable φ = {p : M × M | ∀ (n : M), p.2 ≤ n → (BranchingTime.histories p.1 ∩ BranchingTime.histories n).Nonempty → (p.1, n) ∈ φ}

def RumbergLauer2023.Transition.present {M : Type u_1} [PartialOrder M] (φ : Set (M × M)) : Set (M × M)

The present tense under the transition future holds now or in the future the course admits.

Equations

• RumbergLauer2023.Transition.present φ = φ ∪ RumbergLauer2023.Transition.future φ

@[simp]

theorem RumbergLauer2023.Transition.mem_atom {M : Type u_1} {m n : M} {φ : Set M} : (m, n) ∈ atom φ ↔ m ∈ φ

@[simp]

theorem RumbergLauer2023.Transition.mem_past {M : Type u_1} [PartialOrder M] {φ : Set (M × M)} {m n : M} : (m, n) ∈ past φ ↔ ∃ m' < m, (m', n) ∈ φ

@[simp]

theorem RumbergLauer2023.Transition.mem_future {M : Type u_1} [PartialOrder M] {φ : Set (M × M)} {m n : M} : (m, n) ∈ future φ ↔ ∀ h ∈ BranchingTime.histories m ∩ BranchingTime.histories n, ∃ m' ∈ h, m < m' ∧ (m', n) ∈ φ

@[simp]

theorem RumbergLauer2023.Transition.mem_stable {M : Type u_1} [PartialOrder M] {φ : Set (M × M)} {m n : M} : (m, n) ∈ stable φ ↔ ∀ (n' : M), n ≤ n' → (BranchingTime.histories m ∩ BranchingTime.histories n').Nonempty → (m, n') ∈ φ

@[simp]

theorem RumbergLauer2023.Transition.mem_present {M : Type u_1} [PartialOrder M] {φ : Set (M × M)} {m n : M} : (m, n) ∈ present φ ↔ (m, n) ∈ φ ∨ (m, n) ∈ future φ

theorem RumbergLauer2023.Transition.past_atom {M : Type u_1} [PartialOrder M] (φ : Set M) : past (atom φ) = atom (BranchingTime.Peircean.past φ)

The transition past of an atom is the Peircean past, ignoring the course.

theorem RumbergLauer2023.Transition.future_atom_self {M : Type u_1} [PartialOrder M] (φ : Set M) (m : M) : (m, m) ∈ future (atom φ) ↔ m ∈ BranchingTime.Peircean.future φ

At the actual past the future operator is settledness, since the course admits every history through the moment.

theorem RumbergLauer2023.Transition.present_atom_self {M : Type u_1} [PartialOrder M] (φ : Set M) (m : M) : (m, m) ∈ present (atom φ) ↔ m ∈ peirceanPresent φ

An isolated present is the Peircean present, so future reference requires settledness.

theorem RumbergLauer2023.Transition.future_atom_of_lt {M : Type u_1} [PartialOrder M] {m n : M} {φ : Set M} (hmn : m < n) (hn : n ∈ φ) : (m, n) ∈ future (atom φ)

Relative to a course leading to a later witness, a future claim is true, settled or not.

theorem RumbergLauer2023.Transition.mem_of_mem_stable {M : Type u_1} [PartialOrder M] {φ : Set (M × M)} {m n : M} [IsLeftLinear M] (hmn : m ≤ n ∨ n ≤ m) (h : (m, n) ∈ stable φ) : (m, n) ∈ φ

Stability entails truth at any course compatible with the moment.

theorem RumbergLauer2023.Transition.future_atom_subset_stable {M : Type u_1} [PartialOrder M] [IsLeftLinear M] (φ : Set M) : future (atom φ) ⊆ stable (future (atom φ))

A true future claim stays true under every extension of the course, so the future operator is stable, though not settled.

theorem RumbergLauer2023.Transition.future_atom_ofIsMax {M : Type u_1} [PartialOrder M] {m : M} [IsLeftLinear M] {x : M} (hx : IsMax x) (hmx : m ≤ x) (φ : Set M) : (m, x) ∈ future (atom φ) ↔ (m, Flag.ofIsMax hx) ∈ BranchingTime.Ockhamist.future (BranchingTime.Ockhamist.atom φ)

Relative to the course of a maximal moment the transition future is the Ockhamist future on the history below it, since a complete course leaves one possible future.

The conditional

A conditional is true at the utterance moment when every minimal extension of the actual past making the antecedent true makes the consequent true at its first moment of decidedness.

def RumbergLauer2023.Transition.cond {M : Type u_1} [PartialOrder M] (A C : Set (M × M)) : Set M

The paper's predictive conditional in transition semantics.

Equations

• RumbergLauer2023.Transition.cond A C = {m : M | ∀ (n : M), Minimal (fun (n : M) => m ≤ n ∧ (m, n) ∈ A) n → (n, n) ∈ C}

@[simp]

theorem RumbergLauer2023.Transition.mem_cond {M : Type u_1} [PartialOrder M] {A C : Set (M × M)} {m : M} : m ∈ cond A C ↔ ∀ (n : M), Minimal (fun (n : M) => m ≤ n ∧ (m, n) ∈ A) n → (n, n) ∈ C

theorem RumbergLauer2023.Transition.minimal_eq_of_mem {M : Type u_1} [PartialOrder M] {m n : M} {A : Set (M × M)} (hA : (m, m) ∈ A) (h : Minimal (fun (n : M) => m ≤ n ∧ (m, n) ∈ A) n) : n = m

An antecedent already true at the actual past has it as its only minimal course.

theorem RumbergLauer2023.Transition.minimal_past_atom_iff {M : Type u_1} [PartialOrder M] {m n : M} {φ : Set M} : Minimal (fun (n : M) => m ≤ n ∧ (m, n) ∈ past (atom φ)) n ↔ n = m ∧ m ∈ BranchingTime.Peircean.past φ

A past antecedent's only minimal course is the actual past.

theorem RumbergLauer2023.Transition.cond_past_atom {M : Type u_1} [PartialOrder M] (φ : Set M) (C : Set (M × M)) : cond (past (atom φ)) C = {m : M | m ∈ BranchingTime.Peircean.past φ → (m, m) ∈ C}

A past antecedent's consequent is read at the utterance moment, so past antecedents have no shifted readings.

theorem RumbergLauer2023.Transition.cond_eq_orderingImp {M : Type u_1} [PartialOrder M] (A C : Set (M × M)) : cond A C = Conditional.orderingImp (fun (m : M) => {m} ×ˢ Set.Ici m) (fun (x : M) => Preorder.lift Prod.snd) A ((fun (p : M × M) => (p.2, p.2)) ⁻¹' C)

The paper's conditional is Kratzer's recipe with the extensions of the actual past as the modal base, ordered by extension, except that the consequent is read at the first moment of decidedness rather than at the antecedent index.

Decidability on finite frames

theorem RumbergLauer2023.Transition.mem_future_atom_iff {M : Type u_1} [PartialOrder M] {m n : M} [IsLeftLinear M] [Finite M] {φ : Set M} : (m, n) ∈ future (atom φ) ↔ ∀ (x : M), IsMax x → m ≤ x → n ≤ x → ∃ (m' : M), m < m' ∧ m' ≤ x ∧ m' ∈ φ

The transition future of an atom on a finite frame is a search over the maximal moments.

@[instance_reducible]

instance RumbergLauer2023.Transition.instDecidableMemProdSetFutureAtomOfDecidablePred {M : Type u_1} [PartialOrder M] [IsLeftLinear M] [Fintype M] [DecidableLE M] [DecidableLT M] (φ : Set M) [DecidablePred fun (x : M) => x ∈ φ] (p : M × M) : Decidable (p ∈ future (atom φ))

Equations

• RumbergLauer2023.Transition.instDecidableMemProdSetFutureAtomOfDecidablePred φ p = decidable_of_iff (∀ (x : M), IsMax x → p.1 ≤ x → p.2 ≤ x → ∃ (m' : M), p.1 < m' ∧ m' ≤ x ∧ m' ∈ φ) ⋯

@[instance_reducible]

instance RumbergLauer2023.Transition.instDecidableMemProdSetAtomOfDecidablePred {M : Type u_1} (φ : Set M) [DecidablePred fun (x : M) => x ∈ φ] (p : M × M) : Decidable (p ∈ atom φ)

Equations

• RumbergLauer2023.Transition.instDecidableMemProdSetAtomOfDecidablePred φ p = RumbergLauer2023.Transition.instDecidableMemProdSetAtomOfDecidablePred._aux_1 φ p

@[instance_reducible]

instance RumbergLauer2023.Transition.instDecidableMemProdSetPastAtomOfDecidablePred {M : Type u_1} [PartialOrder M] [Fintype M] [DecidableLT M] (φ : Set M) [DecidablePred fun (x : M) => x ∈ φ] (p : M × M) : Decidable (p ∈ past (atom φ))

Equations

• RumbergLauer2023.Transition.instDecidableMemProdSetPastAtomOfDecidablePred φ p = { decide := decide (∃ a ∈ Finset.univ, (fun (m' : M) => m' < p.1 ∧ m' ∈ φ) a), reflects_decide := ⋯ }

@[instance_reducible]

instance RumbergLauer2023.Transition.instDecidableMemProdSetPresentOfDecidablePredFuture {M : Type u_1} [PartialOrder M] (φ : Set (M × M)) [DecidablePred fun (x : M × M) => x ∈ φ] [DecidablePred fun (x : M × M) => x ∈ future φ] (p : M × M) : Decidable (p ∈ present φ)

Equations

• RumbergLauer2023.Transition.instDecidableMemProdSetPresentOfDecidablePredFuture φ p = { decide := decide (p ∈ φ) || decide (p ∈ RumbergLauer2023.Transition.future φ), reflects_decide := ⋯ }

@[instance_reducible]

instance RumbergLauer2023.Transition.instDecidableMemSetCondOfDecidablePredProd {M : Type u_1} [PartialOrder M] [Fintype M] [DecidableLE M] (A C : Set (M × M)) [DecidablePred fun (x : M × M) => x ∈ A] [DecidablePred fun (x : M × M) => x ∈ C] (m : M) : Decidable (m ∈ cond A C)

Equations

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

Kaufmann's conditional in branching time

The semantics of if forwards the historical accessibility relation: the relevant indices are the later ones the contextual parameter admits, the antecedent is settled there by its covert necessity operator, and the consequent is read at those indices.

def RumbergLauer2023.forwardBase {M : Type u_1} [PartialOrder M] (e : Set M) (m : M) : Set (M × Flag M)

The forward extension of historical accessibility, restricted by the contextual parameter, reaches the Ockhamist indices at or after the moment whose own moment the parameter admits.

Equations

• RumbergLauer2023.forwardBase e m = {p : M × Flag M | m ≤ p.1 ∧ p.1 ∈ p.2 ∧ p.1 ∈ e}

@[simp]

theorem RumbergLauer2023.mem_forwardBase {M : Type u_1} [PartialOrder M] {e : Set M} {m m' : M} {h : Flag M} : (m', h) ∈ forwardBase e m ↔ m ≤ m' ∧ m' ∈ h ∧ m' ∈ e

def RumbergLauer2023.kaufmannCond {M : Type u_1} [PartialOrder M] (e : Set M) (A C : Set (M × Flag M)) : Set M

Kaufmann's conditional reconstructed in Ockhamist branching time holds when the consequent holds at every later index the context admits at which the antecedent is settled. Only the moment of evaluation matters, since no context fixes the history parameter.

Equations

• RumbergLauer2023.kaufmannCond e A C = Conditional.strictImp (RumbergLauer2023.forwardBase e) (BranchingTime.Ockhamist.settled A) C

theorem RumbergLauer2023.mem_kaufmannCond {M : Type u_1} [PartialOrder M] {e : Set M} {A C : Set (M × Flag M)} {m : M} : m ∈ kaufmannCond e A C ↔ ∀ (m' : M) (h : Flag M), m ≤ m' → m' ∈ h → m' ∈ e → (m', h) ∈ BranchingTime.Ockhamist.settled A → (m', h) ∈ C

theorem RumbergLauer2023.mem_kaufmannCond_past_atom {M : Type u_1} [PartialOrder M] {e φ : Set M} {C : Set (M × Flag M)} {m : M} : m ∈ kaufmannCond e (BranchingTime.Ockhamist.past (BranchingTime.Ockhamist.atom φ)) C ↔ ∀ (m' : M) (h : Flag M), m ≤ m' → m' ∈ h → m' ∈ e → m' ∈ BranchingTime.Peircean.past φ → (m', h) ∈ C

Kaufmann's conditional with a past antecedent quantifies over the later admitted moments at which the antecedent has come true.

theorem RumbergLauer2023.mem_kaufmannCond_present_iff {M : Type u_1} [PartialOrder M] [IsLeftLinear M] [Finite M] {e φ ψ : Set M} {m : M} : m ∈ kaufmannCond e (ockhamistPresent (BranchingTime.Ockhamist.atom φ)) (ockhamistPresent (BranchingTime.Ockhamist.atom ψ)) ↔ ∀ (m' : M), m ≤ m' → m' ∈ e → m' ∈ peirceanPresent φ → ∀ (x : M), IsMax x → m' ≤ x → m' ∈ ψ ∨ ∃ m'' ≤ x, m' < m'' ∧ m'' ∈ ψ

Kaufmann's conditional between present-tensed atoms on a finite frame, with the histories reduced to the maximal moments.

Schulz's conditional in branching time

The modal base is the set of later moments, the ordering prefers the earliest by time, and the conditional quantifies over the minimal antecedent moments: the library's ordering conditional under the pullback of the time projection.

def RumbergLauer2023.schulzCond {M : Type u_1} [PartialOrder M] {T : Type u_2} [LinearOrder T] (time : M → T) (A C : Set M) : Set M

Schulz's conditional reconstructed in Peircean branching time.

Equations

• RumbergLauer2023.schulzCond time A C = Conditional.orderingImp Set.Ici (fun (x : M) => Preorder.lift time) A C

theorem RumbergLauer2023.mem_schulzCond_iff {M : Type u_1} [PartialOrder M] {T : Type u_2} [LinearOrder T] {time : M → T} {A C : Set M} {m : M} : m ∈ schulzCond time A C ↔ ∀ (m' : M), m ≤ m' → m' ∈ A → (∀ (m'' : M), m ≤ m'' → m'' ∈ A → time m'' ≤ time m' → time m' ≤ time m'') → m' ∈ C

@[instance_reducible]

instance RumbergLauer2023.instDecidableMemSetSchulzCondOfFintypeOfDecidableLEOfDecidablePred {M : Type u_1} [PartialOrder M] {T : Type u_2} [LinearOrder T] (time : M → T) (A C : Set M) [Fintype M] [DecidableLE M] [DecidablePred fun (x : M) => x ∈ A] [DecidablePred fun (x : M) => x ∈ C] (m : M) : Decidable (m ∈ schulzCond time A C)

Equations

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

theorem RumbergLauer2023.time_eq_of_mem_minimals {M : Type u_1} {T : Type u_2} [LinearOrder T] {time : M → T} {s : Set M} {a b : M} (ha : a ∈ (Preorder.lift time).minimals s) (hb : b ∈ (Preorder.lift time).minimals s) : time a = time b

The relevant antecedent possibilities of Schulz's conditional are co-temporal, since minimality in the time ordering forces a shared time.

The game

The Red Sox play the Yankees tomorrow is felicitous because the game is scheduled; #the Red Sox beat the Yankees tomorrow is odd because the outcome is open.

inductive RumbergLauer2023.Game : Type

The utterance moment, branching into the two outcomes of the game.

• now : Game
• win : Game
• lose : Game

@[instance_reducible]

instance RumbergLauer2023.instDecidableEqGame : DecidableEq Game

Equations

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

@[instance_reducible]

instance RumbergLauer2023.instFintypeGame : Fintype Game

Equations

• RumbergLauer2023.instFintypeGame = { elems := { val := ↑RumbergLauer2023.Game.enumList, nodup := RumbergLauer2023.Game.enumList_nodup }, complete := RumbergLauer2023.instFintypeGame._proof_1 }

def RumbergLauer2023.instReprGame.repr : Game → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• RumbergLauer2023.instReprGame.repr RumbergLauer2023.Game.now prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RumbergLauer2023.Game.now")).group prec✝
• RumbergLauer2023.instReprGame.repr RumbergLauer2023.Game.win prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RumbergLauer2023.Game.win")).group prec✝

@[instance_reducible]

instance RumbergLauer2023.instReprGame : Repr Game

Equations

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

def RumbergLauer2023.Game.addr : Game → Core.Order.TreePath

The tree of the scenario, by Gorn address.

Equations

• RumbergLauer2023.Game.now.addr = { toList := [] }
• RumbergLauer2023.Game.win.addr = { toList := [0] }
• RumbergLauer2023.Game.lose.addr = { toList := [1] }

theorem RumbergLauer2023.Game.addr_injective : Function.Injective addr

@[instance_reducible]

instance RumbergLauer2023.Game.instPartialOrder : PartialOrder Game

Equations

• RumbergLauer2023.Game.instPartialOrder = PartialOrder.lift RumbergLauer2023.Game.addr RumbergLauer2023.Game.addr_injective

@[instance_reducible]

instance RumbergLauer2023.Game.instDecidableLE : DecidableLE Game

Equations

• a.instDecidableLE b = { decide := decide (a.addr.toList <+: b.addr.toList), reflects_decide := ⋯ }

@[instance_reducible]

instance RumbergLauer2023.Game.instDecidableLT : DecidableLT Game

Equations

• RumbergLauer2023.Game.instDecidableLT = decidableLTOfDecidableLE

instance RumbergLauer2023.Game.instIsLeftLinear : IsLeftLinear Game

def RumbergLauer2023.Game.played : Set Game

The Red Sox play the Yankees holds at both outcomes.

Equations

• RumbergLauer2023.Game.played = {RumbergLauer2023.Game.win, RumbergLauer2023.Game.lose}

def RumbergLauer2023.Game.beat : Set Game

The Red Sox beat the Yankees holds at the winning outcome.

Equations

• RumbergLauer2023.Game.beat = {RumbergLauer2023.Game.win}

@[instance_reducible]

instance RumbergLauer2023.Game.instDecidablePredMemSetPlayed : DecidablePred fun (x : Game) => x ∈ played

Equations

• m.instDecidablePredMemSetPlayed = { decide := decide (m = RumbergLauer2023.Game.win) || decide (m = RumbergLauer2023.Game.lose), reflects_decide := ⋯ }

@[instance_reducible]

instance RumbergLauer2023.Game.instDecidablePredMemSetBeat : DecidablePred fun (x : Game) => x ∈ beat

Equations

• m.instDecidablePredMemSetBeat = RumbergLauer2023.Game.instDecidablePredMemSetBeat._aux_1 m

theorem RumbergLauer2023.Game.settledness_contrast : now ∈ BranchingTime.Peircean.future played ∧ now ∉ BranchingTime.Peircean.future beat

The scheduled game is settled at the utterance moment, so its futurate present is felicitous; the win is not settled.

theorem RumbergLauer2023.Game.antecedent_true_without_settledness : (now, win) ∈ Transition.present (Transition.atom beat) ∧ now ∉ peirceanPresent beat

A conditional antecedent needs no settledness. Relative to the course of events leading to the win, the Red Sox beat the Yankees tomorrow is true at the utterance moment, where it is not settled.

theorem RumbergLauer2023.Game.future_truth_without_settledness : (now, Flag.ofIsMax future_truth_without_settledness._proof_1) ∈ BranchingTime.Ockhamist.future (BranchingTime.Ockhamist.atom beat) ∧ now ∉ BranchingTime.Peircean.future beat

Ockhamist future truth and Peircean settledness come apart. The win is future-true on the winning history yet not settled.

The two trains

John decides at short notice whether to take the one o'clock train and arrive at two; if not, he decides later whether to take the two o'clock train and arrive at three, or stay. Intuitively both if John comes today, he arrives at two and if John comes today, he arrives at three are false.

inductive RumbergLauer2023.Trains : Type

The moments of the two-trains scenario.

• now : Trains
• early : Trains
• arriveTwo : Trains
• wait : Trains
• late : Trains
• arriveThree : Trains
• stay : Trains

@[instance_reducible]

instance RumbergLauer2023.instDecidableEqTrains : DecidableEq Trains

Equations

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

@[instance_reducible]

instance RumbergLauer2023.instFintypeTrains : Fintype Trains

Equations

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

@[instance_reducible]

instance RumbergLauer2023.instReprTrains : Repr Trains

Equations

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

def RumbergLauer2023.instReprTrains.repr : Trains → ℕ → Std.Format

Equations

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

def RumbergLauer2023.Trains.addr : Trains → Core.Order.TreePath

The tree of the scenario, by Gorn address. The early decision leads to the two o'clock arrival; waiting leads to the late decision, and then to the three o'clock arrival or to staying.

Equations

• RumbergLauer2023.Trains.now.addr = { toList := [] }
• RumbergLauer2023.Trains.early.addr = { toList := [0] }
• RumbergLauer2023.Trains.arriveTwo.addr = { toList := [0, 0] }
• RumbergLauer2023.Trains.wait.addr = { toList := [1] }
• RumbergLauer2023.Trains.late.addr = { toList := [1, 0] }
• RumbergLauer2023.Trains.arriveThree.addr = { toList := [1, 0, 0] }
• RumbergLauer2023.Trains.stay.addr = { toList := [1, 1] }

theorem RumbergLauer2023.Trains.addr_injective : Function.Injective addr

@[instance_reducible]

instance RumbergLauer2023.Trains.instPartialOrder : PartialOrder Trains

Equations

• RumbergLauer2023.Trains.instPartialOrder = PartialOrder.lift RumbergLauer2023.Trains.addr RumbergLauer2023.Trains.addr_injective

@[instance_reducible]

instance RumbergLauer2023.Trains.instDecidableLE : DecidableLE Trains

Equations

• a.instDecidableLE b = { decide := decide (a.addr.toList <+: b.addr.toList), reflects_decide := ⋯ }

@[instance_reducible]

instance RumbergLauer2023.Trains.instDecidableLT : DecidableLT Trains

Equations

• RumbergLauer2023.Trains.instDecidableLT = decidableLTOfDecidableLE

instance RumbergLauer2023.Trains.instIsLeftLinear : IsLeftLinear Trains

def RumbergLauer2023.Trains.time (m : Trains) : ℕ

The clock time of a moment is its depth in the tree, with the decisions at one and two and the arrivals at two and three.

Equations

• m.time = m.addr.toList.length

def RumbergLauer2023.Trains.come : Set Trains

John comes to Konstanz today holds on arrival.

Equations

• RumbergLauer2023.Trains.come = {RumbergLauer2023.Trains.arriveTwo, RumbergLauer2023.Trains.arriveThree}

def RumbergLauer2023.Trains.atTwo : Set Trains

John arrives at two.

Equations

• RumbergLauer2023.Trains.atTwo = {RumbergLauer2023.Trains.arriveTwo}

def RumbergLauer2023.Trains.atThree : Set Trains

John arrives at three.

Equations

• RumbergLauer2023.Trains.atThree = {RumbergLauer2023.Trains.arriveThree}

@[instance_reducible]

instance RumbergLauer2023.Trains.instDecidablePredMemSetCome : DecidablePred fun (x : Trains) => x ∈ come

Equations

• m.instDecidablePredMemSetCome = { decide := decide (m = RumbergLauer2023.Trains.arriveTwo) || decide (m = RumbergLauer2023.Trains.arriveThree), reflects_decide := ⋯ }

@[instance_reducible]

instance RumbergLauer2023.Trains.instDecidablePredMemSetAtTwo : DecidablePred fun (x : Trains) => x ∈ atTwo

Equations

• m.instDecidablePredMemSetAtTwo = RumbergLauer2023.Trains.instDecidablePredMemSetAtTwo._aux_1 m

@[instance_reducible]

instance RumbergLauer2023.Trains.instDecidablePredMemSetAtThree : DecidablePred fun (x : Trains) => x ∈ atThree

Equations

• m.instDecidablePredMemSetAtThree = RumbergLauer2023.Trains.instDecidablePredMemSetAtThree._aux_1 m

theorem RumbergLauer2023.Trains.schulz_ignores_the_late_decision : early ∈ (Preorder.lift time).minimals {m' : Trains | now ≤ m' ∧ m' ∈ peirceanPresent come} ∧ late ∉ (Preorder.lift time).minimals {m' : Trains | now ≤ m' ∧ m' ∈ peirceanPresent come} ∧ now ≤ late ∧ late ∈ peirceanPresent come

Schulz's minimality keeps only the early decision among the antecedent moments. The late decision makes the antecedent settled but is ignored.

theorem RumbergLauer2023.Trains.schulz_validates_arrival_at_two : now ∈ schulzCond time (peirceanPresent come) (peirceanPresent atTwo)

Schulz's conditional validates if John comes today, he arrives at two, which is false in the scenario.

theorem RumbergLauer2023.Trains.kaufmann_rejects_both_arrivals : now ∉ kaufmannCond Set.univ (ockhamistPresent (BranchingTime.Ockhamist.atom come)) (ockhamistPresent (BranchingTime.Ockhamist.atom atTwo)) ∧ now ∉ kaufmannCond Set.univ (ockhamistPresent (BranchingTime.Ockhamist.atom come)) (ockhamistPresent (BranchingTime.Ockhamist.atom atThree))

With a context that filters nothing, Kaufmann's conditional rejects both arrival conditionals, as the paper grants.

theorem RumbergLauer2023.Trains.transition_rejects_both_arrivals : now ∉ Transition.cond (Transition.present (Transition.atom come)) (Transition.present (Transition.atom atTwo)) ∧ now ∉ Transition.cond (Transition.present (Transition.atom come)) (Transition.present (Transition.atom atThree))

The transition account rejects both arrival conditionals. The two decisions are both minimal courses making the antecedent true, and each falsifies one consequent.

theorem RumbergLauer2023.Trains.decidedness_at_different_times : Minimal (fun (n : Trains) => now ≤ n ∧ (now, n) ∈ Transition.present (Transition.atom come)) early ∧ Minimal (fun (n : Trains) => now ≤ n ∧ (now, n) ∈ Transition.present (Transition.atom come)) late ∧ early.time ≠ late.time

The transition account's moments of decidedness for John comes today are the two decisions, which lie at different times.

The interview

Before tomorrow's job interview, if I smile when I get out, the interview went well has a shifted past-in-the-future consequent, while #if the interview went well, John gets the job cannot read its past antecedent in the future.

inductive RumbergLauer2023.Interview : Type

The moments of the interview scenario. The interview starts, goes well or badly, and after a good interview the speaker leaves smiling or not.

• now : Interview
• start : Interview
• good : Interview
• bad : Interview
• smile : Interview
• frown : Interview

@[instance_reducible]

instance RumbergLauer2023.instDecidableEqInterview : DecidableEq Interview

Equations

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

@[instance_reducible]

instance RumbergLauer2023.instFintypeInterview : Fintype Interview

Equations

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

def RumbergLauer2023.instReprInterview.repr : Interview → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance RumbergLauer2023.instReprInterview : Repr Interview

Equations

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

def RumbergLauer2023.Interview.addr : Interview → Core.Order.TreePath

The tree of the scenario, by Gorn address.

Equations

• RumbergLauer2023.Interview.now.addr = { toList := [] }
• RumbergLauer2023.Interview.start.addr = { toList := [0] }
• RumbergLauer2023.Interview.good.addr = { toList := [0, 0] }
• RumbergLauer2023.Interview.bad.addr = { toList := [0, 1] }
• RumbergLauer2023.Interview.smile.addr = { toList := [0, 0, 0] }
• RumbergLauer2023.Interview.frown.addr = { toList := [0, 0, 1] }

theorem RumbergLauer2023.Interview.addr_injective : Function.Injective addr

@[instance_reducible]

instance RumbergLauer2023.Interview.instPartialOrder : PartialOrder Interview

Equations

• RumbergLauer2023.Interview.instPartialOrder = PartialOrder.lift RumbergLauer2023.Interview.addr RumbergLauer2023.Interview.addr_injective

@[instance_reducible]

instance RumbergLauer2023.Interview.instDecidableLE : DecidableLE Interview

Equations

• a.instDecidableLE b = { decide := decide (a.addr.toList <+: b.addr.toList), reflects_decide := ⋯ }

@[instance_reducible]

instance RumbergLauer2023.Interview.instDecidableLT : DecidableLT Interview

Equations

• RumbergLauer2023.Interview.instDecidableLT = decidableLTOfDecidableLE

instance RumbergLauer2023.Interview.instIsLeftLinear : IsLeftLinear Interview

def RumbergLauer2023.Interview.time (m : Interview) : ℕ

The clock time of a moment, its depth in the tree.

Equations

• m.time = m.addr.toList.length

def RumbergLauer2023.Interview.wentWell : Set Interview

The interview went well.

Equations

• RumbergLauer2023.Interview.wentWell = {RumbergLauer2023.Interview.good}

def RumbergLauer2023.Interview.wentBadly : Set Interview

The interview went badly.

Equations

• RumbergLauer2023.Interview.wentBadly = {RumbergLauer2023.Interview.bad}

def RumbergLauer2023.Interview.smiles : Set Interview

I smile when I get out.

Equations

• RumbergLauer2023.Interview.smiles = {RumbergLauer2023.Interview.smile}

def RumbergLauer2023.Interview.getsJob : Set Interview

John gets the job is settled once a good interview is over.

Equations

• RumbergLauer2023.Interview.getsJob = {RumbergLauer2023.Interview.smile, RumbergLauer2023.Interview.frown}

@[instance_reducible]

instance RumbergLauer2023.Interview.instDecidablePredMemSetWentWell : DecidablePred fun (x : Interview) => x ∈ wentWell

Equations

• m.instDecidablePredMemSetWentWell = RumbergLauer2023.Interview.instDecidablePredMemSetWentWell._aux_1 m

@[instance_reducible]

instance RumbergLauer2023.Interview.instDecidablePredMemSetWentBadly : DecidablePred fun (x : Interview) => x ∈ wentBadly

Equations

• m.instDecidablePredMemSetWentBadly = RumbergLauer2023.Interview.instDecidablePredMemSetWentBadly._aux_1 m

@[instance_reducible]

instance RumbergLauer2023.Interview.instDecidablePredMemSetSmiles : DecidablePred fun (x : Interview) => x ∈ smiles

Equations

• m.instDecidablePredMemSetSmiles = RumbergLauer2023.Interview.instDecidablePredMemSetSmiles._aux_1 m

@[instance_reducible]

instance RumbergLauer2023.Interview.instDecidablePredMemSetGetsJob : DecidablePred fun (x : Interview) => x ∈ getsJob

Equations

• m.instDecidablePredMemSetGetsJob = { decide := decide (m = RumbergLauer2023.Interview.smile) || decide (m = RumbergLauer2023.Interview.frown), reflects_decide := ⋯ }

theorem RumbergLauer2023.Interview.smile_conditional_shifts_consequent : now ∈ Transition.cond (Transition.present (Transition.atom smiles)) (Transition.past (Transition.atom wentWell)) ∧ now ∉ Transition.cond (Transition.present (Transition.atom smiles)) (Transition.past (Transition.atom wentBadly)) ∧ Minimal (fun (n : Interview) => now ≤ n ∧ (now, n) ∈ Transition.present (Transition.atom smiles)) smile ∧ now < smile

Crouch's if I smile when I get out, the interview went well is true at the utterance moment, its past-tensed consequent read at the moment the smiling is decided, after the interview, while the interview went badly fails there.

theorem RumbergLauer2023.Interview.rivals_shift_past_antecedents : now ∉ BranchingTime.Peircean.past wentWell ∧ now ∈ schulzCond time (BranchingTime.Peircean.past wentWell) (peirceanPresent getsJob) ∧ now ∈ kaufmannCond Set.univ (BranchingTime.Ockhamist.past (BranchingTime.Ockhamist.atom wentWell)) (ockhamistPresent (BranchingTime.Ockhamist.atom getsJob))

Both rival accounts shift the past tense antecedent. Before the interview, if the interview went well, John gets the job comes out true on Schulz's and Kaufmann's accounts, its antecedent read at the co-temporal future moments after the interview.

theorem RumbergLauer2023.Interview.no_shifted_antecedent_moment (n : Interview) : ¬Minimal (fun (n : Interview) => now ≤ n ∧ (now, n) ∈ Transition.past (Transition.atom wentWell)) n

The transition account cannot shift a past tense antecedent. No course beyond the actual past is minimal for it, so before the interview the antecedent has no minimal course at all.