[Kri98] The Origins of Telicity

Exercises the K98 incrementality (§3) and movement (§4) substrate with the paper's deepest results: CUM/QUA propagation, telicity by initial/final parts, and the path-bounded movement-relation analysis.

The substrate predicates (MO, MSO, MSE, SINC, INC, CumTheta — K98 §3.2) live in Semantics/Events/; the σ-trace pullback in Semantics/Spatial/Trace.lean. This file inlines the §4 movement-relation predicates (formerly in Semantics/Events/MovementRelations.lean).

Main definitions

• IsInitialPart / IsFinalPart / IsTelic — K98 §2.5 telicity, with isTelic_of_qua the QUA → TEL direction.
• EXP / SEINC / ADJ / SMR / MovementClosure / MR — K98 §4 movement substrate (TANG_H-free), with mr_of_smr and the Event Time instantiations expEv / seincEv / smrPath / mrPath.

Main statements

• eat_apples_cum_propositional / eat_two_apples_qua_propositional — K98 §3.3 CUM/QUA propagation on abstract θ, fired on a constructive IsSincVerb toy (eat_two_apples_toy_qua, eat_some_apples_toy_cum).
• telic_licenses_inX / durative_atelic_licenses_forX — §3 for/in diagnostics.
• walked_from_to_telic_propositional / walked_towards_atelic_propositional — σ-pullback backing the walked from X to Y / walked towards X analyses.
• pathShapeToTelicity_matches_motionData — the substrate reproduces the §4.5 path-shape → telicity judgments of the Data.Examples.Krifka1998 motion rows.

TODO

• TEL ⊋ QUA strict witness: a telic non-QUA predicate (K98's 3-to-4-pm case) needs a concrete event model; isTelic_of_qua covers only QUA → TEL.
• TANG_H tangentiality (K98 eq. 17) on directed paths, without which MR admits telekinetic concatenations (K98 eq. 70.c).
• Cross-dimensional movements (K98 §4.6: heat, bake, whip).
• Full ADJ axioms on adjacency (K98 §2.3 eq. 14.b).

K98 §3.3 propagation (typeclass form)

`cum_propagation` / `qua_propagation` on abstract θ + OBJ instances. 

theorem Krifka1998.eat_apples_cum_propositional {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} [ArgumentStructure.IsCumThetaVerb θ] {Apples : α → Prop} (hApples : Mereology.CUM Apples) : Mereology.CUM (Semantics.Aspect.Cumulativity.VP θ Apples)

eat apples (K98 §3.3): a CUM object through any θ propagates to a CUM VP.

theorem Krifka1998.eat_two_apples_qua_propositional {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} [Semantics.Aspect.Incremental.IsSincVerb θ] {TwoApples : α → Prop} (hTwoApples : Mereology.QUA TwoApples) : Mereology.QUA (Semantics.Aspect.Cumulativity.VP θ TwoApples)

eat two apples (K98 §3.3): a QUA object through a SINC verb gives a QUA VP.

Diagnostic Bridge

CUM/QUA → for/in diagnostic compatibility: atelic (CUM) VPs accept "for X", telic (QUA) VPs accept "in X".

theorem Krifka1998.telic_licenses_inX (c : Features.VendlerClass) (h : c.telicity = Features.Telicity.telic) : Features.inXPrediction c = Features.DiagnosticResult.accept

Telic VPs (QUA) license "in X" adverbials.

theorem Krifka1998.durative_atelic_licenses_forX (c : Features.VendlerClass) (h : c.telicity = Features.Telicity.atelic) (hd : c.duration = Features.Duration.durative) : Features.forXPrediction c = Features.DiagnosticResult.accept

Durative atelic (CUM) VPs license "for X" adverbials.

Concrete IsSincVerb Toy + Applied Propagation

@[reducible, inline]

abbrev Krifka1998.Apple : Type

Toy 3-apple universe: Finset (Fin 3) with ⊔ = ∪ and ≤/< as ⊆/⊊.

Equations

• Krifka1998.Apple = Finset (Fin 3)

@[reducible, inline]

abbrev Krifka1998.EatEvent : Type

Toy eating event, identified with the set of apples eaten (same lattice as Apple).

Equations

• Krifka1998.EatEvent = Finset (Fin 3)

def Krifka1998.eatThemeToy (a : Apple) (e : EatEvent) : Prop

The identity theme eatThemeToy a e := a = e, the canonical SINC example.

Equations

• Krifka1998.eatThemeToy a e = (a = e)

instance Krifka1998.instIsSincVerbAppleEatEventEatThemeToy : Semantics.Aspect.Incremental.IsSincVerb eatThemeToy

eatThemeToy is a strictly incremental verb-theme relation (via IsSincVerb.mk').

Concrete OBJ predicates

def Krifka1998.twoApples : Apple → Prop

"two specific apples": the singleton predicate (· = {0, 1}), QUA.

Equations

• Krifka1998.twoApples a = (a = {0, 1})

def Krifka1998.someApples : Apple → Prop

"(some) apples": non-emptiness, the toy's CUM bare plural.

Equations

• Krifka1998.someApples a = Finset.Nonempty a

theorem Krifka1998.twoApples_qua : Mereology.QUA twoApples

twoApples is QUA: a singleton predicate is trivially an antichain.

theorem Krifka1998.someApples_cum : Mereology.CUM someApples

someApples is CUM: nonempty ⊔ nonempty is nonempty.

K98 §3.3 propagation theorems fire on the toy

theorem Krifka1998.eat_two_apples_toy_qua : Mereology.QUA (Semantics.Aspect.Cumulativity.VP eatThemeToy twoApples)

eat two apples on the toy: SINC verb + QUA object → QUA VP.

theorem Krifka1998.eat_some_apples_toy_cum : Mereology.CUM (Semantics.Aspect.Cumulativity.VP eatThemeToy someApples)

eat (some) apples on the toy: CumTheta verb + CUM object → CUM VP.

def Krifka1998.IsInitialPart {β : Type u_2} [PartialOrder β] (precedes : β → β → Prop) (e' e : β) : Prop

K98 §2.5 eq. 36 INI: e' ≤ e and no part of e precedes e' (printed ≤D read as ≤).

Equations

• Krifka1998.IsInitialPart precedes e' e = (e' ≤ e ∧ ¬∃ e'' ≤ e, precedes e'' e')

def Krifka1998.IsFinalPart {β : Type u_2} [PartialOrder β] (precedes : β → β → Prop) (e' e : β) : Prop

K98 §2.5 eq. 36 FIN: e' ≤ e and no part of e follows e'.

Equations

• Krifka1998.IsFinalPart precedes e' e = (e' ≤ e ∧ ¬∃ e'' ≤ e, precedes e' e'')

theorem Krifka1998.isInitialPart_self {β : Type u_2} [PartialOrder β] (precedes : β → β → Prop) (e : β) (h : ¬∃ e'' ≤ e, precedes e'' e) : IsInitialPart precedes e e

The whole is an initial part of itself when no part of it precedes it.

theorem Krifka1998.isFinalPart_self {β : Type u_2} [PartialOrder β] (precedes : β → β → Prop) (e : β) (h : ¬∃ e'' ≤ e, precedes e e'') : IsFinalPart precedes e e

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

def Krifka1998.IsTelic {β : Type u_2} [PartialOrder β] (precedes : β → β → Prop) (P : β → Prop) : Prop

K98 §2.5 eq. 37 TEL: every P-part of a P-instance is its initial and final part.

Equations

• Krifka1998.IsTelic precedes P = ∀ (e e' : β), P e → P e' → e' ≤ e → Krifka1998.IsInitialPart precedes e' e ∧ Krifka1998.IsFinalPart precedes e' e

theorem Krifka1998.isTelic_of_qua {β : Type u_2} [PartialOrder β] (precedes : β → β → Prop) {P : β → Prop} (hax : ∀ (a b : β), a ≤ b → ¬precedes a b ∧ ¬precedes b a) (hQ : Mereology.QUA P) : IsTelic precedes P

K98 §2.5: quantized predicates are telic (QUA → TEL), given hax (K98 eq. 35).

K98 §4 propositional substrate

def Krifka1998.EXP {α : Type u_1} {β : Type u_2} [PartialOrder α] (precedes : β → β → Prop) (θ : α → β → Prop) : Prop

K98 §4.1 eq. 63 EXP: θ-arguments of temporally-ordered events do not overlap.

Equations

• Krifka1998.EXP precedes θ = ∀ (x y : α) (e e' : β), θ x e → θ y e' → precedes e e' → ¬Mereology.Overlap x y

def Krifka1998.SEINC {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (precedes : β → β → Prop) (θ : α → β → Prop) : Prop

K98 §4.1 eq. 65 SEINC: strictly expansive incremental. EXP ∧ MO.

Equations

• Krifka1998.SEINC precedes θ = (Krifka1998.EXP precedes θ ∧ ArgumentStructure.MO θ)

def Krifka1998.ADJ {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (adjα : α → α → Prop) (adjβ : β → β → Prop) (θ : α → β → Prop) : Prop

K98 §4.2 eq. 68 ADJ: sub-event temporal adjacency ↔ sub-path spatial adjacency.

Equations

• Krifka1998.ADJ adjα adjβ θ = ∀ (x : α) (e : β) (y z : α) (e' e'' : β), θ x e → e' ≤ e → e'' ≤ e → y ≤ x → z ≤ x → θ y e' → θ z e'' → (adjβ e' e'' ↔ adjα y z)

def Krifka1998.SMR {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (adjα : α → α → Prop) (adjβ : β → β → Prop) (isPath : α → Prop) (θ : α → β → Prop) : Prop

K98 §4.2 eq. 69 SMR: ADJ + MO + first-arg constrained to paths.

Equations

• Krifka1998.SMR adjα adjβ isPath θ = (Krifka1998.ADJ adjα adjβ θ ∧ ArgumentStructure.MO θ ∧ ∀ (x : α) (e : β), θ x e → isPath x)

@[reducible, inline]

abbrev Krifka1998.MovementClosure {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (precedes : β → β → Prop) (θ' : α → β → Prop) : α → β → Prop

K98 §4.3 eq. 71: smallest θ-extension closed under precedence-respecting sums.

Equations

• Krifka1998.MovementClosure precedes θ' = Semantics.Aspect.PrecedenceClosure precedes θ'

def Krifka1998.MR {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (adjα : α → α → Prop) (adjβ precedes : β → β → Prop) (isPath : α → Prop) (θ : α → β → Prop) : Prop

K98 §4.3 eq. 71 MR (TANG_H-free): θ is the MovementClosure of some SMR θ'.

Equations

• Krifka1998.MR adjα adjβ precedes isPath θ = ∃ (θ' : α → β → Prop), Krifka1998.SMR adjα adjβ isPath θ' ∧ ∀ (x : α) (e : β), θ x e ↔ Krifka1998.MovementClosure precedes θ' x e

theorem Krifka1998.mr_of_smr {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {adjα : α → α → Prop} {adjβ precedes : β → β → Prop} {isPath : α → Prop} {θ : α → β → Prop} (h : SMR adjα adjβ isPath θ) (hClosed : ∀ (x1 x2 : α) (e1 e2 : β), θ x1 e1 → θ x2 e2 → precedes e1 e2 → θ (x1 ⊔ x2) (e1 ⊔ e2)) : MR adjα adjβ precedes isPath θ

Every SMR is itself an MR, given closure under precedence-respecting sums.

σ-pullback invocations (bounded/unbounded path → telic/atelic VP)

theorem Krifka1998.walked_from_to_telic_propositional {Loc : Type u_3} {Time : Type u_4} [LinearOrder Time] [Event.Mereology Time] [Mereology.ClassicalMereology (Event Time)] [SemilatticeSup (Semantics.Spatial.Path.Path Loc)] [st : Semantics.Spatial.Trace Loc Time] (hinj : Function.Injective Semantics.Spatial.Trace.σ) {P : Semantics.Spatial.Path.Path Loc → Prop} (hP : Mereology.QUA P) : Mereology.QUA (P ∘ Semantics.Spatial.Trace.σ)

Bounded path (QUA) ↦ telic VP via the σ-pullback (K98 §4.5 walked from X to Y).

theorem Krifka1998.walked_towards_atelic_propositional {Loc : Type u_3} {Time : Type u_4} [LinearOrder Time] [Event.Mereology Time] [Mereology.ClassicalMereology (Event Time)] [SemilatticeSup (Semantics.Spatial.Path.Path Loc)] [st : Semantics.Spatial.Trace Loc Time] {P : Semantics.Spatial.Path.Path Loc → Prop} (hP : Mereology.CUM P) : Mereology.CUM (P ∘ Semantics.Spatial.Trace.σ)

Unbounded path (CUM) ↦ atelic VP via the σ-pullback (K98 §4.5 walked towards X).

K98 §4.5 motion data: path shape predicts telicity

structure Krifka1998.MotionDatum : Type

A motion VP datum: the path shape K98 assigns and the telicity it predicts.

• pathShape : Semantics.Spatial.Path.PathShape
• expectedTelicity : Features.Telicity

def Krifka1998.instDecidableEqMotionDatum.decEq (x✝ x✝¹ : MotionDatum) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Krifka1998.instDecidableEqMotionDatum : DecidableEq MotionDatum

Equations

• Krifka1998.instDecidableEqMotionDatum = Krifka1998.instDecidableEqMotionDatum.decEq

def Krifka1998.instReprMotionDatum.repr : MotionDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Krifka1998.instReprMotionDatum : Repr MotionDatum

Equations

• Krifka1998.instReprMotionDatum = { reprPrec := Krifka1998.instReprMotionDatum.repr }

def Krifka1998.fromExample (e : Data.Examples.LinguisticExample) : Option MotionDatum

Lift a Data.Examples.Krifka1998 row to a MotionDatum via its paper features.

Equations

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

def Krifka1998.motionData : List MotionDatum

The K98 §4.5 motion VP data, lifted from the JSON example rows.

Equations

• Krifka1998.motionData = List.filterMap Krifka1998.fromExample Krifka1998.Examples.all

theorem Krifka1998.pathShapeToTelicity_matches_motionData (d : MotionDatum) : d ∈ motionData → Semantics.Spatial.Trace.pathShapeToTelicity d.pathShape = d.expectedTelicity

pathShapeToTelicity reproduces the paper's telicity for every motion VP.

EXP / SEINC instances on Event Time (K98 §4.1)

@[reducible, inline]

abbrev Krifka1998.expEv {α : Type u_1} [SemilatticeSup α] {Time : Type u_3} [LinearOrder Time] (θ : α → Event Time → Prop) : Prop

EXP-as-property of any θ : α → Event Time → Prop using Event.precedes.

Equations

• Krifka1998.expEv θ = Krifka1998.EXP Event.precedes θ

@[reducible, inline]

abbrev Krifka1998.seincEv {α : Type u_1} [SemilatticeSup α] {Time : Type u_3} [LinearOrder Time] [Event.Mereology Time] [Mereology.ClassicalMereology (Event Time)] (θ : α → Event Time → Prop) : Prop

SEINC-as-property of θ over Event Time using Event.precedes.

Equations

• Krifka1998.seincEv θ = Krifka1998.SEINC Event.precedes θ

SMR / MR instances on Path Loc → Event Time → Prop (K98 §4.2-4.3)

@[reducible, inline]

abbrev Krifka1998.smrPath {Loc : Type u_3} {Time : Type u_4} [LinearOrder Time] [Event.Mereology Time] [Mereology.ClassicalMereology (Event Time)] [SemilatticeSup (Semantics.Spatial.Path.Path Loc)] (θ : Semantics.Spatial.Path.Path Loc → Event Time → Prop) : Prop

SMR specialized to paths and events with concrete adjacency.

Equations

• Krifka1998.smrPath θ = Krifka1998.SMR Semantics.Spatial.Path.Path.adjacent Event.adjacent (fun (x : Semantics.Spatial.Path.Path Loc) => True) θ

@[reducible, inline]

abbrev Krifka1998.mrPath {Loc : Type u_3} {Time : Type u_4} [LinearOrder Time] [Event.Mereology Time] [Mereology.ClassicalMereology (Event Time)] [SemilatticeSup (Semantics.Spatial.Path.Path Loc)] (θ : Semantics.Spatial.Path.Path Loc → Event Time → Prop) : Prop

MR specialized to paths and events with concrete adjacency + precedence.

Equations

• Krifka1998.mrPath θ = Krifka1998.MR Semantics.Spatial.Path.Path.adjacent Event.adjacent Event.precedes (fun (x : Semantics.Spatial.Path.Path Loc) => True) θ