Docs / Semantics / ArgumentStructure / AgentivityLattice / OfLifespan

Persistence from life spans

import Linglib.Semantics.ArgumentStructure.AgentivityLattice.OfLifespan · namespace ArgumentStructure.PersistenceLevel

Grimm's persistence features say whether a participant exists, and keeps its qualities, at the beginning and at the end of an event. Given the participant's life span, the event's run time and the participant's qualities over time, Grimm's descriptions of the persistence levels assign the participant a level, and its features are the persistence features the participant has. A created participant, existing at the end of the event but not at the beginning, does not pre-exist the event, and a destroyed one goes out of existence before the event ends.

Main definitions

PersistenceLevel.ofLifespan: the persistence level of a participant in an event.

Main statements

PersistenceLevel.exPersBeginning_le_ofLifespan_iff: a participant is at existential persistence (beginning) or above exactly when it exists when the event begins.
PersistenceLevel.not_preExists_of_ofLifespan_eq_exPersEnd: a created participant does not pre-exist the event.
PersistenceLevel.snd_lt_of_ofLifespan_eq_exPersBeginning: a destroyed participant goes out of existence before the event ends.

Implementation notes

A participant persists existentially at a boundary of the event when the boundary lies in its life span. Its qualities are a function q of times, and it persists qualitatively at the end when it exists there with the qualities it had at the beginning, if it existed then. Only the boundaries of the event are compared, so a quality that changes and changes back counts as persisting. A predicate's persistence level for an argument, the features it entails for every participant, is not formalized.

References

Grimm 2011, Semantics of Case formalized

Declarations

The persistence level of a participant with life span life and qualities q in an event with run time run, by Grimm's descriptions: a participant existing at neither end does not persist, one existing only at the beginning or only at the end persists existentially there, and one existing at both ends persists totally or only at the beginning as its qualities are unchanged or not (Grimm 2011 pp. 524–525).

def ofLifespan L49–58

{T : Type u_1} {Q : Type u_2} [LinearOrder T] [DecidableEq Q] (life run : NonemptyInterval T) (q : T → Q) :

PersistenceLevel

The definition is too large to print here; read it in the source.

Used by ofLifespan_eq_totalNonPersistence_iff, ofLifespan_eq_exPersEnd_iff, ofLifespan_eq_exPersBeginning_iff, ofLifespan_eq_quPersBeginning_iff, ofLifespan_eq_totalPersistence_iff, exPersBeginning_le_ofLifespan_iff, fst_lt_of_ofLifespan_eq_exPersEnd, not_preExists_of_ofLifespan_eq_exPersEnd, snd_lt_of_ofLifespan_eq_exPersBeginning

Used in Grimm2011

A participant is at existential persistence (beginning) or above exactly when it exists when the event begins.

theorem exPersBeginning_le_ofLifespan_iff L82–86

{T : Type u_1} {Q : Type u_2} [LinearOrder T] [DecidableEq Q] {life run : NonemptyInterval T} {q : T → Q} :

exPersBeginning ≤ ofLifespan life run q ↔ run.toProd.1 ∈ life

Built from

L88–91

A participant created in an event, existing at its end but not at its beginning, does not pre-exist it (Grimm 2011 (5)).

theorem not_preExists_of_ofLifespan_eq_exPersEnd L93–98

{T : Type u_1} {Q : Type u_2} [LinearOrder T] [DecidableEq Q] {run : NonemptyInterval T} {q : T → Q} {X : Type u_3} {σ : X → NonemptyInterval T} {x : X} (h : ofLifespan (σ x) run q = exPersEnd) :

¬Event.PreExists σ (fun (x_1 : X) => x_1 = x) run

Built from

A participant destroyed in an event, existing at its beginning but not at its end, goes out of existence before the event ends.

theorem snd_lt_of_ofLifespan_eq_exPersBeginning L100–105

{T : Type u_1} {Q : Type u_2} [LinearOrder T] [DecidableEq Q] {life run : NonemptyInterval T} {q : T → Q} (h : ofLifespan life run q = exPersBeginning) :

life.toProd.2 < run.toProd.2

Built from