Documentation

Linglib.Phenomena.Morphology.Studies.Bhadra2024

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 #

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

Substrate (was Theories/Morphology/ReversalRestitution.lean, relocated 0.230.455) #

The §§1-14 substrate below was previously a separate top-level theory file; Bhadra 2024 is the originating paper, so the substrate now anchors here per CLAUDE.md "every file is anchored". The deferred follow-up is to extract the theory-portable wing (ForceTransmissionClass, BoundaryStates operators, Set.multiMembered) into Theories/Semantics/ArgumentStructure/Affectedness/Profile.lean once a second consumer materialises.

inductive OutcomeCardinality :

Cardinality of a verb root's outcome set.

Instances For

@[implicit_reducible]

instance instDecidableEqOutcomeCardinality :

DecidableEq OutcomeCardinality

Equations

instDecidableEqOutcomeCardinality x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprOutcomeCardinality.repr :

OutcomeCardinality → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.
instReprOutcomeCardinality.repr OutcomeCardinality.multi prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OutcomeCardinality.multi")).group prec✝
instReprOutcomeCardinality.repr OutcomeCardinality.empty prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OutcomeCardinality.empty")).group prec✝

Instances For

@[implicit_reducible]

instance instReprOutcomeCardinality :

Repr OutcomeCardinality

Equations

instReprOutcomeCardinality = { reprPrec := instReprOutcomeCardinality.repr }

inductive ForceTransmissionClass :

potentialForChange : ForceTransmissionClass
impingementEffecting : ForceTransmissionClass
integralChange : ForceTransmissionClass
noForceTransmission : ForceTransmissionClass

Instances For

@[implicit_reducible]

instance instDecidableEqForceTransmissionClass :

DecidableEq ForceTransmissionClass

Equations

instDecidableEqForceTransmissionClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def instReprForceTransmissionClass.repr :

ForceTransmissionClass → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance instReprForceTransmissionClass :

Repr ForceTransmissionClass

Equations

instReprForceTransmissionClass = { reprPrec := instReprForceTransmissionClass.repr }

def ForceTransmissionClass.outcomeCardinality :

ForceTransmissionClass → OutcomeCardinality

Equations

Instances For

structure BoundaryStates (S : Type) :

pre : S
res : S

Instances For

@[implicit_reducible]

instance instBEqBoundaryStates {S : Type} [BEq S] :

BEq (BoundaryStates S)

Equations

instBEqBoundaryStates = { beq := fun (a b : BoundaryStates S) => a.pre == b.pre && a.res == b.res }

def reversible {S : Type} [BEq S] (base affixed : BoundaryStates S) :

Bool

Equations

reversible base affixed = (base.res == affixed.pre && affixed.res == base.pre)

Instances For

def restitutive {S : Type} [BEq S] (base affixed : BoundaryStates S) :

Bool

Equations

restitutive base affixed = (affixed.res == base.res)

Instances For

def ForceTransmissionClass.unCompatible :

ForceTransmissionClass → Bool

Equations

ForceTransmissionClass.potentialForChange.unCompatible = true
x✝.unCompatible = false

Instances For

def ForceTransmissionClass.reCompatible :

ForceTransmissionClass → Bool

Equations

ForceTransmissionClass.potentialForChange.reCompatible = true
ForceTransmissionClass.integralChange.reCompatible = true
x✝.reCompatible = false

Instances For

def LevinClass.forceTransmissionClass :

Semantics.Lexical.LevinClass → ForceTransmissionClass

Equations

Instances For

def LevinClass.reCompatible :

Semantics.Lexical.LevinClass → Bool

Equations

Instances For

theorem un_requires_multi (ftc : ForceTransmissionClass) :

ftc.unCompatible = true → ftc.outcomeCardinality = OutcomeCardinality.multi

theorem pfc_unique_overlap :

ForceTransmissionClass.potentialForChange.unCompatible = true ∧ ForceTransmissionClass.potentialForChange.reCompatible = true

theorem ie_disallows_both :

ForceTransmissionClass.impingementEffecting.unCompatible = false ∧ ForceTransmissionClass.impingementEffecting.reCompatible = false

theorem cos_un_blocked_re_available :

ForceTransmissionClass.integralChange.unCompatible = false ∧ ForceTransmissionClass.integralChange.reCompatible = true

theorem noforce_disallows_both :

ForceTransmissionClass.noForceTransmission.unCompatible = false ∧ ForceTransmissionClass.noForceTransmission.reCompatible = false

theorem pfc_orthogonal_to_hasResultState :

Semantics.Lexical.LevinClass.bend.eventTemplate.HasResultState ∧ ¬Semantics.Lexical.LevinClass.coil.eventTemplate.HasResultState ∧ LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.bend = ForceTransmissionClass.potentialForChange ∧ LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.coil = ForceTransmissionClass.potentialForChange

theorem bend_cos_per_levin_pfc_per_bhadra :

Semantics.Lexical.LevinClass.bend.meaningComponents.changeOfState = true ∧ LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.bend = ForceTransmissionClass.potentialForChange

theorem ie_templates :

Semantics.Lexical.LevinClass.wipe.eventTemplate = Features.EventStructure.Template.motionContact ∧ Semantics.Lexical.LevinClass.hit.eventTemplate = Features.EventStructure.Template.activity

theorem affectedness_bridge_pfc :

Semantics.ArgumentStructure.Affectedness.Profile.profileToDegree { volition := false, sentience := false, causation := false, movement := false, independentExistence := false, changeOfState := false, incrementalTheme := false, causallyAffected := true, stationary := true, dependentExistence := false } = Semantics.ArgumentStructure.Affectedness.Hierarchy.AffectednessDegree.potential

theorem affectedness_bridge_ie_kick :

Semantics.ArgumentStructure.Affectedness.Profile.profileToDegree Semantics.ArgumentStructure.EntailmentProfile.kickObjectProfile = Semantics.ArgumentStructure.Affectedness.Hierarchy.AffectednessDegree.nonquantized

theorem result_roots_singleton_outcomes :

RootType.result.entailsChange = true ∧ RootType.result.allowsRestitutiveAgain = false

theorem pc_roots_allow_restitutive_again :

RootType.propertyConcept.allowsRestitutiveAgain = true ∧ RootType.propertyConcept.entailsChange = false

@[reducible, inline]

abbrev StateFunction (Entity : Type u_4) (State : Type u_5) (Time : Type u_6) :

Type (max (max u_4 u_5) u_6)

Equations

StateFunction Entity State Time = (Time → Entity → State)

Instances For

@[reducible, inline]

abbrev Applies (Entity : Type u_4) (Time : Type u_5) [LinearOrder Time] :

Type (max u_4 u_5)

Equations

Applies Entity Time = (Entity → Semantics.Events.Event Time → Prop)

Instances For

structure VerbRootVRO (Entity : Type u_4) (State : Type u_5) (Time : Type u_6) [LinearOrder Time] :

Type (max (max u_4 u_5) u_6)

verb : Entity → Semantics.Events.Event Time → Prop
applies : Entity → Semantics.Events.Event Time → Prop
outcomes : Set State
thresholds : Set State

Instances For

def resState {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (stateAt : StateFunction Entity State Time) (e : Semantics.Events.Event Time) (x : Entity) :

State

Equations

resState stateAt e x = stateAt e.τ.finish x

Instances For

def preState {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (stateAt : StateFunction Entity State Time) (e : Semantics.Events.Event Time) (x : Entity) :

State

Equations

preState stateAt e x = stateAt e.τ.start x

Instances For

def Set.multiMembered {State : Type u_2} (s : Set State) :

Equations

s.multiMembered = ∃ (s₁ : State) (s₂ : State), s₁ ∈ s ∧ s₂ ∈ s ∧ s₁ ≠ s₂

Instances For

def unSem {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (stateAt : StateFunction Entity State Time) (vro : VerbRootVRO Entity State Time) (x : Entity) (e : Semantics.Events.Event Time) :

Equations

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

Instances For

def rePresupposition {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (stateAt : StateFunction Entity State Time) (vro : VerbRootVRO Entity State Time) (x : Entity) (e : Semantics.Events.Event Time) :

Equations

rePresupposition stateAt vro x e = ∃ (e' : Semantics.Events.Event Time), vro.verb x e' ∧ vro.applies x e' ∧ e'.τ.precedes e.τ ∧ resState stateAt e x = resState stateAt e' x

Instances For

def reSem {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (stateAt : StateFunction Entity State Time) (vro : VerbRootVRO Entity State Time) (x : Entity) (e : Semantics.Events.Event Time) :

Equations

reSem stateAt vro x e = (rePresupposition stateAt vro x e ∧ vro.applies x e ∧ vro.verb x e)

Instances For

theorem singleton_blocks_un {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (stateAt : StateFunction Entity State Time) (vro : VerbRootVRO Entity State Time) (h_single : ∃ (s : State), vro.outcomes = {s}) (x : Entity) (e : Semantics.Events.Event Time) :

¬unSem stateAt vro x e

theorem empty_blocks_un {Entity : Type u_1} {State : Type u_2} {Time : Type u_3} [LinearOrder Time] (stateAt : StateFunction Entity State Time) (vro : VerbRootVRO Entity State Time) (h_empty : vro.outcomes = ∅) (x : Entity) (e : Semantics.Events.Event Time) :

¬unSem stateAt vro x e

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 Bhadra2024.coil_un :

(LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.coil).unCompatible = true

PFC classes allow un-.

theorem Bhadra2024.bend_un :

(LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.bend).unCompatible = true

theorem Bhadra2024.break_no_un :

(LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.break_).unCompatible = false

COS classes disallow un-.

theorem Bhadra2024.color_no_un :

(LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.color).unCompatible = false

theorem Bhadra2024.build_no_un :

(LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.build).unCompatible = false

theorem Bhadra2024.destroy_no_un :

(LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.destroy).unCompatible = false

theorem Bhadra2024.eat_no_un :

(LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.eat).unCompatible = false

theorem Bhadra2024.calibratable_no_un :

(LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.calibratableCoS).unCompatible = false

theorem Bhadra2024.hit_no_un :

(LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.hit).unCompatible = false

IE classes disallow un-.

theorem Bhadra2024.wipe_no_un :

(LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.wipe).unCompatible = false

theorem Bhadra2024.swim_no_un :

(LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.mannerOfMotion).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 Bhadra2024.coil_re :

LevinClass.reCompatible Semantics.Lexical.LevinClass.coil = true

PFC classes allow re-.

theorem Bhadra2024.bend_re :

LevinClass.reCompatible Semantics.Lexical.LevinClass.bend = true

theorem Bhadra2024.break_re :

LevinClass.reCompatible Semantics.Lexical.LevinClass.break_ = true

Physical property and creation COS classes allow re-.

theorem Bhadra2024.color_re :

LevinClass.reCompatible Semantics.Lexical.LevinClass.color = true

theorem Bhadra2024.build_re :

LevinClass.reCompatible Semantics.Lexical.LevinClass.build = true

theorem Bhadra2024.otherCoS_re :

LevinClass.reCompatible Semantics.Lexical.LevinClass.otherCoS = true

theorem Bhadra2024.cooking_re :

LevinClass.reCompatible Semantics.Lexical.LevinClass.cooking = true

theorem Bhadra2024.destroy_no_re :

LevinClass.reCompatible Semantics.Lexical.LevinClass.destroy = false

Consumption, destruction, killing COS classes block re-.

theorem Bhadra2024.eat_no_re :

LevinClass.reCompatible Semantics.Lexical.LevinClass.eat = false

theorem Bhadra2024.murder_no_re :

LevinClass.reCompatible Semantics.Lexical.LevinClass.murder = false

theorem Bhadra2024.turn_no_re :

LevinClass.reCompatible Semantics.Lexical.LevinClass.turn = false

theorem Bhadra2024.hit_no_re :

LevinClass.reCompatible Semantics.Lexical.LevinClass.hit = false

IE classes block re-.

theorem Bhadra2024.wipe_no_re :

LevinClass.reCompatible Semantics.Lexical.LevinClass.wipe = false

theorem Bhadra2024.swim_no_re :

LevinClass.reCompatible Semantics.Lexical.LevinClass.mannerOfMotion = false

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

theorem Bhadra2024.pfc_multi :

ForceTransmissionClass.potentialForChange.outcomeCardinality = OutcomeCardinality.multi

PFC verbs have multi-membered outcome sets.

theorem Bhadra2024.ie_singleton :

ForceTransmissionClass.impingementEffecting.outcomeCardinality = OutcomeCardinality.singleton

IE verbs have singleton outcome sets (impingement only).

theorem Bhadra2024.cos_singleton :

ForceTransmissionClass.integralChange.outcomeCardinality = OutcomeCardinality.singleton

COS verbs have singleton outcome sets (specific result).

theorem Bhadra2024.nochange_empty :

ForceTransmissionClass.noForceTransmission.outcomeCardinality = OutcomeCardinality.empty

No-change verbs have empty outcome sets.

inductive Bhadra2024.ParchmentState :

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

Instances For

@[implicit_reducible]

instance Bhadra2024.instDecidableEqParchmentState :

DecidableEq ParchmentState

Equations

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

@[implicit_reducible]

instance Bhadra2024.instReprParchmentState :

Repr ParchmentState

Equations

Bhadra2024.instReprParchmentState = { reprPrec := Bhadra2024.instReprParchmentState.repr }

def Bhadra2024.instReprParchmentState.repr :

ParchmentState → ℕ → Std.Format

Equations

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

Instances For

def Bhadra2024.foldBoundary :

BoundaryStates ParchmentState

fold(parchment): flat → folded

Equations

Bhadra2024.foldBoundary = { pre := Bhadra2024.ParchmentState.flat, res := Bhadra2024.ParchmentState.folded }

Instances For

def Bhadra2024.unfoldBoundary :

BoundaryStates ParchmentState

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

Equations

Bhadra2024.unfoldBoundary = { pre := Bhadra2024.ParchmentState.folded, res := Bhadra2024.ParchmentState.flat }

Instances For

theorem 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 Bhadra2024.refoldBoundary :

BoundaryStates ParchmentState

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

Equations

Bhadra2024.refoldBoundary = { pre := Bhadra2024.ParchmentState.flat, res := Bhadra2024.ParchmentState.folded }

Instances For

theorem Bhadra2024.fold_refold_restitutive :

restitutive foldBoundary refoldBoundary = true

inductive Bhadra2024.WallState :

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

unpainted : WallState
painted : WallState

Instances For

@[implicit_reducible]

instance Bhadra2024.instDecidableEqWallState :

DecidableEq WallState

Equations

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

@[implicit_reducible]

instance Bhadra2024.instReprWallState :

Equations

Bhadra2024.instReprWallState = { reprPrec := Bhadra2024.instReprWallState.repr }

def Bhadra2024.instReprWallState.repr :

WallState → ℕ → Std.Format

Equations

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

Instances For

def Bhadra2024.paintBoundary :

BoundaryStates WallState

Equations

Bhadra2024.paintBoundary = { pre := Bhadra2024.WallState.unpainted, res := Bhadra2024.WallState.painted }

Instances For

def Bhadra2024.repaintBoundary :

BoundaryStates WallState

Equations

Bhadra2024.repaintBoundary = { pre := Bhadra2024.WallState.unpainted, res := Bhadra2024.WallState.painted }

Instances For

theorem Bhadra2024.paint_repaint_restitutive :

restitutive paintBoundary repaintBoundary = true

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

theorem Bhadra2024.paint_un_blocked :

(LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.color).unCompatible = false

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

theorem 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 Bhadra2024.bend_reclassification :

Semantics.Lexical.LevinClass.bend.meaningComponents.changeOfState = true ∧ LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.bend = ForceTransmissionClass.potentialForChange ∧ (LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.bend).unCompatible = true ∧ LevinClass.reCompatible Semantics.Lexical.LevinClass.bend = 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 Bhadra2024.motionContact_is_ie :

Semantics.Lexical.LevinClass.wipe.eventTemplate = Features.EventStructure.Template.motionContact ∧ LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.wipe = 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 Bhadra2024.kick_end_to_end :

Fragments.English.Predicates.Verbal.kick.levinClass = some Semantics.Lexical.LevinClass.hit ∧ LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.hit = ForceTransmissionClass.impingementEffecting ∧ (LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.hit).unCompatible = false ∧ LevinClass.reCompatible Semantics.Lexical.LevinClass.hit = 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 Bhadra2024.bend_end_to_end :

Fragments.English.Predicates.Verbal.bend.levinClass = some Semantics.Lexical.LevinClass.bend ∧ LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.bend = ForceTransmissionClass.potentialForChange ∧ (LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.bend).unCompatible = true ∧ LevinClass.reCompatible Semantics.Lexical.LevinClass.bend = 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 Bhadra2024.break_end_to_end :

Fragments.English.Predicates.Verbal.break_.levinClass = some Semantics.Lexical.LevinClass.break_ ∧ LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.break_ = ForceTransmissionClass.integralChange ∧ (LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.break_).unCompatible = false ∧ LevinClass.reCompatible Semantics.Lexical.LevinClass.break_ = 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 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.

Instances For

theorem Bhadra2024.fold_outcomes_multi :

foldVRO.outcomes.multiMembered

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

inductive Bhadra2024.LimbState :

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

intact : LimbState
broken : LimbState

Instances For

@[implicit_reducible]

instance Bhadra2024.instDecidableEqLimbState :

DecidableEq LimbState

Equations

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

def Bhadra2024.instReprLimbState.repr :

LimbState → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Bhadra2024.instReprLimbState :

Equations

Bhadra2024.instReprLimbState = { reprPrec := Bhadra2024.instReprLimbState.repr }

def Bhadra2024.breakVRO :

VerbRootVRO Unit LimbState ℤ

Equations

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

Instances For

theorem Bhadra2024.break_blocks_un (stateAt : StateFunction Unit LimbState ℤ) (x : Unit) (e : Semantics.Events.Event ℤ) :

¬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 Bhadra2024.SurfaceState :

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

Instances For

@[implicit_reducible]

instance Bhadra2024.instDecidableEqSurfaceState :

DecidableEq SurfaceState

Equations

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

@[implicit_reducible]

instance Bhadra2024.instReprSurfaceState :

Repr SurfaceState

Equations

Bhadra2024.instReprSurfaceState = { reprPrec := Bhadra2024.instReprSurfaceState.repr }

def Bhadra2024.instReprSurfaceState.repr :

SurfaceState → ℕ → Std.Format

Equations

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

Instances For

def Bhadra2024.hitVRO :

VerbRootVRO Unit SurfaceState ℤ

Equations

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

Instances For

theorem Bhadra2024.hit_blocks_un (stateAt : StateFunction Unit SurfaceState ℤ) (x : Unit) (e : Semantics.Events.Event ℤ) :

¬unSem stateAt hitVRO x e

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

inductive Bhadra2024.ObjectExistence :

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

Instances For

@[implicit_reducible]

instance Bhadra2024.instDecidableEqObjectExistence :

DecidableEq ObjectExistence

Equations

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

@[implicit_reducible]

instance Bhadra2024.instReprObjectExistence :

Repr ObjectExistence

Equations

Bhadra2024.instReprObjectExistence = { reprPrec := Bhadra2024.instReprObjectExistence.repr }

def Bhadra2024.instReprObjectExistence.repr :

ObjectExistence → ℕ → Std.Format

Equations

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

Instances For

def Bhadra2024.destroyVRO :

VerbRootVRO Unit ObjectExistence ℤ

Equations

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

Instances For

theorem Bhadra2024.destroy_blocks_un (stateAt : StateFunction Unit ObjectExistence ℤ) (x : Unit) (e : Semantics.Events.Event ℤ) :

¬unSem stateAt destroyVRO x e

destroy blocks un- (singleton outcomes).

theorem 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 Bhadra2024.fold_un_satisfiable :

∃ (stateAt : StateFunction Unit ParchmentState ℤ) (x : Unit) (e : Semantics.Events.Event ℤ), unSem stateAt foldVRO x e

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

theorem Bhadra2024.fold_re_satisfiable :

∃ (stateAt : StateFunction Unit ParchmentState ℤ) (x : Unit) (e : Semantics.Events.Event ℤ), 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 Bhadra2024.break_re_satisfiable :

∃ (stateAt : StateFunction Unit LimbState ℤ) (x : Unit) (e : Semantics.Events.Event ℤ), 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 Bhadra2024.cross_layer_un_agreement :

(LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.bend).unCompatible = true ∧ (LevinClass.forceTransmissionClass Semantics.Lexical.LevinClass.break_).unCompatible = false ∧ (∃ (stateAt : StateFunction Unit ParchmentState ℤ) (x : Unit) (e : Semantics.Events.Event ℤ), unSem stateAt foldVRO x e) ∧ ∀ (stateAt : StateFunction Unit LimbState ℤ) (x : Unit) (e : Semantics.Events.Event ℤ), ¬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 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.

Instances For

theorem Bhadra2024.destroy_re_blocked_compositionally :

¬reSem Bhadra2024.postDestroyState✝ (destroyVRO_withApplies Bhadra2024.postDestroyState✝) () 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 Bhadra2024.cross_layer_re_agreement :

LevinClass.reCompatible Semantics.Lexical.LevinClass.destroy = false ∧ LevinClass.reCompatible Semantics.Lexical.LevinClass.break_ = true ∧ ¬reSem Bhadra2024.postDestroyState✝ (destroyVRO_withApplies Bhadra2024.postDestroyState✝) () Bhadra2024.ev₃✝ ∧ ∃ (stateAt : StateFunction Unit LimbState ℤ) (x : Unit) (e : Semantics.Events.Event ℤ), 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).