@cite{krifka-1998} The Origins of Telicity

K98's two distinctive contributions, formalized end-to-end:

• Part I — §3 Incrementality (CUM/QUA propagation through SINC/INC verbs; Vendler classification; for/in diagnostics).
• Part II — §4 Movement (path/movement extension of mereological telicity: a movement event is telic iff its path is bounded; EXP / SEINC / ADJ / SMR / MovementClosure / MR propositional substrate).

The substrate predicates (SUM, UO, UE, MO, MSO, MSE, GUE, SINC, INC, CumTheta — K98 §3.2 eq. 43-52, eq. 59) live in Theories/Semantics/Events/{Incrementality,ThematicRoleProperties}.lean; the σ-trace pullback machinery in Theories/Semantics/Spatial/Trace.lean. This file exercises both on the English fragment and inlines the §4 movement-relation predicates (formerly in Theories/Semantics/Events/MovementRelations.lean).

Main definitions

Part I (§3 incrementality):

• Per-verb *_sinc / *_inc / *_cumOnly tripwire theorems
• VendlerClass → MereoTag bridge via Telicity.toMereoTag
• eat_two_apples_qua_propositional / eat_apples_cum_propositional — K98 §3.3 propagation invoked on abstract θ
• IsSincVerb (eatThemeToy) instance + applied propagation theorems (the constructive witness that the typeclass admits non-axiomatic realizations)
• K89 ↔ K98 sister-paper refinement bridge (uses K89ThematicClass.toVerbIncClass from Studies/Krifka1989.lean)

Part II (§4 movement):

• EXP / SEINC / ADJ / SMR — K98 §4 propositional predicates
• MovementClosure / MR — K98 §4.3 closure substrate (TANG_H-free)
• expEv / seincEv / smrPath / mrPath — Event Time instantiations
• MotionVPDatum / motionData — Bool-tag-level VP data
• walked_from_to_telic_propositional / walked_towards_atelic_propositional — σ-pullback theorems backing the K98 §4.5 walked from X to Y / walked towards X analyses

TODO

• TEL substrate: K98 §2.5 eq. 37 defines TEL strictly weaker than QUA. Linglib's Telicity.toMereoTag .telic = .qua collapse is an approximation; a faithful TEL would need INI/FIN initial/final-part predicates over events.
• TANG_H tangentiality (K98 eq. 17) on directed paths. Without it, MR admits telekinetic non-meeting concatenations (K98 eq. 70.c). Adding TANG_H requires a DirectedPath substrate not yet in linglib.
• Cross-dimensional movements (K98 §4.6: heat, bake, whip — eq. 76-77). Structurally identical to spatial movements; require the same DirectedPath generalization.
• Full ADJ axioms on adjacency (K98 §2.3 eq. 14.b). The concrete Path.adjacent + Event.adjacent satisfy them but the propositional theorems are not added.
• cumOnly is the formaliser's term, not K98's. K98 distinguishes verbs that are merely cumulative (CUM, eq. 44) without strict incrementality (¬SINC, ¬MSE). The VerbIncClass.cumOnly constructor name is anachronistic shorthand.

What this file is NOT

• Not a critique of K98's classification — that's Studies/Filip2012.lean (three-way CUM / QUA / ¬CUM ∧ ¬QUA via K98 §3.3 propagation).
• Not a fragment-only verb-annotation file — fragment annotations in Fragments/English/Predicates/Verbal.lean are tested per-verb here as a tripwire layer.

References

• @cite{krifka-1998} (primary, both §3 and §4 covered)
• @cite{krifka-1989} (sister paper: Studies/Krifka1989.lean)
• @cite{vendler-1957} (Vendler classes used in Part I § 6)
• @cite{filip-2012} (downstream critique: Studies/Filip2012.lean)

Per-Verb Incrementality Verification

Each verb's verbIncClass annotation is verified by rfl. Changing any annotation breaks exactly one theorem here. These earn their place as fragment-annotation tripwires; mathlib would call them examples, but as theorems they're discoverable via #check.

theorem Krifka1998.eat_sinc : Fragments.English.Predicates.Verbal.eat.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.sinc

"eat" is strictly incremental (consumption: bijective theme-event map).

theorem Krifka1998.devour_sinc : Fragments.English.Predicates.Verbal.devour.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.sinc

"devour" is strictly incremental (consumption variant of eat).

theorem Krifka1998.build_sinc : Fragments.English.Predicates.Verbal.build.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.sinc

"build" is strictly incremental (creation: bijective theme-event map).

theorem Krifka1998.write_sinc : Fragments.English.Predicates.Verbal.write.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.sinc

"write" is strictly incremental (creation verb).

theorem Krifka1998.read_inc : Fragments.English.Predicates.Verbal.read.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.inc

"read" is incremental but not strictly so (allows re-reading per K98 §3.6).

theorem Krifka1998.push_cumOnly : Fragments.English.Predicates.Verbal.push.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.cumOnly

"push" is cumulative only (no incremental theme — the formaliser's "cumOnly" is shorthand; K98 calls it CUM-without-MSE/MSO).

theorem Krifka1998.pull_cumOnly : Fragments.English.Predicates.Verbal.pull.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.cumOnly

"pull" is cumulative only.

theorem Krifka1998.carry_cumOnly : Fragments.English.Predicates.Verbal.carry.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.cumOnly

"carry" is cumulative only.

theorem Krifka1998.drag_cumOnly : Fragments.English.Predicates.Verbal.drag.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.cumOnly

"drag" is cumulative only.

theorem Krifka1998.sleep_no_inc : Fragments.English.Predicates.Verbal.sleep.verbIncClass = none

Intransitives have no incremental theme.

theorem Krifka1998.run_no_inc : Fragments.English.Predicates.Verbal.run.verbIncClass = none

theorem Krifka1998.arrive_no_inc : Fragments.English.Predicates.Verbal.arrive.verbIncClass = none

Unaccusatives have no incremental theme.

theorem Krifka1998.kick_no_inc : Fragments.English.Predicates.Verbal.kick.verbIncClass = none

Contact verbs have no incremental theme.

Per-Verb Vendler Class Verification

theorem Krifka1998.sleep_state : Fragments.English.Predicates.Verbal.sleep.vendlerClass = some Features.VendlerClass.state

"sleep" is a state.

theorem Krifka1998.run_activity : Fragments.English.Predicates.Verbal.run.vendlerClass = some Features.VendlerClass.activity

"run" is an activity.

theorem Krifka1998.arrive_achievement : Fragments.English.Predicates.Verbal.arrive.vendlerClass = some Features.VendlerClass.achievement

"arrive" is an achievement.

theorem Krifka1998.eat_accomplishment : Fragments.English.Predicates.Verbal.eat.vendlerClass = some Features.VendlerClass.accomplishment

"eat" is an accomplishment (with quantized object).

theorem Krifka1998.build_accomplishment : Fragments.English.Predicates.Verbal.build.vendlerClass = some Features.VendlerClass.accomplishment

"build" is an accomplishment.

theorem Krifka1998.read_accomplishment : Fragments.English.Predicates.Verbal.read.vendlerClass = some Features.VendlerClass.accomplishment

"read" is an accomplishment.

theorem Krifka1998.write_accomplishment : Fragments.English.Predicates.Verbal.write.vendlerClass = some Features.VendlerClass.accomplishment

"write" is an accomplishment.

theorem Krifka1998.kick_activity : Fragments.English.Predicates.Verbal.kick.vendlerClass = some Features.VendlerClass.activity

"kick" is an activity (semelfactive/contact).

theorem Krifka1998.see_state : Fragments.English.Predicates.Verbal.see.vendlerClass = some Features.VendlerClass.state

"see" is a state (perception).

theorem Krifka1998.leave_achievement : Fragments.English.Predicates.Verbal.leave.vendlerClass = some Features.VendlerClass.achievement

"leave" is an achievement.

theorem Krifka1998.push_activity : Fragments.English.Predicates.Verbal.push.vendlerClass = some Features.VendlerClass.activity

"push" is an activity.

theorem Krifka1998.love_state : Fragments.English.Predicates.Verbal.love.vendlerClass = some Features.VendlerClass.state

"love" is a state.

VendlerClass → MereoTag Bridge

These connect the Vendler classification to K89's CUM/QUA distinction via Telicity.toMereoTag. The chain is: VendlerClass → Telicity → MereoTag → CUM/QUA mereological property.

**Caveat: TEL ⊃ QUA in K98, but collapsed here.** K98 §2.5 (eq. 37,
page 9) defines TEL_E (telicity) strictly weaker than QUA
(quantization): every QUA predicate is TEL, but not every TEL
predicate is QUA (K98 gives the run-time-3-4pm counterexample on
page 9). The `Telicity.toMereoTag .telic = .qua` collapse used here
is faithful for the typical Vendler-class accomplishments and
achievements (which are both TEL and QUA), but a complete K98
formalization would need a separate propositional `TEL` predicate
distinct from `QUA`. Adding `def TEL` requires INI/FIN initial/final-
part predicates over events, which linglib's K98 theory doesn't
house — deferred. 

theorem Krifka1998.accomplishment_is_qua : Features.VendlerClass.accomplishment.telicity.toMereoTag = Core.Scale.MereoTag.qua

Accomplishments are telic, hence (under the TEL = QUA collapse) QUA.

theorem Krifka1998.achievement_is_qua : Features.VendlerClass.achievement.telicity.toMereoTag = Core.Scale.MereoTag.qua

Achievements are telic, hence QUA.

theorem Krifka1998.activity_is_cum : Features.VendlerClass.activity.telicity.toMereoTag = Core.Scale.MereoTag.cum

Activities are atelic, hence CUM.

theorem Krifka1998.state_is_cum : Features.VendlerClass.state.telicity.toMereoTag = Core.Scale.MereoTag.cum

States are atelic, hence CUM.

Compositional Telicity (VP = verb + NP)

The payoff: verb incrementality + NP reference property → VP telicity. These instantiate K98 §3.3 (eq. 53-54) for concrete verb entries.

Round-1 audit additions: propositional invocations of K98 theory's
`cum_propagation` and `qua_propagation` on abstract θ instances
(parallel to K89 study §3's `qmod_of_cum_is_qua` calls), making the
Bool-tag conjunctions below into substrate-honest derivations
rather than stipulated `⟨rfl, rfl⟩`. 

theorem Krifka1998.eat_apples_atelic : Fragments.English.Predicates.Verbal.eat.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.sinc ∧ Features.VendlerClass.activity.telicity.toMereoTag = Core.Scale.MereoTag.cum

"eat apples": sinc verb + CUM NP → CUM VP (atelic). K98 §3.3: CumTheta(θ) ∧ CUM(OBJ) → CUM(VP θ OBJ). The verb's incrementality class is sinc, and bare plurals are CUM.

theorem Krifka1998.eat_two_apples_telic : Fragments.English.Predicates.Verbal.eat.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.sinc ∧ Features.VendlerClass.accomplishment.telicity.toMereoTag = Core.Scale.MereoTag.qua

"eat two apples": sinc verb + QUA NP → QUA VP (telic). K98 §3.3: SINC(θ) ∧ QUA(OBJ) → QUA(VP θ OBJ). The verb's incrementality class is sinc, and "two apples" is QUA.

theorem Krifka1998.build_a_house_telic : Fragments.English.Predicates.Verbal.build.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.sinc ∧ Features.VendlerClass.accomplishment.telicity.toMereoTag = Core.Scale.MereoTag.qua

"build a house": sinc verb + QUA NP → QUA VP (telic).

theorem Krifka1998.read_the_book_telic : Fragments.English.Predicates.Verbal.read.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.inc ∧ Features.VendlerClass.accomplishment.telicity.toMereoTag = Core.Scale.MereoTag.qua

"read the book": inc verb + QUA NP → VP is telic (INC is weaker than SINC, but still transmits QUA from NP to VP when the object is quantized, K98 §3.6).

theorem Krifka1998.push_the_cart_atelic : Fragments.English.Predicates.Verbal.push.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.cumOnly

"push the cart": cumOnly verb → no telicity transfer from NP. Regardless of the NP's reference property, cumOnly verbs yield atelic (CUM) VPs.

theorem Krifka1998.write_a_letter_telic : Fragments.English.Predicates.Verbal.write.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.sinc ∧ Features.VendlerClass.accomplishment.telicity.toMereoTag = Core.Scale.MereoTag.qua

"write a letter": sinc verb + QUA NP → QUA VP (telic).

§4.5 Propositional propagation invocations (typeclass form)

The Bool-tag conjunctions above check fragment annotations and tag
composition; the theorems below actually invoke K98 theory's
`cum_propagation` and `qua_propagation` (typeclass-canonical
forms) on abstract θ + OBJ instances. This is the same shape as
K89 study §3's calls of `qmod_of_cum_is_qua` — making the
substrate-bridge promise concrete rather than rhetorical. 

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

eat apples propositional: K98 §3.3 CUM propagation. Given any [IsCumThetaVerb θ] (eat's role — and any of the K98 verb classes via upward instances) and a CUM object (apples), VP is CUM.

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 propositional: K98 §3.3 QUA propagation. Given [IsSincVerb θ] (eat's role, bundling SINC + UP) and a QUA object (two apples), VP is QUA.

Diagnostic Bridge

Connect CUM/QUA → for/in diagnostic compatibility. Atelic (CUM) VPs accept "for X"; telic (QUA) VPs accept "in X".

Round-1 audit deletions: 6 per-verb `inXPrediction .X = .accept := rfl`
theorems removed — they were tautological restatements of the
`Diagnostics.inXPrediction` definition (since `eat_two_apples_licenses_inX`
and `build_a_house_licenses_inX` had identical statements, both
passing `.accomplishment`, neither was about a specific verb). The
general `telic_licenses_inX` and `durative_atelic_licenses_forX`
below carry the diagnostic bridge work. 

theorem Krifka1998.telic_licenses_inX (c : Features.VendlerClass) (h : c.telicity = Features.Telicity.telic) : Phenomena.TenseAspect.Diagnostics.inXPrediction c = Phenomena.TenseAspect.Diagnostics.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) : Phenomena.TenseAspect.Diagnostics.forXPrediction c = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept

Durative atelic VPs (CUM + durative) license "for X" adverbials. Semelfactives are atelic but punctual — "for X" coerces to iterative.

Cross-Verification: Incrementality × Vendler

Verify that incrementality annotations are consistent with Vendler classes: only accomplishments can have non-none verbIncClass.

theorem Krifka1998.sinc_verbs_are_accomplishments : Fragments.English.Predicates.Verbal.eat.vendlerClass = some Features.VendlerClass.accomplishment ∧ Fragments.English.Predicates.Verbal.devour.vendlerClass = some Features.VendlerClass.accomplishment ∧ Fragments.English.Predicates.Verbal.build.vendlerClass = some Features.VendlerClass.accomplishment ∧ Fragments.English.Predicates.Verbal.write.vendlerClass = some Features.VendlerClass.accomplishment

All sinc-annotated verbs are accomplishments.

theorem Krifka1998.inc_verb_is_accomplishment : Fragments.English.Predicates.Verbal.read.vendlerClass = some Features.VendlerClass.accomplishment

The inc-annotated verb "read" is an accomplishment.

theorem Krifka1998.cumOnly_verbs_are_activities : Fragments.English.Predicates.Verbal.push.vendlerClass = some Features.VendlerClass.activity ∧ Fragments.English.Predicates.Verbal.pull.vendlerClass = some Features.VendlerClass.activity ∧ Fragments.English.Predicates.Verbal.carry.vendlerClass = some Features.VendlerClass.activity ∧ Fragments.English.Predicates.Verbal.drag.vendlerClass = some Features.VendlerClass.activity

All cumOnly-annotated verbs are activities.

Gradual Change (GRAD) Predictions

Connects GRAD theory to concrete verb entries.

Round-1 audit fixes: `GRADDatum.verb : String` and
`GRADDatum.objectMeasure : String` were the round-2-K89 String-field
anti-pattern recreated; replaced with `GRADVerb` enum +
`GRADObjectMeasure` enum. `native_decide` on `all_grad_data_matches`
eliminated by structurally lifting the verb match into the enum's
`toIncClass` projection. 

inductive Krifka1998.GRADVerb : Type

Verbs covered by the GRAD-prediction data.

• eat : GRADVerb
• build : GRADVerb
• read : GRADVerb
• push : GRADVerb
• kick : GRADVerb

@[implicit_reducible]

instance Krifka1998.instDecidableEqGRADVerb : DecidableEq GRADVerb

Equations

• Krifka1998.instDecidableEqGRADVerb x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Krifka1998.instReprGRADVerb : Repr GRADVerb

Equations

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

def Krifka1998.instReprGRADVerb.repr : GRADVerb → ℕ → Std.Format

Equations

• Krifka1998.instReprGRADVerb.repr Krifka1998.GRADVerb.eat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka1998.GRADVerb.eat")).group prec✝
• Krifka1998.instReprGRADVerb.repr Krifka1998.GRADVerb.build prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka1998.GRADVerb.build")).group prec✝
• Krifka1998.instReprGRADVerb.repr Krifka1998.GRADVerb.read prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka1998.GRADVerb.read")).group prec✝
• Krifka1998.instReprGRADVerb.repr Krifka1998.GRADVerb.push prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka1998.GRADVerb.push")).group prec✝
• Krifka1998.instReprGRADVerb.repr Krifka1998.GRADVerb.kick prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka1998.GRADVerb.kick")).group prec✝

def Krifka1998.GRADVerb.lemma : GRADVerb → String

English lemma for each GRAD verb.

Equations

• Krifka1998.GRADVerb.eat.lemma = "eat"
• Krifka1998.GRADVerb.build.lemma = "build"
• Krifka1998.GRADVerb.read.lemma = "read"
• Krifka1998.GRADVerb.push.lemma = "push"
• Krifka1998.GRADVerb.kick.lemma = "kick"

def Krifka1998.GRADVerb.expectedIncClass : GRADVerb → Option Semantics.Aspect.Incremental.VerbIncClass

Each verb's expected VerbIncClass per K98. Defined as literal constructors so that decide can close all_grad_data_matches structurally; the fragment-annotation tripwire is the separate gradVerb_matches_fragment theorem below.

Equations

• Krifka1998.GRADVerb.eat.expectedIncClass = some Semantics.Aspect.Incremental.VerbIncClass.sinc
• Krifka1998.GRADVerb.build.expectedIncClass = some Semantics.Aspect.Incremental.VerbIncClass.sinc
• Krifka1998.GRADVerb.read.expectedIncClass = some Semantics.Aspect.Incremental.VerbIncClass.inc
• Krifka1998.GRADVerb.push.expectedIncClass = some Semantics.Aspect.Incremental.VerbIncClass.cumOnly
• Krifka1998.GRADVerb.kick.expectedIncClass = none

theorem Krifka1998.gradVerb_matches_fragment : GRADVerb.eat.expectedIncClass = Fragments.English.Predicates.Verbal.eat.verbIncClass ∧ GRADVerb.build.expectedIncClass = Fragments.English.Predicates.Verbal.build.verbIncClass ∧ GRADVerb.read.expectedIncClass = Fragments.English.Predicates.Verbal.read.verbIncClass ∧ GRADVerb.push.expectedIncClass = Fragments.English.Predicates.Verbal.push.verbIncClass ∧ GRADVerb.kick.expectedIncClass = Fragments.English.Predicates.Verbal.kick.verbIncClass

Tripwire: each GRADVerb.expectedIncClass matches the fragment's verbIncClass annotation. If a fragment annotation drifts, this theorem breaks per-verb (one conjunct per verb). The expectedIncClass literal is what decide consumes for all_grad_data_matches; this theorem keeps the literal in sync with the fragment.

inductive Krifka1998.GRADObjectMeasure : Type

The dimension along which a verb's GRAD measure operates.

• weightOrVolume : GRADObjectMeasure
• proportionDone : GRADObjectMeasure
• pages : GRADObjectMeasure
• weight : GRADObjectMeasure
• force : GRADObjectMeasure

@[implicit_reducible]

instance Krifka1998.instDecidableEqGRADObjectMeasure : DecidableEq GRADObjectMeasure

Equations

• Krifka1998.instDecidableEqGRADObjectMeasure x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Krifka1998.instReprGRADObjectMeasure : Repr GRADObjectMeasure

Equations

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

def Krifka1998.instReprGRADObjectMeasure.repr : GRADObjectMeasure → ℕ → Std.Format

Equations

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

structure Krifka1998.GRADDatum : Type

• verb : GRADVerb
• objectMeasure : GRADObjectMeasure
• expectsGRAD : Bool

def Krifka1998.instReprGRADDatum.repr : GRADDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Krifka1998.instReprGRADDatum : Repr GRADDatum

Equations

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

@[implicit_reducible]

instance Krifka1998.instDecidableEqGRADDatum : DecidableEq GRADDatum

Equations

• Krifka1998.instDecidableEqGRADDatum = Krifka1998.instDecidableEqGRADDatum.decEq

def Krifka1998.instDecidableEqGRADDatum.decEq (x✝ x✝¹ : GRADDatum) : Decidable (x✝ = x✝¹)

Equations

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

def Krifka1998.eatGRAD : GRADDatum

Equations

• Krifka1998.eatGRAD = { verb := Krifka1998.GRADVerb.eat, objectMeasure := Krifka1998.GRADObjectMeasure.weightOrVolume, expectsGRAD := true }

def Krifka1998.buildGRAD : GRADDatum

Equations

• Krifka1998.buildGRAD = { verb := Krifka1998.GRADVerb.build, objectMeasure := Krifka1998.GRADObjectMeasure.proportionDone, expectsGRAD := true }

def Krifka1998.readGRAD : GRADDatum

Equations

• Krifka1998.readGRAD = { verb := Krifka1998.GRADVerb.read, objectMeasure := Krifka1998.GRADObjectMeasure.pages, expectsGRAD := true }

def Krifka1998.pushNoGRAD : GRADDatum

Equations

• Krifka1998.pushNoGRAD = { verb := Krifka1998.GRADVerb.push, objectMeasure := Krifka1998.GRADObjectMeasure.weight, expectsGRAD := false }

def Krifka1998.kickNoGRAD : GRADDatum

Equations

• Krifka1998.kickNoGRAD = { verb := Krifka1998.GRADVerb.kick, objectMeasure := Krifka1998.GRADObjectMeasure.force, expectsGRAD := false }

def Krifka1998.gradData : List GRADDatum

Equations

• Krifka1998.gradData = [Krifka1998.eatGRAD, Krifka1998.buildGRAD, Krifka1998.readGRAD, Krifka1998.pushNoGRAD, Krifka1998.kickNoGRAD]

def Krifka1998.predictsGRAD : Option Semantics.Aspect.Incremental.VerbIncClass → Bool

Whether a verb's incrementality class predicts GRAD.

This is a Bool projection of K98 theory's propositional GRAD predicate; the propositional version is what grad_of_sinc proves. Keeping the Bool-tag projection here as a quick-check; consumers needing the propositional content should use grad_of_sinc directly on abstract θ instances.

Equations

• Krifka1998.predictsGRAD (some Semantics.Aspect.Incremental.VerbIncClass.sinc) = true
• Krifka1998.predictsGRAD (some Semantics.Aspect.Incremental.VerbIncClass.inc) = true
• Krifka1998.predictsGRAD (some Semantics.Aspect.Incremental.VerbIncClass.cumOnly) = false
• Krifka1998.predictsGRAD none = false

theorem Krifka1998.eat_predicts_grad : predictsGRAD Fragments.English.Predicates.Verbal.eat.verbIncClass = true

theorem Krifka1998.build_predicts_grad : predictsGRAD Fragments.English.Predicates.Verbal.build.verbIncClass = true

theorem Krifka1998.read_predicts_grad : predictsGRAD Fragments.English.Predicates.Verbal.read.verbIncClass = true

theorem Krifka1998.push_no_grad : predictsGRAD Fragments.English.Predicates.Verbal.push.verbIncClass = false

theorem Krifka1998.kick_no_grad : predictsGRAD Fragments.English.Predicates.Verbal.kick.verbIncClass = false

theorem Krifka1998.all_grad_data_matches : (gradData.all fun (d : GRADDatum) => predictsGRAD d.verb.expectedIncClass == d.expectsGRAD) = true

All GRAD data matches the K98-expected verb classification. The decide closure works because verb.expectedIncClass is structurally reducible (literal-tag enum), unlike a fragment- projection that goes through Verbal.lean's VerbEntry. The fragment-annotation tripwire is gradVerb_matches_fragment.

K98 §3.5 Eq. 58: Mary ate peanuts in 0.43 seconds

K98 §3.5 (page 18, eq. 58) introduces Mary is an incredibly fast eater. Yesterday she ate peanuts in 0.43 seconds! — K98's own version of K89 §5's Ann drank wine in 0.43 sec. K98 uses it to argue that temporal atomicity (not quantization) is what licenses in-X adverbials: "even though eat peanuts is not quantized, it can be understood as temporally atomic. One chewing move may be a part of an event of eating peanuts, but not yet an event of eating peanuts."

The K89 study has an analogous ATM section (citing K89 T4); this
file mirrors it for K98 §3.5. The substrate-witness theorem
(showing a CUM-but-temporally-atomic predicate accepts *in*-X)
requires event-CEM atom infrastructure beyond this file's scope;
documented as data + linguistic motivation. 

structure Krifka1998.K98AtomicityDatum : Type

The K98 §3.5 atomicity-vs-quantization argument has three structural parts: the object NP's mereological reference type, the VP's licensing condition for in-X, and the temporal-atomicity flag that licenses in-X even when QUA fails. Captured here as a structure with enum-typed fields (MereoTag, DiagnosticResult) rather than a triple of Bools — Bool tags would be the round-2 K89 anti-pattern.

• sentence : String
• objectNP : String
• objectRef : Core.Scale.MereoTag

  Object NP's mereo reference type per K98 §3.3 (CUM or QUA).

• inXAcceptance : Phenomena.TenseAspect.Diagnostics.DiagnosticResult

  Diagnostic acceptance per K98 §3.4.

@[implicit_reducible]

instance Krifka1998.instReprK98AtomicityDatum : Repr K98AtomicityDatum

Equations

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

def Krifka1998.instReprK98AtomicityDatum.repr : K98AtomicityDatum → ℕ → Std.Format

Equations

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

def Krifka1998.maryAtePeanutsIn043Sec : K98AtomicityDatum

Mary ate peanuts in 0.43 seconds (K98 §3.5 eq. 58). The peanuts NP is CUM (mass-bare-plural — bare plurals are CUM via algebraic closure, cf. K89 §3 / Krifka1989.applesNP). The bounded-duration eating predicate is temporally atomic — no sub-event of a 0.43-second peanut-eating is also a 0.43-second peanut-eating. K98 §3.5 argues this licenses in-X via temporal atomicity, not quantization.

Equations

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

theorem Krifka1998.k98_eq58_cum_object_accepts_inX : maryAtePeanutsIn043Sec.objectRef = Core.Scale.MereoTag.cum ∧ maryAtePeanutsIn043Sec.inXAcceptance = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept

The K98 §3.5 eq. 58 witness pattern: CUM object + accepted in-X. The combination is unusual — typical in-X licensing requires QUA objects via the K98 §3.3 propagation chain. K98 introduces this case to motivate temporal atomicity as an alternative licensing pathway. K89 §5 makes the parallel point with Ann drank wine in 0.43 sec (formalized in Krifka1989.annDrankWineInSeconds); this is K98's same observation reformulated as temporal atomicity. The propositional ATM-but-not-QUA witness is deferred (requires event-CEM atom infrastructure beyond this file's scope, as documented in K89 study §5).

K89 ↔ K98 Sister-Paper Bridge

K89 (1989) and K98 (1998) are the same author refining the same theory at two stages. K89 study now defines K89ThematicClass.toVerbIncClass in Studies/Krifka1989.lean, mapping K89's table-14 thematic-relation classes to K98's VerbIncClass. This section provides the K98-side acknowledgement of the bridge: every K89 thematic class corresponds to exactly one K98 VerbIncClass, and the refinement is consistent with K89's GRAD distinction (gradual classes → sinc/inc, non-gradual → cumOnly).

The K89 study's `k89Table14_refines_k98_consistently` provides the
propositional bridge; this section adds K98-side documentation and
a fragment-verb ↔ K89-class consistency theorem for *eat*. 

theorem Krifka1998.eat_refinement_chain : Krifka1989.eatAnApple.thematicClass = Krifka1989.K89ThematicClass.gradualConsumedPatient ∧ Krifka1989.eatAnApple.thematicClass.toVerbIncClass = Semantics.Aspect.Incremental.VerbIncClass.sinc ∧ Fragments.English.Predicates.Verbal.eat.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.sinc

K89's eat an apple (gradual-consumed-patient) refines to K98 sinc (consumption verb), which matches the eat fragment annotation. Cross-paper consistency for the eat verb across K89 §4, K98 §3, and the fragment.

theorem Krifka1998.write_refinement_chain : Krifka1989.writeALetter.thematicClass = Krifka1989.K89ThematicClass.gradualEffectedPatient ∧ Krifka1989.writeALetter.thematicClass.toVerbIncClass = Semantics.Aspect.Incremental.VerbIncClass.sinc ∧ Fragments.English.Predicates.Verbal.write.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.sinc

K89's write a letter (gradual-effected-patient) refines to K98 sinc, matching write's fragment annotation. K89's distinction between effected (creation) and consumed (consumption) patients is finer than K98's binary sinc/non-sinc; both collapse to sinc here.

theorem Krifka1998.read_refinement_chain : Krifka1989.readALetter.thematicClass = Krifka1989.K89ThematicClass.gradualPatient ∧ Krifka1989.readALetter.thematicClass.toVerbIncClass = Semantics.Aspect.Incremental.VerbIncClass.inc ∧ Fragments.English.Predicates.Verbal.read.verbIncClass = some Semantics.Aspect.Incremental.VerbIncClass.inc

K89's read a letter (gradual-patient, lacks UNI-E) refines to K98 inc — matching read's fragment annotation, which K98 §3.6 eq. 59 motivates by appeal to backups (re-reading).

Concrete IsSincVerb Toy + Applied Propagation

§4.5's eat_apples_cum_propositional and eat_two_apples_qua_propositional are parametric over an abstract θ. This section provides a constructive IsSincVerb instance and fires both propagation theorems on it, demonstrating that K98 §3.3's typeclass-bundled meaning postulates admit real (non-axiomatic) realizations.

The toy: a 3-apple universe modelled as `Finset (Fin 3)` (powerset
lattice; ⊔ = ∪, < = ⊊). The eating relation is the identity
`eatThemeToy a e := a = e` — the eating event is identified with
the apple set eaten. Each subevent of an eating-of-{0,1}
corresponds bijectively to a subobject (the apples eaten in that
subevent), which is exactly the SINC bijection.

Lexical commitment: this is a TOY model, not a faithful denotation
of *eat*. A real denotation would (i) use a richer event type with
manner/agent/time information, (ii) admit non-trivial UO failures
(two distinct eatings of the same apple), and (iii) interact with
`Fragments/English/Predicates/Verbal.lean`'s `eat.semantics`. The
purpose here is to demonstrate that the typeclass admits
constructive instances — bridging the gap that prior `class
VerbIncrementality` attempts left open. 

@[reducible, inline]

abbrev Krifka1998.Apple : Type

Toy 3-apple universe. Finset (Fin 3) carries SemilatticeSup automatically (join is Finset.union); ≤/< are ⊆/⊊.

Equations

• Krifka1998.Apple = Finset (Fin 3)

@[reducible, inline]

abbrev Krifka1998.EatEvent : Type

Toy "eating event" — identified with the set of apples eaten. Same powerset lattice as Apple, yielding the bijection that SINC requires.

Equations

• Krifka1998.EatEvent = Finset (Fin 3)

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

The identity-as-relation theme: eatThemeToy a e iff the apple set a equals the apple set eaten in event e. The canonical SINC example, exhibiting a 1-1 correspondence between proper sub-objects (subsets of a) and proper sub-events.

Equations

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

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

eatThemeToy is a strictly incremental verb-theme relation. Constructed via the IsSincVerb.mk' smart constructor, which derives the inherited inc : INC eatThemeToy field automatically via inc_of_sinc.

Concrete OBJ predicates

def Krifka1998.twoApples : Apple → Prop

"two specific apples" — the singleton predicate λ a, a = {0, 1}. QUA: no proper subset of {0, 1} is also {0, 1}.

Equations

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

def Krifka1998.someApples : Apple → Prop

"(some) apples" — non-emptiness in the powerset lattice. CUM: nonempty ∪ nonempty is nonempty. The natural bare-plural interpretation in this toy.

Equations

• Krifka1998.someApples a = Finset.Nonempty a

theorem Krifka1998.twoApples_qua : Mereology.QUA twoApples

twoApples is QUA: a proper part of {0, 1} cannot also equal {0, 1}. This is the standard "exact-cardinality NPs are quantized" property at the K89/K98 level.

theorem Krifka1998.someApples_cum : Mereology.CUM someApples

someApples is CUM: nonempty ⊔ nonempty = nonempty. Bare plurals propagate cumulativity (K89 §3 / K98 §3.3).

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 + UP verb + QUA object → QUA VP. Direct invocation of substrate's typeclass-canonical qua_propagation; [IsSincVerb eatThemeToy] synthesises automatically from the instance above.

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. Direct invocation of substrate's cum_propagation; [IsCumThetaVerb eatThemeToy] synthesises from [IsSincVerb …] via instIsCumThetaVerbOfIsSincVerb.

Part II — K98 §4: Telicity by Precedence and Adjacency

Per-verb path specification (K98 §4.5 eq. 73)

theorem Krifka1998.arrive_levinClass : Fragments.English.Predicates.Verbal.arrive.levinClass = some Semantics.Lexical.LevinClass.inherentlyDirectedMotion

"arrive" is inherently directed motion (K98 §4.7 eq. 78).

theorem Krifka1998.arrive_pathSpec : Semantics.Lexical.LevinClass.inherentlyDirectedMotion.pathSpec = some Semantics.Spatial.Path.PathShape.bounded

Inherently directed motion → bounded path (K98 §4.5 GOAL specified).

theorem Krifka1998.leave_levinClass : Fragments.English.Predicates.Verbal.leave.levinClass = some Semantics.Lexical.LevinClass.leave

"leave" is a leave verb (K98 §4.5 SOURCE-only).

theorem Krifka1998.leave_pathSpec : Semantics.Lexical.LevinClass.leave.pathSpec = some Semantics.Spatial.Path.PathShape.source

Leave verbs → source path.

theorem Krifka1998.run_levinClass : Fragments.English.Predicates.Verbal.run.levinClass = some Semantics.Lexical.LevinClass.mannerOfMotion

"run" is manner-of-motion (K98 §4.5 path-neutral; PP supplies path).

theorem Krifka1998.run_pathSpec : Semantics.Lexical.LevinClass.mannerOfMotion.pathSpec = none

Manner-of-motion verbs are path-neutral (path comes from PP).

theorem Krifka1998.arrive_vendlerClass_achievement : Fragments.English.Predicates.Verbal.arrive.vendlerClass = some Features.VendlerClass.achievement

arrive is annotated as an achievement Vendler class.

theorem Krifka1998.sleep_vendlerClass_state : Fragments.English.Predicates.Verbal.sleep.vendlerClass = some Features.VendlerClass.state

sleep is annotated as a state Vendler class.

PathShape → Telicity → Licensing (K98 §4 MR eq. 71)

theorem Krifka1998.bounded_pipeline : Semantics.Spatial.Trace.pathShapeToTelicity Semantics.Spatial.Path.PathShape.bounded = Features.Telicity.telic ∧ Core.Scale.LicensingPipeline.isLicensed Semantics.Spatial.Path.PathShape.bounded = true

Bounded path → telic → licensed. K98 §4 eq. 74 walked from X to Y.

theorem Krifka1998.source_pipeline : Semantics.Spatial.Trace.pathShapeToTelicity Semantics.Spatial.Path.PathShape.source = Features.Telicity.telic ∧ Core.Scale.LicensingPipeline.isLicensed Semantics.Spatial.Path.PathShape.source = true

Source path → telic → licensed. K98 §4 eq. 73 Mary left the house.

theorem Krifka1998.unbounded_pipeline : Semantics.Spatial.Trace.pathShapeToTelicity Semantics.Spatial.Path.PathShape.unbounded = Features.Telicity.atelic ∧ Core.Scale.LicensingPipeline.isLicensed Semantics.Spatial.Path.PathShape.unbounded = false

Unbounded path → atelic → blocked. K98 §4 eq. 75 walked towards X.

Motion VP data (K98 §4.5 eq. 74-75)

structure Krifka1998.MotionVPDatum : Type

A motion VP datum: verb + PP + path shape + expected telicity.

• verb : String
• pp : String
• pathShape : Semantics.Spatial.Path.PathShape
• expectedTelicity : Features.Telicity

@[implicit_reducible]

instance Krifka1998.instReprMotionVPDatum : Repr MotionVPDatum

Equations

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

def Krifka1998.instReprMotionVPDatum.repr : MotionVPDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Krifka1998.instDecidableEqMotionVPDatum : DecidableEq MotionVPDatum

Equations

• Krifka1998.instDecidableEqMotionVPDatum = Krifka1998.instDecidableEqMotionVPDatum.decEq

def Krifka1998.instDecidableEqMotionVPDatum.decEq (x✝ x✝¹ : MotionVPDatum) : Decidable (x✝ = x✝¹)

Equations

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

def Krifka1998.arriveAtStore : MotionVPDatum

"arrive at the store" — bounded → telic → "in X" ✓. K98 §4.7 eq. 78.

Equations

• Krifka1998.arriveAtStore = { verb := "arrive", pp := "at the store", pathShape := Semantics.Spatial.Path.PathShape.bounded, expectedTelicity := Features.Telicity.telic }

def Krifka1998.leaveTheHouse : MotionVPDatum

"leave the house" — source → telic → "in X" ✓. K98 §4.5 eq. 73.

Equations

• Krifka1998.leaveTheHouse = { verb := "leave", pp := "the house", pathShape := Semantics.Spatial.Path.PathShape.source, expectedTelicity := Features.Telicity.telic }

def Krifka1998.runToThePark : MotionVPDatum

"run to the park" — manner + bounded PP → telic → "in X" ✓. K98 eq. 74.

Equations

• Krifka1998.runToThePark = { verb := "run", pp := "to the park", pathShape := Semantics.Spatial.Path.PathShape.bounded, expectedTelicity := Features.Telicity.telic }

def Krifka1998.runTowardsThePark : MotionVPDatum

"run towards the park" — manner + unbounded PP → atelic → "for X" ✓. K98 §4.5 eq. 75 walked towards Y — direction without goal.

Equations

• Krifka1998.runTowardsThePark = { verb := "run", pp := "towards the park", pathShape := Semantics.Spatial.Path.PathShape.unbounded, expectedTelicity := Features.Telicity.atelic }

def Krifka1998.motionData : List MotionVPDatum

Equations

• Krifka1998.motionData = [Krifka1998.arriveAtStore, Krifka1998.leaveTheHouse, Krifka1998.runToThePark, Krifka1998.runTowardsThePark]

theorem Krifka1998.all_motion_data_correct : (motionData.all fun (d : MotionVPDatum) => Semantics.Spatial.Trace.pathShapeToTelicity d.pathShape == d.expectedTelicity) = true

Path shape determines telicity for all motion data per K98 §4.

§3 ↔ §4 diagnostic bridge (K98 §3 in/for)

theorem Krifka1998.arrive_inX : Fragments.English.Predicates.Verbal.arrive.vendlerClass = some Features.VendlerClass.achievement ∧ Phenomena.TenseAspect.Diagnostics.inXPrediction Features.VendlerClass.achievement = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept

"arrive" (achievement, bounded path) licenses "in X".

theorem Krifka1998.leave_inX : Fragments.English.Predicates.Verbal.leave.vendlerClass = some Features.VendlerClass.achievement ∧ Phenomena.TenseAspect.Diagnostics.inXPrediction Features.VendlerClass.achievement = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept

"leave" (achievement, source path) licenses "in X".

theorem Krifka1998.run_forX : Fragments.English.Predicates.Verbal.run.vendlerClass = some Features.VendlerClass.activity ∧ Phenomena.TenseAspect.Diagnostics.forXPrediction Features.VendlerClass.activity = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept

"run" (activity, path-neutral) licenses "for X".

theorem Krifka1998.motion_vendler_path_coherence : (Fragments.English.Predicates.Verbal.arrive.vendlerClass = some Features.VendlerClass.achievement ∧ Semantics.Lexical.LevinClass.inherentlyDirectedMotion.pathSpec = some Semantics.Spatial.Path.PathShape.bounded) ∧ (Fragments.English.Predicates.Verbal.leave.vendlerClass = some Features.VendlerClass.achievement ∧ Semantics.Lexical.LevinClass.leave.pathSpec = some Semantics.Spatial.Path.PathShape.source) ∧ Fragments.English.Predicates.Verbal.run.vendlerClass = some Features.VendlerClass.activity ∧ Semantics.Lexical.LevinClass.mannerOfMotion.pathSpec = none

Motion verb VendlerClass × LevinClass coherence: bounded-path motion verbs are achievements, path-neutral ones are activities.

K98 §4 propositional substrate

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

K98 §4.1 eq. 63 EXP: expansion. If x is θ-related to e and y to a temporally-following e', then x and y 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 θ ∧ Semantics.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: temporal adjacency on sub-events ↔ spatial adjacency on sub-paths. The Lean form adds extra z ≤ x and e'' ≤ e premises vs the printed equation.

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} [PartialOrder α] [PartialOrder β] [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β θ ∧ Semantics.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 closure: smallest relation containing θ' and closed under precedence-respecting sums. K98's TANG_H clause (eq. 17) is OMITTED — see module TODO. Specialization of Semantics.Aspect.PrecedenceClosure with cond := precedes.

Equations

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

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

K98 §4.3 eq. 71 MR (TANG_H-free): θ is a movement relation iff there exists an SMR θ' such that θ is the MovementClosure of θ'.

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} [PartialOrder α] [PartialOrder β] [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_1} {Time : Type u_2} [LinearOrder Time] [cem : Semantics.Events.CEM.EventCEM 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 predicate (QUA) ↦ telic VP via the σ-pullback. Backs the K98 §4.5 walked from X to Y analysis at the Bool-tag level.

theorem Krifka1998.walked_towards_atelic_propositional {Loc : Type u_1} {Time : Type u_2} [LinearOrder Time] [cem : Semantics.Events.CEM.EventCEM 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 predicate (CUM) ↦ atelic VP via the σ-pullback. Backs the K98 §4.5 walked towards X analysis at the Bool-tag level.

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

@[reducible, inline]

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

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

Equations

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

@[reducible, inline]

abbrev Krifka1998.seincEv {α : Type u_1} [SemilatticeSup α] {Time : Type u_2} [LinearOrder Time] [Semantics.Events.CEM.EventCEM Time] (θ : α → Semantics.Events.Event Time → Prop) : Prop

SEINC-as-property using Event.precedes. EventCEM provides the required [SemilatticeSup (Event Time)].

Equations

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

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

@[reducible, inline]

abbrev Krifka1998.smrPath {Loc : Type u_1} {Time : Type u_2} [LinearOrder Time] [Semantics.Events.CEM.EventCEM Time] [PartialOrder (Semantics.Spatial.Path.Path Loc)] [SemilatticeSup (Semantics.Spatial.Path.Path Loc)] (θ : Semantics.Spatial.Path.Path Loc → Semantics.Events.Event Time → Prop) : Prop

SMR specialized to paths and events with concrete adjacency.

Equations

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

@[reducible, inline]

abbrev Krifka1998.mrPath {Loc : Type u_1} {Time : Type u_2} [LinearOrder Time] [Semantics.Events.CEM.EventCEM Time] [PartialOrder (Semantics.Spatial.Path.Path Loc)] [SemilatticeSup (Semantics.Spatial.Path.Path Loc)] (θ : Semantics.Spatial.Path.Path Loc → Semantics.Events.Event Time → Prop) : Prop

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

Equations

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