Proto-role entailment profiles

[Dow91] [Gri11] [DK00b] [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
• the pointwise BooleanAlgebra instance, EntailmentProfile.support, and the cluster sets ProtoRoleFeature.agentCluster/patientCluster — the Boolean-cube order, with the counting accessors and dominance relations recharacterized as cardinality and cluster-restricted inclusion
• 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/ArgumentStructure/LevinClassProfiles.lean)
• the projection to [Gri11]'s lattice objects and its consistency theorems live in Projection.lean

Implementation notes

The ten entailments are not independent ([Lev19] §2.1): volition presupposes sentience (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.lean, reached via the projection in Projection.lean. [Dow91]'s original flat-counting selection principle is preserved for comparison in Studies/Dowty1991.lean; the counting accessors here are informational only. Causation priority ([DK00b]) 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.

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

Equations

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

@[instance_reducible]

instance ArgumentStructure.instDecidableEqEntailmentProfile : DecidableEq EntailmentProfile

Equations

• ArgumentStructure.instDecidableEqEntailmentProfile = ArgumentStructure.instDecidableEqEntailmentProfile.decEq

@[instance_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.

inductive ArgumentStructure.ProtoRoleFeature : Type

The ten proto-role entailments as a feature index ([Dow91] pp.572–573): five Proto-Agent, then five Proto-Patient.

• volition : ProtoRoleFeature
• sentience : ProtoRoleFeature
• causation : ProtoRoleFeature
• movement : ProtoRoleFeature
• independentExistence : ProtoRoleFeature
• changeOfState : ProtoRoleFeature
• incrementalTheme : ProtoRoleFeature
• causallyAffected : ProtoRoleFeature
• stationary : ProtoRoleFeature
• dependentExistence : ProtoRoleFeature

@[instance_reducible]

instance ArgumentStructure.instDecidableEqProtoRoleFeature : DecidableEq ProtoRoleFeature

Equations

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

@[instance_reducible]

instance ArgumentStructure.instReprProtoRoleFeature : Repr ProtoRoleFeature

Equations

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

def ArgumentStructure.instReprProtoRoleFeature.repr : ProtoRoleFeature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ArgumentStructure.instFintypeProtoRoleFeature : Fintype ProtoRoleFeature

Equations

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

def ArgumentStructure.EntailmentProfile.feature (p : EntailmentProfile) : ProtoRoleFeature → Bool

A profile as its feature-indicator function: the profile is a point of the Boolean cube on ProtoRoleFeature.

Equations

• p.feature ArgumentStructure.ProtoRoleFeature.volition = p.volition
• p.feature ArgumentStructure.ProtoRoleFeature.sentience = p.sentience
• p.feature ArgumentStructure.ProtoRoleFeature.causation = p.causation
• p.feature ArgumentStructure.ProtoRoleFeature.movement = p.movement
• p.feature ArgumentStructure.ProtoRoleFeature.independentExistence = p.independentExistence
• p.feature ArgumentStructure.ProtoRoleFeature.changeOfState = p.changeOfState
• p.feature ArgumentStructure.ProtoRoleFeature.incrementalTheme = p.incrementalTheme
• p.feature ArgumentStructure.ProtoRoleFeature.causallyAffected = p.causallyAffected
• p.feature ArgumentStructure.ProtoRoleFeature.stationary = p.stationary
• p.feature ArgumentStructure.ProtoRoleFeature.dependentExistence = p.dependentExistence

def ArgumentStructure.EntailmentProfile.equivFeatures : EntailmentProfile ≃ (ProtoRoleFeature → Bool)

EntailmentProfile is the Boolean cube ProtoRoleFeature → Bool; the Fintype instance (and any order or Boolean-algebra structure a consumer needs) transports along this equivalence.

Equations

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

@[instance_reducible]

instance ArgumentStructure.EntailmentProfile.instFintype : Fintype EntailmentProfile

Equations

• ArgumentStructure.EntailmentProfile.instFintype = Fintype.ofEquiv (ArgumentStructure.ProtoRoleFeature → Bool) ArgumentStructure.EntailmentProfile.equivFeatures.symm

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

@[instance_reducible]

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

Equations

• ArgumentStructure.instDecidablePAgentDominates p q = id inferInstance

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

@[instance_reducible]

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

Equations

• ArgumentStructure.instDecidablePPatientDominates p q = id inferInstance

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

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

Equations

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

@[instance_reducible]

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

Equations

• ArgumentStructure.instDecidablePAgentStrictlyDominates p q = id inferInstance

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

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

Equations

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

@[instance_reducible]

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

Equations

• ArgumentStructure.instDecidablePPatientStrictlyDominates p q = id inferInstance

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

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

Argument selection

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

The lattice-based Argument Selection Principle ([Gri11], [DK00b]): 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

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

@[instance_reducible]

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

Equations

• ArgumentStructure.instDecidableOutranksForSubject subj obj = id inferInstance

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

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

@[instance_reducible]

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

Equations

• ArgumentStructure.instDecidableAllowsAlternation p q = id inferInstance

Split intransitivity

def ArgumentStructure.PredictsUnaccusative (p : EntailmentProfile) : Prop

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

Equations

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

@[instance_reducible]

instance ArgumentStructure.instDecidablePredEntailmentProfilePredictsUnaccusative : DecidablePred PredictsUnaccusative

Equations

• ArgumentStructure.instDecidablePredEntailmentProfilePredictsUnaccusative p = id inferInstance

def ArgumentStructure.PredictsUnergative (p : EntailmentProfile) : Prop

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

Equations

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

@[instance_reducible]

instance ArgumentStructure.instDecidablePredEntailmentProfilePredictsUnergative : DecidablePred PredictsUnergative

Equations

• ArgumentStructure.instDecidablePredEntailmentProfilePredictsUnergative p = id inferInstance

Well-formedness

def ArgumentStructure.WellFormedInternal (p : EntailmentProfile) : Prop

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

Equations

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

@[instance_reducible]

instance ArgumentStructure.instDecidablePredEntailmentProfileWellFormedInternal : DecidablePred WellFormedInternal

Equations

• ArgumentStructure.instDecidablePredEntailmentProfileWellFormedInternal p = id inferInstance

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

Three Proto-Agent entailments pair asymmetrically across a subject–object pair ([DK00b], [Pri99]): causation → changeOfState, movement → stationary, independentExistence → dependentExistence.

Equations

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

@[instance_reducible]

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

Equations

• ArgumentStructure.instDecidableWellFormedPair subj obj = id inferInstance

The do-test

def ArgumentStructure.PassesDoTestFromProfile (p : EntailmentProfile) : Prop

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

Equations

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

@[instance_reducible]

instance ArgumentStructure.instDecidablePredEntailmentProfilePassesDoTestFromProfile : DecidablePred PassesDoTestFromProfile

Equations

• ArgumentStructure.instDecidablePredEntailmentProfilePassesDoTestFromProfile p = id inferInstance

Effectors and force recipients

def ArgumentStructure.IsEffector (p : EntailmentProfile) : Prop

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

Equations

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

@[instance_reducible]

instance ArgumentStructure.instDecidablePredEntailmentProfileIsEffector : DecidablePred IsEffector

Equations

• ArgumentStructure.instDecidablePredEntailmentProfileIsEffector p = id inferInstance

def ArgumentStructure.IsForceRecipient (p : EntailmentProfile) : Prop

Causally affected or stationary, realized as internal argument.

Equations

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

@[instance_reducible]

instance ArgumentStructure.instDecidablePredEntailmentProfileIsForceRecipient : DecidablePred IsForceRecipient

Equations

• ArgumentStructure.instDecidablePredEntailmentProfileIsForceRecipient p = id inferInstance

theorem ArgumentStructure.two_le_pAgentScore_of_isEffector (p : EntailmentProfile) (h : IsEffector p) : 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/ArgumentStructure/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.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.activitySubjectProfile = { volition := true, sentience := true, movement := true, independentExistence := true }

def ArgumentStructure.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.achievementSubjectProfile = { movement := true, independentExistence := true, changeOfState := true }

def ArgumentStructure.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.accomplishmentSubjectProfile = { volition := true, sentience := true, causation := true, movement := true, independentExistence := true }

def ArgumentStructure.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.accomplishmentObjectProfile = { changeOfState := true, causallyAffected := true }

The Boolean cube order

Pointwise order and Boolean-algebra structure, transported along equivFeatures: p ≤ q is entailment-set inclusion, and p ⊔ q imposes the union of the two profiles' entailments — [RS05]'s role bundling. support is the imposed entailment set; the counting accessors and dominance relations are its cardinality and cluster-restricted inclusion (pAgentScore_eq_card, pAgentDominates_iff_subset).

def ArgumentStructure.ProtoRoleFeature.agentCluster : Finset ProtoRoleFeature

[Dow91]'s five Proto-Agent entailments as a feature set.

Equations

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

def ArgumentStructure.ProtoRoleFeature.patientCluster : Finset ProtoRoleFeature

The five Proto-Patient entailments as a feature set.

Equations

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

theorem ArgumentStructure.ProtoRoleFeature.disjoint_agentCluster_patientCluster : Disjoint agentCluster patientCluster

theorem ArgumentStructure.ProtoRoleFeature.agentCluster_union_patientCluster : agentCluster ∪ patientCluster = Finset.univ

@[instance_reducible]

instance ArgumentStructure.EntailmentProfile.instBooleanAlgebra : BooleanAlgebra EntailmentProfile

Equations

• ArgumentStructure.EntailmentProfile.instBooleanAlgebra = ArgumentStructure.EntailmentProfile.equivFeatures.booleanAlgebra

theorem ArgumentStructure.EntailmentProfile.le_def {p q : EntailmentProfile} : p ≤ q ↔ ∀ (f : ProtoRoleFeature), p.feature f ≤ q.feature f

@[instance_reducible]

instance ArgumentStructure.EntailmentProfile.instDecidableRelLe : DecidableRel fun (x1 x2 : EntailmentProfile) => x1 ≤ x2

Equations

• x✝¹.instDecidableRelLe x✝ = decidable_of_iff (∀ (f : ArgumentStructure.ProtoRoleFeature), x✝¹.feature f ≤ x✝.feature f) ⋯

@[simp]

theorem ArgumentStructure.EntailmentProfile.feature_sup (p q : EntailmentProfile) (f : ProtoRoleFeature) : (p ⊔ q).feature f = (p.feature f || q.feature f)

def ArgumentStructure.EntailmentProfile.support (p : EntailmentProfile) : Finset ProtoRoleFeature

The set of entailments a profile imposes.

Equations

• p.support = {f : ArgumentStructure.ProtoRoleFeature | p.feature f = true}

@[simp]

theorem ArgumentStructure.EntailmentProfile.mem_support {p : EntailmentProfile} {f : ProtoRoleFeature} : f ∈ p.support ↔ p.feature f = true

@[simp]

theorem ArgumentStructure.EntailmentProfile.support_sup (p q : EntailmentProfile) : (p ⊔ q).support = p.support ∪ q.support

theorem ArgumentStructure.EntailmentProfile.le_iff_support_subset {p q : EntailmentProfile} : p ≤ q ↔ p.support ⊆ q.support

theorem ArgumentStructure.EntailmentProfile.support_inter_eq_filter (p : EntailmentProfile) (s : Finset ProtoRoleFeature) : p.support ∩ s = {f ∈ s | p.feature f = true}

theorem ArgumentStructure.EntailmentProfile.pAgentScore_eq_card (p : EntailmentProfile) : p.pAgentScore = (p.support ∩ ProtoRoleFeature.agentCluster).card

The Proto-Agent count is the size of the support's agent-cluster part.

theorem ArgumentStructure.EntailmentProfile.pPatientScore_eq_card (p : EntailmentProfile) : p.pPatientScore = (p.support ∩ ProtoRoleFeature.patientCluster).card

The Proto-Patient count is the size of the support's patient-cluster part.

theorem ArgumentStructure.EntailmentProfile.pAgentScore_mono : Monotone pAgentScore

theorem ArgumentStructure.EntailmentProfile.pPatientScore_mono : Monotone pPatientScore

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

The profile imposes entailments from both proto-role clusters — [RS05]'s complex role.

Equations

• p.IsComplexRole = (0 < p.pAgentScore ∧ 0 < p.pPatientScore)

@[instance_reducible]

instance ArgumentStructure.EntailmentProfile.instDecidablePredIsComplexRole : DecidablePred IsComplexRole

Equations

• p.instDecidablePredIsComplexRole = ArgumentStructure.EntailmentProfile.instDecidablePredIsComplexRole._aux_1 p

theorem ArgumentStructure.EntailmentProfile.isComplexRole_sup {p q : EntailmentProfile} (ha : 0 < p.pAgentScore) (hp : 0 < q.pPatientScore) : (p ⊔ q).IsComplexRole

Joining an agentive profile with an affected one yields a complex role.

theorem ArgumentStructure.pAgentDominates_iff_subset (p q : EntailmentProfile) : PAgentDominates p q ↔ q.support ∩ ProtoRoleFeature.agentCluster ⊆ p.support ∩ ProtoRoleFeature.agentCluster

Proto-Agent dominance is inclusion of the supports' agent-cluster parts.

theorem ArgumentStructure.pPatientDominates_iff_subset (p q : EntailmentProfile) : PPatientDominates p q ↔ q.support ∩ ProtoRoleFeature.patientCluster ⊆ p.support ∩ ProtoRoleFeature.patientCluster

Proto-Patient dominance is inclusion of the supports' patient-cluster parts.

theorem ArgumentStructure.pAgentDominates_sup_left (p q : EntailmentProfile) : PAgentDominates (p ⊔ q) p

The join retains the left component's Proto-Agent entailments.

theorem ArgumentStructure.pAgentDominates_sup_right (p q : EntailmentProfile) : PAgentDominates (p ⊔ q) q

The join retains the right component's Proto-Agent entailments.

theorem ArgumentStructure.pPatientDominates_sup_left (p q : EntailmentProfile) : PPatientDominates (p ⊔ q) p

The join inherits the left component's Proto-Patient entailments.

theorem ArgumentStructure.pPatientDominates_sup_right (p q : EntailmentProfile) : PPatientDominates (p ⊔ q) q

The join inherits the right component's Proto-Patient entailments.