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.ArgumentStructure.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

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

Equations

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

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidableEqEntailmentProfile : DecidableEq EntailmentProfile

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instDecidableEqEntailmentProfile = Semantics.ArgumentStructure.EntailmentProfile.instDecidableEqEntailmentProfile.decEq

def Semantics.ArgumentStructure.EntailmentProfile.instReprEntailmentProfile.repr : EntailmentProfile → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instReprEntailmentProfile : Repr EntailmentProfile

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instReprEntailmentProfile = { reprPrec := Semantics.ArgumentStructure.EntailmentProfile.instReprEntailmentProfile.repr }

def Semantics.ArgumentStructure.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.ArgumentStructure.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.ArgumentStructure.EntailmentProfile.PAgentDominates (p q : EntailmentProfile) : Prop

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.

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidablePAgentDominates (p q : EntailmentProfile) : Decidable (PAgentDominates p q)

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instDecidablePAgentDominates p q = id inferInstance

def Semantics.ArgumentStructure.EntailmentProfile.PPatientDominates (p q : EntailmentProfile) : Prop

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.

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidablePPatientDominates (p q : EntailmentProfile) : Decidable (PPatientDominates p q)

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instDecidablePPatientDominates p q = id inferInstance

def Semantics.ArgumentStructure.EntailmentProfile.PAgentStrictlyDominates (p q : EntailmentProfile) : Prop

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.

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidablePAgentStrictlyDominates (p q : EntailmentProfile) : Decidable (PAgentStrictlyDominates p q)

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instDecidablePAgentStrictlyDominates p q = id inferInstance

def Semantics.ArgumentStructure.EntailmentProfile.PPatientStrictlyDominates (p q : EntailmentProfile) : Prop

Strict P-Patient dominance.

Equations

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

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidablePPatientStrictlyDominates (p q : EntailmentProfile) : Decidable (PPatientStrictlyDominates p q)

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instDecidablePPatientStrictlyDominates p q = id inferInstance

def Semantics.ArgumentStructure.EntailmentProfile.OutranksForSubject (subj obj : EntailmentProfile) : Prop

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.

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidableOutranksForSubject (subj obj : EntailmentProfile) : Decidable (OutranksForSubject subj obj)

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instDecidableOutranksForSubject subj obj = id inferInstance

def Semantics.ArgumentStructure.EntailmentProfile.AllowsAlternation (arg1 arg2 : EntailmentProfile) : Prop

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.

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidableAllowsAlternation (arg1 arg2 : EntailmentProfile) : Decidable (AllowsAlternation arg1 arg2)

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instDecidableAllowsAlternation arg1 arg2 = id inferInstance

def Semantics.ArgumentStructure.EntailmentProfile.PredictsUnaccusative (p : EntailmentProfile) : Prop

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.ArgumentStructure.EntailmentProfile.PredictsUnaccusative p = (p.volition = false ∧ p.causation = false ∧ p.pPatientScore > 0)

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidablePredictsUnaccusative (p : EntailmentProfile) : Decidable (PredictsUnaccusative p)

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instDecidablePredictsUnaccusative p = id inferInstance

def Semantics.ArgumentStructure.EntailmentProfile.PredictsUnergative (p : EntailmentProfile) : Prop

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.ArgumentStructure.EntailmentProfile.PredictsUnergative p = ((p.volition = true ∨ p.causation = true) ∧ p.pPatientScore = 0)

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidablePredictsUnergative (p : EntailmentProfile) : Decidable (PredictsUnergative p)

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instDecidablePredictsUnergative p = id inferInstance

def Semantics.ArgumentStructure.EntailmentProfile.EntailmentProfile.WellFormedInternal (p : EntailmentProfile) : Prop

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 = true → p.sentience = true)

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidableWellFormedInternal (p : EntailmentProfile) : Decidable p.WellFormedInternal

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instDecidableWellFormedInternal p = id inferInstance

def Semantics.ArgumentStructure.EntailmentProfile.WellFormedPair (subj obj : EntailmentProfile) : Prop

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.

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidableWellFormedPair (subj obj : EntailmentProfile) : Decidable (WellFormedPair subj obj)

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instDecidableWellFormedPair subj obj = id inferInstance

inductive Semantics.ArgumentStructure.EntailmentProfile.DoTestSource : Type

Source of do-test acceptability.

• semantic : DoTestSource
• pragmatic : DoTestSource

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidableEqDoTestSource : DecidableEq DoTestSource

Equations

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

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

Equations

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

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instReprDoTestSource : Repr DoTestSource

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instReprDoTestSource = { reprPrec := Semantics.ArgumentStructure.EntailmentProfile.instReprDoTestSource.repr }

def Semantics.ArgumentStructure.EntailmentProfile.PassesDoTestFromProfile (p : EntailmentProfile) : Prop

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

Equations

• Semantics.ArgumentStructure.EntailmentProfile.PassesDoTestFromProfile p = (p.volition = true ∨ p.causation = true ∨ p.movement = true)

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidablePassesDoTestFromProfile (p : EntailmentProfile) : Decidable (PassesDoTestFromProfile p)

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instDecidablePassesDoTestFromProfile p = id inferInstance

def Semantics.ArgumentStructure.EntailmentProfile.IsEffector (p : EntailmentProfile) : Prop

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

Equations

• Semantics.ArgumentStructure.EntailmentProfile.IsEffector p = (p.movement = true ∧ p.independentExistence = true)

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidableIsEffector (p : EntailmentProfile) : Decidable (IsEffector p)

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instDecidableIsEffector p = id inferInstance

def Semantics.ArgumentStructure.EntailmentProfile.IsForceRecipient (p : EntailmentProfile) : Prop

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

Equations

• Semantics.ArgumentStructure.EntailmentProfile.IsForceRecipient p = (p.causallyAffected = true ∨ p.stationary = true)

@[implicit_reducible]

instance Semantics.ArgumentStructure.EntailmentProfile.instDecidableIsForceRecipient (p : EntailmentProfile) : Decidable (IsForceRecipient p)

Equations

• Semantics.ArgumentStructure.EntailmentProfile.instDecidableIsForceRecipient p = id inferInstance

theorem Semantics.ArgumentStructure.EntailmentProfile.effector_has_pAgent (p : EntailmentProfile) (h : IsEffector p) : p.pAgentScore ≥ 2

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

def Semantics.ArgumentStructure.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.ArgumentStructure.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.ArgumentStructure.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.ArgumentStructure.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.ArgumentStructure.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.ArgumentStructure.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.ArgumentStructure.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.ArgumentStructure.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.ArgumentStructure.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.ArgumentStructure.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.ArgumentStructure.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.ArgumentStructure.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.ArgumentStructure.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.ArgumentStructure.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.ArgumentStructure.EntailmentProfile.pAgentDominates_refl (p : EntailmentProfile) : PAgentDominates p p

theorem Semantics.ArgumentStructure.EntailmentProfile.pPatientDominates_refl (p : EntailmentProfile) : PPatientDominates p p