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
• 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: [Lan13]'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 ([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.

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 ⋯

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

Equations

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

@[implicit_reducible]

instance Minimalist.MinimalPronoun.instReprBVAContext : Repr BVAContext

Equations

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

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 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.

[Saf14]: "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 ([Saf14]).

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 → Nat → 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)

@[implicit_reducible]

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

Equations

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

structure Minimalist.MinimalPronoun.OCSignature : Type

[Lan13]'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

Partial control is a subspecies of OC per [Lan13] — "PRO (or part of it)" explicitly accommodates it.

• controllerCodependent : Bool

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

• boundVariable : Bool

  (b): Embedded subject interpreted as bound variable

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.instDecidableEqOCSignature : DecidableEq OCSignature

Equations

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

@[implicit_reducible]

instance Minimalist.MinimalPronoun.instReprOCSignature : Repr OCSignature

Equations

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

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

Equations

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

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)