Bhadra 2024: Verb roots encode outcomes

@cite{bhadra-2024}

Bhadra, D. (2024). Verb roots encode outcomes: argument structure and lexical semantics of reversal and restitution. Linguistics and Philosophy 47: 557–610.

Summary

The reversative prefix un- and the restitutive prefix re- are sensitive to the outcome set of the base verb root. All verb roots come equipped with sets of outcomes (possible states of the object after the action). The cardinality of this set determines affix compatibility:

• PFC verbs (fold, wrap, coil): multi-membered outcomes → un- ✓, re- ✓
• IE verbs (hit, scrub, kick): singleton outcomes, surface only → un- ✗, re- ✗
• COS verbs (break, destroy, paint): singleton outcomes → un- ✗, re- partial

Key formalizations

1. ForceTransmissionClass classifies verbs by impact type (§§2, 3, 4)
2. BoundaryStates formalizes res/pre operators for state equivalence (§5.2)
3. LevinClass.forceTransmissionClass bridges Levin classes to outcome classes
4. Per-verb un- and re- predictions verified against empirical data from (12), (45)

Only surface contact verbs (PFC class) allow un-: - (d) Surface contact: unpin, unwrap, untwist, unpack, unplug ✓ - (a) Physical property: *unpaint, *unclean, *unfix, *unbreak ✗ - (b) Transforms: *unturn, *uncarve ✗ - (e) Creation: *unbuild, *unconstruct ✗ - (f) Consumption: *undestroy, *uneat ✗ - (g) Degree achievements: *unfill, *unwarm ✗ - (h) No change: *unswim, *unwalk ✗

theorem Phenomena.Morphology.Studies.Bhadra2024.coil_un : LevinClass.coil.forceTransmissionClass.unCompatible = true

PFC classes allow un-.

theorem Phenomena.Morphology.Studies.Bhadra2024.bend_un : LevinClass.bend.forceTransmissionClass.unCompatible = true

theorem Phenomena.Morphology.Studies.Bhadra2024.break_no_un : LevinClass.break_.forceTransmissionClass.unCompatible = false

COS classes disallow un-.

theorem Phenomena.Morphology.Studies.Bhadra2024.color_no_un : LevinClass.color.forceTransmissionClass.unCompatible = false

theorem Phenomena.Morphology.Studies.Bhadra2024.build_no_un : LevinClass.build.forceTransmissionClass.unCompatible = false

theorem Phenomena.Morphology.Studies.Bhadra2024.destroy_no_un : LevinClass.destroy.forceTransmissionClass.unCompatible = false

theorem Phenomena.Morphology.Studies.Bhadra2024.eat_no_un : LevinClass.eat.forceTransmissionClass.unCompatible = false

theorem Phenomena.Morphology.Studies.Bhadra2024.calibratable_no_un : LevinClass.calibratableCoS.forceTransmissionClass.unCompatible = false

theorem Phenomena.Morphology.Studies.Bhadra2024.hit_no_un : LevinClass.hit.forceTransmissionClass.unCompatible = false

IE classes disallow un-.

theorem Phenomena.Morphology.Studies.Bhadra2024.wipe_no_un : LevinClass.wipe.forceTransmissionClass.unCompatible = false

theorem Phenomena.Morphology.Studies.Bhadra2024.swim_no_un : LevinClass.mannerOfMotion.forceTransmissionClass.unCompatible = false

No-change classes disallow un-.

re- is more permissive than un-: - (a) Physical property: repaint ✓, reclean ✓, refix ✓, rebreak ✓ - (d) Surface contact: repin ✓, rewrap ✓, retwist ✓ - (e) Creation: rebuild ✓, reconstruct ✓, recreate ✓ - (g) Degree achievements: refill ⊳, rewarm ⊳ But re- is blocked when the object is eliminated: - (f) Consumption: *redestroy, *reeat ✗ - (b) Transforms: *retransform ✗ (mostly) - IE: *rehit, *rescrub ✗ - No change: *reswim, *rewalk ✗

theorem Phenomena.Morphology.Studies.Bhadra2024.coil_re : LevinClass.coil.reCompatible = true

PFC classes allow re-.

theorem Phenomena.Morphology.Studies.Bhadra2024.bend_re : LevinClass.bend.reCompatible = true

theorem Phenomena.Morphology.Studies.Bhadra2024.break_re : LevinClass.break_.reCompatible = true

Physical property and creation COS classes allow re-.

theorem Phenomena.Morphology.Studies.Bhadra2024.color_re : LevinClass.color.reCompatible = true

theorem Phenomena.Morphology.Studies.Bhadra2024.build_re : LevinClass.build.reCompatible = true

theorem Phenomena.Morphology.Studies.Bhadra2024.otherCoS_re : LevinClass.otherCoS.reCompatible = true

theorem Phenomena.Morphology.Studies.Bhadra2024.cooking_re : LevinClass.cooking.reCompatible = true

theorem Phenomena.Morphology.Studies.Bhadra2024.destroy_no_re : LevinClass.destroy.reCompatible = false

Consumption, destruction, killing COS classes block re-.

theorem Phenomena.Morphology.Studies.Bhadra2024.eat_no_re : LevinClass.eat.reCompatible = false

theorem Phenomena.Morphology.Studies.Bhadra2024.murder_no_re : LevinClass.murder.reCompatible = false

theorem Phenomena.Morphology.Studies.Bhadra2024.turn_no_re : LevinClass.turn.reCompatible = false

theorem Phenomena.Morphology.Studies.Bhadra2024.hit_no_re : LevinClass.hit.reCompatible = false

IE classes block re-.

theorem Phenomena.Morphology.Studies.Bhadra2024.wipe_no_re : LevinClass.wipe.reCompatible = false

theorem Phenomena.Morphology.Studies.Bhadra2024.swim_no_re : LevinClass.mannerOfMotion.reCompatible = false

No-change classes block re- (paper's (45h): *reswim, *rewalk).

theorem Phenomena.Morphology.Studies.Bhadra2024.pfc_multi : ForceTransmissionClass.potentialForChange.outcomeCardinality = OutcomeCardinality.multi

PFC verbs have multi-membered outcome sets.

theorem Phenomena.Morphology.Studies.Bhadra2024.ie_singleton : ForceTransmissionClass.impingementEffecting.outcomeCardinality = OutcomeCardinality.singleton

IE verbs have singleton outcome sets (impingement only).

theorem Phenomena.Morphology.Studies.Bhadra2024.cos_singleton : ForceTransmissionClass.integralChange.outcomeCardinality = OutcomeCardinality.singleton

COS verbs have singleton outcome sets (specific result).

theorem Phenomena.Morphology.Studies.Bhadra2024.nochange_empty : ForceTransmissionClass.noForceTransmission.outcomeCardinality = OutcomeCardinality.empty

No-change verbs have empty outcome sets.

inductive Phenomena.Morphology.Studies.Bhadra2024.ParchmentState : Type

Possible states of a parchment under folding. Illustrates the multi-membered outcome set of a PFC verb: folding can yield any of these states depending on the force and manner of folding.

• flat : ParchmentState
• slightlyCreased : ParchmentState
• folded : ParchmentState
• tightlyFolded : ParchmentState

instance Phenomena.Morphology.Studies.Bhadra2024.instDecidableEqParchmentState : DecidableEq ParchmentState

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instDecidableEqParchmentState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Morphology.Studies.Bhadra2024.instBEqParchmentState : BEq ParchmentState

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instBEqParchmentState = { beq := Phenomena.Morphology.Studies.Bhadra2024.instBEqParchmentState.beq }

def Phenomena.Morphology.Studies.Bhadra2024.instBEqParchmentState.beq : ParchmentState → ParchmentState → Bool

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instBEqParchmentState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Morphology.Studies.Bhadra2024.instReprParchmentState : Repr ParchmentState

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instReprParchmentState = { reprPrec := Phenomena.Morphology.Studies.Bhadra2024.instReprParchmentState.repr }

def Phenomena.Morphology.Studies.Bhadra2024.instReprParchmentState.repr : ParchmentState → ℕ → Std.Format

Equations

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

def Phenomena.Morphology.Studies.Bhadra2024.foldBoundary : BoundaryStates ParchmentState

fold(parchment): flat → folded

Equations

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

def Phenomena.Morphology.Studies.Bhadra2024.unfoldBoundary : BoundaryStates ParchmentState

unfold(parchment): folded → flat (reverses fold)

Equations

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

theorem Phenomena.Morphology.Studies.Bhadra2024.fold_unfold_reversible : reversible foldBoundary unfoldBoundary = true

Reversibility: fold and unfold satisfy the inverse equivalence condition. res(fold) = pre(unfold) and res(unfold) = pre(fold).

def Phenomena.Morphology.Studies.Bhadra2024.refoldBoundary : BoundaryStates ParchmentState

Restitution: refold achieves the same result as fold. res(refold) = res(fold).

Equations

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

theorem Phenomena.Morphology.Studies.Bhadra2024.fold_refold_restitutive : restitutive foldBoundary refoldBoundary = true

inductive Phenomena.Morphology.Studies.Bhadra2024.WallState : Type

States of a wall under painting. Singleton outcome set: painting deterministically yields the painted state.

• unpainted : WallState
• painted : WallState

instance Phenomena.Morphology.Studies.Bhadra2024.instDecidableEqWallState : DecidableEq WallState

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instDecidableEqWallState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Morphology.Studies.Bhadra2024.instBEqWallState : BEq WallState

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instBEqWallState = { beq := Phenomena.Morphology.Studies.Bhadra2024.instBEqWallState.beq }

def Phenomena.Morphology.Studies.Bhadra2024.instBEqWallState.beq : WallState → WallState → Bool

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instBEqWallState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Morphology.Studies.Bhadra2024.instReprWallState.repr : WallState → ℕ → Std.Format

Equations

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

instance Phenomena.Morphology.Studies.Bhadra2024.instReprWallState : Repr WallState

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instReprWallState = { reprPrec := Phenomena.Morphology.Studies.Bhadra2024.instReprWallState.repr }

def Phenomena.Morphology.Studies.Bhadra2024.paintBoundary : BoundaryStates WallState

Equations

• Phenomena.Morphology.Studies.Bhadra2024.paintBoundary = { pre := Phenomena.Morphology.Studies.Bhadra2024.WallState.unpainted, res := Phenomena.Morphology.Studies.Bhadra2024.WallState.painted }

def Phenomena.Morphology.Studies.Bhadra2024.repaintBoundary : BoundaryStates WallState

Equations

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

theorem Phenomena.Morphology.Studies.Bhadra2024.paint_repaint_restitutive : restitutive paintBoundary repaintBoundary = true

repaint satisfies restitution: res(repaint) = res(paint).

theorem Phenomena.Morphology.Studies.Bhadra2024.paint_un_blocked : LevinClass.color.forceTransmissionClass.unCompatible = false

*unpaint is blocked: color (24) is COS with singleton outcomes. un- requires multi-membered outcomes (PFC only).

theorem Phenomena.Morphology.Studies.Bhadra2024.pfc_is_overlap_class : (ForceTransmissionClass.potentialForChange.unCompatible = true ∧ ForceTransmissionClass.potentialForChange.reCompatible = true) ∧ ForceTransmissionClass.impingementEffecting.unCompatible = false ∧ ForceTransmissionClass.integralChange.unCompatible = false ∧ ForceTransmissionClass.noForceTransmission.unCompatible = false

PFC is the unique class compatible with BOTH un- and re-. This is the central distributional generalization of the paper.

theorem Phenomena.Morphology.Studies.Bhadra2024.bend_reclassification : LevinClass.bend.meaningComponents.changeOfState = true ∧ LevinClass.bend.forceTransmissionClass = ForceTransmissionClass.potentialForChange ∧ LevinClass.bend.forceTransmissionClass.unCompatible = true ∧ LevinClass.bend.reCompatible = true

@cite{bhadra-2024} reclassifies the bend class (45.2) from COS to PFC.

@cite{levin-1993}: bend has changeOfState = true (diagnosed by causative/inchoative alternation: "the paper folded" / "she folded the paper").

@cite{bhadra-2024}: fold has multi-membered outcomes (slightly creased, halfway bent, tightly folded, etc.) → PFC, not COS. The change IS possible but not to a SPECIFIC fixed state.

This is the paper's central theoretical move: outcome set structure is a finer-grained classification than the traditional COS label.

theorem Phenomena.Morphology.Studies.Bhadra2024.motionContact_is_ie : LevinClass.wipe.eventTemplate = Semantics.Lexical.Verb.EventStructure.Template.motionContact ∧ LevinClass.wipe.forceTransmissionClass = ForceTransmissionClass.impingementEffecting

@cite{rappaport-hovav-levin-2024}'s motionContact template corresponds exactly to @cite{bhadra-2024}'s IE class. The wipe class (10.4) has the motionContact template and is classified as IE.

theorem Phenomena.Morphology.Studies.Bhadra2024.kick_end_to_end : Fragments.English.Predicates.Verbal.kick.levinClass = some LevinClass.hit ∧ LevinClass.hit.forceTransmissionClass = ForceTransmissionClass.impingementEffecting ∧ LevinClass.hit.forceTransmissionClass.unCompatible = false ∧ LevinClass.hit.reCompatible = false

End-to-end chain: the Fragment entry for "kick" (Levin 18.1 hit class) derives IE classification and correctly predicts both un- and re- blocking. kick.levinClass → .hit → .impingementEffecting → unCompatible=false, reCompatible=false

theorem Phenomena.Morphology.Studies.Bhadra2024.bend_end_to_end : Fragments.English.Predicates.Verbal.bend.levinClass = some LevinClass.bend ∧ LevinClass.bend.forceTransmissionClass = ForceTransmissionClass.potentialForChange ∧ LevinClass.bend.forceTransmissionClass.unCompatible = true ∧ LevinClass.bend.reCompatible = true

End-to-end chain: the Fragment entry for "bend" (Levin 45.2) derives PFC classification and correctly predicts both un- and re- compatibility. bend.levinClass → .bend → .potentialForChange → unCompatible=true, reCompatible=true

theorem Phenomena.Morphology.Studies.Bhadra2024.break_end_to_end : Fragments.English.Predicates.Verbal.break_.levinClass = some LevinClass.break_ ∧ LevinClass.break_.forceTransmissionClass = ForceTransmissionClass.integralChange ∧ LevinClass.break_.forceTransmissionClass.unCompatible = false ∧ LevinClass.break_.reCompatible = true

End-to-end chain: the Fragment entry for "break" (Levin 45.1) derives COS classification → un- blocked, re- allowed. break.levinClass → .break_ → .integralChange → unCompatible=false, reCompatible=true

def Phenomena.Morphology.Studies.Bhadra2024.foldVRO : VerbRootVRO Unit ParchmentState ℤ

VRO for "fold": PFC verb with multi-membered outcome set. The parchment can end up in any of several states after folding. Outcome set = {slightlyCreased, folded, tightlyFolded} (3 members). Threshold set = {flat, slightlyCreased} (contextual pre-states).

Equations

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

theorem Phenomena.Morphology.Studies.Bhadra2024.fold_outcomes_multi : foldVRO.outcomes.multiMembered

fold's outcome set is multi-membered: slightlyCreased ≠ folded.

inductive Phenomena.Morphology.Studies.Bhadra2024.LimbState : Type

VRO for "break": COS verb with singleton outcome set. Breaking yields exactly one lexically specified result: broken.

• intact : LimbState
• broken : LimbState

instance Phenomena.Morphology.Studies.Bhadra2024.instDecidableEqLimbState : DecidableEq LimbState

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instDecidableEqLimbState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Morphology.Studies.Bhadra2024.instBEqLimbState : BEq LimbState

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instBEqLimbState = { beq := Phenomena.Morphology.Studies.Bhadra2024.instBEqLimbState.beq }

def Phenomena.Morphology.Studies.Bhadra2024.instBEqLimbState.beq : LimbState → LimbState → Bool

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instBEqLimbState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Morphology.Studies.Bhadra2024.instReprLimbState.repr : LimbState → ℕ → Std.Format

Equations

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

instance Phenomena.Morphology.Studies.Bhadra2024.instReprLimbState : Repr LimbState

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instReprLimbState = { reprPrec := Phenomena.Morphology.Studies.Bhadra2024.instReprLimbState.repr }

def Phenomena.Morphology.Studies.Bhadra2024.breakVRO : VerbRootVRO Unit LimbState ℤ

Equations

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

theorem Phenomena.Morphology.Studies.Bhadra2024.break_blocks_un (stateAt : StateFunction Unit LimbState ℤ) (x : Unit) (e : Semantics.Events.Ev ℤ) : ¬unSem stateAt breakVRO x e

break's singleton outcome set blocks un-: *unbreak is predicted to fail because |O| = 1, so the multi-membered presupposition of un- (eq. 66) cannot be satisfied.

inductive Phenomena.Morphology.Studies.Bhadra2024.SurfaceState : Type

VRO for "hit": IE verb with singleton outcome set (surface alteration). The object's surface is altered in exactly one way.

• unaltered : SurfaceState
• surfaceAltered : SurfaceState

instance Phenomena.Morphology.Studies.Bhadra2024.instDecidableEqSurfaceState : DecidableEq SurfaceState

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instDecidableEqSurfaceState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Morphology.Studies.Bhadra2024.instBEqSurfaceState : BEq SurfaceState

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instBEqSurfaceState = { beq := Phenomena.Morphology.Studies.Bhadra2024.instBEqSurfaceState.beq }

def Phenomena.Morphology.Studies.Bhadra2024.instBEqSurfaceState.beq : SurfaceState → SurfaceState → Bool

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instBEqSurfaceState.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Morphology.Studies.Bhadra2024.instReprSurfaceState : Repr SurfaceState

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instReprSurfaceState = { reprPrec := Phenomena.Morphology.Studies.Bhadra2024.instReprSurfaceState.repr }

def Phenomena.Morphology.Studies.Bhadra2024.instReprSurfaceState.repr : SurfaceState → ℕ → Std.Format

Equations

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

def Phenomena.Morphology.Studies.Bhadra2024.hitVRO : VerbRootVRO Unit SurfaceState ℤ

Equations

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

theorem Phenomena.Morphology.Studies.Bhadra2024.hit_blocks_un (stateAt : StateFunction Unit SurfaceState ℤ) (x : Unit) (e : Semantics.Events.Ev ℤ) : ¬unSem stateAt hitVRO x e

hit's singleton outcome set blocks un-: *unhit is predicted to fail for the same reason as *unbreak.

inductive Phenomena.Morphology.Studies.Bhadra2024.ObjectExistence : Type

VRO for "destroy": COS consumption verb with singleton outcome set. The outcome (ceased to exist) is also a blocking threshold for re-, since the object cannot be acted on again after being destroyed.

• exists_ : ObjectExistence
• ceasedToExist : ObjectExistence

instance Phenomena.Morphology.Studies.Bhadra2024.instDecidableEqObjectExistence : DecidableEq ObjectExistence

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instDecidableEqObjectExistence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Morphology.Studies.Bhadra2024.instBEqObjectExistence : BEq ObjectExistence

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instBEqObjectExistence = { beq := Phenomena.Morphology.Studies.Bhadra2024.instBEqObjectExistence.beq }

def Phenomena.Morphology.Studies.Bhadra2024.instBEqObjectExistence.beq : ObjectExistence → ObjectExistence → Bool

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instBEqObjectExistence.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Morphology.Studies.Bhadra2024.instReprObjectExistence.repr : ObjectExistence → ℕ → Std.Format

Equations

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

instance Phenomena.Morphology.Studies.Bhadra2024.instReprObjectExistence : Repr ObjectExistence

Equations

• Phenomena.Morphology.Studies.Bhadra2024.instReprObjectExistence = { reprPrec := Phenomena.Morphology.Studies.Bhadra2024.instReprObjectExistence.repr }

def Phenomena.Morphology.Studies.Bhadra2024.destroyVRO : VerbRootVRO Unit ObjectExistence ℤ

Equations

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

theorem Phenomena.Morphology.Studies.Bhadra2024.destroy_blocks_un (stateAt : StateFunction Unit ObjectExistence ℤ) (x : Unit) (e : Semantics.Events.Ev ℤ) : ¬unSem stateAt destroyVRO x e

destroy blocks un- (singleton outcomes).

theorem Phenomena.Morphology.Studies.Bhadra2024.distributional_split_derived : foldVRO.outcomes.multiMembered ∧ (∃ (s : LimbState), breakVRO.outcomes = {s}) ∧ ∃ (s : SurfaceState), hitVRO.outcomes = {s}

The three-way distributional split is derived from outcome set structure:

• PFC (fold): multi-membered → un- possible
• COS (break): singleton → un- blocked
• IE (hit): singleton → un- blocked

The theorems in § 10 prove that un- is BLOCKED for certain verb classes. But blocking theorems alone don't guarantee the compositional semantics is non-vacuous. We also need to show un- and re- are SATISFIABLE for the classes that should allow them. The following construct concrete event witnesses and state functions to demonstrate positive satisfiability.

theorem Phenomena.Morphology.Studies.Bhadra2024.fold_un_satisfiable : ∃ (stateAt : StateFunction Unit ParchmentState ℤ) (x : Unit) (e : Semantics.Events.Ev ℤ), unSem stateAt foldVRO x e

Positive existence: un- IS satisfiable for PFC verbs. Constructs a concrete witness showing unSem holds for fold.

theorem Phenomena.Morphology.Studies.Bhadra2024.fold_re_satisfiable : ∃ (stateAt : StateFunction Unit ParchmentState ℤ) (x : Unit) (e : Semantics.Events.Ev ℤ), reSem stateAt foldVRO x e

Positive existence: re- IS satisfiable for PFC verbs. Three-event scenario: fold(ev₁), unfold(ev₂), refold(ev₃). The rePresupposition of ev₃ is witnessed by ev₁ (prior fold with matching result state).

theorem Phenomena.Morphology.Studies.Bhadra2024.break_re_satisfiable : ∃ (stateAt : StateFunction Unit LimbState ℤ) (x : Unit) (e : Semantics.Events.Ev ℤ), reSem stateAt breakVRO x e

Positive existence: re- IS satisfiable for COS verbs. COS verbs (break) block un- but allow re-. This demonstrates that reSem is satisfiable for break despite singleton outcomes.

theorem Phenomena.Morphology.Studies.Bhadra2024.cross_layer_un_agreement : LevinClass.bend.forceTransmissionClass.unCompatible = true ∧ LevinClass.break_.forceTransmissionClass.unCompatible = false ∧ (∃ (stateAt : StateFunction Unit ParchmentState ℤ) (x : Unit) (e : Semantics.Events.Ev ℤ), unSem stateAt foldVRO x e) ∧ ∀ (stateAt : StateFunction Unit LimbState ℤ) (x : Unit) (e : Semantics.Events.Ev ℤ), ¬unSem stateAt breakVRO x e

Cross-layer agreement: Boolean and compositional predictions align. The Boolean layer (ForceTransmissionClass) and compositional layer (VRO) agree on the un- prediction for fold (both allow) and break (both block).

With APPLIES in the semantics, we can now compositionally derive that *redestroy is blocked — not just via the Boolean layer, but because APPLIES fails when the object has ceased to exist. This closes the gap between the Boolean prediction (destroy_no_re) and the compositional semantics (reSem).

def Phenomena.Morphology.Studies.Bhadra2024.destroyVRO_withApplies (stateAt : StateFunction Unit ObjectExistence ℤ) : VerbRootVRO Unit ObjectExistence ℤ

VRO for "destroy" with state-aware APPLIES: force can only be exerted on an object that exists at the start of the event. The applies predicate is parameterized by a state function, capturing the fact that you can't destroy what doesn't exist.

Equations

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

theorem Phenomena.Morphology.Studies.Bhadra2024.destroy_re_blocked_compositionally : ¬reSem Phenomena.Morphology.Studies.Bhadra2024.postDestroyState✝ (destroyVRO_withApplies Phenomena.Morphology.Studies.Bhadra2024.postDestroyState✝¹) () Phenomena.Morphology.Studies.Bhadra2024.ev₃✝

Compositional re- blocking for destroy. With state-aware APPLIES, reSem is unsatisfiable for destroy because the re-event requires APPLIES(e)(x), but the object has ceased to exist after the first destruction. The proof shows the assertion's APPLIES condition directly contradicts the post-destruction state.

theorem Phenomena.Morphology.Studies.Bhadra2024.cross_layer_re_agreement : LevinClass.destroy.reCompatible = false ∧ LevinClass.break_.reCompatible = true ∧ ¬reSem Phenomena.Morphology.Studies.Bhadra2024.postDestroyState✝ (destroyVRO_withApplies Phenomena.Morphology.Studies.Bhadra2024.postDestroyState✝¹) () Phenomena.Morphology.Studies.Bhadra2024.ev₃✝ ∧ ∃ (stateAt : StateFunction Unit LimbState ℤ) (x : Unit) (e : Semantics.Events.Ev ℤ), reSem stateAt breakVRO x e

Cross-layer re- agreement for destroy. The Boolean layer (destroy_no_re) and the compositional layer (destroy_re_blocked_compositionally) now agree: *redestroy is blocked at both levels.

For break, both layers agree that re- IS allowed: Boolean (break_re) and compositional (break_re_satisfiable).