Déchaine & Wiltschko 2002: Decomposing Pronouns

[DW02]

"The notion 'pronoun' is not a primitive of linguistic theory." Pronouns decompose into three categories by internal constituent size — proDP ⊃ prophiP ⊃ proNP — and that size determines distribution, semantics, and binding-theoretic status ([DW02] table (24)):

category	internal syntax	distribution	semantics	binding
pro-DP	D; morph. complex	argument	definite	R-expression (Cond C)
pro-φP	neither D nor N	arg or pred	—	variable (Cond B)
pro-NP	N	predicate	constant	— (inherent semantics)

This categorial axis cross-cuts Cardinaletti & Starke's deficiency hierarchy (Pronoun.Strength, [CS99a]): see strength_category_independent. It is the structural rival to the deficiency view that Pronoun.Strength's docstring flags as orthogonal.

Main declarations

• Category — pro-DP / pro-φP / pro-NP, with hasDLayer/hasPhiLayer recording size.
• Category.bindingStatus — derived from size, not stipulated: D&W's claim that the D layer yields a Condition-C R-expression, a φP-top yields a Condition-B variable, and a bare NP is binding-unconstrained.
• strength_category_independent — the C&S Strength and D&W Category axes are functionally independent (neither determines the other), with English witnesses from [DW02] §3.2.

Implementation notes

The φP layer is the locus of the person/number/gender φ-features modelled in UD.Person etc.; hasPhiLayer marks which categories project it. A full federation of the φ-internal geometry to UD.Person is left to follow-up.

inductive DechaineWiltschko2002.Category : Type

[DW02]'s three pronoun categories, by internal constituent size: a full DP ([DP D [φP φ [NP N]]]), a φP ([φP φ [NP N]]), or a bare NP ([NP N]).

• proDP : Category
• prophiP : Category
• proNP : Category

@[implicit_reducible]

instance DechaineWiltschko2002.instDecidableEqCategory : DecidableEq Category

Equations

• DechaineWiltschko2002.instDecidableEqCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance DechaineWiltschko2002.instReprCategory : Repr Category

Equations

• DechaineWiltschko2002.instReprCategory = { reprPrec := DechaineWiltschko2002.instReprCategory.repr }

def DechaineWiltschko2002.instReprCategory.repr : Category → ℕ → Std.Format

Equations

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

def DechaineWiltschko2002.Category.hasDLayer : Category → Bool

Whether the category projects a D layer (definiteness / R-expression locus).

Equations

• DechaineWiltschko2002.Category.proDP.hasDLayer = true
• DechaineWiltschko2002.Category.prophiP.hasDLayer = false
• DechaineWiltschko2002.Category.proNP.hasDLayer = false

def DechaineWiltschko2002.Category.hasPhiLayer : Category → Bool

Whether the category projects a φP layer — the locus of the person/number/ gender φ-features (cf. UD.Person). A bare proNP has none.

Equations

• DechaineWiltschko2002.Category.proDP.hasPhiLayer = true
• DechaineWiltschko2002.Category.prophiP.hasPhiLayer = true
• DechaineWiltschko2002.Category.proNP.hasPhiLayer = false

inductive DechaineWiltschko2002.BindingStatus : Type

Binding-theoretic status ([DW02] table (24)).

• rExpression : BindingStatus

  Subject to Condition C (a referring expression).

• boundVariable : BindingStatus

  Subject to Condition B (can be a bound variable).

• unconstrained : BindingStatus

  Undefined for binding theory; behaviour follows from inherent semantics.

@[implicit_reducible]

instance DechaineWiltschko2002.instDecidableEqBindingStatus : DecidableEq BindingStatus

Equations

• DechaineWiltschko2002.instDecidableEqBindingStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance DechaineWiltschko2002.instReprBindingStatus : Repr BindingStatus

Equations

• DechaineWiltschko2002.instReprBindingStatus = { reprPrec := DechaineWiltschko2002.instReprBindingStatus.repr }

def DechaineWiltschko2002.instReprBindingStatus.repr : BindingStatus → ℕ → Std.Format

Equations

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

inductive DechaineWiltschko2002.Distribution : Type

External distribution ([DW02] (24)–(25)).

• argument : Distribution
• predicate : Distribution
• either : Distribution

@[implicit_reducible]

instance DechaineWiltschko2002.instDecidableEqDistribution : DecidableEq Distribution

Equations

• DechaineWiltschko2002.instDecidableEqDistribution x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def DechaineWiltschko2002.instReprDistribution.repr : Distribution → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DechaineWiltschko2002.instReprDistribution : Repr Distribution

Equations

• DechaineWiltschko2002.instReprDistribution = { reprPrec := DechaineWiltschko2002.instReprDistribution.repr }

inductive DechaineWiltschko2002.Sem : Type

Inherent semantics ([DW02] (24)).

• definite : Sem
• const : Sem
• underspecified : Sem

@[implicit_reducible]

instance DechaineWiltschko2002.instDecidableEqSem : DecidableEq Sem

Equations

• DechaineWiltschko2002.instDecidableEqSem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance DechaineWiltschko2002.instReprSem : Repr Sem

Equations

• DechaineWiltschko2002.instReprSem = { reprPrec := DechaineWiltschko2002.instReprSem.repr }

def DechaineWiltschko2002.instReprSem.repr : Sem → ℕ → Std.Format

Equations

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

def DechaineWiltschko2002.Category.bindingStatus (c : Category) : BindingStatus

D&W's central thesis: binding status is determined by size. A D layer makes the proform an R-expression (Condition C); a φP top (φ-features but no D) makes it a bound variable (Condition B); a bare NP is unconstrained by binding theory. Derived from hasDLayer/hasPhiLayer, not stipulated.

Equations

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

def DechaineWiltschko2002.Category.distribution : Category → Distribution

Distribution: DPs are arguments, NPs are predicates, φPs are type-flexible ([DW02] (25): DP → Argument, NP → Predicate).

Equations

• DechaineWiltschko2002.Category.proDP.distribution = DechaineWiltschko2002.Distribution.argument
• DechaineWiltschko2002.Category.prophiP.distribution = DechaineWiltschko2002.Distribution.either
• DechaineWiltschko2002.Category.proNP.distribution = DechaineWiltschko2002.Distribution.predicate

def DechaineWiltschko2002.Category.semantics : Category → Sem

Inherent semantics: definite (DP), constant (NP), or unspecified (φP).

Equations

• DechaineWiltschko2002.Category.proDP.semantics = DechaineWiltschko2002.Sem.definite
• DechaineWiltschko2002.Category.prophiP.semantics = DechaineWiltschko2002.Sem.underspecified
• DechaineWiltschko2002.Category.proNP.semantics = DechaineWiltschko2002.Sem.const

The size → binding-status entailment

theorem DechaineWiltschko2002.rExpression_iff_hasDLayer (c : Category) : c.bindingStatus = BindingStatus.rExpression ↔ c.hasDLayer = true

A proform is an R-expression (Condition C) iff it has a D layer.

theorem DechaineWiltschko2002.boundVariable_iff_phi_without_D (c : Category) : c.bindingStatus = BindingStatus.boundVariable ↔ c.hasPhiLayer = true ∧ c.hasDLayer = false

A proform is a bound variable (Condition B) iff it has φ-features but no D.

theorem DechaineWiltschko2002.binding_statuses_distinct : Category.proDP.bindingStatus ≠ Category.prophiP.bindingStatus ∧ Category.prophiP.bindingStatus ≠ Category.proNP.bindingStatus ∧ Category.proDP.bindingStatus ≠ Category.proNP.bindingStatus

The three categories yield three distinct binding statuses — the typology is non-degenerate.

Case studies ([DW02] table (24))

Each language's independent/personal proform instantiates a different category: Halkomelem independent pronouns = pro-DP (R-expressions, Condition C); Shuswap independent pronouns = pro-φP (bound variables, Condition B); Japanese kare = pro-NP (a constant, binding-unconstrained).

theorem DechaineWiltschko2002.halkomelem_proDP_rExpression : Category.proDP.bindingStatus = BindingStatus.rExpression

theorem DechaineWiltschko2002.shuswap_prophiP_boundVariable : Category.prophiP.bindingStatus = BindingStatus.boundVariable

theorem DechaineWiltschko2002.japanese_kare_proNP_unconstrained : Category.proNP.bindingStatus = BindingStatus.unconstrained

Orthogonality to Cardinaletti & Starke deficiency

[DW02] §3.2 analyses English personal pronouns as pro-DP (1st/2nd person — they can be determiners: we/us linguists) and pro-φP (3rd person — *they linguists), and one as pro-NP. Cross-classifying those categories with [CS99a] deficiency (Pronoun.Strength: full we/they are strong, enclitic 'em is a clitic) shows the two axes are independent — neither determines the other.

structure DechaineWiltschko2002.Datum : Type

A pronoun cross-classified on both axes: D&W Category × C&S Strength.

• form : String
• strength : Pronoun.Strength
• category : Category

def DechaineWiltschko2002.instReprDatum.repr : Datum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DechaineWiltschko2002.instReprDatum : Repr Datum

Equations

• DechaineWiltschko2002.instReprDatum = { reprPrec := DechaineWiltschko2002.instReprDatum.repr }

def DechaineWiltschko2002.englishInventory : List Datum

English inventory ([DW02] §3), each form tagged with its D&W category and its C&S strength.

Equations

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

theorem DechaineWiltschko2002.category_not_determined_by_strength : ∃ (p : Datum) (q : Datum), p.strength = q.strength ∧ p.category ≠ q.category

Strength does not determine Category: we and they are both strong, yet we is pro-DP (1st person) and they is pro-φP (3rd person).

theorem DechaineWiltschko2002.strength_not_determined_by_category : ∃ (p : Datum) (q : Datum), p.category = q.category ∧ p.strength ≠ q.strength

Category does not determine Strength: they and 'em are both pro-φP (3rd person), yet they is strong and 'em is a clitic.

theorem DechaineWiltschko2002.strength_category_independent : (∃ (p : Datum) (q : Datum), p.strength = q.strength ∧ p.category ≠ q.category) ∧ ∃ (p : Datum) (q : Datum), p.category = q.category ∧ p.strength ≠ q.strength

The Déchaine-Wiltschko categorial axis and the Cardinaletti-Starke deficiency axis are functionally independent — neither is a function of the other. This is the theorem behind Pronoun.Strength's docstring claim of orthogonality.