Affectedness Hierarchy: EntailmentProfile Projection #

@cite{beavers-2010} @cite{dowty-1991} @cite{beavers-2011} @cite{beavers-koontz-garboden-2020}

The affectedness hierarchy is a projection of @cite{dowty-1991}'s P-Patient entailments onto a four-level total order measuring the strength of truth conditions about change in the affected argument.

The AffectednessDegree enum and the typeclass extends chain (IsUnspecifiedAffected → IsPotentialAffected → IsNonQuantizedAffected → IsQuantizedAffected) live in Theories/Semantics/Events/Scalar/Affectedness.lean (substrate-level, referenceable by K98 verb-class typeclasses). This file's role: project Dowty's EntailmentProfile to AffectednessDegree and verify the projection on canonical verb profiles. The enum, strength, and LE instance are re-exported here for backward compatibility with existing consumers.

As a projection of EntailmentProfile #

profileToDegree projects the 10-Boolean EntailmentProfile onto AffectednessDegree, retaining only the P-Patient features relevant to truth-conditional strength. The projection depends on exactly 4 of the 10 features: changeOfState, incrementalTheme, causallyAffected, and stationary. All 5 P-Agent features and dependentExistence are irrelevant (profileToDegree_depends_only_on_patient).

This is one of three canonical projections of EntailmentProfile:

AgentivityNode.fromEntailmentProfile → agentivity lattice (@cite{grimm-2011})
profileToDegree → affectedness hierarchy (@cite{beavers-2010}) ← this file
PersistenceLevel.fromPatientProfile → persistence lattice (@cite{grimm-2011})

Each projection preserves different information and serves different grammatical predictions:

Projection	Preserves	Used for
AgentivityNode	4 P-Agent features	Subject selection, case
AffectednessDegree	P-Patient strength	MAP, direct/oblique
PersistenceLevel	Persistence pattern	Case regions, DOM

Grammatical consequence #

The affectedness hierarchy predicts the Morphosyntactic Alignment Principle (MAP): when an argument alternates between direct and oblique realization, the direct variant has truth conditions at least as strong as the oblique. See Phenomena/ArgumentStructure/Studies/Beavers2010.lean for the empirical verification.

Interface to root semantics #

AffectednessDegree relates to three levels of change-of-state representation in the codebase:

EntailmentProfile.changeOfState — the proto-patient entailment (this file's input)
MeaningComponents.changeOfState — the surface diagnostic (in Core/RootDimensions)
RootEntailments.result — whether the root itself entails change (in Core/RootDimensions)

These are NOT the same concept. @cite{beavers-koontz-garboden-2020} show that surface CoS can come from either the root or the template. The projection here operates on the proto-role level, which is the final composed meaning — not the root-level or surface-diagnostic level.

The 4-level Beavers affectedness enum, declared in Theories/Semantics/Events/Scalar/Affectedness.lean and re-exported here for backward compatibility with consumers (Beavers2010, BeaversUdayana2022, StapsRooryck2024, AgentivityLattice).

source

def Semantics.ArgumentStructure.Affectedness.Profile.profileToDegree (p : EntailmentProfile.EntailmentProfile) :

AffectednessDegree

Project an EntailmentProfile onto the affectedness hierarchy.

This is the canonical P-Patient projection: it retains truth-conditional strength while discarding the specific identity of the entailments.

The projection depends on exactly 4 of the 10 features:

changeOfState and incrementalTheme (distinguish quantized/nonquantized)
causallyAffected and stationary (distinguish potential/unspecified)

All 5 P-Agent features and dependentExistence are irrelevant (profileToDegree_depends_only_on_patient).

@cite{beavers-2010} Table 5: | Dowty P-Patient | Beavers entailment | |-------------------------|-----------------------| | (a) changeOfState | nonquantized change | | (b) incrementalTheme | totally traversed | | (c) causallyAffected | potential change | | (d) stationary | potential change | | (e) dependentExistence | (irrelevant here) |

Equations

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

Instances For

source

theorem Semantics.ArgumentStructure.Affectedness.Profile.profileToDegree_depends_only_on_patient (p q : EntailmentProfile.EntailmentProfile) (hcos : p.changeOfState = q.changeOfState) (hit : p.incrementalTheme = q.incrementalTheme) (hca : p.causallyAffected = q.causallyAffected) (hst : p.stationary = q.stationary) :

profileToDegree p = profileToDegree q

The projection depends only on {CoS, IT, CA, St}. Profiles agreeing on these four features always map to the same degree. The remaining 6 features (V, S, C, M, IE, DE) are irrelevant.

This is the forward kernel characterization: sufficient conditions for two profiles to have the same image under profileToDegree.

source

theorem Semantics.ArgumentStructure.Affectedness.Profile.quantized_implies (p : EntailmentProfile.EntailmentProfile) (h : profileToDegree p = AffectednessDegree.quantized) :

p.changeOfState = true ∧ p.incrementalTheme = true

What quantized guarantees: both CoS and IT hold.

source

theorem Semantics.ArgumentStructure.Affectedness.Profile.nonquantized_implies (p : EntailmentProfile.EntailmentProfile) (h : profileToDegree p = AffectednessDegree.nonquantized) :

p.changeOfState = true ∧ p.incrementalTheme = false

What nonquantized guarantees: CoS without IT.

source

theorem Semantics.ArgumentStructure.Affectedness.Profile.potential_implies (p : EntailmentProfile.EntailmentProfile) (h : profileToDegree p = AffectednessDegree.potential) :

p.changeOfState = false ∧ (p.causallyAffected = true ∨ p.stationary = true)

What potential guarantees: no CoS, but CA or St.

source

theorem Semantics.ArgumentStructure.Affectedness.Profile.unspecified_implies (p : EntailmentProfile.EntailmentProfile) (h : profileToDegree p = AffectednessDegree.unspecified) :

p.changeOfState = false ∧ p.causallyAffected = false ∧ p.stationary = false

What unspecified guarantees: no CoS, no CA, no St.

source

theorem Semantics.ArgumentStructure.Affectedness.Profile.build_object_quantized :

profileToDegree EntailmentProfile.buildObjectProfile = AffectednessDegree.quantized

Build object: incremental theme + CoS → quantized.

source

theorem Semantics.ArgumentStructure.Affectedness.Profile.eat_object_quantized :

profileToDegree EntailmentProfile.eatObjectProfile = AffectednessDegree.quantized

Eat object: incremental theme + CoS → quantized.

source

theorem Semantics.ArgumentStructure.Affectedness.Profile.kick_object_nonquantized :

profileToDegree EntailmentProfile.kickObjectProfile = AffectednessDegree.nonquantized

Kick object: CoS but no IT → nonquantized.

source

theorem Semantics.ArgumentStructure.Affectedness.Profile.see_unspecified :

profileToDegree EntailmentProfile.seeSubjectProfile = AffectednessDegree.unspecified

See subject has no P-Patient features → unspecified.

source

theorem Semantics.ArgumentStructure.Affectedness.Profile.die_nonquantized :

profileToDegree EntailmentProfile.dieSubjectProfile = AffectednessDegree.nonquantized

Die subject: CoS but no IT → nonquantized (the dying entity undergoes change but not incrementally).

The Bool-side profileToDegree p = .quantized and the typeclass-side IsQuantizedAffected θ say the same thing about Beavers level — modulo the missing primitive that connects a verb's Dowty profile to its substrate-level θ relation.

**Substrate gap (acknowledged):** linglib has no `HasObjectTheme V α β`
typeclass providing the canonical θ for a fragment verb. EntailmentProfile
is per-(verb, argument) Bool data; θ is the abstract semantic relation. A
structural bridge between them requires per-verb instances binding the
two — fragment-level work that is not yet built.

**Available now:** an explicit-witness smart constructor for the
`(profile, θ, scalar witnesses)` triple. The user provides BOTH the Bool
declaration (the profile projects to .quantized) AND the scalar witness
(`Quantized θ g_φ`); the smart constructor packages them into a
typeclass instance, ensuring the two declarations are jointly consistent.

Mathlib pattern: when a structural bridge requires content the substrate
doesn't carry, expose an explicit-witness smart constructor (cf. mathlib's
`MetricSpace.ofDistTopology` and similar).

source

@[reducible]

def Semantics.ArgumentStructure.Affectedness.Profile.IsQuantizedAffected.ofProfileAndWitness {α : Type u_1} {β : Type u_2} {δ : Type u_3} [HasScalarResult α δ β] [HasLatentScale α β] (θ : α → β → Prop) (p : EntailmentProfile.EntailmentProfile) (_h_profile : profileToDegree p = AffectednessDegree.quantized) (forget : ∀ (x : α) (e : β), (∃ (g : δ), HasScalarResult.resultAt x g e) → HasLatentScale.latentScale x e) (g_φ : δ) (h_quantized : Quantized θ g_φ) :

Hierarchy.IsQuantizedAffected θ

Joint consistency smart constructor: given a profile that projects to .quantized AND a scalar witness for some θ on a dimension δ, produce an IsQuantizedAffected θ instance.

The two arguments encode parallel commitments — the Bool side (p.profileToDegree = .quantized) and the scalar side (Quantized θ g_φ). The smart constructor makes joint consistency structural: a consumer cannot construct an instance with a profile that projects to .nonquantized while declaring Quantized on the scalar side.

Equations

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

Instances For

Documentation

Linglib.Theories.Semantics.ArgumentStructure.Affectedness.Profile

Affectedness Hierarchy: EntailmentProfile Projection #

As a projection of EntailmentProfile #

Grammatical consequence #

Interface to root semantics #