Documentation

Linglib.Theories.Semantics.Lexical.Verb.Affectedness

Affectedness Hierarchy #

@cite{beavers-2010} @cite{dowty-1991}

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.

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.

inductive Semantics.Lexical.Verb.Affectedness.AffectednessDegree :

Four degrees of affectedness, defined by increasingly weaker truth conditions about what change — if any — occurs in the event.

Each degree is an existential generalization over the result' relation:

quantized: φ → [result'(x, s, g_φ, e)] (specific result state)
nonquantized: φ → ∃g[result'(x, s, g, e)] (some change occurred)
potential: φ → ◇∃g[result'(x, s, g, e)] (change is possible)
unspecified: φ → ∃θ[θ(x, e)] (x merely participates)

The hierarchy forms a total order by truth-conditional entailment: quantized ≥ nonquantized ≥ potential ≥ unspecified.

quantized : AffectednessDegree
nonquantized : AffectednessDegree
potential : AffectednessDegree
unspecified : AffectednessDegree

Instances For

instance Semantics.Lexical.Verb.Affectedness.instDecidableEqAffectednessDegree :

DecidableEq AffectednessDegree

Equations

Semantics.Lexical.Verb.Affectedness.instDecidableEqAffectednessDegree x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Verb.Affectedness.instBEqAffectednessDegree.beq :

AffectednessDegree → AffectednessDegree → Bool

Equations

Semantics.Lexical.Verb.Affectedness.instBEqAffectednessDegree.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Semantics.Lexical.Verb.Affectedness.instBEqAffectednessDegree :

BEq AffectednessDegree

Equations

Semantics.Lexical.Verb.Affectedness.instBEqAffectednessDegree = { beq := Semantics.Lexical.Verb.Affectedness.instBEqAffectednessDegree.beq }

instance Semantics.Lexical.Verb.Affectedness.instReprAffectednessDegree :

Repr AffectednessDegree

Equations

Semantics.Lexical.Verb.Affectedness.instReprAffectednessDegree = { reprPrec := Semantics.Lexical.Verb.Affectedness.instReprAffectednessDegree.repr }

def Semantics.Lexical.Verb.Affectedness.instReprAffectednessDegree.repr :

AffectednessDegree → Nat → Std.Format

Equations

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

Instances For

def Semantics.Lexical.Verb.Affectedness.AffectednessDegree.strength :

AffectednessDegree → Nat

Numeric strength: higher = stronger truth conditions.

Equations

Instances For

def Semantics.Lexical.Verb.Affectedness.AffectednessDegree.ge (a b : AffectednessDegree) :

The hierarchy ordering: stronger degrees entail weaker ones.

Equations

a.ge b = decide (a.strength ≥ b.strength)

Instances For

instance Semantics.Lexical.Verb.Affectedness.AffectednessDegree.instLE :

LE AffectednessDegree

Equations

Semantics.Lexical.Verb.Affectedness.AffectednessDegree.instLE = { le := fun (a b : Semantics.Lexical.Verb.Affectedness.AffectednessDegree) => b.strength ≥ a.strength }

instance Semantics.Lexical.Verb.Affectedness.AffectednessDegree.instDecidableLe (a b : AffectednessDegree) :

Decidable (a ≤ b)

Equations

a.instDecidableLe b = inferInstanceAs (Decidable (b.strength ≥ a.strength))

theorem Semantics.Lexical.Verb.Affectedness.AffectednessDegree.quantized_entails_nonquantized :

quantized.ge nonquantized = true

Each degree entails all weaker degrees (implicational hierarchy).

theorem Semantics.Lexical.Verb.Affectedness.AffectednessDegree.nonquantized_entails_potential :

nonquantized.ge potential = true

theorem Semantics.Lexical.Verb.Affectedness.AffectednessDegree.potential_entails_unspecified :

potential.ge unspecified = true

theorem Semantics.Lexical.Verb.Affectedness.AffectednessDegree.quantized_entails_potential :

quantized.ge potential = true

Transitivity: quantized entails potential.

theorem Semantics.Lexical.Verb.Affectedness.AffectednessDegree.quantized_entails_unspecified :

quantized.ge unspecified = true

Transitivity: quantized entails unspecified.

theorem Semantics.Lexical.Verb.Affectedness.AffectednessDegree.ge_refl (a : AffectednessDegree) :

Reflexivity.

def Semantics.Lexical.Verb.Affectedness.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

theorem Semantics.Lexical.Verb.Affectedness.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.

theorem Semantics.Lexical.Verb.Affectedness.quantized_implies (p : EntailmentProfile.EntailmentProfile) (h : profileToDegree p = AffectednessDegree.quantized) :

p.changeOfState = true ∧ p.incrementalTheme = true

What quantized guarantees: both CoS and IT hold.

theorem Semantics.Lexical.Verb.Affectedness.nonquantized_implies (p : EntailmentProfile.EntailmentProfile) (h : profileToDegree p = AffectednessDegree.nonquantized) :

p.changeOfState = true ∧ p.incrementalTheme = false

What nonquantized guarantees: CoS without IT.

theorem Semantics.Lexical.Verb.Affectedness.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.

theorem Semantics.Lexical.Verb.Affectedness.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.

theorem Semantics.Lexical.Verb.Affectedness.build_object_quantized :

profileToDegree EntailmentProfile.buildObjectProfile = AffectednessDegree.quantized

Build object: incremental theme + CoS → quantized.

theorem Semantics.Lexical.Verb.Affectedness.eat_object_quantized :

profileToDegree EntailmentProfile.eatObjectProfile = AffectednessDegree.quantized

Eat object: incremental theme + CoS → quantized.

theorem Semantics.Lexical.Verb.Affectedness.kick_object_nonquantized :

profileToDegree EntailmentProfile.kickObjectProfile = AffectednessDegree.nonquantized

Kick object: CoS but no IT → nonquantized.

theorem Semantics.Lexical.Verb.Affectedness.see_unspecified :

profileToDegree EntailmentProfile.seeSubjectProfile = AffectednessDegree.unspecified

See subject has no P-Patient features → unspecified.

theorem Semantics.Lexical.Verb.Affectedness.die_nonquantized :

profileToDegree EntailmentProfile.dieSubjectProfile = AffectednessDegree.nonquantized

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