Minimal pronouns

A minimal pronoun is a bare D head with unvalued φ-features, [D, uφ], valued by its antecedent. Kratzer takes reflexives, controlled PRO and bound-variable pronouns to be one such object, and Safir concludes that all anaphoric diversity is morphological: a language's vocabulary items realize the valued pronoun according to the context it is bound in, and where no item is conditioned on that context the elsewhere item applies, yielding the shape of the referential pronoun. English has a null item for controlled subjects and a reflexive item for local binding; a language without the null item has overt PRO.

Main definitions

• MinimalPronoun.Context: the binding contexts an item can be conditioned on
• MinimalPronoun.Form: the shapes a minimal pronoun takes, null, pronominal or reflexive
• MinimalPronoun.Vocabulary: a language's items for minimal pronouns and its elsewhere form
• Vocabulary.realize, Vocabulary.controlForm: the form in a context, by the Subset Principle
• Vocabulary.syncretic: the contexts whose form is the referential pronoun's

Main results

• Vocabulary.some_realize: the elsewhere form is the Subset Principle's elsewhere item
• Vocabulary.realize_eq_elsewhere: a context no item applies to gets the elsewhere form
• Vocabulary.exists_null_item_of_controlForm_eq_null: silent PRO needs a null item

Implementation notes

The free, referential pronoun is not a context: it is what no context conditions, the elsewhere form. The elsewhere form is a field of the vocabulary rather than an item, so that every vocabulary realizes every context; some_realize identifies it with the empty-site item of Distributed Morphology. Safir states the variation as shape conditions at Spell-Out; the vocabulary-item formulation is Landau's and Ostrove's. The theory of control that consumes minimal pronouns, Landau's two tiers, is in Studies/Landau2015.lean.

References

• [Kra98a]
• [Kra09b]
• [Saf14]
• [Lan15]
• [HM93]
• [Ost26]

inductive Binding.MinimalPronoun.Context : Type

The binding contexts a vocabulary item for minimal pronouns can be conditioned on.

• controlledSubject : Context

  The subject of a controlled clause, English PRO.

• locallyBound : Context

  Bound within its local domain, the English reflexive.

• boundVariable : Context

  Bound from outside its local domain, a bound-variable pronoun.

@[instance_reducible]

instance Binding.MinimalPronoun.instDecidableEqContext : DecidableEq Context

Equations

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

def Binding.MinimalPronoun.instReprContext.repr : Context → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Binding.MinimalPronoun.instReprContext : Repr Context

Equations

• Binding.MinimalPronoun.instReprContext = { reprPrec := Binding.MinimalPronoun.instReprContext.repr }

@[instance_reducible]

instance Binding.MinimalPronoun.instFintypeContext : Fintype Context

Equations

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

inductive Binding.MinimalPronoun.Form : Type

The shapes a minimal pronoun takes.

• null : Form

  Silent, as English PRO.

• pronoun : Form

  A pronoun, with the shape of the referential pronoun.

• reflexive : Form

  A reflexive anaphor, as English himself or San Martín Peras Mixtec mí with a clitic.

@[instance_reducible]

instance Binding.MinimalPronoun.instDecidableEqForm : DecidableEq Form

Equations

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

def Binding.MinimalPronoun.instReprForm.repr : Form → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Binding.MinimalPronoun.instReprForm : Repr Form

Equations

• Binding.MinimalPronoun.instReprForm = { reprPrec := Binding.MinimalPronoun.instReprForm.repr }

structure Binding.MinimalPronoun.Vocabulary (E : Type u_1) : Type u_1

A language's vocabulary for minimal pronouns: the items that realize the valued pronoun in binding contexts, and the elsewhere form, which realizes it where no item applies.

• items : Morphology.Exponence.RuleSet (DistributedMorphology.VocabularyItem Context E)

  The items, each conditioned on binding contexts.

• elsewhere : E

  The elsewhere form, the shape of the referential pronoun.

def Binding.MinimalPronoun.Vocabulary.realize {E : Type u_1} (v : Vocabulary E) (c : Context) : E

The form of the minimal pronoun in a context is the exponent of the most specific item that applies there, by the Subset Principle, and the elsewhere form where none does.

Equations

• v.realize c = (DistributedMorphology.subsetPrinciple v.items ↑[c]).getD v.elsewhere

def Binding.MinimalPronoun.Vocabulary.controlForm {E : Type u_1} (v : Vocabulary E) : E

The form of a controlled subject, silent PRO or an overt pronoun.

Equations

• v.controlForm = v.realize Binding.MinimalPronoun.Context.controlledSubject

def Binding.MinimalPronoun.Vocabulary.syncretic {E : Type u_1} (v : Vocabulary E) [DecidableEq E] : Finset Context

The contexts in which the minimal pronoun is syncretic with the referential pronoun are those whose form is the elsewhere form.

Equations

• v.syncretic = {c : Binding.MinimalPronoun.Context | v.realize c = v.elsewhere}

@[simp]

theorem Binding.MinimalPronoun.Vocabulary.mem_syncretic {E : Type u_1} {v : Vocabulary E} {c : Context} [DecidableEq E] : c ∈ v.syncretic ↔ v.realize c = v.elsewhere

theorem Binding.MinimalPronoun.Vocabulary.some_realize {E : Type u_1} {v : Vocabulary E} (c : Context) : some (v.realize c) = DistributedMorphology.subsetPrinciple (v.items ++ [DistributedMorphology.VocabularyItem.ofFeatures [] v.elsewhere]) ↑[c]

The elsewhere form is the elsewhere item of the Subset Principle: realizing a context is selecting among the items followed by the item of empty site.

theorem Binding.MinimalPronoun.Vocabulary.realize_eq_elsewhere {E : Type u_1} {v : Vocabulary E} {c : Context} (h : ∀ i ∈ v.items, ¬i.site ⊆ ↑[c]) : v.realize c = v.elsewhere

A context that no item applies to gets the elsewhere form.

theorem Binding.MinimalPronoun.Vocabulary.exists_item_of_realize_ne {E : Type u_1} {v : Vocabulary E} {c : Context} (h : v.realize c ≠ v.elsewhere) : ∃ i ∈ v.items, i.site ⊆ ↑[c] ∧ i.exponent = v.realize c

A form other than the elsewhere form is the exponent of an item that applies in the context.

theorem Binding.MinimalPronoun.Vocabulary.exists_null_item_of_controlForm_eq_null {v : Vocabulary Form} (he : v.elsewhere ≠ Form.null) (h : v.controlForm = Form.null) : ∃ i ∈ v.items, i.site ⊆ ↑[Context.controlledSubject] ∧ i.exponent = Form.null

Silent PRO needs a null item: where the elsewhere form is overt, a controlled subject is null only through an item for that context whose exponent is null.