The agentivity cube ([Gri11] §2.1)

[Gri11] reformulates [Dow91]'s Proto-Agent entailments as four privative features: Proto-Patient is not a separate cluster but the underspecified (∅) pole of each feature, and Dowty's relational "causation" is decomposed into participant-bound "instigation" (p.521). Agentivity is the Boolean cube on Agentivity.Feature, ordered by feature-set inclusion; Grimm's Fig. 1 lattice is its 12-element Agentivity.Valid subset.

The persistence axis is PersistenceLevel.lean; the product object is ParticipantType.lean; the projection from [Dow91]'s profiles is Projection.lean.

inductive ArgumentStructure.Agentivity.Feature : Type

The four agentivity primitives (Table 2 (agentive properties), p.520).

Each has an agentive (+) and non-agentive (∅) pole; the non-agentive pole is simply the absence of the property — the privative opposition that replaces Dowty's two independent clusters.

• volition : Feature

  +volition: the participant intends to bring about the event.

• sentience : Feature

  +sentience: conscious involvement in the action or state.

• instigation : Feature

  +instigation: prior independent action whose effects can be attributed to this argument. Replaces Dowty's "causation" (p.521).

• motion : Feature

  +motion: the argument is in motion during the event.

@[implicit_reducible]

instance ArgumentStructure.Agentivity.instDecidableEqFeature : DecidableEq Feature

Equations

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

@[implicit_reducible]

instance ArgumentStructure.Agentivity.instReprFeature : Repr Feature

Equations

• ArgumentStructure.Agentivity.instReprFeature = { reprPrec := ArgumentStructure.Agentivity.instReprFeature.repr }

def ArgumentStructure.Agentivity.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ArgumentStructure.Agentivity.instFintypeFeature : Fintype Feature

Equations

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

def ArgumentStructure.Agentivity : Type

An argument's agentivity: which of the four primitives it bears, as a point of the Boolean cube on Agentivity.Feature. Order, lattice, and Boolean-algebra structure are pointwise, so a ≤ b is feature-set inclusion; Grimm's Fig. 1 lattice is the 12-element Valid subset of the 16-element cube.

Equations

• ArgumentStructure.Agentivity = (ArgumentStructure.Agentivity.Feature → Bool)

@[implicit_reducible]

instance ArgumentStructure.Agentivity.instDecidableEq : DecidableEq Agentivity

Equations

• ArgumentStructure.Agentivity.instDecidableEq = ArgumentStructure.Agentivity.instDecidableEq._aux_1

@[implicit_reducible]

instance ArgumentStructure.Agentivity.instFintype : Fintype Agentivity

Equations

• ArgumentStructure.Agentivity.instFintype = { elems := ArgumentStructure.Agentivity.instFintype._aux_1, complete := ArgumentStructure.Agentivity.instFintype._proof_3 }

@[implicit_reducible]

instance ArgumentStructure.Agentivity.instBooleanAlgebra : BooleanAlgebra Agentivity

Equations

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

@[implicit_reducible]

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

Equations

• a.instDecidableRelLe b = decidable_of_iff (∀ (f : ArgumentStructure.Agentivity.Feature), a f ≤ b f) ⋯

@[implicit_reducible]

instance ArgumentStructure.Agentivity.instDecidableRelLt : DecidableRel fun (x1 x2 : Agentivity) => x1 < x2

Equations

• x✝¹.instDecidableRelLt x✝ = decidable_of_iff' (x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹) ⋯

def ArgumentStructure.Agentivity.mk (volition sentience instigation motion : Bool) : Agentivity

Build an agentivity value from the four indicators, in Table 2 order.

Equations

• ArgumentStructure.Agentivity.mk volition sentience instigation motion ArgumentStructure.Agentivity.Feature.volition = volition
• ArgumentStructure.Agentivity.mk volition sentience instigation motion ArgumentStructure.Agentivity.Feature.sentience = sentience
• ArgumentStructure.Agentivity.mk volition sentience instigation motion ArgumentStructure.Agentivity.Feature.instigation = instigation
• ArgumentStructure.Agentivity.mk volition sentience instigation motion ArgumentStructure.Agentivity.Feature.motion = motion

@[implicit_reducible]

instance ArgumentStructure.Agentivity.instRepr : Repr Agentivity

Equations

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

@[simp]

theorem ArgumentStructure.Agentivity.mk_inj {v s i m v' s' i' m' : Bool} : mk v s i m = mk v' s' i' m' ↔ v = v' ∧ s = s' ∧ i = i' ∧ m = m'

def ArgumentStructure.Agentivity.volition (a : Agentivity) : Bool

Volition indicator.

Equations

• a.volition = a ArgumentStructure.Agentivity.Feature.volition

def ArgumentStructure.Agentivity.sentience (a : Agentivity) : Bool

Sentience indicator.

Equations

• a.sentience = a ArgumentStructure.Agentivity.Feature.sentience

def ArgumentStructure.Agentivity.instigation (a : Agentivity) : Bool

Instigation indicator.

Equations

• a.instigation = a ArgumentStructure.Agentivity.Feature.instigation

def ArgumentStructure.Agentivity.motion (a : Agentivity) : Bool

Motion indicator.

Equations

• a.motion = a ArgumentStructure.Agentivity.Feature.motion

def ArgumentStructure.Agentivity.Valid (a : Agentivity) : Prop

Validity: volition presupposes sentience (p.521, following [Dow91] p.607). Carves Grimm's 12-element Fig. 1 lattice out of the 16-element cube.

Equations

• a.Valid = (a.volition = true → a.sentience = true)

@[implicit_reducible]

instance ArgumentStructure.Agentivity.instDecidableValid (a : Agentivity) : Decidable a.Valid

Equations

• a.instDecidableValid = id inferInstance

def ArgumentStructure.Agentivity.featureCount (a : Agentivity) : ℕ

Number of positive features (= height in the cube).

Equations

• a.featureCount = a.volition.toNat + a.sentience.toNat + a.instigation.toNat + a.motion.toNat

theorem ArgumentStructure.Agentivity.le_iff (a b : Agentivity) : a ≤ b ↔ (a.volition = true → b.volition = true) ∧ (a.sentience = true → b.sentience = true) ∧ (a.instigation = true → b.instigation = true) ∧ (a.motion = true → b.motion = true)

The inclusion order, componentwise.