Minimal Pronoun Theory

@cite{kratzer-1998} @cite{kratzer-2009} @cite{safir-2014} @cite{landau-2015}

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 @cite{landau-2015}: 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
• VocabItem: A context-sensitive realization rule (D[uφ] → Form / context)
• MinPronInventory: A language's vocabulary item inventory + elsewhere default
• PronForm: Standard surface form categories (null, pronoun, reflexive)
• OCSignature: @cite{landau-2013}'s Obligatory Control diagnostic package

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 (@cite{safir-2014}: "all anaphoric diversity is morphological"). The DM vocabulary-item implementation used here follows @cite{landau-2015} and @cite{ostrove-2026}; 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 Phenomena/Control/Studies/Landau2015.lean.

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)

@[implicit_reducible]

instance Minimalist.MinimalPronoun.instDecidableEqBVAContext : DecidableEq BVAContext

Equations

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

@[implicit_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.

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

A vocabulary item: a context-specific realization rule for a minimal pronoun.

In DM terms: D[uφ] → form / context ...

Vocabulary items are ordered by specificity. When multiple items could apply, the most specific (first in the list) wins.

This is a specialization of the general DM Morphology.DM.VI.VocabItem in Theories/Morphology/DM/VocabularyInsertion.lean, restricted to BVAContext matching with a parameterized Form type.

• context : BVAContext

  The syntactic context this item is restricted to

• form : Form

  The surface form this item realizes

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

A language's inventory of vocabulary items for minimal pronouns.

The items list is ordered by specificity (most specific first). The elsewhere form applies when no context-specific item matches.

@cite{safir-2014}: "from this single element, all anaphoric diversity is morphological"

• items : List (VocabItem Form)

  Context-specific vocabulary items, ordered by specificity

• elsewhere : Form

  Default exponence: applies when no specific item matches. Crosslinguistically, this is the pronoun form (@cite{safir-2014}).

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

The Elsewhere Condition: find the first vocabulary item whose context matches; if none does, use the elsewhere (default pronoun) form.

Equations

• inv.realize ctx = match List.find? (fun (x : Minimalist.MinimalPronoun.VocabItem Form) => x.context == ctx) inv.items with | some item => item.form | none => 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

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)

@[implicit_reducible]

instance Minimalist.MinimalPronoun.instDecidableEqPronForm : DecidableEq PronForm

Equations

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

@[implicit_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. This is the Minimalism-side bridge to Phenomena.NullSubject.ProDropProfile.hasOvertPRO. The typological criterion is non-nullness, not specifically .pronoun: @cite{ostrove-2026}'s universal is about overt-vs-null PRO, so an inventory whose controlled-subject form is .reflexive would also count as overt PRO.

Equations

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

@[implicit_reducible]

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

Equations

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

def Minimalist.MinimalPronoun.PronForm.toExponent : PronForm → Phenomena.NullSubject.Exponent

Project a PronForm to the framework-agnostic Exponent (null vs overt). Both .pronoun and .reflexive count as overt — the typological criterion in Phenomena.NullSubject is non-nullness.

Equations

• Minimalist.MinimalPronoun.PronForm.null.toExponent = Phenomena.NullSubject.Exponent.null
• Minimalist.MinimalPronoun.PronForm.pronoun.toExponent = Phenomena.NullSubject.Exponent.overt
• Minimalist.MinimalPronoun.PronForm.reflexive.toExponent = Phenomena.NullSubject.Exponent.overt

def Minimalist.MinimalPronoun.MinPronInventory.toSubjectAssignment (inv : MinPronInventory PronForm) : Phenomena.NullSubject.SubjectAssignment

Project a Minimalist MinPronInventory to the framework-agnostic SubjectAssignment. The BVAContext axis maps controlled SubjectContexts to controlledSubject; all other contexts get the elsewhere/free realization, since the minimal-pronoun inventory does not directly track person, finiteness, or Ā-status. Refinements (per-person inventories, anti-agreement inventories) extend this projection.

Equations

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

theorem Minimalist.MinimalPronoun.MinPronInventory.subjectAssignment_overtPRO_iff (inv : MinPronInventory PronForm) : inv.toSubjectAssignment.hasOvertPRO ↔ inv.hasOvertPRO

Bridge theorem: the abstract hasOvertPRO over the projected assignment agrees with the inventory's own hasOvertPRO. This is the Minimalism→Core grounding: changing the inventory propagates to the abstract universal by construction.

structure Minimalist.MinimalPronoun.OCSignature : Type

@cite{landau-2013}'s Obligatory Control signature (simplified).

A clause S exhibits OC iff its subject satisfies two core conditions: (a) the controller(s) must be codependent(s) of S (b) PRO (or part of it) must be interpreted as a bound variable

Two additional diagnostics are derived from (a):

• Sloppy-only under VPE (from (a): controller must be local codependent of the elided clause, forcing sloppy construal; Morgan 1970)
• Local c-commanding antecedent required (from (a): codependency excludes arbitrary, long-distance, and non-c-commanding control)

Note: partial control IS a subspecies of OC per @cite{landau-2013} — (74b) says "PRO (or part of it)", explicitly accommodating it.

• controllerCodependent : Bool

  (a): Controller must be argument of the matrix predicate

• boundVariable : Bool

  (b): Embedded subject interpreted as bound variable

@[implicit_reducible]

instance Minimalist.MinimalPronoun.instDecidableEqOCSignature : DecidableEq OCSignature

Equations

• Minimalist.MinimalPronoun.instDecidableEqOCSignature = Minimalist.MinimalPronoun.instDecidableEqOCSignature.decEq

def Minimalist.MinimalPronoun.instDecidableEqOCSignature.decEq (x✝ x✝¹ : OCSignature) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Minimalist.MinimalPronoun.instReprOCSignature : Repr OCSignature

Equations

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

def Minimalist.MinimalPronoun.instReprOCSignature.repr : OCSignature → ℕ → Std.Format

Equations

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

def Minimalist.MinimalPronoun.OCSignature.sloppyOnly (sig : OCSignature) : Bool

Derived: VPE allows only sloppy, not strict readings (from codependency: controller must be local codependent of elided clause).

Equations

• sig.sloppyOnly = sig.controllerCodependent

def Minimalist.MinimalPronoun.OCSignature.localCCommand (sig : OCSignature) : Bool

Derived: Antecedent must locally c-command (from codependency).

Equations

• sig.localCCommand = sig.controllerCodependent

def Minimalist.MinimalPronoun.ocFull : OCSignature

The full OC signature: both core diagnostics positive.

Equations

• Minimalist.MinimalPronoun.ocFull = { controllerCodependent := true, boundVariable := true }

def Minimalist.MinimalPronoun.ocNone : OCSignature

No OC: neither core diagnostic holds.

Equations

• Minimalist.MinimalPronoun.ocNone = { controllerCodependent := false, boundVariable := false }

def Minimalist.MinimalPronoun.OCSignature.isOC (sig : OCSignature) : Bool

Does a clause type show obligatory control?

Equations

• sig.isOC = (sig.controllerCodependent && sig.boundVariable)

def Minimalist.MinimalPronoun.MinPronInventory.toDMRules {Form : Type} (inv : MinPronInventory Form) (render : Form → String) : List (Morphology.DM.VI.VocabItem BVAContext Unit)

Convert a MinPronInventory to a list of DM VocabItems.

Each context-specific item becomes a DM rule with specificity = 1, and the elsewhere form becomes a DM rule with specificity = 0. This preserves the Elsewhere Condition: DM's specificity-sorted insertion will select the context-specific rule when it matches, falling back to the elsewhere rule otherwise.

The Form type is rendered to String via the supplied function.

Equations

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