Initial and Final Parts (via Precedence)

@cite{krifka-1998} @cite{krifka-1989}

A part e' of a whole e is INITIAL iff no other part precedes e', FINAL iff no other part follows e'. Generic over a partial order and a precedence relation; specialize with Event.precedes for events (Theories/Semantics/Events/Adjacency.lean).

These are the substrate predicates for the planned propositional TEL predicate that captures K98 §2.5 eq. 37 (every part of a P-event that is also P is both initial and final), which is strictly weaker than QUA. (Previously also for K98 §4.5 SOURCE/GOAL — those were dropped during the MovementRelations cleanup since K98 states them as necessary conditions on movement relations, not as definitions.)

def Semantics.Events.InitialFinalParts.IsInitialPart {β : Type u_1} [PartialOrder β] (precedes : β → β → Prop) (e' e : β) : Prop

K98 §2.5 eq. 36 INI: e' is an initial part of e iff e' ≤ e and no other part of e precedes e'. Generic over a part order and a precedence relation; specialize with Event.precedes for events.

Equations

• Semantics.Events.InitialFinalParts.IsInitialPart precedes e' e = (e' ≤ e ∧ ¬∃ (e'' : β), e'' ≤ e ∧ precedes e'' e')

def Semantics.Events.InitialFinalParts.IsFinalPart {β : Type u_1} [PartialOrder β] (precedes : β → β → Prop) (e' e : β) : Prop

K98 §2.5 eq. 36 FIN: e' is a final part of e iff e' ≤ e and no other part of e follows e'.

Equations

• Semantics.Events.InitialFinalParts.IsFinalPart precedes e' e = (e' ≤ e ∧ ¬∃ (e'' : β), e'' ≤ e ∧ precedes e' e'')

theorem Semantics.Events.InitialFinalParts.isInitialPart_self {β : Type u_1} [PartialOrder β] (precedes : β → β → Prop) (e : β) (h : ¬∃ (e'' : β), e'' ≤ e ∧ precedes e'' e) : IsInitialPart precedes e e

The whole is trivially an initial part of itself when no proper part precedes it (vacuously true if precedence is empty).

theorem Semantics.Events.InitialFinalParts.isFinalPart_self {β : Type u_1} [PartialOrder β] (precedes : β → β → Prop) (e : β) (h : ¬∃ (e'' : β), e'' ≤ e ∧ precedes e e'') : IsFinalPart precedes e e

The whole is trivially a final part of itself when no proper part follows it.

def Semantics.Events.InitialFinalParts.IsTelic {β : Type u_1} [PartialOrder β] (precedes : β → β → Prop) (P : β → Prop) : Prop

K98 §2.5 eq. 37 propositional telicity (TEL). A predicate P is telic iff every P-instance e' that is part of a P-instance e is both an initial part and a final part of e. K98 page 9: "all parts of e that fall under X are initial and final parts of e."

Strictly weaker than QUA: every QUA predicate is TEL because it has no proper P-parts (vacuously initial-and-final), but not every TEL predicate is QUA — K98's run-time-3-4pm counterexample on page 9 is a telic predicate that isn't quantized.

Equations

• One or more equations did not get rendered due to their size.