Proto-role entailment profiles

An EntailmentProfile is the set of Dowty's ten proto-role entailments a verb imposes on one of its arguments. Proto-Agent and Proto-Patient are cluster concepts: each is a set of five entailments, and an argument's agenthood and patienthood are the parts of its profile that fall in each cluster, protoAgent and protoPatient.

Main definitions

• EntailmentProfile: the entailments a verb imposes on an argument.
• EntailmentProfile.protoAgent, EntailmentProfile.protoPatient: its parts in the two clusters.
• EntailmentProfile.IsComplexRole: entailments from both clusters.

Implementation notes

The entailments are not independent: volition presupposes sentience (WellFormedInternal). Since profiles are sets, p ⊆ q is entailment inclusion and p ∪ q imposes both profiles' entailments, Reinhart and Siloni's role bundling. Argument selection by inclusion is OutranksForSubject, the traditional labels are ThetaRole, the class templates are RoleList, and the projection to Grimm's agentivity lattice is EntailmentProfile.toAgentivity.

References

• [Dow91]
• [Lev20]
• [RS05]

inductive ArgumentStructure.ProtoRoleFeature : Type

The ten entailments defining the proto-roles ([Dow91] pp.572–573): the first five are Proto-Agent, the last five Proto-Patient.

• volition : ProtoRoleFeature

  Volitional involvement in the event.

• sentience : ProtoRoleFeature

  Sentience or perception.

• causation : ProtoRoleFeature

  Causes an event or change of state in another participant.

• movement : ProtoRoleFeature

  Movement relative to another participant.

• independentExistence : ProtoRoleFeature

  Exists independently of the event named by the verb.

• changeOfState : ProtoRoleFeature

  Undergoes a change of state.

• incrementalTheme : ProtoRoleFeature

  The argument is an incremental theme, measuring out the event.

• causallyAffected : ProtoRoleFeature

  Causally affected by another participant.

• stationary : ProtoRoleFeature

  Stationary relative to another participant.

• dependentExistence : ProtoRoleFeature

  Does not exist independently of the event.

@[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.ProtoRoleFeature.agentCluster : Finset ProtoRoleFeature

Dowty's five Proto-Agent entailments.

Equations

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

def ArgumentStructure.ProtoRoleFeature.patientCluster : Finset ProtoRoleFeature

Dowty's five Proto-Patient entailments.

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

@[reducible, inline]

abbrev ArgumentStructure.EntailmentProfile : Type

The proto-role entailments a verb imposes on one of its arguments.

Equations

• ArgumentStructure.EntailmentProfile = Finset ArgumentStructure.ProtoRoleFeature

@[instance_reducible]

instance ArgumentStructure.instReprEntailmentProfile : Repr EntailmentProfile

A profile is printed as the list of its entailments in Dowty's order.

Equations

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

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

The Proto-Agent entailments of a profile.

Equations

• p.protoAgent = p ∩ ArgumentStructure.ProtoRoleFeature.agentCluster

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

The Proto-Patient entailments of a profile.

Equations

• p.protoPatient = p ∩ ArgumentStructure.ProtoRoleFeature.patientCluster

theorem ArgumentStructure.EntailmentProfile.protoAgent_mono : Monotone protoAgent

theorem ArgumentStructure.EntailmentProfile.protoPatient_mono : Monotone protoPatient

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

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

Equations

• p.IsComplexRole = (p.protoAgent.Nonempty ∧ p.protoPatient.Nonempty)

@[instance_reducible]

instance ArgumentStructure.EntailmentProfile.instDecidablePredIsComplexRole : DecidablePred IsComplexRole

Equations

• p.instDecidablePredIsComplexRole = { decide := decide p.protoAgent.Nonempty && decide p.protoPatient.Nonempty, reflects_decide := ⋯ }

theorem ArgumentStructure.EntailmentProfile.isComplexRole_union {p q : EntailmentProfile} (ha : p.protoAgent.Nonempty) (hp : q.protoPatient.Nonempty) : (p ∪ q).IsComplexRole

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

Well-formedness

def ArgumentStructure.WellFormedInternal (p : EntailmentProfile) : Prop

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

Equations

• ArgumentStructure.WellFormedInternal p = (ArgumentStructure.ProtoRoleFeature.volition ∈ p → ArgumentStructure.ProtoRoleFeature.sentience ∈ p)

@[instance_reducible]

instance ArgumentStructure.instDecidablePredEntailmentProfileWellFormedInternal : DecidablePred WellFormedInternal

Equations

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