Ostrove (2026): Obligatorily Overt PRO in San Martín Peras Mixtec

Ostrove argues that San Martín Peras Mixtec (SMPM) has obligatory control whose controlled subject must be an overt clitic pronoun. Its three embedded clause types, finite clauses, tensed subjunctives and untensed subjunctives, are told apart by aspect, tense and restructuring (unrestrictedTAM_iff, independentTense_iff, frontingOut_iff), and only the untensed subjunctive shows Landau's signature of obligatory control (isObligatory_iff). Exempt anaphors reject quantified antecedents yet occur in untensed subjunctives under quantified controllers, so the controlled subject is a pronoun rather than a copy left by movement (smpm_refutes_movement). The analysis is morphological: bound variables are minimal pronouns realized by vocabulary items, and SMPM lacks the null item that yields silent PRO elsewhere, so the elsewhere pronoun surfaces (smpm_overt_pro, syncretism_typology). A tentative universal closes the argument: overt PRO entails no pro-drop (Universal54).

Implementation notes

The properties of (26) and the control profile are read off the paper's example rows (Data/Examples/Ostrove2026.json), whose clause types agree with the fragment's verbs (clauseTypeOf_mem_verbOf). The rows bear out (26) except in its restructuring column, which footnote 8's exception under kòni 'want' breaks (restructures_iff). The paper's examples of non-exhaustive binding in tensed subjunctives are a missing cross-reference in the manuscript, so partial control is attested only as absent from untensed subjunctives. Landau's calculus fits the three types only if the tensed subjunctive is [+Agr] (landau_predicts_control_iff), which the paper does not discuss. The pro-drop status is the paper's own 101A cell, as WALS does not sample the language. Example numbers follow the manuscript version of the article.

References

• [Ost26]
• [Lan04a]
• [Lan15]
• [Kra09b]
• [Saf14]
• [CS99a]
• [PP06]
• [All21]
• [DH13b]
• [Sul21]
• [Bla94a]
• [DM94]

The clause typology (26)

inductive Ostrove2026.EmbeddedClauseType : Type

The three embedded clause types of (26).

• finite : EmbeddedClauseType
• tensedSubjunctive : EmbeddedClauseType
• untensedSubjunctive : EmbeddedClauseType

@[instance_reducible]

instance Ostrove2026.instDecidableEqEmbeddedClauseType : DecidableEq EmbeddedClauseType

Equations

• Ostrove2026.instDecidableEqEmbeddedClauseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Ostrove2026.instReprEmbeddedClauseType : Repr EmbeddedClauseType

Equations

• Ostrove2026.instReprEmbeddedClauseType = { reprPrec := Ostrove2026.instReprEmbeddedClauseType.repr }

def Ostrove2026.instReprEmbeddedClauseType.repr : EmbeddedClauseType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Ostrove2026.instFintypeEmbeddedClauseType : Fintype EmbeddedClauseType

Equations

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

def Ostrove2026.EmbeddedClauseType.ofFrame (v : Verb) (fr : ArgumentFrame) : EmbeddedClauseType

A verb's complement frame is finite in the indicative coding and otherwise a subjunctive, untensed exactly when the verb's reading of the frame is controlled (§3).

Equations

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

theorem Ostrove2026.control_iff_untensed (v : Verb) : v ∈ Mixtec.SMPM.verbs → ∀ fr ∈ v.valency.frames, ((v.reading? fr).bind fun (x : Verb.Reading) => x.control).isSome = true ↔ EmbeddedClauseType.ofFrame v fr = EmbeddedClauseType.untensedSubjunctive

The fragment's controlled complements are exactly its untensed subjunctives: no finite complement is controlled, not even that of kònì 'know', which also takes an untensed one.

The rows

def Ostrove2026.clauseTypeOf (row : Datum) : Option EmbeddedClauseType

The clause type a row's clauseType feature names.

Equations

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

def Ostrove2026.verbOf (row : Datum) : Option Verb

The fragment verb a row's verb feature names.

Equations

• Ostrove2026.verbOf row = (row.feature? "verb").bind fun (x : String) => Verb.find? Mixtec.SMPM.verbs x

theorem Ostrove2026.clauseTypeOf_mem_verbOf (row : Datum) : row ∈ Examples.all → ∀ c ∈ clauseTypeOf row, ∃ v ∈ verbOf row, ∃ fr ∈ v.valency.frames, EmbeddedClauseType.ofFrame v fr = c

The rows agree with the predicate lists (27): each row's clause type is one its matrix verb takes in the fragment.

def Ostrove2026.reads (row : Datum) (r : String) (j : Judgment) : Prop

A row records reading r with judgment j.

Equations

• Ostrove2026.reads row r j = ∃ x ∈ row.readings, x = (r, j)

@[instance_reducible]

instance Ostrove2026.instDecidableReads (row : Datum) (r : String) (j : Judgment) : Decidable (reads row r j)

Equations

• Ostrove2026.instDecidableReads row r j = Ostrove2026.instDecidableReads._aux_1 row r j

The clause typology (26) from the rows

def Ostrove2026.UnrestrictedTAM (c : EmbeddedClauseType) : Prop

A clause type has unrestricted TAM when it has an acceptable row in each of the three aspects ((9), (13)).

Equations

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

@[instance_reducible]

instance Ostrove2026.instDecidableUnrestrictedTAM (c : EmbeddedClauseType) : Decidable (UnrestrictedTAM c)

Equations

• Ostrove2026.instDecidableUnrestrictedTAM c = id inferInstance

def Ostrove2026.IndependentTense (c : EmbeddedClauseType) : Prop

A clause type has a tense of its own when an acceptable row gives it a time adverb the matrix clause does not share ((10), (16), (17)).

Equations

• Ostrove2026.IndependentTense c = ∃ row ∈ Ostrove2026.Examples.all, Ostrove2026.clauseTypeOf row = some c ∧ row.feature? "diagnostic" = some "tense" ∧ row.judgment = Judgment.acceptable

@[instance_reducible]

instance Ostrove2026.instDecidableIndependentTense (c : EmbeddedClauseType) : Decidable (IndependentTense c)

Equations

• Ostrove2026.instDecidableIndependentTense c = id inferInstance

def Ostrove2026.Restructures (c : EmbeddedClauseType) : Prop

A clause type restructures when an acceptable row fronts a quantifier out of it into the matrix clause ((20), (22), (24)).

Equations

• Ostrove2026.Restructures c = ∃ row ∈ Ostrove2026.Examples.all, Ostrove2026.clauseTypeOf row = some c ∧ row.feature? "fronting" = some "out" ∧ row.judgment = Judgment.acceptable

@[instance_reducible]

instance Ostrove2026.instDecidableRestructures (c : EmbeddedClauseType) : Decidable (Restructures c)

Equations

• Ostrove2026.instDecidableRestructures c = id inferInstance

theorem Ostrove2026.unrestrictedTAM_iff (c : EmbeddedClauseType) : UnrestrictedTAM c ↔ c = EmbeddedClauseType.finite

The TAM column of (26): only finite clauses take every aspect.

theorem Ostrove2026.independentTense_iff (c : EmbeddedClauseType) : IndependentTense c ↔ c ≠ EmbeddedClauseType.untensedSubjunctive

The tense column: only untensed subjunctives lack a tense of their own.

theorem Ostrove2026.restructures_iff (c : EmbeddedClauseType) : Restructures c ↔ c ≠ EmbeddedClauseType.finite

The restructuring column holds of the rows except under kòni 'want', out of whose tensed subjunctive a quantifier fronts (fn. 8): the rows make tensed subjunctives restructure too.

theorem Ostrove2026.frontingOut_iff (row : Datum) : row ∈ Examples.all → row.feature? "fronting" = some "out" → (row.judgment = Judgment.acceptable ↔ clauseTypeOf row = some EmbeddedClauseType.untensedSubjunctive ∨ row.feature? "verb" = some "kòni")

The restructuring column with its exception: a quantifier fronts out of an embedded clause exactly when the clause is an untensed subjunctive or the verb is kòni 'want' ((20), (22), (24), (109)).

Obligatory control (§4)

def Ostrove2026.attests (row : Datum) : Control.Diagnostic → Prop

The control diagnostic an acceptable reading of a row attests: a free reading of the embedded subject, a strict reading under ellipsis, or a non-c-commanding antecedent. The paper tests neither long-distance antecedents nor readings under only.

Equations

• Ostrove2026.attests row Control.Diagnostic.arbitraryControl = Ostrove2026.reads row "free" Judgment.acceptable
• Ostrove2026.attests row Control.Diagnostic.strictEllipsis = Ostrove2026.reads row "strict" Judgment.acceptable
• Ostrove2026.attests row Control.Diagnostic.nonCCommandingControl = (row.feature? "antecedent" = some "nonCCommanding" ∧ row.judgment = Judgment.acceptable)
• Ostrove2026.attests row Control.Diagnostic.longDistanceControl = False
• Ostrove2026.attests row Control.Diagnostic.strictUnderOnly = False

@[instance_reducible]

instance Ostrove2026.instDecidablePredDiagnosticAttests (row : Datum) : DecidablePred (attests row)

Equations

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

def Ostrove2026.attested (c : EmbeddedClauseType) : Set Control.Diagnostic

The diagnostics the rows attest for a clause type.

Equations

• Ostrove2026.attested c = {d : Control.Diagnostic | ∃ row ∈ Ostrove2026.Examples.all, Ostrove2026.clauseTypeOf row = some c ∧ Ostrove2026.attests row d}

@[instance_reducible]

instance Ostrove2026.instDecidablePredDiagnosticMemSetAttested (c : EmbeddedClauseType) : DecidablePred fun (x : Control.Diagnostic) => x ∈ attested c

Equations

• Ostrove2026.instDecidablePredDiagnosticMemSetAttested c d = id inferInstance

theorem Ostrove2026.attested_eq_empty_iff (c : EmbeddedClauseType) : attested c = ∅ ↔ c = EmbeddedClauseType.untensedSubjunctive

No row attests a criterial configuration of an untensed subjunctive, and every other clause type attests one: free subjects (12), (18), strict ellipsis (30), (32), and non-c-commanding antecedents (43), (45) against (19), (33), (44), (46).

def Ostrove2026.smpmProfile (c : EmbeddedClauseType) : Set Landau2013.Clause74

The control profile of a clause type in [Lan13]'s signature: the clauses no attested diagnostic refutes.

Equations

• Ostrove2026.smpmProfile c = Control.ofAttested (Ostrove2026.attested c)

theorem Ostrove2026.isObligatory_iff (c : EmbeddedClauseType) : smpmProfile c = Set.univ ↔ c = EmbeddedClauseType.untensedSubjunctive

Only untensed subjunctives are obligatory-control clauses.

theorem Ostrove2026.partialControl_rows (row : Datum) : row ∈ Examples.all → row.feature? "diagnostic" = some "partialControl" → clauseTypeOf row = some EmbeddedClauseType.untensedSubjunctive ∧ row.judgment = Judgment.ungrammatical

Untensed subjunctives reject partial control (37).

Landau's scale

def Ostrove2026.landauToSMPM : Control.ClauseClass → EmbeddedClauseType

The clause types on the finiteness scale of [Lan04a]: untensed subjunctives are C-subjunctives and tensed ones F-subjunctives (§3).

Equations

• Ostrove2026.landauToSMPM Control.ClauseClass.cSubjunctive = Ostrove2026.EmbeddedClauseType.untensedSubjunctive
• Ostrove2026.landauToSMPM Control.ClauseClass.fSubjunctive = Ostrove2026.EmbeddedClauseType.tensedSubjunctive
• Ostrove2026.landauToSMPM Control.ClauseClass.finite = Ostrove2026.EmbeddedClauseType.finite

def Ostrove2026.smpmToLandau (c : EmbeddedClauseType) : Control.ClauseClass

The scale position of a clause type, from its TAM and tense properties.

Equations

• Ostrove2026.smpmToLandau c = Control.ClauseClass.ofFiniteness (decide (Ostrove2026.UnrestrictedTAM c)) (decide (Ostrove2026.IndependentTense c))

theorem Ostrove2026.smpmToLandau_landauToSMPM (c : Control.ClauseClass) : smpmToLandau (landauToSMPM c) = c

SMPM realizes every position of the scale, unlike Gã (Allotey2021.ga_no_fSubjunctive).

theorem Ostrove2026.landau_predicts_control_iff (agr : Bool) : (∀ (c : EmbeddedClauseType), smpmProfile c = Set.univ ↔ (smpmToLandau c).HasOC agr) ↔ agr = true

Landau's calculus predicts the control profile of every clause type exactly when the clauses are [+Agr]: at [−Agr] it makes the tensed subjunctive, an F-subjunctive, obligatory control, yet its subject may be disjoint from the matrix subject (18b).

Against movement (§6)

theorem Ostrove2026.exemptAnaphor_rows (row : Datum) : row ∈ Examples.all → row.feature? "diagnostic" = some "exemptAnaphor" → (row.judgment = Judgment.acceptable ↔ clauseTypeOf row = some EmbeddedClauseType.untensedSubjunctive)

An exempt anaphor with a quantified antecedent is out in a simple clause (75) and good inside an untensed subjunctive under a quantified controller ((86), (87)).

inductive Ostrove2026.Ex86Item : Type

The occupants of the configurations (86) and (87): a quantified controller and the overt controlled clitic that antecedes an exempt anaphor.

• quantifierDP : Ex86Item
• pronoun : Ex86Item

@[instance_reducible]

instance Ostrove2026.instDecidableEqEx86Item : DecidableEq Ex86Item

Equations

• Ostrove2026.instDecidableEqEx86Item x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ostrove2026.ex86Dependency : SetRel (Fin 2) (Fin 2)

The control dependency of (86) and (87), from the controller position to the embedded clitic position.

Equations

• Ostrove2026.ex86Dependency = {(0, 1)}

def Ostrove2026.ex86Occupant : Fin 2 → Ex86Item

The attested occupants of the two positions.

Equations

• Ostrove2026.ex86Occupant p = if p = 0 then Ostrove2026.Ex86Item.quantifierDP else Ostrove2026.Ex86Item.pronoun

theorem Ostrove2026.smpm_refutes_movement : ¬Control.IsExhaustive ex86Occupant ex86Dependency

Exempt anaphors reject quantified antecedents (78) yet are available in untensed subjunctives under quantified controllers (exemptAnaphor_rows), so the embedded position holds a referential pronoun and not a copy of the quantifier: the dependency is not movement.

Minimal pronoun inventories (§7)

def Ostrove2026.englishInventory : Binding.MinimalPronoun.Vocabulary Binding.MinimalPronoun.Form

English (94): a null item for controlled subjects, a reflexive for local binding, and the pronoun elsewhere.

Equations

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

def Ostrove2026.haitianInventory : Binding.MinimalPronoun.Vocabulary Binding.MinimalPronoun.Form

Haitian Creole (96): a null item for controlled subjects and no reflexive item, reflexives surfacing as pronouns ([DM94]).

Equations

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

def Ostrove2026.smpmInventory : Binding.MinimalPronoun.Vocabulary Binding.MinimalPronoun.Form

SMPM (98): a reflexive item, mí with a clitic, and no null item.

Equations

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

def Ostrove2026.quiegolaniInventory : Binding.MinimalPronoun.Vocabulary Binding.MinimalPronoun.Form

Quiegolani Zapotec ([Bla94a]): no context-specific item at all.

Equations

• Ostrove2026.quiegolaniInventory = { items := [], elsewhere := Binding.MinimalPronoun.Form.pronoun }

theorem Ostrove2026.smpm_overt_pro : smpmInventory.controlForm = smpmInventory.elsewhere ∧ englishInventory.controlForm = Binding.MinimalPronoun.Form.null

Overt PRO: no SMPM item is conditioned on the controlled subject, so it takes the elsewhere pronoun (98), where English's null item yields silent PRO (94a).

theorem Ostrove2026.smpm_no_null_item (i : DistributedMorphology.VocabularyItem Binding.MinimalPronoun.Context Binding.MinimalPronoun.Form) : i ∈ smpmInventory.items → i.exponent ≠ Binding.MinimalPronoun.Form.null

The analysis in general form: with the pronoun as its elsewhere form, a language has silent PRO only through a null item for controlled subjects, which SMPM lacks.

theorem Ostrove2026.syncretism_typology : englishInventory.syncretic = {Binding.MinimalPronoun.Context.boundVariable} ∧ quiegolaniInventory.syncretic = Finset.univ ∧ haitianInventory.syncretic = {Binding.MinimalPronoun.Context.locallyBound, Binding.MinimalPronoun.Context.boundVariable} ∧ smpmInventory.syncretic = {Binding.MinimalPronoun.Context.controlledSubject, Binding.MinimalPronoun.Context.boundVariable}

The syncretism table (92), each row derived from its inventory: the contexts in which the bound form is the referential pronoun's, whose own column is the elsewhere form itself. The four languages occupy four distinct cells.

Copy control (§5)

inductive Ostrove2026.CopyControlType : Type

The four types of copy control, an overt element in the controlled position ([PP06]): a full copy of the controller, or a pronoun that is overt in attitude reports only, under scope-taking operators only, or unconditionally.

• fullCopy : CopyControlType

  San Lucas Quiaviní Zapotec, Copala Triqui.

• logophoricPronominal : CopyControlType

  Gengbe, Mandarin.

• scopeSensitivePronominal : CopyControlType

  Italian, Hungarian, European Portuguese, alternating with null PRO (60).

• obligatoryPronominal : CopyControlType

  SMPM, Gã ([All21]), Bùlì ([Sul21]).

@[instance_reducible]

instance Ostrove2026.instDecidableEqCopyControlType : DecidableEq CopyControlType

Equations

• Ostrove2026.instDecidableEqCopyControlType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Ostrove2026.smpmCopyControlType : CopyControlType

SMPM's type: the controlled subject is a pronoun rather than a full copy (57), it is overt outside attitude reports, and it cannot bear focus, so the scope-sensitive alternation with null PRO is unavailable.

Equations

• Ostrove2026.smpmCopyControlType = Ostrove2026.CopyControlType.obligatoryPronominal

theorem Ostrove2026.nonclitic_rows (row : Datum) : row ∈ Examples.all → row.feature? "embeddedSubject" = some "nonclitic" → (row.judgment = Judgment.acceptable ↔ clauseTypeOf row = some EmbeddedClauseType.tensedSubjunctive)

A non-clitic embedded subject, a clitic strengthened by the article or a demonstrative, is out exactly in untensed subjunctives ((67), (68)).

def Ostrove2026.controlledSubjectStrength : Pronoun.Strength

A controlled subject is of the clitic class of [CS99a], since non-clitic forms are ungrammatical there (nonclitic_rows).

Equations

• Ostrove2026.controlledSubjectStrength = Pronoun.Strength.clitic

theorem Ostrove2026.controlledSubject_iff_mem_clitics (p : PersonalPronoun) : p ∈ Mixtec.SMPM.pronouns → (p.strength = some controlledSubjectStrength ↔ p ∈ Mixtec.SMPM.clitics)

The pronouns that can be a controlled subject are exactly the clitics, none of which bears focus (65), (66): the overt subject is not the focused pronoun of scope-sensitive copy control.

The implicational universal (54)

def Ostrove2026.pronominalSubjects : Data.WALS.F101A.ExpressionOfPronominalSubjects

SMPM's cell of [DH13b]'s 101A, which does not sample the language, is obligatory subject pronouns, expletive and impersonal ones included (3).

Equations

• Ostrove2026.pronominalSubjects = Data.WALS.F101A.ExpressionOfPronominalSubjects.obligatoryPronounsInSubjectPosition

def Ostrove2026.Universal54 (inv : Binding.MinimalPronoun.Vocabulary Binding.MinimalPronoun.Form) (s : Data.WALS.F101A.ExpressionOfPronominalSubjects) : Prop

A language with minimal-pronoun inventory inv and 101A cell s satisfies the implicational universal (54) when overt PRO implies obligatory subject pronouns, that is, no pro-drop.

Equations

• Ostrove2026.Universal54 inv s = (inv.controlForm ≠ Binding.MinimalPronoun.Form.null → s = Data.WALS.F101A.ExpressionOfPronominalSubjects.obligatoryPronounsInSubjectPosition)

theorem Ostrove2026.smpm_universal54 : Universal54 smpmInventory pronominalSubjects

SMPM instantiates the universal: overt PRO and no pro-drop.

theorem Ostrove2026.english_universal54 (s : Data.WALS.F101A.ExpressionOfPronominalSubjects) : Universal54 englishInventory s

English satisfies it vacuously, whatever its 101A cell, since its PRO is null.

theorem Ostrove2026.ga_patterns_with_smpm : Allotey2021.gaInventory.controlForm = smpmInventory.controlForm ∧ Allotey2021.pronominalSubjects = pronominalSubjects

Gã sits in SMPM's cell: the same controlled-subject realization, derived from the Gã inventory of [All21], and the same 101A cell.

theorem Ostrove2026.ga_universal54 : Universal54 Allotey2021.gaInventory Allotey2021.pronominalSubjects

Gã instantiates the universal ([All21]).

theorem Ostrove2026.ga_violates_universal54_of_wals (s : Data.WALS.F101A.ExpressionOfPronominalSubjects) : s ∈ List.lookup "ga" Data.WALS.F101A.allData → ¬Universal54 Allotey2021.gaInventory s

The universal has bite for Gã: under [DH13b]'s coding of its subject markers as affixes (Allotey2021.wals_codes_affixes) Gã violates it, so its instance rests on [All21]'s analysis of the markers as pronouns.