Quantificational tense

Read quantificationally, a tense quantifies over the times its cell admits, as in the tense logic of Prior: the past holds of a predicate at a time when the predicate holds at some earlier time. The quantificational tense of a cell is possibility ◇ along the cell's relation (Tense.toSetRel, and Tense.Perspective.toSetRel on intervals), so ◇[toSetRel ⟦past⟧] P t says that P held at some time before t, and necessity □ along the relation holds when P held at all of them. The laws of Logic/Modal then apply. The past and the future are converse relations, so sometime in the one is adjoint to always in the other. A tense under a tense entails the tense of the composed cell, and is that tense when time is dense and has no first or last moment. The past of a past is a past as soon as time is dense, the density law of tense logic.

Main statements

• Tense.diamond_toSetRel_past: the quantificational past holds when the predicate held at some earlier time.
• Tense.diamond_past_box_future_gc, Tense.diamond_future_box_past_gc: sometime in the past is left adjoint to always in the future, and sometime in the future to always in the past.
• Tense.diamond_diamond_toSetRel, Tense.diamond_toSetRel_comp: a quantificational tense under another entails the quantificational tense of the composed cell, and is that tense on dense time without endpoints.
• Tense.diamond_past_diamond_past: on dense time the past of a past is a past.

References

• [Pri67]

@[simp]

theorem Tense.diamond_toSetRel_past {T : Type u_1} {P : T → Prop} {t : T} [LT T] : ModalLogic.Diamond (toSetRel (Semantics.Denotes.denote past)) P t ↔ ∃ t' < t, P t'

@[simp]

theorem Tense.diamond_toSetRel_future {T : Type u_1} {P : T → Prop} {t : T} [LT T] : ModalLogic.Diamond (toSetRel (Semantics.Denotes.denote future)) P t ↔ ∃ t' > t, P t'

@[simp]

theorem Tense.diamond_toSetRel_present {T : Type u_1} [LT T] (P : T → Prop) : ModalLogic.Diamond (toSetRel (Semantics.Denotes.denote present)) P = P

@[simp]

theorem Tense.box_toSetRel_past {T : Type u_1} {P : T → Prop} {t : T} [LT T] : ModalLogic.Box (toSetRel (Semantics.Denotes.denote past)) P t ↔ ∀ t' < t, P t'

@[simp]

theorem Tense.box_toSetRel_future {T : Type u_1} {P : T → Prop} {t : T} [LT T] : ModalLogic.Box (toSetRel (Semantics.Denotes.denote future)) P t ↔ ∀ t' > t, P t'

theorem Tense.diamond_past_box_future_gc {T : Type u_1} [LT T] : GaloisConnection (ModalLogic.Diamond (toSetRel (Semantics.Denotes.denote past))) (ModalLogic.Box (toSetRel (Semantics.Denotes.denote future)))

Sometime in the past is left adjoint to always in the future.

theorem Tense.diamond_future_box_past_gc {T : Type u_1} [LT T] : GaloisConnection (ModalLogic.Diamond (toSetRel (Semantics.Denotes.denote future))) (ModalLogic.Box (toSetRel (Semantics.Denotes.denote past)))

Sometime in the future is left adjoint to always in the past.

theorem Tense.diamond_past_diamond_past {T : Type u_1} [Preorder T] [DenselyOrdered T] (P : T → Prop) : ModalLogic.Diamond (toSetRel (Semantics.Denotes.denote past)) (ModalLogic.Diamond (toSetRel (Semantics.Denotes.denote past)) P) = ModalLogic.Diamond (toSetRel (Semantics.Denotes.denote past)) P

On dense time the past of a past is a past, the density law of tense logic.

theorem Tense.diamond_diamond_toSetRel {T : Type u_1} {C D : Finset Ordering} {P : T → Prop} {t : T} [LinearOrder T] (h : ModalLogic.Diamond (toSetRel C) (ModalLogic.Diamond (toSetRel D) P) t) : ModalLogic.Diamond (toSetRel (comp D C)) P t

A quantificational tense under another entails the quantificational tense of the composed cell.

theorem Tense.diamond_toSetRel_comp {T : Type u_1} [LinearOrder T] [DenselyOrdered T] [NoMinOrder T] [NoMaxOrder T] (C D : Finset Ordering) (P : T → Prop) : ModalLogic.Diamond (toSetRel (comp D C)) P = ModalLogic.Diamond (toSetRel C) (ModalLogic.Diamond (toSetRel D) P)

On dense time without endpoints, the quantificational tense of a composed cell is one quantificational tense under the other.

@[simp]

theorem Tense.Perspective.diamond_toSetRel_past {T : Type u_1} [LinearOrder T] {π : NonemptyInterval T} {Q : NonemptyInterval T → Prop} : ModalLogic.Diamond (toSetRel (Semantics.Denotes.denote past)) Q π ↔ ∃ (r : NonemptyInterval T), r.Precedes π ∧ Q r

theorem Tense.Perspective.diamond_past_diamond_past {T : Type u_1} [LinearOrder T] [DenselyOrdered T] (Q : NonemptyInterval T → Prop) : ModalLogic.Diamond (toSetRel (Semantics.Denotes.denote past)) (ModalLogic.Diamond (toSetRel (Semantics.Denotes.denote past)) Q) = ModalLogic.Diamond (toSetRel (Semantics.Denotes.denote past)) Q

On dense time the past of a past is a past on intervals too.