The Dowty→Grimm projection ([Gri11] §2.1)

The morphisms from [Dow91]'s EntailmentProfile to [Gri11]'s lattice objects: Agentivity.fromEntailmentProfile (the four P-Agent features minus independent existence), PersistenceLevel.fromPatientProfile (the P-Patient entailments read as persistence), and their pairing ParticipantType.fromSubjectProfile / fromObjectProfile.

The consistency theorems make the projection exact: its kernel (fromEntailmentProfile_eq_iff), its monotonicity, the decomposition of Dowty's flat count through it (pAgentScore_decomposition), dominance as lattice order plus independent existence (pAgentDominates_iff), and the Argument Selection Principle as lattice dominance (outranks_of_lattice_dominance).

def ArgumentStructure.Agentivity.fromEntailmentProfile (p : EntailmentProfile) : Agentivity

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.Agentivity.fromEntailmentProfile p = ArgumentStructure.Agentivity.mk p.volition p.sentience p.causation p.movement

theorem ArgumentStructure.Agentivity.fromEntailmentProfile_eq_iff (p q : EntailmentProfile) : fromEntailmentProfile p = fromEntailmentProfile q ↔ p.volition = q.volition ∧ p.sentience = q.sentience ∧ p.causation = q.causation ∧ p.movement = q.movement

Two profiles project to the same agentivity node iff they agree on the four lattice features: the projection drops independent existence and all five Proto-Patient entailments ([Gri11] §2.1 recasts them on the persistence axis).

def ArgumentStructure.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.ParticipantType.fromSubjectProfile (p : EntailmentProfile) : ParticipantType

Map a full EntailmentProfile to a ParticipantType.

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.ParticipantType.fromObjectProfile (p : EntailmentProfile) : ParticipantType

Equations

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

Grimm ↔ Dowty ASP consistency

theorem ArgumentStructure.grimm_agentivity_consistent_with_dowty (p q : EntailmentProfile) (h : Agentivity.fromEntailmentProfile p ≤ Agentivity.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.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) : Agentivity.fromEntailmentProfile p ≤ Agentivity.fromEntailmentProfile q

The Dowty→Grimm projection is monotone: if one EntailmentProfile dominates another on P-Agent features, the projected agentivity values 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 projection, 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.Agentivity.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.pAgentScore_decomposition (p : EntailmentProfile) : p.pAgentScore = (Agentivity.fromEntailmentProfile p).featureCount + p.independentExistence.toNat

Dowty's flat P-Agent count decomposes through the projection: 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.pAgentDominates_iff (p q : EntailmentProfile) : PAgentDominates p q ↔ Agentivity.fromEntailmentProfile q ≤ Agentivity.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 projection loses no dominance information. Derived from fromEntailmentProfile_monotone and grimm_agentivity_consistent_with_dowty.

theorem ArgumentStructure.outranks_of_lattice_dominance (subj obj : EntailmentProfile) (hlt : Agentivity.fromEntailmentProfile obj < Agentivity.fromEntailmentProfile subj) (hIE : obj.independentExistence = true → subj.independentExistence = true) : OutranksForSubject subj obj

[Gri11]'s Argument Selection Principle as lattice dominance: if subj's agentivity node strictly dominates obj's and independent existence is preserved, subj is selected — for every profile pair, via pAgentDominates_iff, not per-verb checking.