Minimal Pronoun Theory

[Kra98a] [Kra09b] [Saf14] [Lan15]

All instances of bound variable anaphora — reflexives, PRO, bound variable pronouns — are syntactically identical: bare D heads with unvalued φ-features ("minimal pronouns"). Cross-linguistic variation in their surface form (null, reflexive, pronoun) reduces entirely to variation in vocabulary items, language-specific contextual allomorphs applied postsyntactically.

Definition (28) of [Lan15]: X is a minimal pronoun iff X = [D,uφ]. Within different derivations, X can become a reflexive, a bound lexical pronoun, a resumptive pronoun, a pro element, a relative pronoun, or controlled PRO. The choice is determined by the syntactic context and the language's vocabulary item inventory.

Key Definitions

• BVAContext: The four licensing contexts for bound variable anaphora
• MinPronInventory: A language's Vocabulary Items (D[uφ] → Form / context) + elsewhere default
• PronForm: Standard surface form categories (null, pronoun, reflexive)

Core Claims

1. Minimal pronouns are D heads with unvalued φ-features (28)
2. φ-values are transmitted from the antecedent (via Agree or variable binding)
3. Vocabulary items map valued feature bundles to surface forms, conditioned by syntactic context (locally bound, controlled subject, etc.)
4. The Elsewhere Condition (DM; Halle & Marantz 1993): if no context-specific item matches, the default (pronoun) applies
5. Cross-linguistic variation in anaphoric form is morphological, not syntactic ([Saf14]: "all anaphoric diversity is morphological"). The DM vocabulary-item implementation used here follows [Lan15] and [Ost26]; Safir's own mechanism is morphological shape conditions at Spell-Out, not Vocabulary Insertion per se.

Landau-specific theory (the Two-Tiered Theory of Control, predicate classification, clause classes) is in Studies/Landau2015.lean.

Licensing Contexts

inductive Minimalist.MinimalPronoun.BVAContext : Type

The four syntactic contexts in which a minimal pronoun can occur. Each context may trigger a different vocabulary item (surface form).

These correspond to the traditional binding domains:

• controlledSubject: PRO position (subject of controlled clause)
• locallyBound: Condition A domain (reflexives)
• boundVariable: Condition B domain (bound pronoun, non-local)
• free: Condition C / referential (unbound)

• controlledSubject : BVAContext

  Subject of a controlled clause — PRO in English

• locallyBound : BVAContext

  Locally bound — reflexive in English (Condition A domain)

• boundVariable : BVAContext

  Bound by a non-local c-commanding antecedent

• free : BVAContext

  Free / referential (unbound)

@[instance_reducible]

instance Minimalist.MinimalPronoun.instDecidableEqBVAContext : DecidableEq BVAContext

Equations

• Minimalist.MinimalPronoun.instDecidableEqBVAContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.MinimalPronoun.instReprBVAContext : Repr BVAContext

Equations

• Minimalist.MinimalPronoun.instReprBVAContext = { reprPrec := Minimalist.MinimalPronoun.instReprBVAContext.repr }

def Minimalist.MinimalPronoun.instReprBVAContext.repr : BVAContext → ℕ → Std.Format

Equations

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

Vocabulary Items and the Elsewhere Condition

structure Minimalist.MinimalPronoun.MinPronInventory (Form : Type) : Type

A language's inventory of Vocabulary Items for minimal pronouns: each item realizes D[uφ] as a form in one BVAContext — D[uφ] → form / context — and the elsewhere form applies when no item matches.

[Saf14]: "from this single element, all anaphoric diversity is morphological"

• items : List (DistributedMorphology.VocabularyItem BVAContext Form)

  Context-specific Vocabulary Items.

• elsewhere : Form

  Default exponence: applies when no specific item matches. Crosslinguistically, this is the pronoun form ([Saf14]).

def Minimalist.MinimalPronoun.MinPronInventory.realize {Form : Type} (inv : MinPronInventory Form) (ctx : BVAContext) : Form

The Elsewhere Condition: the Subset Principle over the items at the context, falling back to the elsewhere (default pronoun) form.

Equations

• inv.realize ctx = (DistributedMorphology.subsetPrinciple inv.items (DistributedMorphology.Neighborhood.ofBundle [ctx])).getD inv.elsewhere

def Minimalist.MinimalPronoun.MinPronInventory.controlForm {Form : Type} (inv : MinPronInventory Form) : Form

A language's realized form for controlled subjects specifically. This is the function that distinguishes null-PRO from overt-PRO languages.

Equations

• inv.controlForm = inv.realize Minimalist.MinimalPronoun.BVAContext.controlledSubject

Standard Surface Forms

inductive Minimalist.MinimalPronoun.PronForm : Type

Standard surface form categories for bound variable anaphora.

These are the cross-linguistically attested exponence options for minimal pronouns. Each vocabulary item maps a BVA context to one of these forms.

• null : PronForm

  Silent (null PRO)

• pronoun : PronForm

  Overt pronoun (φ-matching clitic or full form)

• reflexive : PronForm

  Reflexive anaphor (English -self, SMPM mí + pronoun)

@[instance_reducible]

instance Minimalist.MinimalPronoun.instDecidableEqPronForm : DecidableEq PronForm

Equations

• Minimalist.MinimalPronoun.instDecidableEqPronForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Minimalist.MinimalPronoun.instReprPronForm : Repr PronForm

Equations

• Minimalist.MinimalPronoun.instReprPronForm = { reprPrec := Minimalist.MinimalPronoun.instReprPronForm.repr }

def Minimalist.MinimalPronoun.instReprPronForm.repr : PronForm → ℕ → Std.Format

Equations

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

def Minimalist.MinimalPronoun.MinPronInventory.hasOvertPRO (inv : MinPronInventory PronForm) : Prop

Whether a language's minimal-pronoun inventory realizes the controlled-subject context with an overt form. The criterion is non-nullness, not specifically .pronoun: [Ost26]'s universal is about overt-vs-null PRO, so an inventory whose controlled-subject form is .reflexive also counts as overt PRO.

Equations

• inv.hasOvertPRO = (inv.controlForm ≠ Minimalist.MinimalPronoun.PronForm.null)

@[instance_reducible]

instance Minimalist.MinimalPronoun.instDecidableHasOvertPRO (inv : MinPronInventory PronForm) : Decidable inv.hasOvertPRO

Equations

• Minimalist.MinimalPronoun.instDecidableHasOvertPRO inv = Minimalist.MinimalPronoun.instDecidableHasOvertPRO._aux_1 inv

The overt-PRO / pro-drop universal

def Minimalist.MinimalPronoun.MinPronInventory.OvertPROUniversal (inv : MinPronInventory PronForm) (proDrop : Bool) : Prop

[Ost26]'s implicational universal, for a language with minimal-pronoun inventory inv and matrix pro-drop observable proDrop: overt PRO entails no pro-drop. An empirical universal, so each language's study proves its own instance.

Equations

• inv.OvertPROUniversal proDrop = (inv.hasOvertPRO → proDrop = false)

theorem Minimalist.MinimalPronoun.MinPronInventory.overtPROUniversal_of_controlForm_eq_null {inv : MinPronInventory PronForm} (h : inv.controlForm = PronForm.null) (proDrop : Bool) : inv.OvertPROUniversal proDrop

A null-PRO inventory satisfies the universal vacuously.

theorem Minimalist.MinimalPronoun.MinPronInventory.overtPROUniversal_of_not_proDrop (inv : MinPronInventory PronForm) : inv.OvertPROUniversal false

A non-pro-drop language satisfies the universal trivially.

theorem Minimalist.MinimalPronoun.MinPronInventory.controlForm_eq_null_of_overtPROUniversal {inv : MinPronInventory PronForm} (h : inv.OvertPROUniversal true) : inv.controlForm = PronForm.null

The universal's bite: a pro-drop language must realize controlled subjects as null.

Cross-Linguistic BVA Syncretism

structure Minimalist.MinimalPronoun.BVASyncretism : Type

Cross-linguistic syncretism among BVA forms: whether each BVA context uses the same form as the referential (free) pronoun. Used by [Ost26]'s syncretism typology and grounded in the minimal pronoun approach of [Kra09b] and [Saf14].

• language : String
• reflexiveEqReferential : Bool

  Is the reflexive form identical to the referential pronoun?

• controlledEqReferential : Bool

  Is the controlled subject form identical to the referential pronoun?

• boundVarEqReferential : Bool

  Is the bound variable pronoun identical to the referential pronoun?

@[instance_reducible]

instance Minimalist.MinimalPronoun.instDecidableEqBVASyncretism : DecidableEq BVASyncretism

Equations

• Minimalist.MinimalPronoun.instDecidableEqBVASyncretism = Minimalist.MinimalPronoun.instDecidableEqBVASyncretism.decEq

def Minimalist.MinimalPronoun.instDecidableEqBVASyncretism.decEq (x✝ x✝¹ : BVASyncretism) : Decidable (x✝ = x✝¹)

Equations

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

def Minimalist.MinimalPronoun.instReprBVASyncretism.repr : BVASyncretism → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Minimalist.MinimalPronoun.instReprBVASyncretism : Repr BVASyncretism

Equations

• Minimalist.MinimalPronoun.instReprBVASyncretism = { reprPrec := Minimalist.MinimalPronoun.instReprBVASyncretism.repr }

def Minimalist.MinimalPronoun.syncretismFromInventory {Form : Type} [BEq Form] (inv : MinPronInventory Form) (lang : String := "") : BVASyncretism

Derive syncretism from a vocabulary item inventory: a context is syncretic with the referential pronoun iff its realized form equals the elsewhere (pronoun) form — no context-specific vocabulary item overrides the default.

Equations

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