Documentation

Linglib.Semantics.ArgumentStructure.AgentivityLattice.Persistence

Persistence levels #

Grimm replaces Dowty's five Proto-Patient entailments by four persistence features, existential and qualitative persistence at the beginning and at the end of the event. Their logical dependencies, that an entity that exists does so with its qualities and that nonexistence at a boundary erases them, leave five valid combinations, ordered by inclusion: a lattice with a creation branch (exPersEnd) and an affectedness branch (exPersBeginning ≤ quPersBeginning) rejoining at totalPersistence.

Main definitions #

Implementation notes #

A level is SetLike over its features, so its order is inclusion. Grimm's first principle, that some qualitative persistence accompanies existential persistence, is read as qualitative persistence at the beginning with existence there and some qualitative persistence with existence at the end; this is the reading under which exactly five combinations remain, as the paper says. The levels are closed under union but not under intersection, so the meet is the largest level inside the intersection, given by a table.

References #

source
inductive ArgumentStructure.PersistenceLevel :
Type

The five valid persistence levels ([Gri11] pp.524–525, Fig. 2).

  • totalNonPersistence : PersistenceLevel

    No entailed existence, as for the arguments of seek, want and negated copulas.

  • exPersEnd : PersistenceLevel

    The entity comes into existence, as the objects of build, invent and the subject of appear do.

  • exPersBeginning : PersistenceLevel

    The entity exists before the event and ceases to, as the subjects of die, evaporate and the objects of destroy, ruin do.

  • quPersBeginning : PersistenceLevel

    The entity persists but is qualitatively changed, as the objects of transitive move, dim, frighten and the intransitive subject of fall are.

  • totalPersistence : PersistenceLevel

    The entity persists unchanged throughout, as prototypical transitive subjects and the unaffected objects of see and cut at do.

Instances For
    source
    @[instance_reducible]
    instance ArgumentStructure.instDecidableEqPersistenceLevel :
    DecidableEq PersistenceLevel
    Equations
    source
    def ArgumentStructure.instReprPersistenceLevel.repr :
    PersistenceLevel → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[instance_reducible]
      instance ArgumentStructure.instReprPersistenceLevel :
      Repr PersistenceLevel
      Equations
      source
      @[instance_reducible]
      instance ArgumentStructure.instFintypePersistenceLevel :
      Fintype PersistenceLevel
      Equations
      • One or more equations did not get rendered due to their size.
      source
      inductive ArgumentStructure.PersistenceLevel.Feature :
      Type

      The four persistence features ([Gri11] Table 2).

      • exPB : Feature

        Existential persistence at the beginning of the event.

      • exPE : Feature

        Existential persistence at the end of the event.

      • quPB : Feature

        Qualitative persistence at the beginning of the event.

      • quPE : Feature

        Qualitative persistence at the end of the event.

      Instances For
        source
        @[instance_reducible]
        instance ArgumentStructure.PersistenceLevel.instDecidableEqFeature :
        DecidableEq Feature
        Equations
        source
        def ArgumentStructure.PersistenceLevel.instReprFeature.repr :
        Feature → ℕ → Std.Format
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[instance_reducible]
          instance ArgumentStructure.PersistenceLevel.instReprFeature :
          Repr Feature
          Equations
          source
          @[instance_reducible]
          instance ArgumentStructure.PersistenceLevel.instFintypeFeature :
          Fintype Feature
          Equations
          • One or more equations did not get rendered due to their size.
          source
          def ArgumentStructure.PersistenceLevel.features :
          PersistenceLevel → Finset Feature

          The features of a level.

          Equations
          Instances For
            source
            theorem ArgumentStructure.PersistenceLevel.features_injective :
            Function.Injective features
            source
            def ArgumentStructure.PersistenceLevel.Valid (s : Finset Feature) :
            Prop

            Grimm's exclusion principles on persistence features: qualities persist at a boundary only where the entity exists there, existence at the beginning brings qualitative persistence at the beginning, and existence at the end brings some qualitative persistence.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              instance ArgumentStructure.PersistenceLevel.instDecidablePredFinsetFeatureValid :
              DecidablePred Valid
              Equations
              • One or more equations did not get rendered due to their size.
              source
              theorem ArgumentStructure.PersistenceLevel.range_features :
              Set.range features = {s : Finset Feature | Valid s}

              The five levels are exactly the combinations of features the exclusion principles leave.

              source
              @[instance_reducible]
              instance ArgumentStructure.PersistenceLevel.instSetLikeFeature :
              SetLike PersistenceLevel Feature
              Equations
              • One or more equations did not get rendered due to their size.
              source
              @[instance_reducible]
              instance ArgumentStructure.PersistenceLevel.instPartialOrder :
              PartialOrder PersistenceLevel
              Equations
              source
              @[simp]
              theorem ArgumentStructure.PersistenceLevel.mem_features {l : PersistenceLevel} {f : Feature} :
              f ∈ l.features ↔ f ∈ l
              source
              @[instance_reducible]
              instance ArgumentStructure.PersistenceLevel.instDecidablePredFeatureMem (l : PersistenceLevel) :
              DecidablePred fun (x : Feature) => x ∈ l
              Equations
              source
              theorem ArgumentStructure.PersistenceLevel.le_iff_features_subset {l m : PersistenceLevel} :
              l ≤ m ↔ l.features ⊆ m.features
              source
              @[instance_reducible]
              instance ArgumentStructure.PersistenceLevel.instDecidableRelLe :
              DecidableRel fun (x1 x2 : PersistenceLevel) => x1 ≤ x2
              Equations
              source
              def ArgumentStructure.PersistenceLevel.sup' :
              PersistenceLevel → PersistenceLevel → PersistenceLevel

              The join of two levels, the level whose features are the union of theirs.

              Equations
              Instances For
                source
                def ArgumentStructure.PersistenceLevel.inf' :
                PersistenceLevel → PersistenceLevel → PersistenceLevel

                The meet of two levels, the largest level inside the intersection of their features.

                Equations
                Instances For
                  source
                  theorem ArgumentStructure.PersistenceLevel.features_sup' (l m : PersistenceLevel) :
                  (l.sup' m).features = l.features ∪ m.features

                  The features of a join are the union of the features.

                  source
                  @[instance_reducible]
                  instance ArgumentStructure.PersistenceLevel.instLattice :
                  Lattice PersistenceLevel
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  @[instance_reducible]
                  instance ArgumentStructure.PersistenceLevel.instBoundedOrder :
                  BoundedOrder PersistenceLevel
                  Equations
                  • One or more equations did not get rendered due to their size.