Hafeez (2025): Agentivity and causation in Urdu

[Haf25] asks which Urdu causal constructions speakers accept for which causal scenes. The scenes are the 43 video clips of the Causality Across Languages project, and they vary along three variables: the causer is an intentional human (IHCr), an accidental human (AHCr) or a natural force (NFCr); the second participant of the chain is a controlling human causee (ContrHCEAF), a physically or a psychologically impacted human (PhysImpHCEAF, PsychImpHCEAF) or an inanimate affectee (InanCEAF); and a third participant does or does not mediate the chain (Mediation).

The acceptability study (chapter 5) had twelve raters judge a description of every clip in each of seven response types, and fits one conditional inference tree per response type. Each leaf of a tree is a conjunction of signed predictors such as [+IHCr, -Mediation, +InanCEAF], and the leaf with the highest share of ceiling ratings is the response type's hypothesized semantic prototype when that share exceeds 50% (Table 18). The response types are the lexical ergative LEX-ERG (ergative causer, transitive verb), the lexical instrumental LEX-INST (instrumental causer, intransitive verb), the lexical dative LEX-DAT (dative causee or affectee, infinitive and light verb), the morphological causative verb MCV (the indirect causative -va; verbs with the direct causative -aa count as lexical), the adverbial ADV (two clauses joined by keyoonkeh 'because'), the non-sentential cause adjunct NCA (a cause NP with =par, wajhan=se or =se) and the non-sentential causer adjunct NCrA (a causer NP with wajhan=se). The printed tables are Data/Experiments/Hafeez2025.

• The coding. A clip's scene is read off its name by the code of Appendix L (Clip.scene), and every clip is a scene the design can stage (clips_stageable). The predictor table as printed (Table 4) codes five clips otherwise (table4_disagreements), and it cannot be the coding the trees were fit on: three leaves hold more responses than twelve raters give their clips under it (table4_exceeded), while under the clip names no leaf does (responses_le) and all but three hold exactly that many (responses_shortfall).
• The trees. The trees reproduce Table 18's leaves with their node numbers (tree_leaves) and partition the scenes (leaves_partition, from Tree.countP_leaves). Table 18 prints the InanCEAF split of the ADV tree with reversed signs: section 5.3.5 puts the 90.8% peak on [-InanCEAF], and with the printed signs no ADV leaf holds its clips' responses (adv_printed_misfit). Every printed percentage is a count out of its responses except the 0.08 of the LEX-INST tree (attainablePercent_iff).
• The prototypes are derived as the highest leaf above 50% (prototype); LEX-DAT has none (prototype_eq_none_iff). Table 19 prints the peaks of NCA and NCrA swapped (summary_percent_swapped). The printed prototypes of Tables 19 and 25 denote the derived ones (summary_iff_prototype), LEX-ERG's only on stageable scenes, since it drops the leaf's [-Mediation] (lexErg_summary_not_prototype), and ADV's is the complement of the derived one (adv_summary_iff_not_prototype).
• Agentivity. The agentivity reading of the prototypes in the chapter's conclusion (lexErg_full, ncrA_nonagentive, …) follows from the prototypes and the agentivity degrees of the participants.
• Production. The production study's preferences (chapter 6, Table 25) refine the prototypes, the dovetailing the abstract reports (individual_le_prototype). The combined model's NCA preference reaches the clip of a woman startled by thunder, outside the NCA prototype (nca_combined_not_le_prototype).
• Comrie. The LEX-ERG prototype is unmediated and the MCV prototype mediated (lexErg_mcv_mediation), the order [Com89]'s compactness generalization demands of a lexical and a morphological causative (lexErg_mcv_comrieMonotone).

Implementation notes

The second participant is one variable with four values, so a scene type such as [-ContrHCEAF, +InanCEAF] and its shorter form [+InanCEAF] are equivalent, which is how Table 18's LEX-INST leaf and the LEX-INST prototype of Tables 19 and 25 agree. The scene's mediation is the substrate's Causation.Morphological.Mediation: [+Mediation] is a third participant between causer and result, the narrow sense of directness the dissertation distinguishes from the broad one.

References

• [Haf25]
• [Boh04]
• [Com89]

Scenes

inductive Hafeez2025.Causer : Type

The causer of a scene.

• intentionalHuman : Causer

  IHCr: acts intentionally and in control.

• accidentalHuman : Causer

  AHCr: acts accidentally, without intention or control.

• naturalForce : Causer

  NFCr: a natural force.

@[instance_reducible]

instance Hafeez2025.instDecidableEqCauser : DecidableEq Causer

Equations

• Hafeez2025.instDecidableEqCauser x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hafeez2025.instReprCauser : Repr Causer

Equations

• Hafeez2025.instReprCauser = { reprPrec := Hafeez2025.instReprCauser.repr }

def Hafeez2025.instReprCauser.repr : Causer → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Hafeez2025.instFintypeCauser : Fintype Causer

Equations

• Hafeez2025.instFintypeCauser = { elems := { val := ↑Hafeez2025.Causer.enumList, nodup := Hafeez2025.Causer.enumList_nodup }, complete := Hafeez2025.instFintypeCauser._proof_1 }

inductive Hafeez2025.CauseeAffectee : Type

The second participant of the causal chain: a causee when it is an induced agent, an affectee when it is a patient.

• controlling : CauseeAffectee

  ContrHCEAF: a human who controls the induced action.

• physicallyImpacted : CauseeAffectee

  PhysImpHCEAF: a human impacted physically.

• psychologicallyImpacted : CauseeAffectee

  PsychImpHCEAF: a human impacted psychologically.

• inanimate : CauseeAffectee

  InanCEAF: an inanimate affectee.

@[instance_reducible]

instance Hafeez2025.instDecidableEqCauseeAffectee : DecidableEq CauseeAffectee

Equations

• Hafeez2025.instDecidableEqCauseeAffectee x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Hafeez2025.instReprCauseeAffectee : Repr CauseeAffectee

Equations

• Hafeez2025.instReprCauseeAffectee = { reprPrec := Hafeez2025.instReprCauseeAffectee.repr }

def Hafeez2025.instReprCauseeAffectee.repr : CauseeAffectee → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Hafeez2025.instFintypeCauseeAffectee : Fintype CauseeAffectee

Equations

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

structure Hafeez2025.Scene : Type

A causal scene: its causer, its second participant, and whether a third participant mediates the chain.

• causer : Causer
• causeeAffectee : CauseeAffectee
• mediation : Causation.Morphological.Mediation

def Hafeez2025.instDecidableEqScene.decEq (x✝ x✝¹ : Scene) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Hafeez2025.instDecidableEqScene : DecidableEq Scene

Equations

• Hafeez2025.instDecidableEqScene = Hafeez2025.instDecidableEqScene.decEq

def Hafeez2025.instReprScene.repr : Scene → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Hafeez2025.instReprScene : Repr Scene

Equations

• Hafeez2025.instReprScene = { reprPrec := Hafeez2025.instReprScene.repr }

@[instance_reducible]

instance Hafeez2025.instFintypeScene : Fintype Scene

Equations

• Hafeez2025.instFintypeScene = Fintype.ofEquiv ((_ : Hafeez2025.Causer) × (_ : Hafeez2025.CauseeAffectee) × Causation.Morphological.Mediation) Hafeez2025.Scene.proxyTypeEquiv

def Hafeez2025.Scene.Stageable (s : Scene) : Prop

A scene the design can stage: a mediated chain's second participant is a human causee, never an inanimate affectee.

Equations

• s.Stageable = (s.mediation = Causation.Morphological.Mediation.indirect → s.causeeAffectee ≠ Hafeez2025.CauseeAffectee.inanimate)

@[instance_reducible]

instance Hafeez2025.instDecidablePredSceneStageable : DecidablePred Scene.Stageable

Equations

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

Predictors and scene types

def Hafeez2025.Scene.Is (s : Scene) : Predictor → Prop

The scenes a predictor is true of.

Equations

• s.Is Hafeez2025.Predictor.ihcr = (s.causer = Hafeez2025.Causer.intentionalHuman)
• s.Is Hafeez2025.Predictor.ahcr = (s.causer = Hafeez2025.Causer.accidentalHuman)
• s.Is Hafeez2025.Predictor.nfcr = (s.causer = Hafeez2025.Causer.naturalForce)
• s.Is Hafeez2025.Predictor.contrHCEAF = (s.causeeAffectee = Hafeez2025.CauseeAffectee.controlling)
• s.Is Hafeez2025.Predictor.physImpHCEAF = (s.causeeAffectee = Hafeez2025.CauseeAffectee.physicallyImpacted)
• s.Is Hafeez2025.Predictor.psychImpHCEAF = (s.causeeAffectee = Hafeez2025.CauseeAffectee.psychologicallyImpacted)
• s.Is Hafeez2025.Predictor.inanCEAF = (s.causeeAffectee = Hafeez2025.CauseeAffectee.inanimate)
• s.Is Hafeez2025.Predictor.mediation = (s.mediation = Causation.Morphological.Mediation.indirect)

@[instance_reducible]

instance Hafeez2025.instDecidablePredPredictorIs (s : Scene) : DecidablePred s.Is

Equations

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

def Hafeez2025.Scene.Has (s : Scene) : Predictor × Data.Experiments.Sign → Prop

The scenes a signed predictor, [+F] or [-F], is true of.

Equations

• s.Has (p, Data.Experiments.Sign.plus) = s.Is p
• s.Has (p, Data.Experiments.Sign.minus) = ¬s.Is p

@[instance_reducible]

instance Hafeez2025.instDecidablePredProdPredictorSignHas (s : Scene) : DecidablePred s.Has

Equations

• Hafeez2025.instDecidablePredProdPredictorSignHas s (p, Data.Experiments.Sign.plus) = Hafeez2025.instDecidablePredProdPredictorSignHas._aux_1 s p
• Hafeez2025.instDecidablePredProdPredictorSignHas s (p, Data.Experiments.Sign.minus) = { decide := !decide (s.Is p), reflects_decide := ⋯ }

def Hafeez2025.negate : Predictor × Data.Experiments.Sign → Predictor × Data.Experiments.Sign

The signed predictor with the opposite sign.

Equations

• Hafeez2025.negate (p, Data.Experiments.Sign.plus) = (p, Data.Experiments.Sign.minus)
• Hafeez2025.negate (p, Data.Experiments.Sign.minus) = (p, Data.Experiments.Sign.plus)

@[simp]

theorem Hafeez2025.Scene.has_negate (s : Scene) (l : Predictor × Data.Experiments.Sign) : s.Has (negate l) ↔ ¬s.Has l

def Hafeez2025.Scene.Fits (s : Scene) (t : List (Predictor × Data.Experiments.Sign)) : Prop

A scene falls under a scene type, a conjunction of signed predictors, when it has each.

Equations

• s.Fits t = ∀ l ∈ t, s.Has l

@[instance_reducible]

instance Hafeez2025.instDecidablePredListProdPredictorSignFits (s : Scene) : DecidablePred s.Fits

Equations

• Hafeez2025.instDecidablePredListProdPredictorSignFits s x✝ = List.decidableBAll s.Has x✝

@[simp]

theorem Hafeez2025.Scene.fits_nil (s : Scene) : s.Fits []

@[simp]

theorem Hafeez2025.Scene.fits_cons (s : Scene) (l : Predictor × Data.Experiments.Sign) (t : List (Predictor × Data.Experiments.Sign)) : s.Fits (l :: t) ↔ s.Has l ∧ s.Fits t

The clips

def Hafeez2025.Clip.scene (c : Clip) : Scene

A clip's scene, read off its name by the code of Appendix L: the first letter is the causer, the second the second participant, and a third letter O an inanimate affectee behind a mediating causee. The code's one exception is clip 22, whose M marks an umbrella.

Equations

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

theorem Hafeez2025.clips_stageable (c : Clip) : c ∈ clips → c.scene.Stageable

Every clip is a scene the design can stage.

theorem Hafeez2025.table4_disagreements : List.map (fun (x : Clip) => x.number) (List.filter (fun (c : Clip) => decide ¬∀ (p : Predictor), p ∈ c.present ↔ c.scene.Is p) clips) = [1, 11, 21, 22, 23]

The predictor table as printed (Table 4) disagrees with the clip names on five clips: it codes clips 11 and 21, where a pushed or bumped man knocks down a cup tower, with an inanimate second participant, the umbrella of clip 22 without one, and adds a human impact to the paper of clips 1 and 23.

Conditional inference trees

inductive Hafeez2025.Tree : Type

A binary conditional inference tree: an inner node tests a signed predictor, sending the scenes that pass it left.

• leaf : Tree
• node (test : Predictor × Data.Experiments.Sign) (pass fail : Tree) : Tree

def Hafeez2025.Tree.size : Tree → ℕ

The number of nodes.

Equations

• Hafeez2025.Tree.leaf.size = 1
• (Hafeez2025.Tree.node test p f).size = p.size + f.size + 1

def Hafeez2025.Tree.leaves : Tree → ℕ → List (ℕ × List (Predictor × Data.Experiments.Sign))

The leaves of a tree whose root is node n, numbered in preorder as the dissertation's tree plots number them, each with the scene type of its path.

Equations

• One or more equations did not get rendered due to their size.
• Hafeez2025.Tree.leaf.leaves x✝ = [(x✝, [])]

theorem Hafeez2025.Tree.countP_leaves (t : Tree) (n : ℕ) (s : Scene) : List.countP (fun (p : ℕ × List (Predictor × Data.Experiments.Sign)) => decide (s.Fits p.2)) (t.leaves n) = 1

The leaves of a tree partition the scenes: each scene falls under exactly one leaf.

def Hafeez2025.leafPath (l : Leaf) : List (Predictor × Data.Experiments.Sign)

The scene type of a leaf of Table 18, with the InanCEAF signs of the ADV tree as section 5.3.5 states them.

Equations

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

def Hafeez2025.leavesOf (r : ResponseType) : List Leaf

The leaves of a response type's tree in Table 18.

Equations

• Hafeez2025.leavesOf r = List.filter (fun (x : Hafeez2025.Leaf) => decide (x.responseType = r)) Hafeez2025.leaves

def Hafeez2025.tree : ResponseType → Option Tree

The tree of a response type of the acceptability study.

Equations

• One or more equations did not get rendered due to their size.
• Hafeez2025.tree x✝ = none

theorem Hafeez2025.tree_leaves (r : ResponseType) (t : Tree) (h : tree r = some t) : t.leaves 1 = List.map (fun (l : Leaf) => (l.node, leafPath l)) (leavesOf r)

The trees reproduce Table 18: their leaves, numbered in preorder, are the printed leaves.

theorem Hafeez2025.leaves_partition (r : ResponseType) (t : Tree) (h : tree r = some t) (s : Scene) : List.countP (fun (l : Leaf) => decide (s.Fits (leafPath l))) (leavesOf r) = 1

Each tree's leaves in Table 18 partition the scenes.

Response counts

def Hafeez2025.clipCount (t : List (Predictor × Data.Experiments.Sign)) : ℕ

The number of clips whose scene falls under a scene type.

Equations

• Hafeez2025.clipCount t = List.countP (fun (c : Hafeez2025.Clip) => decide (c.scene.Fits t)) Hafeez2025.clips

theorem Hafeez2025.responses_le (l : Leaf) : l ∈ leaves → l.responses ≤ raters * clipCount (leafPath l)

Under the clip names, no leaf holds more responses than the twelve raters give its clips.

theorem Hafeez2025.responses_shortfall : List.map (fun (l : Leaf) => (l.responseType, l.node)) (List.filter (fun (l : Leaf) => decide (l.responses ≠ raters * clipCount (leafPath l))) leaves) = [(ResponseType.lexInst, 8), (ResponseType.lexDat, 5), (ResponseType.ncrA, 7)]

Every leaf holds exactly the responses of its clips but three, which fall short.

theorem Hafeez2025.adv_printed_misfit (l : Leaf) : l ∈ leavesOf ResponseType.adv → l.responses ≠ raters * clipCount l.path

With the InanCEAF signs Table 18 prints, no ADV leaf holds the responses of its clips.

def Hafeez2025.table4Has (c : Clip) : Predictor × Data.Experiments.Sign → Prop

Whether Table 4 marks a clip with a signed predictor.

Equations

• Hafeez2025.table4Has c (p, Data.Experiments.Sign.plus) = (p ∈ c.present)
• Hafeez2025.table4Has c (p, Data.Experiments.Sign.minus) = (p ∉ c.present)

@[instance_reducible]

instance Hafeez2025.instDecidablePredProdPredictorSignTable4Has (c : Clip) : DecidablePred (table4Has c)

Equations

• Hafeez2025.instDecidablePredProdPredictorSignTable4Has c (p, Data.Experiments.Sign.plus) = { decide := decide (List.elem p c.present = true), reflects_decide := ⋯ }
• Hafeez2025.instDecidablePredProdPredictorSignTable4Has c (p, Data.Experiments.Sign.minus) = { decide := !decide (p ∈ c.present), reflects_decide := ⋯ }

theorem Hafeez2025.table4_exceeded : List.map (fun (l : Leaf) => (l.responseType, l.node)) (List.filter (fun (l : Leaf) => decide (raters * List.countP (fun (c : Clip) => decide (∀ q ∈ leafPath l, table4Has c q)) clips < l.responses)) leaves) = [(ResponseType.lexInst, 4), (ResponseType.adv, 5), (ResponseType.nca, 3)]

Under the coding of Table 4 as printed, three leaves hold more responses than the twelve raters could give their clips, so Table 4 is not the coding the trees were fit on.

theorem Hafeez2025.attainablePercent_iff (l : Leaf) : l ∈ leaves → (l.ceilingPercent.AttainablePercent l.responses ↔ ¬(l.responseType = ResponseType.lexInst ∧ l.node = 4))

Every printed percentage is some count of the leaf's responses, rounded, except the 0.08 of the LEX-INST tree, which no count out of 252 rounds to.

Prototypes

def Hafeez2025.peakLeaf (r : ResponseType) : Option Leaf

The leaf with the peak share of ceiling ratings.

Equations

• Hafeez2025.peakLeaf r = List.argmax (fun (x : Hafeez2025.Leaf) => x.ceilingPercent.toRat) (Hafeez2025.leavesOf r)

def Hafeez2025.prototype (r : ResponseType) : Option (List (Predictor × Data.Experiments.Sign))

The hypothesized semantic prototype: the scene type of the peak leaf, when its share of ceiling ratings exceeds 50%.

Equations

• Hafeez2025.prototype r = Option.map Hafeez2025.leafPath (Option.filter (fun (l : Hafeez2025.Leaf) => decide (50 < l.ceilingPercent.toRat)) (Hafeez2025.peakLeaf r))

def Hafeez2025.Prototypical (r : ResponseType) (s : Scene) : Prop

The scenes of the response type's prototype.

Equations

• Hafeez2025.Prototypical r s = ∃ t ∈ Hafeez2025.prototype r, s.Fits t

@[instance_reducible]

instance Hafeez2025.instDecidablePredScenePrototypical (r : ResponseType) : DecidablePred (Prototypical r)

Equations

• Hafeez2025.instDecidablePredScenePrototypical r s = decidable_of_iff (∃ t ∈ (Hafeez2025.prototype r).toList, s.Fits t) ⋯

theorem Hafeez2025.prototype_eq_none_iff (r : ResponseType) : prototype r = none ↔ r ∈ [ResponseType.lexNom, ResponseType.lexDat, ResponseType.acc, ResponseType.impCausRel]

LEX-DAT, whose peak is 41.7%, has no prototype; the response types the acceptability study did not test have none either.

theorem Hafeez2025.exists_clip_prototypical (r : ResponseType) (hr : prototype r ≠ none) : ∃ c ∈ clips, Prototypical r c.scene

Every prototype holds of a clip, so the statements about prototypical scenes below are not vacuous.

theorem Hafeez2025.summary_percent (row : SummaryRow) : row ∈ summary → row.responseType ≠ ResponseType.nca → row.responseType ≠ ResponseType.ncrA → some row.percent = Option.map (fun (x : Leaf) => x.ceilingPercent) (peakLeaf row.responseType)

Table 19 prints each response type's peak, except that it swaps those of NCA and NCrA.

theorem Hafeez2025.summary_percent_swapped (row : SummaryRow) : row ∈ summary → (row.responseType = ResponseType.nca → some row.percent = Option.map (fun (x : Leaf) => x.ceilingPercent) (peakLeaf ResponseType.ncrA)) ∧ (row.responseType = ResponseType.ncrA → some row.percent = Option.map (fun (x : Leaf) => x.ceilingPercent) (peakLeaf ResponseType.nca))

theorem Hafeez2025.summary_prototype_eq (row : SummaryRow) : row ∈ summary → ∃ c ∈ comparison, c.responseType = row.responseType ∧ c.prototype = row.prototype

Tables 19 and 25 print the same prototypes.

theorem Hafeez2025.summary_iff_prototype (row : ComparisonRow) : row ∈ comparison → row.responseType ≠ ResponseType.adv → ∀ (s : Scene), s.Stageable → ((∃ t ∈ row.prototype, s.Fits t) ↔ Prototypical row.responseType s)

The printed prototypes denote the derived ones on the scenes the design can stage, ADV's excepted.

theorem Hafeez2025.summary_iff_prototype_of_ne (row : ComparisonRow) : row ∈ comparison → row.responseType ≠ ResponseType.adv → row.responseType ≠ ResponseType.lexErg → ∀ (s : Scene), (∃ t ∈ row.prototype, s.Fits t) ↔ Prototypical row.responseType s

Apart from LEX-ERG's and ADV's, the printed prototypes denote the derived ones on every scene.

theorem Hafeez2025.lexErg_summary_not_prototype : ∃ (s : Scene), ¬s.Stageable ∧ s.Fits [(Predictor.ihcr, Data.Experiments.Sign.plus), (Predictor.inanCEAF, Data.Experiments.Sign.plus)] ∧ ¬Prototypical ResponseType.lexErg s

LEX-ERG's printed prototype [+IHCr, +InanCEAF] drops its leaf's [-Mediation]: it also holds of a mediated scene with an inanimate second participant, which the design never stages.

theorem Hafeez2025.adv_summary_iff_not_prototype (row : ComparisonRow) : row ∈ comparison → row.responseType = ResponseType.adv → ∀ (s : Scene), (∃ t ∈ row.prototype, s.Fits t) ↔ ¬Prototypical ResponseType.adv s

ADV's printed prototype [+InanCEAF] is the complement of the derived one.

Agentivity

inductive Hafeez2025.Degree : Type

The degrees of agentivity, from intentionality and control, the ability to initiate or terminate an action in [Boh04]'s sense: full for an intentional actor in control, marginal for an actor involved accidentally, without intention or control, and induced for a causee in control of an action it was induced to perform.

• full : Degree
• induced : Degree
• marginal : Degree

@[instance_reducible]

instance Hafeez2025.instDecidableEqDegree : DecidableEq Degree

Equations

• Hafeez2025.instDecidableEqDegree x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Hafeez2025.instReprDegree.repr : Degree → ℕ → Std.Format

Equations

• Hafeez2025.instReprDegree.repr Hafeez2025.Degree.full prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hafeez2025.Degree.full")).group prec✝
• Hafeez2025.instReprDegree.repr Hafeez2025.Degree.induced prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hafeez2025.Degree.induced")).group prec✝
• Hafeez2025.instReprDegree.repr Hafeez2025.Degree.marginal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hafeez2025.Degree.marginal")).group prec✝

@[instance_reducible]

instance Hafeez2025.instReprDegree : Repr Degree

Equations

• Hafeez2025.instReprDegree = { reprPrec := Hafeez2025.instReprDegree.repr }

def Hafeez2025.Causer.degree : Causer → Option Degree

A causer's agentivity; a natural force has none.

Equations

• Hafeez2025.Causer.intentionalHuman.degree = some Hafeez2025.Degree.full
• Hafeez2025.Causer.accidentalHuman.degree = some Hafeez2025.Degree.marginal
• Hafeez2025.Causer.naturalForce.degree = none

def Hafeez2025.CauseeAffectee.degree : CauseeAffectee → Option Degree

A second participant's agentivity; an inanimate affectee has none.

Equations

• Hafeez2025.CauseeAffectee.controlling.degree = some Hafeez2025.Degree.induced
• Hafeez2025.CauseeAffectee.physicallyImpacted.degree = some Hafeez2025.Degree.marginal
• Hafeez2025.CauseeAffectee.psychologicallyImpacted.degree = some Hafeez2025.Degree.marginal
• Hafeez2025.CauseeAffectee.inanimate.degree = none

theorem Hafeez2025.lexErg_full (s : Scene) : Prototypical ResponseType.lexErg s → s.causer.degree = some Degree.full

LEX-ERG expresses the highest degree of agentivity: an intentional causer.

theorem Hafeez2025.lexInst_marginal (s : Scene) : Prototypical ResponseType.lexInst s → s.causer.degree ≠ some Degree.full ∧ s.causeeAffectee.degree = none

LEX-INST expresses marginal agentivity or none.

theorem Hafeez2025.mcv_full_induced (s : Scene) : Prototypical ResponseType.mcv s → s.causer.degree = some Degree.full ∧ s.causeeAffectee.degree = some Degree.induced

MCV is causation by communication: an intentional causer and a causee in control.

theorem Hafeez2025.adv_agentive (s : Scene) : Prototypical ResponseType.adv s → s.causeeAffectee.degree ≠ none

ADV wants an agentive second participant, partially or marginally.

theorem Hafeez2025.nca_agentive (s : Scene) : Prototypical ResponseType.nca s → s.causer.degree ≠ none ∧ s.causeeAffectee.degree ≠ none

NCA wants an agentive causer, fully or marginally, and an agentive second participant, partially or marginally.

theorem Hafeez2025.ncrA_nonagentive (s : Scene) : Prototypical ResponseType.ncrA s → s.causer.degree = none ∧ s.causeeAffectee.degree ≠ none

NCrA wants a non-agentive causer and an agentive second participant.

Production

theorem Hafeez2025.individual_le_prototype (row : ComparisonRow) : row ∈ comparison → row.rated = Answer.yes → ∀ t ∈ row.individualPreferences, ∀ (s : Scene), s.Stageable → s.Fits t → Prototypical row.responseType s

The production study's preferences refine the acceptability prototypes: every stageable scene a rated response type's own model prefers it for is prototypical for it.

theorem Hafeez2025.nca_combined_not_le_prototype (row : ComparisonRow) : row ∈ comparison → row.responseType = ResponseType.nca → ∃ t ∈ row.combinedPreference, ∃ c ∈ clips, c.scene.Fits t ∧ ¬Prototypical ResponseType.nca c.scene

The model of all response types prefers NCA for a psychologically impacted second participant, and the clip of a woman startled by thunder is such a scene outside the NCA prototype.

Compactness and directness

theorem Hafeez2025.lexErg_mcv_mediation (s₁ s₂ : Scene) : Prototypical ResponseType.lexErg s₁ → Prototypical ResponseType.mcv s₂ → s₁.mediation < s₂.mediation

The LEX-ERG prototype is unmediated and the MCV prototype mediated.

theorem Hafeez2025.lexErg_mcv_comrieMonotone (s₁ s₂ : Scene) (h₁ : Prototypical ResponseType.lexErg s₁) (h₂ : Prototypical ResponseType.mcv s₂) : { complexity := Causation.Morphological.CausativeComplexity.lexical, mediation := s₁.mediation }.ComrieMonotone { complexity := Causation.Morphological.CausativeComplexity.morphological, mediation := s₂.mediation }

The lexical LEX-ERG and the morphological MCV, located by the mediation of their prototypes, satisfy [Com89]'s monotonicity strictly.