Entailment Profiles and the Argument Selection Principle

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

Entailment profiles encode the lexical entailments a verb imposes on each of its arguments. Proto-Agent and Proto-Patient are cluster concepts: each is defined by a set of independent entailments, and an argument's "degree of agenthood/patienthood" is determined by which entailments it satisfies.

Modern ASP (lattice-based)

@cite{dowty-1991}'s original Argument Selection Principle used flat counting (more P-Agent entailments → subject). Subsequent work (@cite{davis-koenig-2000}, @cite{grimm-2011}, @cite{levin-2019}) identified two problems:

1. Entailment non-independence: causation↔changeOfState, movement↔stationary, and independentExistence↔dependentExistence are paired across arguments; volition presupposes sentience within an argument.
2. Priority: causation outranks other P-Agent entailments for subject selection.

The modern 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.

structure Semantics.Events.ProtoRoles.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.Events.ProtoRoles.instDecidableEqEntailmentProfile : DecidableEq EntailmentProfile

Equations

• Semantics.Events.ProtoRoles.instDecidableEqEntailmentProfile = Semantics.Events.ProtoRoles.instDecidableEqEntailmentProfile.decEq

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

Equations

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

def Semantics.Events.ProtoRoles.instReprEntailmentProfile.repr : EntailmentProfile → Nat → Std.Format

Equations

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

instance Semantics.Events.ProtoRoles.instReprEntailmentProfile : Repr EntailmentProfile

Equations

• Semantics.Events.ProtoRoles.instReprEntailmentProfile = { reprPrec := Semantics.Events.ProtoRoles.instReprEntailmentProfile.repr }

def Semantics.Events.ProtoRoles.instBEqEntailmentProfile.beq : EntailmentProfile → EntailmentProfile → Bool

Equations

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

instance Semantics.Events.ProtoRoles.instBEqEntailmentProfile : BEq EntailmentProfile

Equations

• Semantics.Events.ProtoRoles.instBEqEntailmentProfile = { beq := Semantics.Events.ProtoRoles.instBEqEntailmentProfile.beq }

def Semantics.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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

• Semantics.Events.ProtoRoles.pAgentStrictlyDominates p q = (Semantics.Events.ProtoRoles.pAgentDominates p q && !Semantics.Events.ProtoRoles.pAgentDominates q p)

def Semantics.Events.ProtoRoles.pPatientStrictlyDominates (p q : EntailmentProfile) : Bool

Strict P-Patient dominance.

Equations

• Semantics.Events.ProtoRoles.pPatientStrictlyDominates p q = (Semantics.Events.ProtoRoles.pPatientDominates p q && !Semantics.Events.ProtoRoles.pPatientDominates q p)

def Semantics.Events.ProtoRoles.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.Events.ProtoRoles.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

• Semantics.Events.ProtoRoles.allowsAlternation arg1 arg2 = (!Semantics.Events.ProtoRoles.outranksForSubject arg1 arg2 && !Semantics.Events.ProtoRoles.outranksForSubject arg2 arg1)

def Semantics.Events.ProtoRoles.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.Events.ProtoRoles.predictsUnaccusative p = (!p.volition && !p.causation && decide (p.pPatientScore > 0))

def Semantics.Events.ProtoRoles.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.Events.ProtoRoles.predictsUnergative p = ((p.volition || p.causation) && p.pPatientScore == 0)

def Semantics.Events.ProtoRoles.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.Events.ProtoRoles.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

• Semantics.Events.ProtoRoles.wellFormedPair subj obj = ((!subj.causation || obj.changeOfState) && (!subj.movement || obj.stationary) && (!subj.independentExistence || obj.dependentExistence))

inductive Semantics.Events.ProtoRoles.DoTestSource : Type

Source of do-test acceptability.

• semantic : DoTestSource
• pragmatic : DoTestSource

instance Semantics.Events.ProtoRoles.instDecidableEqDoTestSource : DecidableEq DoTestSource

Equations

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

def Semantics.Events.ProtoRoles.instReprDoTestSource.repr : DoTestSource → Nat → Std.Format

Equations

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

instance Semantics.Events.ProtoRoles.instReprDoTestSource : Repr DoTestSource

Equations

• Semantics.Events.ProtoRoles.instReprDoTestSource = { reprPrec := Semantics.Events.ProtoRoles.instReprDoTestSource.repr }

instance Semantics.Events.ProtoRoles.instBEqDoTestSource : BEq DoTestSource

Equations

• Semantics.Events.ProtoRoles.instBEqDoTestSource = { beq := Semantics.Events.ProtoRoles.instBEqDoTestSource.beq }

def Semantics.Events.ProtoRoles.instBEqDoTestSource.beq : DoTestSource → DoTestSource → Bool

Equations

• Semantics.Events.ProtoRoles.instBEqDoTestSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Events.ProtoRoles.passesDoTestFromProfile (p : EntailmentProfile) : Bool

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

Equations

• Semantics.Events.ProtoRoles.passesDoTestFromProfile p = (p.volition || p.causation || p.movement)

theorem Semantics.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.isEffector p = (p.movement && p.independentExistence)

def Semantics.Events.ProtoRoles.isForceRecipient (p : EntailmentProfile) : Bool

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

Equations

• Semantics.Events.ProtoRoles.isForceRecipient p = (p.causallyAffected || p.stationary)

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

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

def Semantics.Events.ProtoRoles.ThetaRole.canonicalProfile : ThetaRole → EntailmentProfile

Map each ThetaRole to its canonical entailment profile.

Traditional role labels are cluster concepts: each name picks out a typical combination of entailments. This mapping derives the labels from the underlying entailment space.

Equations

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

def Semantics.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.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.Events.ProtoRoles.agent_outranks_patient : outranksForSubject (ThetaRole.canonicalProfile ThetaRole.agent) (ThetaRole.canonicalProfile ThetaRole.patient) = true

Agent outranks patient for subjecthood (lattice: {V,S,C,M,IE} ⊃ {}).

theorem Semantics.Events.ProtoRoles.agent_outranks_instrument : outranksForSubject (ThetaRole.canonicalProfile ThetaRole.agent) (ThetaRole.canonicalProfile ThetaRole.instrument) = true

Agent outranks instrument (lattice: {V,S,C,M,IE} ⊃ {C,IE}).

theorem Semantics.Events.ProtoRoles.agent_outranks_experiencer : outranksForSubject (ThetaRole.canonicalProfile ThetaRole.agent) (ThetaRole.canonicalProfile ThetaRole.experiencer) = true

Agent outranks experiencer (lattice: {V,S,C,M,IE} ⊃ {S,IE}).

theorem Semantics.Events.ProtoRoles.experiencer_instrument_alternation : allowsAlternation (ThetaRole.canonicalProfile ThetaRole.experiencer) (ThetaRole.canonicalProfile ThetaRole.instrument) = true

Experiencer and instrument have incomparable P-Agent sets ({S,IE} ⊥ {C,IE}), but also equal P-Patient (both 0) → alternation predicted.

theorem Semantics.Events.ProtoRoles.experiencer_stimulus_alternation : allowsAlternation (ThetaRole.canonicalProfile ThetaRole.experiencer) (ThetaRole.canonicalProfile ThetaRole.stimulus) = true

Experiencer and stimulus have equal profiles → alternation (like/please).

theorem Semantics.Events.ProtoRoles.agent_pAgent_score : (ThetaRole.canonicalProfile ThetaRole.agent).pAgentScore = 5

theorem Semantics.Events.ProtoRoles.patient_pAgent_score : (ThetaRole.canonicalProfile ThetaRole.patient).pAgentScore = 0

theorem Semantics.Events.ProtoRoles.agent_pPatient_score : (ThetaRole.canonicalProfile ThetaRole.agent).pPatientScore = 0

theorem Semantics.Events.ProtoRoles.patient_pPatient_score : (ThetaRole.canonicalProfile ThetaRole.patient).pPatientScore = 3

theorem Semantics.Events.ProtoRoles.canonical_agent_wellformed : (ThetaRole.canonicalProfile ThetaRole.agent).wellFormedInternal = true

theorem Semantics.Events.ProtoRoles.canonical_experiencer_wellformed : (ThetaRole.canonicalProfile ThetaRole.experiencer).wellFormedInternal = true

theorem Semantics.Events.ProtoRoles.canonical_patient_wellformed : (ThetaRole.canonicalProfile ThetaRole.patient).wellFormedInternal = true

theorem Semantics.Events.ProtoRoles.pAgentDominates_refl (p : EntailmentProfile) : pAgentDominates p p = true

theorem Semantics.Events.ProtoRoles.pPatientDominates_refl (p : EntailmentProfile) : pPatientDominates p p = true