Branching time

The branching-time model of Prior and Thomason depicts the open future as an order of moments that is linear towards the past and branches towards the future: a left-linear partial order (Core.Order.IsLeftLinear). A history is a complete possible course of the world, a maximal chain of moments, mathlib's Flag; the histories through a moment are its possible futures (histories). Propositions are sets, of moments or of moment–history pairs.

The two classic postsemantics evaluate the future operator differently. Peircean truth is at a moment, and future truth requires settledness: a later witness on every history through the moment (Peircean.future). Ockhamist truth is at a moment–history pair, future truth is a later witness on the fixed history (Ockhamist.future), and settledness is a quantifier over the histories through the moment (Ockhamist.settled). The history parameter is not fixed by a context of utterance, since there is no actual future; only the moment is, which is why settledness carries the felicity facts. The Peircean future is the settled Ockhamist future (Ockhamist.settled_future_atom). On a finite frame every history is the down-set of a maximal moment, so settledness is decidable.

Main definitions

• histories: the histories through a moment.
• Peircean.past, Peircean.future: the Peircean operators on sets of moments.
• Ockhamist.atom, Ockhamist.past, Ockhamist.future, Ockhamist.settled: the Ockhamist operators on sets of moment–history pairs.

Main results

• histories_antitone, histories_eq_singleton, histories_inter_nonempty_iff: later moments lie on fewer histories, a maximal moment lies on exactly one, and two moments share a history exactly when they are comparable.
• Ockhamist.settled_atom, Ockhamist.settled_future_atom: atomic propositions are settled, and the Peircean future is the settled Ockhamist future.
• Ockhamist.mem_past_atom_iff, Ockhamist.mem_future_atom_iff: the Ockhamist operators quantify along the relations of the library's tense cells.
• Peircean.mem_future_iff: on a finite frame settled future truth is a bounded search over the maximal moments, hence decidable.

Implementation notes

Historical connectedness, the condition that any two moments share a common past, figures in no theorem here, so it is not bundled into a frame class; theorems assume the exact mixins they use.

References

• [Pri67]
• [RL23]

Histories

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

The histories through a moment are the maximal chains containing it, written Hist(m) in the branching-time literature.

Equations

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

@[simp]

theorem BranchingTime.mem_histories {M : Type u_1} [PartialOrder M] {m : M} {h : Flag M} : h ∈ histories m ↔ m ∈ h

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

Every moment lies on a history.

theorem BranchingTime.histories_antitone {M : Type u_1} [PartialOrder M] [IsLeftLinear M] : Antitone histories

Later moments lie on fewer histories.

theorem BranchingTime.histories_eq_singleton {M : Type u_1} [PartialOrder M] [IsLeftLinear M] {x : M} (hx : IsMax x) : histories x = {Flag.ofIsMax hx}

A maximal moment lies on exactly one history, its past.

theorem BranchingTime.histories_inter_nonempty_iff {M : Type u_1} [PartialOrder M] [IsLeftLinear M] {m n : M} : (histories m ∩ histories n).Nonempty ↔ m ≤ n ∨ n ≤ m

Two moments share a history exactly when they are comparable.

The Peircean postsemantics

Sentences are evaluated at a moment, and future truth is settled truth.

def BranchingTime.Peircean.past {M : Type u_1} [PartialOrder M] (φ : Set M) : Set M

The Peircean past of a proposition holds where it held at an earlier moment.

Equations

• BranchingTime.Peircean.past φ = {m : M | ∃ m' < m, m' ∈ φ}

def BranchingTime.Peircean.future {M : Type u_1} [PartialOrder M] (φ : Set M) : Set M

The Peircean future of a proposition holds where every history through the moment has a later witness. This is settled future truth, historical inevitability.

Equations

• BranchingTime.Peircean.future φ = {m : M | ∀ h ∈ BranchingTime.histories m, ∃ m' ∈ h, m < m' ∧ m' ∈ φ}

@[simp]

theorem BranchingTime.Peircean.mem_past {M : Type u_1} [PartialOrder M] {φ : Set M} {m : M} : m ∈ past φ ↔ ∃ m' < m, m' ∈ φ

@[simp]

theorem BranchingTime.Peircean.mem_future {M : Type u_1} [PartialOrder M] {φ : Set M} {m : M} : m ∈ future φ ↔ ∀ h ∈ histories m, ∃ m' ∈ h, m < m' ∧ m' ∈ φ

The Ockhamist postsemantics

Sentences are evaluated at a moment–history pair, future truth is truth later on the given history, and settledness quantifies over the histories through the moment.

def BranchingTime.Ockhamist.atom {M : Type u_1} [PartialOrder M] (φ : Set M) : Set (M × Flag M)

A proposition of moments read at any history.

Equations

• BranchingTime.Ockhamist.atom φ = Prod.fst ⁻¹' φ

def BranchingTime.Ockhamist.past {M : Type u_1} [PartialOrder M] (φ : Set (M × Flag M)) : Set (M × Flag M)

The Ockhamist past of a proposition holds where it held at an earlier moment, on the same history.

Equations

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

def BranchingTime.Ockhamist.future {M : Type u_1} [PartialOrder M] (φ : Set (M × Flag M)) : Set (M × Flag M)

The Ockhamist future of a proposition holds where a later moment of the fixed history is a witness.

Equations

• BranchingTime.Ockhamist.future φ = {p : M × Flag M | ∃ m' ∈ p.2, p.1 < m' ∧ (m', p.2) ∈ φ}

def BranchingTime.Ockhamist.settled {M : Type u_1} [PartialOrder M] (φ : Set (M × Flag M)) : Set (M × Flag M)

A proposition is settled where it holds at the moment on every history through it. The history coordinate of the index is idle, since settledness quantifies it away.

Equations

• BranchingTime.Ockhamist.settled φ = {p : M × Flag M | ∀ h ∈ BranchingTime.histories p.1, (p.1, h) ∈ φ}

@[simp]

theorem BranchingTime.Ockhamist.mem_atom {M : Type u_1} [PartialOrder M] {m : M} {h : Flag M} {φ : Set M} : (m, h) ∈ atom φ ↔ m ∈ φ

@[simp]

theorem BranchingTime.Ockhamist.mem_past {M : Type u_1} [PartialOrder M] {φ : Set (M × Flag M)} {m : M} {h : Flag M} : (m, h) ∈ past φ ↔ ∃ m' < m, (m', h) ∈ φ

@[simp]

theorem BranchingTime.Ockhamist.mem_future {M : Type u_1} [PartialOrder M] {φ : Set (M × Flag M)} {m : M} {h : Flag M} : (m, h) ∈ future φ ↔ ∃ m' ∈ h, m < m' ∧ (m', h) ∈ φ

@[simp]

theorem BranchingTime.Ockhamist.mem_settled {M : Type u_1} [PartialOrder M] {φ : Set (M × Flag M)} {m : M} {h : Flag M} : (m, h) ∈ settled φ ↔ ∀ h' ∈ histories m, (m, h') ∈ φ

@[simp]

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

Atomic propositions are settled, since the valuation depends only on the moment.

theorem BranchingTime.Ockhamist.settled_past_atom {M : Type u_1} [PartialOrder M] (φ : Set M) : settled (past (atom φ)) = atom (Peircean.past φ)

The settled past of an atom is the Peircean past, since the past does not depend on the history.

theorem BranchingTime.Ockhamist.settled_future_atom {M : Type u_1} [PartialOrder M] (φ : Set M) : settled (future (atom φ)) = atom (Peircean.future φ)

The settled future of an atom is the Peircean future.

Grounding in the library's tense cells

The Ockhamist past and future quantify along the relations of the library's tense cells (Tense.toSetRel), which relate a moment to the moments below it and above it in the order of the frame. The witness of the future is kept on the history of evaluation.

theorem BranchingTime.Ockhamist.mem_past_atom_iff {M : Type u_1} [PartialOrder M] (φ : Set M) (m : M) (h : Flag M) : (m, h) ∈ past (atom φ) ↔ m ∈ (Tense.toSetRel (Semantics.Denotes.denote Tense.past)).preimage φ

theorem BranchingTime.Ockhamist.mem_future_atom_iff {M : Type u_1} [PartialOrder M] (φ : Set M) (m : M) (h : Flag M) : (m, h) ∈ future (atom φ) ↔ m ∈ (Tense.toSetRel (Semantics.Denotes.denote Tense.future)).preimage (↑h ∩ φ)

Finite frames

On a finite frame every history is the down-set of a maximal moment (Flag.exists_isMax_eq_ofIsMax), so quantifying over the histories through a moment is quantifying over the maximal moments above it, and settled future truth is decidable.

theorem BranchingTime.Peircean.mem_future_iff {M : Type u_1} [PartialOrder M] [IsLeftLinear M] [Finite M] {φ : Set M} {m : M} : m ∈ future φ ↔ ∀ (x : M), IsMax x → m ≤ x → ∃ (m' : M), m < m' ∧ m' ≤ x ∧ m' ∈ φ

Settled future truth on a finite frame is a search over the maximal moments.

@[instance_reducible]

instance BranchingTime.Peircean.instDecidableMemSetFutureOfIsLeftLinear {M : Type u_1} [PartialOrder M] [Fintype M] [DecidableLE M] [DecidableLT M] (φ : Set M) [DecidablePred fun (x : M) => x ∈ φ] (m : M) [IsLeftLinear M] : Decidable (m ∈ future φ)

Equations

• BranchingTime.Peircean.instDecidableMemSetFutureOfIsLeftLinear φ m = decidable_of_iff (∀ (x : M), IsMax x → m ≤ x → ∃ (m' : M), m < m' ∧ m' ≤ x ∧ m' ∈ φ) ⋯

@[instance_reducible]

instance BranchingTime.Peircean.instDecidableMemSetPast {M : Type u_1} [PartialOrder M] [Fintype M] [DecidableLT M] (φ : Set M) [DecidablePred fun (x : M) => x ∈ φ] (m : M) : Decidable (m ∈ past φ)

Equations

• BranchingTime.Peircean.instDecidableMemSetPast φ m = { decide := decide (∃ a ∈ Finset.univ, (fun (m' : M) => m' < m ∧ m' ∈ φ) a), reflects_decide := ⋯ }