Documentation

Linglib.Semantics.ArgumentStructure.AgentivityLattice.OfEntailmentProfile

From Dowty's entailments to Grimm's lattice #

Grimm keeps volition and sentience from Dowty's Proto-Agent entailments, recasts causation as instigation, bound to a single participant, and movement as motion, and moves independent existence to the persistence axis. The four agentivity features thus embed in Dowty's entailments, and the agentivity of a profile is its preimage under that embedding. The projection is monotone, and Dowty's inclusion of Proto-Agent entailments is exactly Grimm's order on agentivity together with independent existence, so Grimm's dominance criterion selects a subject wherever it strictly dominates.

Main definitions #

Main results #

Implementation notes #

Grimm states the persistence counterparts of Dowty's Proto-Patient entailments as two constraints, not as a function, so a profile is related to the levels it admits rather than mapped to one.

References #

source
def ArgumentStructure.Agentivity.Feature.toProtoRole :
Feature ↪ ProtoRoleFeature

The agentivity features as Dowty's Proto-Agent entailments ([Gri11] p.521).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def ArgumentStructure.EntailmentProfile.toAgentivity (p : EntailmentProfile) :
    Agentivity

    The agentivity of a profile, the features whose Dowty counterparts it entails.

    Equations
    Instances For
      source
      @[simp]
      theorem ArgumentStructure.EntailmentProfile.mem_toAgentivity {p : EntailmentProfile} {f : Agentivity.Feature} :
      f ∈ p.toAgentivity ↔ Agentivity.Feature.toProtoRole f ∈ p
      source
      theorem ArgumentStructure.EntailmentProfile.toAgentivity_eq_preimage (p : EntailmentProfile) :
      p.toAgentivity = Finset.preimage p ⇑Agentivity.Feature.toProtoRole ⋯

      The agentivity of a profile is its preimage under the embedding.

      source
      theorem ArgumentStructure.EntailmentProfile.toAgentivity_monotone :
      Monotone toAgentivity
      source
      theorem ArgumentStructure.EntailmentProfile.protoAgent_subset_iff {p q : EntailmentProfile} :
      q.protoAgent ⊆ p.protoAgent ↔ q.toAgentivity ⊆ p.toAgentivity ∧ (ProtoRoleFeature.independentExistence ∈ q → ProtoRoleFeature.independentExistence ∈ p)

      Dowty's inclusion of Proto-Agent entailments is Grimm's order on agentivity together with independent existence, which Grimm moves to the persistence axis.

      source
      theorem ArgumentStructure.outranks_of_lattice_dominance {subj obj : EntailmentProfile} (hlt : obj.toAgentivity ⊂ subj.toAgentivity) (hie : ProtoRoleFeature.independentExistence ∈ obj → ProtoRoleFeature.independentExistence ∈ subj) :
      OutranksForSubject subj obj

      Grimm's dominance criterion selects the subject when its agentivity strictly includes the object's and independent existence is preserved.

      source
      def ArgumentStructure.EntailmentProfile.Admits (p : EntailmentProfile) (l : PersistenceLevel) :
      Prop

      A profile admits a persistence level when the level respects Grimm's two correspondences with Dowty's Proto-Patient entailments: an argument entailed to change state is not entailed to persist qualitatively at the end ([Gri11] p.522), and one whose existence depends on the event, created, destroyed or not entailed to exist, does not persist existentially at both ends (p.524).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance ArgumentStructure.instDecidablePredPersistenceLevelAdmits (p : EntailmentProfile) :
        DecidablePred p.Admits
        Equations
        • One or more equations did not get rendered due to their size.