Proto-role entailment profiles

[Dow91] [Gri11] [davis-koenig-2000] [Lev19]

An EntailmentProfile records which of [Dow91]'s ten proto-role entailments (pp.572–573) a verb imposes on one of its arguments. Proto-Agent and Proto-Patient are cluster concepts: each is a set of entailments, and an argument's degree of agenthood or patienthood is the set it satisfies. The Argument Selection Principle is stated lattice-theoretically ([Gri11]): subjecthood tracks strict superset dominance on Proto-Agent feature sets, with Proto-Patient dominance breaking ties.

Main declarations

• EntailmentProfile — the ten Boolean entailment fields
• EntailmentProfile.pAgentScore, EntailmentProfile.pPatientScore — flat feature counts
• PAgentDominates, PPatientDominates — subset ordering on feature sets
• OutranksForSubject — the lattice-based Argument Selection Principle
• PredictsUnaccusative, PredictsUnergative — split-intransitivity predictions
• activitySubjectProfile … accomplishmentObjectProfile — the [RHL98] template-level profile defaults (per-verb content lives in the class map, Semantics/Lexical/LevinClassProfiles.lean)
• AgentivityLattice.AgentivityNode.fromEntailmentProfile, AgentivityLattice.PersistenceLevel.fromPatientProfile — bridges from profiles to [Gri11]'s agentivity lattice, with the consistency theorems relating the two dominance orders

Implementation notes

The ten entailments are not independent ([Lev19] §2.1): volition presupposes sentience (EntailmentProfile.WellFormedInternal); causation, movement, and independent existence pair asymmetrically with Proto-Patient entailments (WellFormedPair); and the affectedness-related Proto-Patient entailments form an implicational hierarchy ([Bea10]). Their algebraic counterparts live in Agentivity/Defs.lean, whose lattice carriers this file imports and bridges to. [Dow91]'s original flat-counting selection principle is preserved for comparison in Studies/Dowty1991.lean; the counting accessors here are informational only. Causation priority ([davis-koenig-2000]) needs no extra clause: it falls out of feature-set inclusion.

structure ArgumentStructure.EntailmentProfile : Type

The ten entailments defining the proto-roles ([Dow91] pp.572–573): the first five are Proto-Agent, the last five Proto-Patient. Fields default to false, so a profile lists only the entailments it imposes.

• volition : Bool

  Volitional involvement in the event.

• sentience : Bool

  Sentience or perception.

• causation : Bool

  Causes an event or change of state in another participant.

• movement : Bool

  Movement relative to another participant.

• independentExistence : Bool

  Exists independently of the event named by the verb.

• changeOfState : Bool

  Undergoes a change of state.

• incrementalTheme : Bool

  Incremental theme: the argument measures out the event.

• causallyAffected : Bool

  Causally affected by another participant.

• stationary : Bool

  Stationary relative to another participant.

• dependentExistence : Bool

  Does not exist independently of the event.

@[implicit_reducible]

instance ArgumentStructure.instDecidableEqEntailmentProfile : DecidableEq EntailmentProfile

Equations

• ArgumentStructure.instDecidableEqEntailmentProfile = ArgumentStructure.instDecidableEqEntailmentProfile.decEq

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

Equations

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

@[implicit_reducible]

instance ArgumentStructure.instReprEntailmentProfile : Repr EntailmentProfile

Equations

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

def ArgumentStructure.instReprEntailmentProfile.repr : EntailmentProfile → ℕ → Std.Format

Equations

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

Feature counting

def ArgumentStructure.EntailmentProfile.pAgentScore (p : EntailmentProfile) : ℕ

Number of Proto-Agent entailments. Informational: the Argument Selection Principle uses lattice comparison ([Gri11]), not counting.

Equations

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

def ArgumentStructure.EntailmentProfile.pPatientScore (p : EntailmentProfile) : ℕ

Number of Proto-Patient entailments.

Equations

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

Lattice comparison

def ArgumentStructure.EntailmentProfile.PAgentDominates (p q : EntailmentProfile) : Prop

p has every Proto-Agent feature that q has: the subset ordering on Proto-Agent feature sets.

Equations

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

@[implicit_reducible]

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

Equations

• p.instDecidablePAgentDominates q = id inferInstance

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

p has every Proto-Patient feature that q has.

Equations

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

@[implicit_reducible]

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

Equations

• p.instDecidablePPatientDominates q = id inferInstance

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

p's Proto-Agent feature set is a strict superset of q's.

Equations

• p.PAgentStrictlyDominates q = (p.PAgentDominates q ∧ ¬q.PAgentDominates p)

@[implicit_reducible]

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

Equations

• p.instDecidablePAgentStrictlyDominates q = id inferInstance

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

p's Proto-Patient feature set is a strict superset of q's.

Equations

• p.PPatientStrictlyDominates q = (p.PPatientDominates q ∧ ¬q.PPatientDominates p)

@[implicit_reducible]

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

Equations

• p.instDecidablePPatientStrictlyDominates q = id inferInstance

theorem ArgumentStructure.EntailmentProfile.pAgentDominates_refl (p : EntailmentProfile) : p.PAgentDominates p

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

Argument selection

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

The lattice-based Argument Selection Principle ([Gri11], [davis-koenig-2000]): subj outranks obj for subjecthood iff subj strictly Proto-Agent-dominates obj, or the two are Proto-Agent-incomparable and obj strictly Proto-Patient-dominates subj. Causation priority is structural: {causation, IE} strictly dominates {IE} yet is incomparable with {sentience, IE}.

Equations

• subj.OutranksForSubject obj = (subj.PAgentStrictlyDominates obj ∨ ¬subj.PAgentStrictlyDominates obj ∧ ¬obj.PAgentStrictlyDominates subj ∧ obj.PPatientStrictlyDominates subj)

@[implicit_reducible]

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

Equations

• subj.instDecidableOutranksForSubject obj = id inferInstance

def ArgumentStructure.EntailmentProfile.AllowsAlternation (p q : EntailmentProfile) : Prop

[Dow91]'s Corollary 1 (p.579): neither argument outranks the other, so subject choice may alternate (buy/sell, like/please).

Equations

• p.AllowsAlternation q = (¬p.OutranksForSubject q ∧ ¬q.OutranksForSubject p)

@[implicit_reducible]

instance ArgumentStructure.EntailmentProfile.instDecidableAllowsAlternation (p q : EntailmentProfile) : Decidable (p.AllowsAlternation q)

Equations

• p.instDecidableAllowsAlternation q = id inferInstance

Split intransitivity

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

The sole argument lacks the priority Proto-Agent entailments — volition and causation ([davis-koenig-2000]) — and bears at least one Proto-Patient entailment ([Dow91] Table 1). Unlike flat counting, this classifies arrive as unaccusative.

Equations

• p.PredictsUnaccusative = (p.volition = false ∧ p.causation = false ∧ p.pPatientScore > 0)

@[implicit_reducible]

instance ArgumentStructure.EntailmentProfile.instDecidablePredPredictsUnaccusative : DecidablePred PredictsUnaccusative

Equations

• p.instDecidablePredPredictsUnaccusative = id inferInstance

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

The sole argument bears a priority Proto-Agent entailment (volition or causation) and no Proto-Patient entailment.

Equations

• p.PredictsUnergative = ((p.volition = true ∨ p.causation = true) ∧ p.pPatientScore = 0)

@[implicit_reducible]

instance ArgumentStructure.EntailmentProfile.instDecidablePredPredictsUnergative : DecidablePred PredictsUnergative

Equations

• p.instDecidablePredPredictsUnergative = id inferInstance

Well-formedness

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

Volition presupposes sentience: only sentient entities can act volitionally ([Dow91] p.607, [Lev19] §2.1).

Equations

• p.WellFormedInternal = (p.volition = true → p.sentience = true)

@[implicit_reducible]

instance ArgumentStructure.EntailmentProfile.instDecidablePredWellFormedInternal : DecidablePred WellFormedInternal

Equations

• p.instDecidablePredWellFormedInternal = id inferInstance

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

Three Proto-Agent entailments pair asymmetrically across a subject–object pair ([davis-koenig-2000], [primus-1999]): causation → changeOfState, movement → stationary, independentExistence → dependentExistence.

Equations

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

@[implicit_reducible]

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

Equations

• subj.instDecidableWellFormedPair obj = id inferInstance

The do-test

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

The do-test ([Cru73] via [Dow91]) passes on semantic grounds iff the profile entails volition, causation, or movement.

Equations

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

@[implicit_reducible]

instance ArgumentStructure.EntailmentProfile.instDecidablePredPassesDoTestFromProfile : DecidablePred PassesDoTestFromProfile

Equations

• p.instDecidablePredPassesDoTestFromProfile = id inferInstance

Effectors and force recipients

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

A self-energetic force bearer ([VVW96]): movement plus independent existence, realized as external argument.

Equations

• p.IsEffector = (p.movement = true ∧ p.independentExistence = true)

@[implicit_reducible]

instance ArgumentStructure.EntailmentProfile.instDecidablePredIsEffector : DecidablePred IsEffector

Equations

• p.instDecidablePredIsEffector = id inferInstance

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

Causally affected or stationary, realized as internal argument.

Equations

• p.IsForceRecipient = (p.causallyAffected = true ∨ p.stationary = true)

@[implicit_reducible]

instance ArgumentStructure.EntailmentProfile.instDecidablePredIsForceRecipient : DecidablePred IsForceRecipient

Equations

• p.instDecidablePredIsForceRecipient = id inferInstance

theorem ArgumentStructure.EntailmentProfile.two_le_pAgentScore_of_isEffector (p : EntailmentProfile) (h : p.IsEffector) : 2 ≤ p.pAgentScore

An effector carries at least two Proto-Agent entailments.

Template-level proto-role defaults

Per-template subject/object defaults ([RHL98] with [Dow91]'s entailments), consumed by Template.subjectProfile and Template.objectProfile in EventStructure.lean and by Fragment-level verb entries. Per-verb entailment content is NOT stored here: it lives in the Levin-class → template map (Semantics/Lexical/LevinClassProfiles.lean), and Dowty's own per-verb attributions are typed data rows in Data/ProtoRoles/Dowty1991.json consumed by Studies/Dowty1991.lean.

def ArgumentStructure.EntailmentProfile.activitySubjectProfile : EntailmentProfile

Activity template subject: V+S+M+IE. Transitive activities like hit add causation at the class level via root-contributed objects.

Equations

• ArgumentStructure.EntailmentProfile.activitySubjectProfile = { volition := true, sentience := true, movement := true, independentExistence := true }

def ArgumentStructure.EntailmentProfile.achievementSubjectProfile : EntailmentProfile

Achievement template subject: undergoes change (M+IE+CoS). Caveat: the movement entailment fits directed-motion achievements (arrive) but overgeneralizes to non-motion achievements (recognize, notice), whose subjects are sentient rather than moving — those pattern with the psych-state templates in LevinClassProfiles.lean.

Equations

• ArgumentStructure.EntailmentProfile.achievementSubjectProfile = { movement := true, independentExistence := true, changeOfState := true }

def ArgumentStructure.EntailmentProfile.accomplishmentSubjectProfile : EntailmentProfile

Accomplishment template subject: full proto-agent (V+S+C+M+IE). Dowty-confirmed at the class level: the primary transitive verbs of [Dow91] (35) (build, write, murder, eat, wash) have subjects with "volition, sentience, causation, and movement" and no Proto-Patient entailments (p. 577); independent existence is the parenthesized (27e).

Equations

• ArgumentStructure.EntailmentProfile.accomplishmentSubjectProfile = { volition := true, sentience := true, causation := true, movement := true, independentExistence := true }

def ArgumentStructure.EntailmentProfile.accomplishmentObjectProfile : EntailmentProfile

Accomplishment template object: result patient (CoS+CA). Dowty-confirmed at the class level: the (35) objects have "change, causally affected" (p. 577); the remaining Proto-Patient entailments are hedged there as "(mostly) incremental theme, stationary, dependent existence", so incremental themes (eat, build) add IT per class or per verb — not all accomplishment objects measure the event.

Equations

• ArgumentStructure.EntailmentProfile.accomplishmentObjectProfile = { changeOfState := true, causallyAffected := true }

Bridge to the Grimm agentivity lattice

The Dowty→Grimm feature translation ([Gri11] §2.1, Tables 1–2) and the consistency theorems relating [Dow91]'s dominance orders to the lattice order of Agentivity/Defs.lean. The bridge lives here, with the profiles it translates, so the lattice substrate stays Mathlib-only.

def ArgumentStructure.AgentivityLattice.AgentivityNode.fromEntailmentProfile (p : EntailmentProfile) : AgentivityNode

Map Dowty's P-Agent entailments to Grimm's agentivity features.

The correspondence is direct for 3 of 4 features:

• volition = volition
• sentience = sentience
• causation → instigation (p.521)
• movement = motion

Independent existence is handled by the persistence dimension.

Equations

• ArgumentStructure.AgentivityLattice.AgentivityNode.fromEntailmentProfile p = { volition := p.volition, sentience := p.sentience, instigation := p.causation, motion := p.movement }

def ArgumentStructure.AgentivityLattice.PersistenceLevel.fromPatientProfile (p : EntailmentProfile) : PersistenceLevel

Map Dowty's P-Patient entailments to Grimm's persistence level.

This is an approximate mapping — Grimm's system is genuinely different from Dowty's. The diagnostic features:

• DE + IT → exPersEnd: entity created incrementally (build, invent)
• DE + ¬IT → exPersBeginning: entity ceases to exist (die, evaporate)
• IT + ¬DE → exPersBeginning: entity consumed incrementally (eat)
• CoS + ¬IT + ¬DE → quPersBeginning: changed but persists (move, dim)
• ¬CoS + ¬DE → totalPersistence or totalNonPersistence

Dowty's DE ("does not exist independently of the event") maps to Grimm's creation/destruction axis. IT (incremental theme) disambiguates: DE+IT = creation (exPersEnd), DE+¬IT = destruction (exPersBeginning).

Equations

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

def ArgumentStructure.AgentivityLattice.GrimmNode.fromSubjectProfile (p : EntailmentProfile) : GrimmNode

Map a full EntailmentProfile to a GrimmNode.

The agentivity features come from the P-Agent entailments; the persistence level comes from the P-Patient entailments.

Equations

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

def ArgumentStructure.AgentivityLattice.GrimmNode.fromObjectProfile (p : EntailmentProfile) : GrimmNode

Equations

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

Grimm ↔ Dowty ASP consistency

theorem ArgumentStructure.AgentivityLattice.grimm_agentivity_consistent_with_dowty (p q : EntailmentProfile) (h : AgentivityNode.fromEntailmentProfile p ≤ AgentivityNode.fromEntailmentProfile q) : (!p.volition || q.volition) = true ∧ (!p.sentience || q.sentience) = true ∧ (!p.causation || q.causation) = true ∧ (!p.movement || q.movement) = true

Grimm's agentivity lattice ordering is consistent with Dowty's PAgentDominates: if Grimm a ≤ Grimm b on agentivity, then Dowty a dominates Dowty b on P-Agent features.

This holds because the feature-to-feature mapping is a bijection on the first 4 P-Agent features (volition, sentience, causation=instigation, movement=motion).

theorem ArgumentStructure.AgentivityLattice.fromEntailmentProfile_monotone (p q : EntailmentProfile) (hv : p.volition = true → q.volition = true) (hs : p.sentience = true → q.sentience = true) (hc : p.causation = true → q.causation = true) (hm : p.movement = true → q.movement = true) : AgentivityNode.fromEntailmentProfile p ≤ AgentivityNode.fromEntailmentProfile q

The Dowty→Grimm bridge is monotone: if one EntailmentProfile dominates another on P-Agent features, the corresponding AgentivityNodes are ordered.

Dominance is lattice order plus independent existence

[Dow91]'s five P-Agent entailments (Table 1 of [Gri11]) split into [Gri11]'s four agentivity primitives (Table 2) plus independent existence, which Grimm recasts on the persistence axis (§2.1). The three theorems below make the split exact: the flat count decomposes through the bridge, the lattice's feature count is monotone in the inclusion order (§2.3: higher in the lattice = higher degree of agentivity), and Dowty's PAgentDominates is precisely lattice order plus an independent-existence implication (§2.2).

theorem ArgumentStructure.AgentivityLattice.AgentivityNode.featureCount_monotone : Monotone featureCount

Feature count is monotone in the inclusion order ([Gri11] §2.3): ascending the Fig. 1 lattice never loses agentivity features.

theorem ArgumentStructure.AgentivityLattice.pAgentScore_decomposition (p : EntailmentProfile) : p.pAgentScore = (AgentivityNode.fromEntailmentProfile p).featureCount + p.independentExistence.toNat

Dowty's flat P-Agent count decomposes through the bridge: the four lattice features ([Gri11] Table 2) plus independent existence, the one Table 1 entailment Grimm moves to the persistence axis (§2.1).

theorem ArgumentStructure.AgentivityLattice.pAgentDominates_iff (p q : EntailmentProfile) : p.PAgentDominates q ↔ AgentivityNode.fromEntailmentProfile q ≤ AgentivityNode.fromEntailmentProfile p ∧ (q.independentExistence = true → p.independentExistence = true)

Dowty's subset dominance is exactly Grimm's lattice order plus an independent-existence implication ([Gri11] §2.2, Fig. 1): the bridge loses no dominance information. Derived from fromEntailmentProfile_monotone and grimm_agentivity_consistent_with_dowty.