Pre-existence

An individual pre-exists a time when its time span, the run time of an event or the life span of an entity, starts before that time. [Bon20] derives the factive inference of Buryat hanaxa 'think' with a nominal complement from a presupposition that the complement describes something that pre-exists the thinking, and [Wil25] places a covert modal under English forget exactly where the complement would otherwise contradict the same presupposition.

Pre-existence entails existence (Event.PreExists.exists), which is how it yields a factive inference. What it adds depends on where a description locates its individuals: one that locates them before the time pre-exists it as soon as it describes anything (Event.preExists_iff_exists_of_precedes), and one that locates them within the time never does (Event.not_preExists_of_le).

[Bon20] takes the presupposition to come from the head that introduces a verb's internal argument, which also gives verbs of destruction and use theirs (Sue broke a vase), so it is not specific to attitude verbs.

Main definitions

• Event.PreExists τ Q a: some individual of Q has a time span starting before a.

Main statements

• Event.PreExists.exists: pre-existence entails existence.
• Event.preExists_iff_exists_of_precedes, Event.not_preExists_of_le: pre-existence under descriptions that locate their individuals before, or within, a time.

Implementation notes

The time spans are given by a function τ into NonemptyInterval, as an event's run time (Event.τ) or an entity's life span. Pre-existence compares left boundaries only, and leaves the right boundary free, so an individual can outlast the time it pre-exists ([Bon20]'s (10)).

References

• [Bon20]
• [Wil25]

def Event.PreExists {X : Type u_1} {T : Type u_2} [Preorder T] (τ : X → NonemptyInterval T) (Q : X → Prop) (a : T) : Prop

Some individual of Q pre-exists a: its time span starts before a.

Equations

• Event.PreExists τ Q a = ∃ (x : X), Q x ∧ (τ x).toProd.1 < a

theorem Event.PreExists.exists {X : Type u_1} {T : Type u_2} [Preorder T] {τ : X → NonemptyInterval T} {Q : X → Prop} {a : T} (h : PreExists τ Q a) : ∃ (x : X), Q x

Pre-existence entails existence.

theorem Event.PreExists.mono {X : Type u_1} {T : Type u_2} [Preorder T] {τ : X → NonemptyInterval T} {Q Q' : X → Prop} {a : T} (hQ : ∀ (x : X), Q x → Q' x) (h : PreExists τ Q a) : PreExists τ Q' a

theorem Event.PreExists.mono_right {X : Type u_1} {T : Type u_2} [Preorder T] {τ : X → NonemptyInterval T} {Q : X → Prop} {a b : T} (hab : a ≤ b) (h : PreExists τ Q a) : PreExists τ Q b

What pre-exists a time pre-exists every later one.

@[simp]

theorem Event.preExists_eq_iff {X : Type u_1} {T : Type u_2} [Preorder T] {τ : X → NonemptyInterval T} {a : T} {x : X} : PreExists τ (fun (x_1 : X) => x_1 = x) a ↔ (τ x).toProd.1 < a

A single individual pre-exists a time when its time span starts before it.

theorem Event.preExists_of_precedes {X : Type u_1} {T : Type u_2} [Preorder T] {τ : X → NonemptyInterval T} {Q : X → Prop} {t : NonemptyInterval T} {x : X} (hx : Q x) (h : (τ x).Precedes t) : PreExists τ Q t.toProd.1

An individual preceding an interval pre-exists it.

theorem Event.preExists_iff_exists_of_precedes {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.toProd.1 ↔ ∃ (x : X), Q x

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

theorem Event.not_preExists_of_le {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.toProd.1

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