Documentation

Linglib.Phenomena.TenseAspect.Studies.Krifka1998

@cite{krifka-1998} Bridge: Telicity Propagation → Fragment Verbs #

@cite{krifka-1998} @cite{vendler-1957}

Connects Krifka's mereological telicity theory (Events/Krifka1998.lean) to concrete verb entries in Fragments/English/Predicates/Verbal.lean and diagnostic predictions in DiagnosticsBridge.lean.

Structure #

  1. Per-verb incrementality verification — each verb's verbIncClass annotation is checked by rfl.
  2. VendlerClass → MereoTag bridge — accomplishments map to QUA, activities to CUM, connecting Vendler to Krifka.
  3. Compositional telicity — sinc verb + QUA NP → QUA VP (telic); sinc verb + CUM NP → CUM VP (atelic). Instantiated for eat.
  4. Diagnostic bridge — for/in compatibility follows from CUM/QUA via Vendler class.

Each verb's verbIncClass annotation is verified by rfl. Changing any annotation breaks exactly one theorem here.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.eat_sinc :
Fragments.English.Predicates.Verbal.eat.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.sinc

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

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.devour_sinc :
Fragments.English.Predicates.Verbal.devour.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.sinc

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

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.build_sinc :
Fragments.English.Predicates.Verbal.build.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.sinc

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

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.write_sinc :
Fragments.English.Predicates.Verbal.write.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.sinc

"write" is strictly incremental (creation verb).

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.read_inc :
Fragments.English.Predicates.Verbal.read.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.inc

"read" is incremental but not strictly so (allows re-reading).

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.push_cumOnly :
Fragments.English.Predicates.Verbal.push.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.cumOnly

"push" is cumulative only (no incremental theme).

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.pull_cumOnly :
Fragments.English.Predicates.Verbal.pull.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.cumOnly

"pull" is cumulative only (no incremental theme).

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.carry_cumOnly :
Fragments.English.Predicates.Verbal.carry.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.cumOnly

"carry" is cumulative only (no incremental theme).

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.drag_cumOnly :
Fragments.English.Predicates.Verbal.drag.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.cumOnly

"drag" is cumulative only (no incremental theme).

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.sleep_no_inc :
Fragments.English.Predicates.Verbal.sleep.verbIncClass = none

Intransitives have no incremental theme.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.run_no_inc :
Fragments.English.Predicates.Verbal.run.verbIncClass = none
source
theorem Phenomena.TenseAspect.Studies.Krifka1998.arrive_no_inc :
Fragments.English.Predicates.Verbal.arrive.verbIncClass = none

Unaccusatives have no incremental theme.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.kick_no_inc :
Fragments.English.Predicates.Verbal.kick.verbIncClass = none

Contact verbs have no incremental theme.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.sleep_state :
Fragments.English.Predicates.Verbal.sleep.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state

"sleep" is a state.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.run_activity :
Fragments.English.Predicates.Verbal.run.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity

"run" is an activity.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.arrive_achievement :
Fragments.English.Predicates.Verbal.arrive.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement

"arrive" is an achievement.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.eat_accomplishment :
Fragments.English.Predicates.Verbal.eat.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

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

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.build_accomplishment :
Fragments.English.Predicates.Verbal.build.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

"build" is an accomplishment.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.read_accomplishment :
Fragments.English.Predicates.Verbal.read.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

"read" is an accomplishment.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.write_accomplishment :
Fragments.English.Predicates.Verbal.write.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

"write" is an accomplishment.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.kick_activity :
Fragments.English.Predicates.Verbal.kick.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity

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

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.see_state :
Fragments.English.Predicates.Verbal.see.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state

"see" is a state (perception).

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.leave_achievement :
Fragments.English.Predicates.Verbal.leave.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement

"leave" is an achievement.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.push_activity :
Fragments.English.Predicates.Verbal.push.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity

"push" is an activity.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.love_state :
Fragments.English.Predicates.Verbal.love.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state

"love" is a state.

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

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.accomplishment_is_qua :
Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment.telicity.toMereoTag = Core.Scale.MereoTag.qua

Accomplishments are telic, hence QUA.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.achievement_is_qua :
Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement.telicity.toMereoTag = Core.Scale.MereoTag.qua

Achievements are telic, hence QUA.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.activity_is_cum :
Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity.telicity.toMereoTag = Core.Scale.MereoTag.cum

Activities are atelic, hence CUM.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.state_is_cum :
Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state.telicity.toMereoTag = Core.Scale.MereoTag.cum

States are atelic, hence CUM.

The payoff: verb incrementality + NP reference property → VP telicity. These instantiate @cite{krifka-1998} §3.3 for concrete verb entries.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.eat_apples_atelic :
Fragments.English.Predicates.Verbal.eat.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.sinc ∧ Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity.telicity.toMereoTag = Core.Scale.MereoTag.cum

"eat apples": sinc verb + CUM NP → CUM VP (atelic). @cite{krifka-1998}: CumTheta(θ) ∧ CUM(OBJ) → CUM(VP θ OBJ). The verb's incrementality class is sinc, and bare plurals are CUM.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.eat_two_apples_telic :
Fragments.English.Predicates.Verbal.eat.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.sinc ∧ Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment.telicity.toMereoTag = Core.Scale.MereoTag.qua

"eat two apples": sinc verb + QUA NP → QUA VP (telic). @cite{krifka-1998}: SINC(θ) ∧ QUA(OBJ) → QUA(VP θ OBJ). The verb's incrementality class is sinc, and "two apples" is QUA.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.build_a_house_telic :
Fragments.English.Predicates.Verbal.build.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.sinc ∧ Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment.telicity.toMereoTag = Core.Scale.MereoTag.qua

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

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.read_the_book_telic :
Fragments.English.Predicates.Verbal.read.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.inc ∧ Semantics.Tense.Aspect.LexicalAspect.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).

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.push_the_cart_atelic :
Fragments.English.Predicates.Verbal.push.verbIncClass = some Semantics.Events.Krifka1998.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.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.write_a_letter_telic :
Fragments.English.Predicates.Verbal.write.verbIncClass = some Semantics.Events.Krifka1998.VerbIncClass.sinc ∧ Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment.telicity.toMereoTag = Core.Scale.MereoTag.qua

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

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

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.telic_licenses_inX (c : Semantics.Tense.Aspect.LexicalAspect.VendlerClass) (h : c.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.telic) :
Diagnostics.inXPrediction c = Diagnostics.DiagnosticResult.accept

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

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.atelic_licenses_forX (c : Semantics.Tense.Aspect.LexicalAspect.VendlerClass) (h : c.telicity = Semantics.Tense.Aspect.LexicalAspect.Telicity.atelic) :
Diagnostics.forXPrediction c = Diagnostics.DiagnosticResult.accept

Atelic VPs (CUM) license "for X" adverbials.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.eat_two_apples_licenses_inX :
Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = Diagnostics.DiagnosticResult.accept

"eat two apples" (accomplishment) licenses "in X".

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.eat_apples_licenses_forX :
Diagnostics.forXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = Diagnostics.DiagnosticResult.accept

"eat apples" (activity) licenses "for X".

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.build_a_house_licenses_inX :
Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment = Diagnostics.DiagnosticResult.accept

"build a house" (accomplishment) licenses "in X".

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.run_licenses_forX :
Diagnostics.forXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity = Diagnostics.DiagnosticResult.accept

"run" (activity) licenses "for X".

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.sleep_licenses_forX :
Diagnostics.forXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state = Diagnostics.DiagnosticResult.accept

"sleep" (state) licenses "for X".

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.arrive_licenses_inX :
Diagnostics.inXPrediction Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement = Diagnostics.DiagnosticResult.accept

"arrive" (achievement) licenses "in X".

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

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.sinc_verbs_are_accomplishments :
Fragments.English.Predicates.Verbal.eat.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment ∧ Fragments.English.Predicates.Verbal.devour.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment ∧ Fragments.English.Predicates.Verbal.build.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment ∧ Fragments.English.Predicates.Verbal.write.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

All sinc-annotated verbs are accomplishments.

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.inc_verb_is_accomplishment :
Fragments.English.Predicates.Verbal.read.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

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

source
theorem Phenomena.TenseAspect.Studies.Krifka1998.cumOnly_verbs_are_activities :
Fragments.English.Predicates.Verbal.push.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity ∧ Fragments.English.Predicates.Verbal.pull.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity ∧ Fragments.English.Predicates.Verbal.carry.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity ∧ Fragments.English.Predicates.Verbal.drag.vendlerClass = some Semantics.Tense.Aspect.LexicalAspect.VendlerClass.activity

All cumOnly-annotated verbs are activities.

Connects GRAD/GRADSquare theory from Events/Krifka1998.lean and Events/Krifka1989.lean to concrete verb entries.

source
structure Phenomena.TenseAspect.Studies.Krifka1998.GRADDatum :
Type

A gradual change datum.

Instances For
    source
    def Phenomena.TenseAspect.Studies.Krifka1998.instReprGRADDatum.repr :
    GRADDatum → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      instance Phenomena.TenseAspect.Studies.Krifka1998.instReprGRADDatum :
      Repr GRADDatum
      Equations
      source
      instance Phenomena.TenseAspect.Studies.Krifka1998.instDecidableEqGRADDatum :
      DecidableEq GRADDatum
      Equations
      source
      def Phenomena.TenseAspect.Studies.Krifka1998.instDecidableEqGRADDatum.decEq (x✝ x✝¹ : GRADDatum) :
      Decidable (x✝ = x✝¹)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        instance Phenomena.TenseAspect.Studies.Krifka1998.instBEqGRADDatum :
        BEq GRADDatum
        Equations
        source
        def Phenomena.TenseAspect.Studies.Krifka1998.instBEqGRADDatum.beq :
        GRADDatum → GRADDatum → Bool
        Equations
        Instances For
          source
          def Phenomena.TenseAspect.Studies.Krifka1998.eatGRAD :
          GRADDatum
          Equations
          Instances For
            source
            def Phenomena.TenseAspect.Studies.Krifka1998.buildGRAD :
            GRADDatum
            Equations
            Instances For
              source
              def Phenomena.TenseAspect.Studies.Krifka1998.readGRAD :
              GRADDatum
              Equations
              Instances For
                source
                def Phenomena.TenseAspect.Studies.Krifka1998.pushNoGRAD :
                GRADDatum
                Equations
                Instances For
                  source
                  def Phenomena.TenseAspect.Studies.Krifka1998.kickNoGRAD :
                  GRADDatum
                  Equations
                  Instances For
                    source
                    def Phenomena.TenseAspect.Studies.Krifka1998.gradData :
                    List GRADDatum
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Phenomena.TenseAspect.Studies.Krifka1998.predictsGRAD :
                      Option Semantics.Events.Krifka1998.VerbIncClass → Bool

                      Whether a verb's incrementality class predicts GRAD.

                      Equations
                      Instances For
                        source
                        theorem Phenomena.TenseAspect.Studies.Krifka1998.grad_decidable :
                        predictsGRAD (some Semantics.Events.Krifka1998.VerbIncClass.sinc) = true ∧ predictsGRAD (some Semantics.Events.Krifka1998.VerbIncClass.inc) = true ∧ predictsGRAD (some Semantics.Events.Krifka1998.VerbIncClass.cumOnly) = false ∧ predictsGRAD none = false
                        source
                        theorem Phenomena.TenseAspect.Studies.Krifka1998.eat_predicts_grad :
                        predictsGRAD Fragments.English.Predicates.Verbal.eat.verbIncClass = true
                        source
                        theorem Phenomena.TenseAspect.Studies.Krifka1998.build_predicts_grad :
                        predictsGRAD Fragments.English.Predicates.Verbal.build.verbIncClass = true
                        source
                        theorem Phenomena.TenseAspect.Studies.Krifka1998.read_predicts_grad :
                        predictsGRAD Fragments.English.Predicates.Verbal.read.verbIncClass = true
                        source
                        theorem Phenomena.TenseAspect.Studies.Krifka1998.push_no_grad :
                        predictsGRAD Fragments.English.Predicates.Verbal.push.verbIncClass = false
                        source
                        theorem Phenomena.TenseAspect.Studies.Krifka1998.kick_no_grad :
                        predictsGRAD Fragments.English.Predicates.Verbal.kick.verbIncClass = false
                        source
                        theorem Phenomena.TenseAspect.Studies.Krifka1998.all_grad_data_matches :
                        (gradData.all fun (d : GRADDatum) => predictsGRAD (match d.verb with | "eat" => Fragments.English.Predicates.Verbal.eat.verbIncClass | "build" => Fragments.English.Predicates.Verbal.build.verbIncClass | "read" => Fragments.English.Predicates.Verbal.read.verbIncClass | "push" => Fragments.English.Predicates.Verbal.push.verbIncClass | "kick" => Fragments.English.Predicates.Verbal.kick.verbIncClass | x => none) == d.expectsGRAD) = true

                        All GRAD data matches fragment verb annotations.

                        source
                        theorem Phenomena.TenseAspect.Studies.Krifka1998.grad_requires_incrementality :
                        predictsGRAD (some Semantics.Events.Krifka1998.VerbIncClass.sinc) = true ∧ predictsGRAD (some Semantics.Events.Krifka1998.VerbIncClass.cumOnly) = false

                        sinc verbs have prerequisites for GRADSquare; cumOnly verbs don't.