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 Syntax.Minimalism.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 Syntax.Minimalism.MinimalPronoun.instDecidableEqBVAContext : DecidableEq BVAContext

Equations

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

def Syntax.Minimalism.MinimalPronoun.instBEqBVAContext.beq : BVAContext → BVAContext → Bool

Equations

• Syntax.Minimalism.MinimalPronoun.instBEqBVAContext.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Syntax.Minimalism.MinimalPronoun.instBEqBVAContext : BEq BVAContext

Equations

• Syntax.Minimalism.MinimalPronoun.instBEqBVAContext = { beq := Syntax.Minimalism.MinimalPronoun.instBEqBVAContext.beq }

instance Syntax.Minimalism.MinimalPronoun.instReprBVAContext : Repr BVAContext

Equations

• Syntax.Minimalism.MinimalPronoun.instReprBVAContext = { reprPrec := Syntax.Minimalism.MinimalPronoun.instReprBVAContext.repr }

def Syntax.Minimalism.MinimalPronoun.instReprBVAContext.repr : BVAContext → ℕ → Std.Format

Equations

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

structure Syntax.Minimalism.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 Syntax.Minimalism.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 Syntax.Minimalism.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 : Syntax.Minimalism.MinimalPronoun.VocabItem Form) => x.context == ctx) inv.items with | some item => item.form | none => inv.elsewhere

def Syntax.Minimalism.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 Syntax.Minimalism.MinimalPronoun.BVAContext.controlledSubject

inductive Syntax.Minimalism.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 Syntax.Minimalism.MinimalPronoun.instDecidableEqPronForm : DecidableEq PronForm

Equations

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

instance Syntax.Minimalism.MinimalPronoun.instBEqPronForm : BEq PronForm

Equations

• Syntax.Minimalism.MinimalPronoun.instBEqPronForm = { beq := Syntax.Minimalism.MinimalPronoun.instBEqPronForm.beq }

def Syntax.Minimalism.MinimalPronoun.instBEqPronForm.beq : PronForm → PronForm → Bool

Equations

• Syntax.Minimalism.MinimalPronoun.instBEqPronForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Syntax.Minimalism.MinimalPronoun.instReprPronForm.repr : PronForm → ℕ → Std.Format

Equations

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

instance Syntax.Minimalism.MinimalPronoun.instReprPronForm : Repr PronForm

Equations

• Syntax.Minimalism.MinimalPronoun.instReprPronForm = { reprPrec := Syntax.Minimalism.MinimalPronoun.instReprPronForm.repr }

structure Syntax.Minimalism.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

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

Equations

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

instance Syntax.Minimalism.MinimalPronoun.instDecidableEqOCSignature : DecidableEq OCSignature

Equations

• Syntax.Minimalism.MinimalPronoun.instDecidableEqOCSignature = Syntax.Minimalism.MinimalPronoun.instDecidableEqOCSignature.decEq

def Syntax.Minimalism.MinimalPronoun.instBEqOCSignature.beq : OCSignature → OCSignature → Bool

Equations

• Syntax.Minimalism.MinimalPronoun.instBEqOCSignature.beq { controllerCodependent := a, boundVariable := a_1 } { controllerCodependent := b, boundVariable := b_1 } = (a == b && a_1 == b_1)
• Syntax.Minimalism.MinimalPronoun.instBEqOCSignature.beq x✝¹ x✝ = false

instance Syntax.Minimalism.MinimalPronoun.instBEqOCSignature : BEq OCSignature

Equations

• Syntax.Minimalism.MinimalPronoun.instBEqOCSignature = { beq := Syntax.Minimalism.MinimalPronoun.instBEqOCSignature.beq }

instance Syntax.Minimalism.MinimalPronoun.instReprOCSignature : Repr OCSignature

Equations

• Syntax.Minimalism.MinimalPronoun.instReprOCSignature = { reprPrec := Syntax.Minimalism.MinimalPronoun.instReprOCSignature.repr }

def Syntax.Minimalism.MinimalPronoun.instReprOCSignature.repr : OCSignature → ℕ → Std.Format

Equations

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

def Syntax.Minimalism.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 Syntax.Minimalism.MinimalPronoun.OCSignature.localCCommand (sig : OCSignature) : Bool

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

Equations

• sig.localCCommand = sig.controllerCodependent

def Syntax.Minimalism.MinimalPronoun.ocFull : OCSignature

The full OC signature: both core diagnostics positive.

Equations

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

def Syntax.Minimalism.MinimalPronoun.ocNone : OCSignature

No OC: neither core diagnostic holds.

Equations

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

def Syntax.Minimalism.MinimalPronoun.OCSignature.isOC (sig : OCSignature) : Bool

Does a clause type show obligatory control?

Equations

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

def Syntax.Minimalism.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.