Docs / Semantics / Events / Lifespan

Life spans

import Linglib.Semantics.Events.Lifespan · namespace Event

Source

The life span of an individual is the interval of times at which it exists: the run time of an event, or the time from an entity's coming into existence to its going out of it. A description pre-exists an interval when some individual it describes has a life span starting before the interval does, that is, when its life spans are before ever the interval (Tense.beforeEver). A predicate of individuals at times is permanent when it holds of an individual throughout its life span if it holds of it at all, as individual-level predicates such as tall are taken to be.

Main definitions

  • Event.PreExists τ Q t: the description Q pre-exists the interval t.
  • Event.Permanent span P: P holds of an individual throughout its life span if at all.

Main statements

Implementation notes

Life spans are given by a function τ into NonemptyInterval, as an event's run time is (Event.τ), so a description denotes the run times τ '' {x | Q x}, as an event predicate does in Semantics/Tense/RunTimes.lean. Permanent takes life spans of any type with a membership relation, such as intervals or sets of times, and Permanent.precedes_pure takes them as intervals, since it needs them convex.

References

Pre-existence

The description Q pre-exists the interval t when the life spans of its individuals are before ever t.

def PreExistsL61–64
{X : Type u_1} {T : Type u_2} [Preorder T] (τ : X → NonemptyInterval T) (Q : X → Prop) (t : NonemptyInterval T) :
Prop

Used by preExists_iff, PreExists.exists, PreExists.mono, PreExists.mono_right, preExists_eq_iff, preExists_of_precedes, preExists_iff_exists_of_precedes, not_preExists_of_le

Used in Semantics/ArgumentStructure/AgentivityLattice/OfLifespan, Bondarenko2020, Musan1995, Williams2025

theorem preExists_iffL68–69
{X : Type u_1} {T : Type u_2} [Preorder T] {τ : X → NonemptyInterval T} {Q : X → Prop} {t : NonemptyInterval T} :
PreExists τ Q t ↔ ∃ (x : X), Q x ∧ (τ x).toProd.1 < t.toProd.1

Built from

L77–79
L81–83
L87–88
L90–91

A description of individuals preceding an interval pre-exists it exactly when it describes something.

theorem preExists_iff_exists_of_precedesL93–97
{X : Type u_1} {T : Type u_2} [Preorder T] {τ : X → NonemptyInterval T} {Q : X → Prop} {t : NonemptyInterval T} (h : ∀ (x : X), Q x → (τ x).Precedes t) :
PreExists τ Q t ↔ ∃ (x : X), Q x

Built from

A description of individuals within an interval never pre-exists it.

theorem not_preExists_of_leL99–102
{X : Type u_1} {T : Type u_2} [Preorder T] {τ : X → NonemptyInterval T} {Q : X → Prop} {t : NonemptyInterval T} (h : ∀ (x : X), Q x → τ x ≤ t) :
¬PreExists τ Q t

Built from

Permanent predicates

L119–123

A permanent predicate that holds only within life spans holds of an individual at no time or at exactly the times of its life span.

theorem Permanent.forall_not_or_forall_iff_memL125–131
{X : Type u_1} {T : Type u_2} {S : Type u_3} [Membership T S] {span : X → S} {P : X → T → Prop} {x : X} (hP : Permanent span P) (hd : ∀ (t : T), P x t → t ∈ span x) :
(∀ (t : T), ¬P x t) ∨ ∀ (t : T), P x t ↔ t ∈ span x

Built from

A permanent predicate that held of an individual at a time of its life span before now and fails at now places the individual's life span before now.

theorem Permanent.precedes_pureL133–139
{X : Type u_1} {T : Type u_2} {P : X → T → Prop} {x : X} [LinearOrder T] {τ : X → NonemptyInterval T} (hP : Permanent τ P) {t now : T} (ht : t ∈ τ x) (hPt : P x t) (hlt : t < now) (hnow : ¬P x now) :
(τ x).Precedes (NonemptyInterval.pure now)

Built from