Documentation

Linglib.Studies.Bhadra2024

Bhadra 2024: Verb roots encode outcomes #

[Bha24]

The reversative prefix un- and the restitutive prefix re- are result-state modifiers sensitive to the outcome set a verb root lexically encodes ([Bha24], §5). Every verb root carries a set of outcomes O — the states its object can be in after the action — and a contextual set of thresholds T of states it can start from.

The two affixes split along two independent axes:

One idealization: each VerbOutcomes fixes its outcome and threshold sets once per root, freezing the [verb + object] unit that Bhadra's Level-2 story varies with the object (✓rebreak a limb vs. #rebreak a sewer, her (73)).

Main definitions #

Main results #

References #

The compositional verb root (eqs. 53–60) #

A verb root lexically encodes its base predicate P (the ⟨v,⟨e,t⟩⟩ meaning the affixes modify), its outcome set O (states at the right boundary, eq. 56a), and its threshold set T (left boundary, eq. 56b) — the substrate VerbOutcomes (Semantics/Verb/Root/Outcomes.lean), with resState/preState the eq. 64–65 boundary operators and StateFunction the paper's state k : t ↦ l(x) (eq. 53). APPLIES (eq. 59) is folded into verb.

un- and re- as result-state modifiers (eqs. 66, 68) #

source
def Bhadra2024.unSem {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : Semantics.Lexical.StateFunction Entity State Time) (vro : Semantics.Lexical.VerbOutcomes Entity State Time) (e : Event Time) (x : Entity) :
Prop

Reversative un- (eq. 66). unSem k vro e x holds iff there is a prior base event e' whose result is the un-event's start state (res(e') = pre(e)), the outcome set is multi-membered (O.Nontrivial, |O| > 1), and the un-event undoes it (res(e) = pre(e')). The vacuous ∃Q. Q(e)(x) — which sits in the assertion of eq. 66, not its presupposition — is dropped.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Bhadra2024.reSem {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : Semantics.Lexical.StateFunction Entity State Time) (vro : Semantics.Lexical.VerbOutcomes Entity State Time) (e : Event Time) (x : Entity) :
    Prop

    Restitutive re- (eq. 68). reSem k vro e x holds iff there is a prior base event e' with the same result (res(e) = res(e'), eq. 68 i), the re-event starts from a valid threshold state (pre(e) ∈ T), and the base predicate holds of the re-event (P(e)(x)). The threshold clause is a rational reconstruction — not a transcription — of eq. 68 ii's negative existential (no threshold state may render the re-action undefined; the cyclic-re- condition, eq. 72). Unlike unSem, this places no cardinality demand on O.

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

      Cardinality blocks un- (eq. 67) #

      source
      theorem Bhadra2024.subsingleton_blocks_un {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : Semantics.Lexical.StateFunction Entity State Time) (vro : Semantics.Lexical.VerbOutcomes Entity State Time) (h : ¬vro.outcomes.Nontrivial) (e : Event Time) (x : Entity) :
      ¬unSem k vro e x

      The core asymmetry: a verb whose outcome set is not multi-membered cannot host un- ([Bha24], eq. 67). The multi-membered presupposition of unSem fails.

      source
      theorem Bhadra2024.singleton_blocks_un {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : Semantics.Lexical.StateFunction Entity State Time) (vro : Semantics.Lexical.VerbOutcomes Entity State Time) (s : State) (hs : vro.outcomes = {s}) (e : Event Time) (x : Entity) :
      ¬unSem k vro e x

      Singleton outcome sets (IE and COS verbs) block un-.

      source
      theorem Bhadra2024.empty_blocks_un {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : Semantics.Lexical.StateFunction Entity State Time) (vro : Semantics.Lexical.VerbOutcomes Entity State Time) (hs : vro.outcomes = ∅) (e : Event Time) (x : Entity) :
      ¬unSem k vro e x

      Empty outcome sets (no-change-specified verbs) block un-.

      source
      theorem Bhadra2024.un_requires_multi_cardinality {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (k : Semantics.Lexical.StateFunction Entity State Time) (vro : Semantics.Lexical.VerbOutcomes Entity State Time) (e : Event Time) (x : Entity) (h : unSem k vro e x) :
      vro.cardinality = Verb.OutcomeCardinality.multi

      un-'s cardinality demand (eq. 67, |O| > 1) is exactly the substrate OutcomeCardinality.multi tier (eq. 62, empty < singleton < multi): hosting un- forces the verb root's outcome set into the top tier. Wires Bhadra's outcome cardinality to the OutcomeCardinality substrate.

      The Levin-class → outcome-cardinality bridge (eq. 62) #

      The single per-class datum: the cardinality of a verb root's lexical outcome set, valued in ℕ∞. PFC roots have open-ended outcome sets (eq. 60: O = {k | k = APPLIES(e)(x)}, unbounded), idealized as ⊤; IE and COS roots have a single lexically-specified result (eqs. 61a–g); no-change roots have none (eq. 61h). Only 1 < · is load-bearing (it drives un-); the three tiers realize the eq. 62 hierarchy multi > singleton > empty.

      source
      def Bhadra2024.LevinClass.outcomeCard :
      Semantics.Lexical.LevinClass → ℕ∞

      Outcome-set cardinality of a Levin verb class ([Bha24], eq. 62).

      Equations
      Instances For
        source
        theorem Bhadra2024.outcome_hierarchy :
        LevinClass.outcomeCard Semantics.Lexical.LevinClass.bend = ⊤ ∧ LevinClass.outcomeCard Semantics.Lexical.LevinClass.hit = 1 ∧ LevinClass.outcomeCard Semantics.Lexical.LevinClass.break_ = 1 ∧ LevinClass.outcomeCard Semantics.Lexical.LevinClass.mannerOfMotion = 0 ∧ 0 < 1 ∧ 1 < ⊤

        The eq. 62 hierarchy, witnessed on a representative of each tier: multi-membered (PFC) > singleton (IE, COS) > empty (no change).

        source
        theorem Bhadra2024.bend_predicts_un :
        1 < LevinClass.outcomeCard Semantics.Lexical.LevinClass.bend

        un- prediction is derived from cardinality: PFC classes have 1 < outcomeCard, every other class does not.

        source
        theorem Bhadra2024.coil_predicts_un :
        1 < LevinClass.outcomeCard Semantics.Lexical.LevinClass.coil
        source
        theorem Bhadra2024.break_blocks_un_class :
        ¬1 < LevinClass.outcomeCard Semantics.Lexical.LevinClass.break_
        source
        theorem Bhadra2024.hit_blocks_un_class :
        ¬1 < LevinClass.outcomeCard Semantics.Lexical.LevinClass.hit
        source
        theorem Bhadra2024.destroy_blocks_un_class :
        ¬1 < LevinClass.outcomeCard Semantics.Lexical.LevinClass.destroy
        source
        theorem Bhadra2024.color_blocks_un_class :
        ¬1 < LevinClass.outcomeCard Semantics.Lexical.LevinClass.color
        source
        theorem Bhadra2024.mannerOfMotion_blocks_un_class :
        ¬1 < LevinClass.outcomeCard Semantics.Lexical.LevinClass.mannerOfMotion

        Worked examples (eqs. 60–61, 66–71) #

        fold: a PFC root (multi-membered outcomes), un- and re- both attach #

        source
        inductive Bhadra2024.ParchmentState :
        Type

        States of a parchment under folding (eq. 54: a multi-membered outcome set).

        Instances For
          source
          @[implicit_reducible]
          instance Bhadra2024.instDecidableEqParchmentState :
          DecidableEq ParchmentState
          Equations
          source
          def Bhadra2024.instReprParchmentState.repr :
          ParchmentState → ℕ → Std.Format
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[implicit_reducible]
            instance Bhadra2024.instReprParchmentState :
            Repr ParchmentState
            Equations
            source
            def Bhadra2024.foldVRO :
            Semantics.Lexical.VerbOutcomes Unit ParchmentState ℤ

            fold (Levin bend class): a multi-membered outcome set.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem Bhadra2024.fold_outcomes_multi :
              foldVRO.outcomes.Nontrivial
              source
              theorem Bhadra2024.fold_un_satisfiable :
              unSem Bhadra2024.foldUnfoldState✝ foldVRO Bhadra2024.ev₂✝ ()

              Positive: un- IS satisfiable for fold (eq. 66 worked example, "Veena unfolded the parchment").

              source
              theorem Bhadra2024.fold_re_satisfiable :
              reSem Bhadra2024.foldRefoldState✝ foldVRO Bhadra2024.ev₃✝ ()

              Positive: re- IS satisfiable for fold — the multi-membered (PFC) tier's re- cell, completing the Fig. 5 distribution: re- attaches across the multi and singleton tiers (eq. 72), where un- takes the multi tier only. Reuses the root of her worked unfold derivation (74)–(75).

              break: a COS root (singleton outcome), un- blocked, re- allowed #

              source
              inductive Bhadra2024.LimbState :
              Type
              Instances For
                source
                @[implicit_reducible]
                instance Bhadra2024.instDecidableEqLimbState :
                DecidableEq LimbState
                Equations
                source
                @[implicit_reducible]
                instance Bhadra2024.instReprLimbState :
                Repr LimbState
                Equations
                source
                def Bhadra2024.instReprLimbState.repr :
                LimbState → ℕ → Std.Format
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Bhadra2024.breakVRO :
                  Semantics.Lexical.VerbOutcomes Unit LimbState ℤ

                  break (Levin break_ class): a single lexically-specified result (eq. 61a).

                  Equations
                  Instances For
                    source
                    theorem Bhadra2024.break_blocks_un (k : Semantics.Lexical.StateFunction Unit LimbState ℤ) (e : Event ℤ) :
                    ¬unSem k breakVRO e ()

                    unbreak is blocked: the singleton outcome set fails eq. 67.

                    source
                    theorem Bhadra2024.break_re_satisfiable :
                    reSem Bhadra2024.breakRebreakState✝ breakVRO Bhadra2024.ev₃✝ ()

                    Positive: re- IS satisfiable for break (rebreak a limb): result equivalence holds and the re-event starts from the intact threshold.

                    hit: an IE root (singleton outcome), un- and re- both blocked #

                    source
                    inductive Bhadra2024.SurfaceState :
                    Type
                    Instances For
                      source
                      @[implicit_reducible]
                      instance Bhadra2024.instDecidableEqSurfaceState :
                      DecidableEq SurfaceState
                      Equations
                      source
                      @[implicit_reducible]
                      instance Bhadra2024.instReprSurfaceState :
                      Repr SurfaceState
                      Equations
                      source
                      def Bhadra2024.instReprSurfaceState.repr :
                      SurfaceState → ℕ → Std.Format
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        def Bhadra2024.hitVRO :
                        Semantics.Lexical.VerbOutcomes Unit SurfaceState ℤ

                        hit (Levin hit class): impingement, a single surface-alteration result (eq. 61g).

                        Equations
                        Instances For
                          source
                          theorem Bhadra2024.hit_blocks_un (k : Semantics.Lexical.StateFunction Unit SurfaceState ℤ) (e : Event ℤ) :
                          ¬unSem k hitVRO e ()
                          source
                          theorem Bhadra2024.hit_re_blocked :
                          ¬reSem Bhadra2024.hitState✝ hitVRO Bhadra2024.ev₃✝ ()

                          Negative: re- is blocked for hit — IE verbs block re- as well as un- ((25), (48)): the impingement outcome never re-enters the pre-state (threshold) set, so the cyclic-re- condition (eq. 68 ii) fails.

                          load vs shatter: the re- minimal pair (eqs. 69–71) #

                          Both are singleton-outcome (so both block un-); they differ on re- purely through the threshold condition (eq. 68 ii). After loading, the truck can be loaded again (it re-enters a threshold); after shattering, the mirror cannot.

                          source
                          inductive Bhadra2024.TruckState :
                          Type
                          Instances For
                            source
                            @[implicit_reducible]
                            instance Bhadra2024.instDecidableEqTruckState :
                            DecidableEq TruckState
                            Equations
                            source
                            @[implicit_reducible]
                            instance Bhadra2024.instReprTruckState :
                            Repr TruckState
                            Equations
                            source
                            def Bhadra2024.instReprTruckState.repr :
                            TruckState → ℕ → Std.Format
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def Bhadra2024.loadVRO :
                              Semantics.Lexical.VerbOutcomes Unit TruckState ℤ

                              load (degree achievement, eq. 70): a single contextually-salient result; the object stays loadable.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                theorem Bhadra2024.load_re_satisfiable :
                                reSem Bhadra2024.loadReloadState✝ loadVRO Bhadra2024.ev₃✝ ()

                                Positive: re- IS satisfiable for load (eq. 69a "reloaded the truck").

                                source
                                inductive Bhadra2024.MirrorState :
                                Type
                                Instances For
                                  source
                                  @[implicit_reducible]
                                  instance Bhadra2024.instDecidableEqMirrorState :
                                  DecidableEq MirrorState
                                  Equations
                                  source
                                  @[implicit_reducible]
                                  instance Bhadra2024.instReprMirrorState :
                                  Repr MirrorState
                                  Equations
                                  source
                                  def Bhadra2024.instReprMirrorState.repr :
                                  MirrorState → ℕ → Std.Format
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    source
                                    def Bhadra2024.shatterVRO :
                                    Semantics.Lexical.VerbOutcomes Unit MirrorState ℤ

                                    shatter (eq. 71): a single result that leaves the object outside every threshold — it cannot be shattered again.

                                    Equations
                                    Instances For
                                      source
                                      theorem Bhadra2024.shatter_re_blocked :
                                      ¬reSem Bhadra2024.shatterState✝ shatterVRO Bhadra2024.ev₃✝ ()

                                      Negative: re- is blocked for shatter (eq. 69b "#reshattered the mirror"): the cyclic-re- threshold condition (eq. 68 ii) fails — the shattered mirror is never in the intact threshold the re-event needs.

                                      End-to-end: Fragment entry → Levin class → prediction #

                                      The Fragment verb's levinClass drives the outcome cardinality, which drives the un- prediction.

                                      source
                                      theorem Bhadra2024.kick_un_blocked :
                                      English.Predicates.Verbal.kick.levinClass = some Semantics.Lexical.LevinClass.hit ∧ ¬1 < LevinClass.outcomeCard Semantics.Lexical.LevinClass.hit

                                      kick (Levin 18.1 hit) → singleton outcomes → un- blocked.

                                      source
                                      theorem Bhadra2024.bend_un_predicted :
                                      English.Predicates.Verbal.bend.levinClass = some Semantics.Lexical.LevinClass.bend ∧ 1 < LevinClass.outcomeCard Semantics.Lexical.LevinClass.bend

                                      bend (Levin 45.2) → multi-membered outcomes → un- predicted.

                                      source
                                      theorem Bhadra2024.break_un_blocked :
                                      English.Predicates.Verbal.break_.levinClass = some Semantics.Lexical.LevinClass.break_ ∧ ¬1 < LevinClass.outcomeCard Semantics.Lexical.LevinClass.break_

                                      break (Levin 45.1) → singleton outcomes → un- blocked.

                                      Bridges to the substrate #

                                      The outcome-cardinality classification is finer than the change-of-state label ([Bha24]'s central move): bend is CoS per [Lev93] yet has a multi-membered (PFC) outcome set.

                                      source
                                      theorem Bhadra2024.bend_reclassification :
                                      Semantics.Lexical.LevinClass.bend.meaningComponents.changeOfState = true ∧ LevinClass.outcomeCard Semantics.Lexical.LevinClass.bend = ⊤ ∧ 1 < LevinClass.outcomeCard Semantics.Lexical.LevinClass.bend

                                      [Bha24] reclassifies bend from a flat change-of-state verb to a potential-for-change root: CoS per [Lev93]'s meaning components, but multi-membered (and hence un--compatible) by outcome cardinality.

                                      source
                                      theorem Bhadra2024.outcomeCard_orthogonal_to_hasResultState :
                                      Semantics.Lexical.LevinClass.bend.eventTemplate.HasResultState ∧ ¬Semantics.Lexical.LevinClass.coil.eventTemplate.HasResultState ∧ LevinClass.outcomeCard Semantics.Lexical.LevinClass.bend = ⊤ ∧ LevinClass.outcomeCard Semantics.Lexical.LevinClass.coil = ⊤

                                      The outcome-cardinality classification is orthogonal to event-template result states: bend and coil share the PFC profile but differ on whether their template carries a result state.

                                      source
                                      theorem Bhadra2024.affectedness_bridge :
                                      ArgumentStructure.Affectedness.profileToDegree { causallyAffected := true, stationary := true } = ArgumentStructure.Affectedness.profileToDegree Features.LevinClassProfiles.contactObject ∧ 1 < LevinClass.outcomeCard Semantics.Lexical.LevinClass.bend ∧ ¬1 < LevinClass.outcomeCard Semantics.Lexical.LevinClass.hit

                                      Affectedness bridge ([Bha24] §2.4.2, §6.1): the affectedness projection cannot separate PFC roots from IE roots — the PFC object profile (causally affected, no entailed change) and kick's object profile both land on Beavers's potential-for-change degree, whose exemplars include surface-contact hit/kick. Bhadra carves the IE class (kick is named in her (25)) out of exactly that cell (§2.4.2), and her §6.1 point is that the split needs outcome-set structure a bare latent-scale existential cannot see: outcome cardinality separates the two (⊤ vs 1) where the affectedness degree does not.

                                      source
                                      theorem Bhadra2024.roottype_bridge :
                                      RootType.result.entailsChange = true ∧ RootType.result.allowsRestitutiveAgain = false ∧ RootType.propertyConcept.entailsChange = false ∧ RootType.propertyConcept.allowsRestitutiveAgain = true

                                      RootTypology bridge: result roots entail change and lack the restitutive again reading; property-concept roots are the reverse.