Urdu Causative Construction System

@cite{hafeez-2025}

Urdu distinguishes at least 7 causative constructions tested in @cite{hafeez-2025}'s acceptability rating study. Each construction is sensitive to three semantic variables: causer type (IHCr/AHCr/NFCr), causee/affectee type (ContrHCEAF/PhysImpHCEAF/PsychImpHCEAF/InanCEAF), and mediation (direct/indirect).

The 7 Constructions (Acceptability Study, Ch. 5)

#	Construction	Abbrev	Complexity	Description
1	Lexical Ergative	LEX-ERG	lexical	Ergative case on causer NP (perfective)
2	Lexical Instrumental	LEX-INST	lexical	Instrumental case on causer NP
3	Lexical Dative	LEX-DAT	lexical	Dative case on highest-ranked NP
4	Morphological Causative Verb	MCV	morphological	-aa suffix, always mediated
5	Adverbial Causative	ADV	periphrastic	keyoonkeh 'because', itni...keh
6	Non-sentential Cause Adjunct	NCA	periphrastic	wajah=se 'because of'
7	Non-sentential Causer Adjunct	NCrA	periphrastic	Causer NP as adjunct

Semantic Prototypes (Table 25)

@cite{hafeez-2025} identifies hypothesized semantic prototypes for 5 of the 7 constructions via acceptability rating peaks (>50% ceiling). Prototypes use both positive ([+F]) and negative ([-F]) features:

• LEX-ERG: [+IHCr, +InanCEAF] — prototypical direct causation
• LEX-INST: [-IHCr, +InanCEAF] — accidental causer acting on object
• MCV: [+Mediation, +IHCr, +ContrHCEAF] — causation by command
• NCrA: [-InanCEAF, +NFCr] — natural force causer with human affectee
• NCA: [-InanCEAF, -NFCr] — human causer, human affectee
• ADV: [+InanCEAF] — broad acceptability, weaker prototype
• LEX-DAT: No prototype (default case, high acceptability across the board)

Discourse Production (Ch. 6)

The discourse production study confirms key patterns:

• LEX-ERG preferred for [+InanCEAF, +IHCr] (53.7% production rate)
• NCrA used exclusively with natural force causers (categorical)
• IMP-CAUS-REL preferred for [+ContrHCEAF, +IHCr] (communication scenes)

Bridges

• Each construction is typed as CausativeConstruction from Theories/Semantics/Causation/MorphologicalCausation.lean
• prototype field encodes Table 25 semantic prototypes using presentCausers/absentCausers/presentCausees/absentCausees
• Per-datum verification theorems check complexity, mediation, and restriction properties
• Key empirical generalizations are encoded as theorems

structure Fragments.Urdu.CausativeSystem.ConstructionEntry : Type

A construction entry bundles a CausativeConstruction with its empirically derived semantic prototype.

• construction : Semantics.Causation.MorphologicalCausation.CausativeConstruction
• prototype : Semantics.Causation.MorphologicalCausation.SemanticPrototype

instance Fragments.Urdu.CausativeSystem.instDecidableEqConstructionEntry : DecidableEq ConstructionEntry

Equations

• Fragments.Urdu.CausativeSystem.instDecidableEqConstructionEntry = Fragments.Urdu.CausativeSystem.instDecidableEqConstructionEntry.decEq

def Fragments.Urdu.CausativeSystem.instDecidableEqConstructionEntry.decEq (x✝ x✝¹ : ConstructionEntry) : Decidable (x✝ = x✝¹)

Equations

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

instance Fragments.Urdu.CausativeSystem.instBEqConstructionEntry : BEq ConstructionEntry

Equations

• Fragments.Urdu.CausativeSystem.instBEqConstructionEntry = { beq := Fragments.Urdu.CausativeSystem.instBEqConstructionEntry.beq }

def Fragments.Urdu.CausativeSystem.instBEqConstructionEntry.beq : ConstructionEntry → ConstructionEntry → Bool

Equations

• Fragments.Urdu.CausativeSystem.instBEqConstructionEntry.beq { construction := a, prototype := a_1 } { construction := b, prototype := b_1 } = (a == b && a_1 == b_1)
• Fragments.Urdu.CausativeSystem.instBEqConstructionEntry.beq x✝¹ x✝ = false

instance Fragments.Urdu.CausativeSystem.instReprConstructionEntry : Repr ConstructionEntry

Equations

• Fragments.Urdu.CausativeSystem.instReprConstructionEntry = { reprPrec := Fragments.Urdu.CausativeSystem.instReprConstructionEntry.repr }

def Fragments.Urdu.CausativeSystem.instReprConstructionEntry.repr : ConstructionEntry → ℕ → Std.Format

Equations

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

def Fragments.Urdu.CausativeSystem.lexErg : ConstructionEntry

Lexical Ergative (LEX-ERG): transitive/causative verb with ergative case on the causer NP in perfective aspect. Prototype: [+IHCr, +InanCEAF] — prototypical direct causation. This is Hopper & Thompson's (1980) prototypical transitive clause.

Equations

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

def Fragments.Urdu.CausativeSystem.lexInst : ConstructionEntry

Lexical Instrumental (LEX-INST): intransitive verb with instrumental case on the causer NP. The causer appears as an adjunct rather than a core argument. Prototype: [-IHCr, +InanCEAF] — non-intentional causer acting on inanimate affectee.

Equations

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

def Fragments.Urdu.CausativeSystem.lexDat : ConstructionEntry

Lexical Dative (LEX-DAT): causative verb with dative case on the highest-ranked NP. No semantic prototype identified — high acceptability across all scene types. @cite{hafeez-2025} suggests this may be a default case in Urdu, consistent with Van Valin (2018).

Equations

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

def Fragments.Urdu.CausativeSystem.mcv : ConstructionEntry

Morphological Causative Verb (MCV): productive -aa suffix. Always involves mediation — the causer instructs a causee who performs the action. Prototype: [+Mediation, +IHCr, +ContrHCEAF] — causation by command/communication.

Equations

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

def Fragments.Urdu.CausativeSystem.adv : ConstructionEntry

Adverbial Causative (ADV): two clauses connected by keyoonkeh 'because' or itni...keh 'so...that'. Prototype: [+InanCEAF] — weak prototype, broad acceptability.

Equations

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

def Fragments.Urdu.CausativeSystem.nca : ConstructionEntry

Non-sentential Cause Adjunct (NCA): phrasal cause adjunct marked with wajah=se 'because of', par/pe 'on', or =se INST. Matrix clause expresses the result; adjunct expresses the cause. Prototype: [-InanCEAF, -NFCr] — human causer with human affectee.

Equations

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

def Fragments.Urdu.CausativeSystem.ncrA : ConstructionEntry

Non-sentential Causer Adjunct (NCrA): causer NP as adjunct phrase in a matrix clause predicting the result. Categorically restricted to natural force causers in @cite{hafeez-2025}'s data — human causers never trigger NCrA. Prototype: [-InanCEAF, +NFCr] — natural force causer with human affectee.

Equations

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

def Fragments.Urdu.CausativeSystem.system : List ConstructionEntry

The acceptability study system as a list, from most compact to most analytic.

Equations

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

theorem Fragments.Urdu.CausativeSystem.lexErg_lexical : lexErg.construction.complexity = Semantics.Causation.MorphologicalCausation.CausativeComplexity.lexical

theorem Fragments.Urdu.CausativeSystem.lexInst_lexical : lexInst.construction.complexity = Semantics.Causation.MorphologicalCausation.CausativeComplexity.lexical

theorem Fragments.Urdu.CausativeSystem.lexDat_lexical : lexDat.construction.complexity = Semantics.Causation.MorphologicalCausation.CausativeComplexity.lexical

theorem Fragments.Urdu.CausativeSystem.mcv_morphological : mcv.construction.complexity = Semantics.Causation.MorphologicalCausation.CausativeComplexity.morphological

theorem Fragments.Urdu.CausativeSystem.adv_periphrastic : adv.construction.complexity = Semantics.Causation.MorphologicalCausation.CausativeComplexity.periphrastic

theorem Fragments.Urdu.CausativeSystem.nca_periphrastic : nca.construction.complexity = Semantics.Causation.MorphologicalCausation.CausativeComplexity.periphrastic

theorem Fragments.Urdu.CausativeSystem.ncrA_periphrastic : ncrA.construction.complexity = Semantics.Causation.MorphologicalCausation.CausativeComplexity.periphrastic

theorem Fragments.Urdu.CausativeSystem.mcv_indirect : mcv.construction.mediation = Semantics.Causation.MorphologicalCausation.Mediation.indirect

MCV always involves mediation (causer → causee → result).

theorem Fragments.Urdu.CausativeSystem.lexErg_direct : lexErg.construction.mediation = Semantics.Causation.MorphologicalCausation.Mediation.direct

Lexical constructions encode direct causation.

theorem Fragments.Urdu.CausativeSystem.lexInst_direct : lexInst.construction.mediation = Semantics.Causation.MorphologicalCausation.Mediation.direct

theorem Fragments.Urdu.CausativeSystem.lexDat_direct : lexDat.construction.mediation = Semantics.Causation.MorphologicalCausation.Mediation.direct

theorem Fragments.Urdu.CausativeSystem.lexErg_prototype_ihcr : lexErg.prototype.presentCausers = [Semantics.Causation.MorphologicalCausation.CauserType.intentionalHuman]

LEX-ERG prototype: [+IHCr].

theorem Fragments.Urdu.CausativeSystem.lexErg_prototype_inan : lexErg.prototype.presentCausees = [Semantics.Causation.MorphologicalCausation.CauseeAffecteeType.inanimate]

LEX-ERG prototype: [+InanCEAF].

theorem Fragments.Urdu.CausativeSystem.lexInst_prototype_no_ihcr : lexInst.prototype.absentCausers = [Semantics.Causation.MorphologicalCausation.CauserType.intentionalHuman]

LEX-INST prototype: [-IHCr] — excludes intentional causers.

theorem Fragments.Urdu.CausativeSystem.lexInst_prototype_inan : lexInst.prototype.presentCausees = [Semantics.Causation.MorphologicalCausation.CauseeAffecteeType.inanimate]

LEX-INST prototype: [+InanCEAF].

theorem Fragments.Urdu.CausativeSystem.mcv_prototype_mediation : mcv.prototype.requiresMediation = some true

MCV prototype requires mediation.

theorem Fragments.Urdu.CausativeSystem.mcv_prototype_command : mcv.prototype.presentCausers = [Semantics.Causation.MorphologicalCausation.CauserType.intentionalHuman] ∧ mcv.prototype.presentCausees = [Semantics.Causation.MorphologicalCausation.CauseeAffecteeType.controllingHuman]

MCV prototype: [+IHCr, +ContrHCEAF].

theorem Fragments.Urdu.CausativeSystem.ncrA_prototype_nfcr : ncrA.prototype.presentCausers = [Semantics.Causation.MorphologicalCausation.CauserType.naturalForce]

NCrA prototype: [+NFCr].

theorem Fragments.Urdu.CausativeSystem.ncrA_prototype_no_inan : ncrA.prototype.absentCausees = [Semantics.Causation.MorphologicalCausation.CauseeAffecteeType.inanimate]

NCrA prototype: [-InanCEAF] — requires human affectee.

theorem Fragments.Urdu.CausativeSystem.nca_prototype_human : nca.prototype.absentCausers = [Semantics.Causation.MorphologicalCausation.CauserType.naturalForce] ∧ nca.prototype.absentCausees = [Semantics.Causation.MorphologicalCausation.CauseeAffecteeType.inanimate]

NCA prototype: [-NFCr, -InanCEAF] — human causer, human affectee.

theorem Fragments.Urdu.CausativeSystem.adv_prototype_inan : adv.prototype.presentCausees = [Semantics.Causation.MorphologicalCausation.CauseeAffecteeType.inanimate]

ADV prototype: [+InanCEAF] (weak).

theorem Fragments.Urdu.CausativeSystem.lexDat_no_prototype : lexDat.prototype.presentCausers = [] ∧ lexDat.prototype.absentCausers = [] ∧ lexDat.prototype.presentCausees = [] ∧ lexDat.prototype.absentCausees = [] ∧ lexDat.prototype.requiresMediation = none

LEX-DAT has no prototype features (default case).

theorem Fragments.Urdu.CausativeSystem.ncrA_requires_natural_force : ncrA.construction.causerRestriction = some Semantics.Causation.MorphologicalCausation.CauserType.naturalForce

NCrA categorical restriction: NCrA is restricted to natural force causers. No human causer (intentional or accidental) triggers NCrA in @cite{hafeez-2025}'s data.

theorem Fragments.Urdu.CausativeSystem.mcv_always_mediated : mcv.construction.mediation = Semantics.Causation.MorphologicalCausation.Mediation.indirect

MCV encodes indirect causation: The morphological causative verb (-aa suffix) always involves an intermediary causee.

theorem Fragments.Urdu.CausativeSystem.all_lexical_compact : lexErg.construction.complexity = Semantics.Causation.MorphologicalCausation.CausativeComplexity.lexical ∧ lexInst.construction.complexity = Semantics.Causation.MorphologicalCausation.CausativeComplexity.lexical ∧ lexDat.construction.complexity = Semantics.Causation.MorphologicalCausation.CausativeComplexity.lexical

Lexical constructions are compact: All three lexical constructions (ERG, INST, DAT) are at the lexical complexity level.

theorem Fragments.Urdu.CausativeSystem.mcv_between : mcv.construction.complexity = Semantics.Causation.MorphologicalCausation.CausativeComplexity.morphological ∧ lexErg.construction.complexity < mcv.construction.complexity ∧ mcv.construction.complexity < adv.construction.complexity

MCV sits between lexical and periphrastic: Morphological complexity is strictly between the two.

theorem Fragments.Urdu.CausativeSystem.comrie_lexErg_mcv : Semantics.Causation.MorphologicalCausation.comrie_monotone lexErg.construction mcv.construction

Lexical (compact, direct) vs. MCV (morphological, indirect): Comrie's monotonicity holds.

theorem Fragments.Urdu.CausativeSystem.comrie_lexErg_adv : Semantics.Causation.MorphologicalCausation.comrie_monotone lexErg.construction adv.construction

Lexical (compact, direct) vs. periphrastic ADV: Comrie's monotonicity holds trivially (LEX-ERG is direct).

theorem Fragments.Urdu.CausativeSystem.system_size : system.length = 7

The system has exactly 7 constructions.

theorem Fragments.Urdu.CausativeSystem.system_has_all_complexities : List.elem Semantics.Causation.MorphologicalCausation.CausativeComplexity.lexical (List.map (fun (x : ConstructionEntry) => x.construction.complexity) system) = true ∧ List.elem Semantics.Causation.MorphologicalCausation.CausativeComplexity.morphological (List.map (fun (x : ConstructionEntry) => x.construction.complexity) system) = true ∧ List.elem Semantics.Causation.MorphologicalCausation.CausativeComplexity.periphrastic (List.map (fun (x : ConstructionEntry) => x.construction.complexity) system) = true

The system spans all three complexity levels.

theorem Fragments.Urdu.CausativeSystem.system_has_both_mediations : List.elem Semantics.Causation.MorphologicalCausation.Mediation.direct (List.map (fun (x : ConstructionEntry) => x.construction.mediation) system) = true ∧ List.elem Semantics.Causation.MorphologicalCausation.Mediation.indirect (List.map (fun (x : ConstructionEntry) => x.construction.mediation) system) = true

The system has both direct and indirect constructions.

theorem Fragments.Urdu.CausativeSystem.full_agentivity_drives_lexErg : Semantics.Causation.MorphologicalCausation.CauserType.intentionalHuman.agentivityDegree = Semantics.Causation.MorphologicalCausation.AgentivityDegree.full ∧ lexErg.prototype.presentCausers = [Semantics.Causation.MorphologicalCausation.CauserType.intentionalHuman]

Full agentivity (IHCr) drives LEX-ERG selection: the prototype requires an intentional causer.

theorem Fragments.Urdu.CausativeSystem.nonagentive_drives_ncrA : Semantics.Causation.MorphologicalCausation.CauserType.naturalForce.agentivityDegree = Semantics.Causation.MorphologicalCausation.AgentivityDegree.marginal ∧ ncrA.construction.causerRestriction = some Semantics.Causation.MorphologicalCausation.CauserType.naturalForce

Non-agentive causer (NFCr) drives NCrA selection: NCrA is categorically restricted to natural force.

theorem Fragments.Urdu.CausativeSystem.induced_agentivity_drives_mcv : Semantics.Causation.MorphologicalCausation.CauseeAffecteeType.controllingHuman.hasInducedAgentivity = true ∧ mcv.prototype.presentCausees = [Semantics.Causation.MorphologicalCausation.CauseeAffecteeType.controllingHuman]

Induced agentivity (ContrHCEAF) drives MCV: the controlling causee has partial agentivity.