Entailment Profiles and the Argument Selection Principle

@cite{dowty-1991} @cite{davis-koenig-2000} @cite{grimm-2011} @cite{levin-2019} @cite{beavers-2010}

Entailment profiles encode the lexical entailments a verb imposes on each of its arguments, reflecting the modern consensus on proto-roles (@cite{levin-2019}). Proto-Agent and Proto-Patient are cluster concepts: each is a set of entailments, and an argument's "degree of agenthood/patienthood" is determined by which entailments it satisfies.

Entailment structure

The 10 entailments are not fully independent (@cite{levin-2019} §2.1):

• P-Agent pairing: three P-Agent entailments are paired with P-Patient entailments in asymmetric relations (causation↔changeOfState, movement↔stationary, independentExistence↔dependentExistence).
• P-Agent dependency: volition presupposes sentience.
• P-Agent priority: causation outranks other P-Agent entailments for subject selection (@cite{davis-koenig-2000}).
• P-Patient implicational structure: the affectedness-related entailments (changeOfState, incrementalTheme, causallyAffected) form an implicational hierarchy (@cite{beavers-2010}).

These dependencies are exploited by the modern ASP (lattice comparison, §3–4) and formalized algebraically in AgentivityLattice.lean:

• P-Agent → AgentivityNode (4 privative features on a lattice; @cite{grimm-2011})
• P-Patient → PersistenceLevel (4 persistence dimensions; @cite{grimm-2011}), and AffectednessDegree (implicational hierarchy of truth-conditional strength; @cite{beavers-2010})

Argument Selection Principle (lattice-based)

The ASP uses lattice comparison (@cite{grimm-2011}): argument A outranks argument B for subjecthood iff A's P-Agent feature set dominates (is a superset of) B's. When P-Agent features are incomparable, P-Patient features break the tie. This naturally handles priority because feature-set inclusion respects the entailment dependencies.

For unaccusativity, the priority-based approach checks whether the sole argument has core agentive features (volition/causation) rather than flat-counting.

@cite{dowty-1991}'s original flat-counting ASP is preserved in Phenomena/ArgumentStructure/Studies/Dowty1991.lean for comparison.

structure Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile : Type

The 10 entailments defining Proto-Agent and Proto-Patient (@cite{dowty-1991} pp.572–573).

Proto-Agent entailments (a)–(e):

• volition, sentience, causation, movement, independent existence

Proto-Patient entailments (a)–(e):

• change of state, incremental theme, causally affected, stationary, dependent existence

• volition : Bool

  (a) volitional involvement in the event

• sentience : Bool

  (b) sentience/perception

• causation : Bool

  (c) causing an event or change of state in another participant

• movement : Bool

  (d) movement (relative to another participant)

• independentExistence : Bool

  (e) exists independently of the event named by the verb

• changeOfState : Bool

  (a) undergoes change of state

• incrementalTheme : Bool

  (b) incremental theme (Krifka's SINC)

• causallyAffected : Bool

  (c) causally affected by another participant

• stationary : Bool

  (d) stationary relative to another participant

• dependentExistence : Bool

  (e) does not exist independently of the event

instance Semantics.Lexical.Verb.EntailmentProfile.instDecidableEqEntailmentProfile : DecidableEq EntailmentProfile

Equations

• Semantics.Lexical.Verb.EntailmentProfile.instDecidableEqEntailmentProfile = Semantics.Lexical.Verb.EntailmentProfile.instDecidableEqEntailmentProfile.decEq

def Semantics.Lexical.Verb.EntailmentProfile.instDecidableEqEntailmentProfile.decEq (x✝ x✝¹ : EntailmentProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.instReprEntailmentProfile.repr : EntailmentProfile → Nat → Std.Format

Equations

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

instance Semantics.Lexical.Verb.EntailmentProfile.instReprEntailmentProfile : Repr EntailmentProfile

Equations

• Semantics.Lexical.Verb.EntailmentProfile.instReprEntailmentProfile = { reprPrec := Semantics.Lexical.Verb.EntailmentProfile.instReprEntailmentProfile.repr }

instance Semantics.Lexical.Verb.EntailmentProfile.instBEqEntailmentProfile : BEq EntailmentProfile

Equations

• Semantics.Lexical.Verb.EntailmentProfile.instBEqEntailmentProfile = { beq := Semantics.Lexical.Verb.EntailmentProfile.instBEqEntailmentProfile.beq }

def Semantics.Lexical.Verb.EntailmentProfile.instBEqEntailmentProfile.beq : EntailmentProfile → EntailmentProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Lexical.Verb.EntailmentProfile.instBEqEntailmentProfile.beq x✝¹ x✝ = false

def Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile.pAgentScore (p : EntailmentProfile) : Nat

Count of Proto-Agent entailments. Informational — the modern ASP uses lattice comparison, not counting. Retained for bridge theorems and backward compatibility with study files.

Equations

• p.pAgentScore = p.volition.toNat + p.sentience.toNat + p.causation.toNat + p.movement.toNat + p.independentExistence.toNat

def Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile.pPatientScore (p : EntailmentProfile) : Nat

Count of Proto-Patient entailments.

Equations

• p.pPatientScore = p.changeOfState.toNat + p.incrementalTheme.toNat + p.causallyAffected.toNat + p.stationary.toNat + p.dependentExistence.toNat

def Semantics.Lexical.Verb.EntailmentProfile.pAgentDominates (p q : EntailmentProfile) : Bool

P-Agent feature dominance: p has every P-Agent feature that q has. This is the subset ordering on P-Agent feature sets.

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.pPatientDominates (p q : EntailmentProfile) : Bool

P-Patient feature dominance: p has every P-Patient feature that q has.

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.pAgentStrictlyDominates (p q : EntailmentProfile) : Bool

Strict P-Agent dominance: p dominates q but not vice versa. Means p has a strict superset of q's P-Agent features.

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.pPatientStrictlyDominates (p q : EntailmentProfile) : Bool

Strict P-Patient dominance.

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.outranksForSubject (subj obj : EntailmentProfile) : Bool

Modern ASP: subj outranks obj for subjecthood iff: (1) subj strictly dominates obj on P-Agent features (subj's P-Agent set ⊃ obj's P-Agent set), OR (2) Neither strictly dominates the other on P-Agent, AND obj strictly dominates subj on P-Patient (obj is a "better" object, hence subj wins by exclusion).

This replaces @cite{dowty-1991}'s flat counting with lattice comparison (@cite{grimm-2011}, @cite{davis-koenig-2000}). Priority of causation is captured structurally: {causation, IE} ⊃ {IE} but {causation, IE} ⊥ {sentience, IE} (incomparable).

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.allowsAlternation (arg1 arg2 : EntailmentProfile) : Bool

Corollary 1 (@cite{dowty-1991} p.579): Neither argument outranks the other → alternation is possible (buy/sell, like/please).

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.predictsUnaccusative (p : EntailmentProfile) : Bool

Predicts unaccusativity for intransitive verbs.

An intransitive subject is unaccusative iff it lacks core agentive features (volition AND causation) and has at least one P-Patient feature. This matches @cite{dowty-1991}'s Table 1 cell 4 and fixes the arrive anomaly that flat counting gets wrong.

@cite{davis-koenig-2000}: causation and volition are the priority P-Agent entailments. Their absence signals non-agentivity.

Equations

• Semantics.Lexical.Verb.EntailmentProfile.predictsUnaccusative p = (!p.volition && !p.causation && decide (p.pPatientScore > 0))

def Semantics.Lexical.Verb.EntailmentProfile.predictsUnergative (p : EntailmentProfile) : Bool

Predicts unergative for intransitive verbs.

An intransitive subject is unergative iff it has at least one core agentive feature (volition or causation) and no P-Patient features.

Equations

• Semantics.Lexical.Verb.EntailmentProfile.predictsUnergative p = ((p.volition || p.causation) && p.pPatientScore == 0)

def Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile.wellFormedInternal (p : EntailmentProfile) : Bool

Intra-profile well-formedness: volition presupposes sentience. Only sentient entities can be volitional (@cite{dowty-1991} p.607, @cite{levin-2019} §2.1).

Equations

• p.wellFormedInternal = (!p.volition || p.sentience)

def Semantics.Lexical.Verb.EntailmentProfile.wellFormedPair (subj obj : EntailmentProfile) : Bool

Inter-argument well-formedness (@cite{davis-koenig-2000}, @cite{primus-1999}): three P-Agent entailments are paired with P-Patient entailments in asymmetric relations.

• causation (subject) → changeOfState (object)
• movement (subject) → stationary (object)
• independentExistence (subject) → dependentExistence (object)

Equations

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

inductive Semantics.Lexical.Verb.EntailmentProfile.DoTestSource : Type

Source of do-test acceptability.

• semantic : DoTestSource
• pragmatic : DoTestSource

instance Semantics.Lexical.Verb.EntailmentProfile.instDecidableEqDoTestSource : DecidableEq DoTestSource

Equations

• Semantics.Lexical.Verb.EntailmentProfile.instDecidableEqDoTestSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Verb.EntailmentProfile.instReprDoTestSource.repr : DoTestSource → Nat → Std.Format

Equations

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

instance Semantics.Lexical.Verb.EntailmentProfile.instReprDoTestSource : Repr DoTestSource

Equations

• Semantics.Lexical.Verb.EntailmentProfile.instReprDoTestSource = { reprPrec := Semantics.Lexical.Verb.EntailmentProfile.instReprDoTestSource.repr }

def Semantics.Lexical.Verb.EntailmentProfile.instBEqDoTestSource.beq : DoTestSource → DoTestSource → Bool

Equations

• Semantics.Lexical.Verb.EntailmentProfile.instBEqDoTestSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Verb.EntailmentProfile.instBEqDoTestSource : BEq DoTestSource

Equations

• Semantics.Lexical.Verb.EntailmentProfile.instBEqDoTestSource = { beq := Semantics.Lexical.Verb.EntailmentProfile.instBEqDoTestSource.beq }

def Semantics.Lexical.Verb.EntailmentProfile.passesDoTestFromProfile (p : EntailmentProfile) : Bool

The do-test passes (semantically) iff at least one of {volition, causation, movement} holds.

Equations

• Semantics.Lexical.Verb.EntailmentProfile.passesDoTestFromProfile p = (p.volition || p.causation || p.movement)

theorem Semantics.Lexical.Verb.EntailmentProfile.doTest_from_profile_iff_hasAgentEntailment (p : EntailmentProfile) : passesDoTestFromProfile p = true ↔ p.volition = true ∨ p.causation = true ∨ p.movement = true

Passing the do-test is equivalent to having at least one P-Agent entailment from {volition, causation, movement}.

def Semantics.Lexical.Verb.EntailmentProfile.isEffector (p : EntailmentProfile) : Bool

An effector (@cite{van-valin-wilkins-1996}) is a self-energetic force bearer: movement + independent existence. Realized as external argument.

Equations

• Semantics.Lexical.Verb.EntailmentProfile.isEffector p = (p.movement && p.independentExistence)

def Semantics.Lexical.Verb.EntailmentProfile.isForceRecipient (p : EntailmentProfile) : Bool

A force recipient is causally affected or stationary. Realized as internal argument.

Equations

• Semantics.Lexical.Verb.EntailmentProfile.isForceRecipient p = (p.causallyAffected || p.stationary)

theorem Semantics.Lexical.Verb.EntailmentProfile.effector_has_pAgent (p : EntailmentProfile) (h : isEffector p = true) : p.pAgentScore ≥ 2

Effectors have at least 2 P-Agent entailments (movement + IE).

def Semantics.Lexical.Verb.EntailmentProfile.kickSubjectProfile : EntailmentProfile

"kick" subject: V+S+C+M+IE (prototypical agent, 5 P-Ag)

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.kickObjectProfile : EntailmentProfile

"kick" object: CoS+CA+St (3 P-Pat)

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.buildSubjectProfile : EntailmentProfile

"build" subject: V+S+C+M+IE (5 P-Ag)

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.buildObjectProfile : EntailmentProfile

"build" object: CoS+IT+CA+DE (4 P-Pat, incremental theme, dependent existence)

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.seeSubjectProfile : EntailmentProfile

"see" subject: S+IE (experiencer, 2 P-Ag)

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.runSubjectProfile : EntailmentProfile

"run" subject: V+S+M+IE (4 P-Ag, unergative)

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.arriveSubjectProfile : EntailmentProfile

"arrive" subject: M+IE+CoS (2 P-Ag, 1 P-Pat — unaccusative)

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.dieSubjectProfile : EntailmentProfile

"die" subject: CoS+CA+DE (0 P-Ag, 3 P-Pat — unaccusative)

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.eatSubjectProfile : EntailmentProfile

"eat" subject: V+S+C+M+IE (5 P-Ag)

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.eatObjectProfile : EntailmentProfile

"eat" object: CoS+IT+CA (3 P-Pat, incremental theme)

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.buySubjectProfile : EntailmentProfile

"buy" subject: V+S+C+IE (4 P-Ag)

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.sellSubjectProfile : EntailmentProfile

"sell" subject: V+S+C+IE (same as buy — 4 P-Ag)

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.sweepBasicSubjectProfile : EntailmentProfile

"sweep" basic-sense subject: M+IE (movement + independent existence). Underspecified for volition — agentivity is pragmatically resolved.

Equations

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

def Semantics.Lexical.Verb.EntailmentProfile.sweepBroomSubjectProfile : EntailmentProfile

"sweep" broom-sense subject: V+S+C+M+IE (obligatory agent, 5 P-Ag). Instrument lexicalization forces volition, sentience, causation.

Equations

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

theorem Semantics.Lexical.Verb.EntailmentProfile.pAgentDominates_refl (p : EntailmentProfile) : pAgentDominates p p = true

theorem Semantics.Lexical.Verb.EntailmentProfile.pPatientDominates_refl (p : EntailmentProfile) : pPatientDominates p p = true