Documentation

Linglib.Phenomena.Control.Studies.Ostrove2026

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

@cite{ostrove-2026}

Linguistic Inquiry 57(1): 1–48.

San Martín Peras Mixtec (SMPM), an Oto-Manguean language (ISO: jmx), has obligatory control constructions where the controlled subject must be an overt clitic pronoun — null PRO is strongly ungrammatical. This is analyzed via the minimal pronoun framework (@cite{kratzer-2009}, @cite{safir-2014}, @cite{landau-2015}): SMPM simply lacks a null vocabulary item for controlled subject position. The elsewhere item (→ pronoun) applies.

Core Contributions #

Three-way clause typology: finite embedded, tensed subjunctive, untensed subjunctive — distinguished by TAM, noncoreferential subjects, and restructuring (26)
OC with overt pronouns: untensed subjunctives show the full OC signature despite having an overt clitic pronoun, not null PRO
Against movement, for base-generation: exempt anaphor distribution shows the controlled pronoun is base-generated (§6)
Morphological analysis: overt PRO derived by lacking a null vocabulary item; cross-linguistic syncretism typology (92)
Copy control typology: four types of copy control distinguished cross-linguistically (§5)
Implicational universal: overt PRO → non-pro-drop (54)

Landau (2004) Bridge #

SMPM's subjunctive types map onto @cite{landau-2004}'s finiteness scale, connecting clause-level tense properties to control. The paper explicitly discusses this connection (p.8), following Landau's distinction between "C-subjunctives" (untensed, OC) and "F-subjunctives" (tensed, non-OC).

Wurmbrand (2014) Partial Bridge #

@cite{wurmbrand-2014}'s three-way classification of infinitival tense (futureIrrealis, restructuring, propositional) maps partially to SMPM's subjunctive types. The mapping applies only to subjunctives — SMPM's finite embedded clauses are genuinely finite and fall outside Wurmbrand's infinitival classification.

Wurmbrand class	SMPM clause type	OC?
futureIrrealis	tensed subjunctive	No
restructuring	untensed subjunctive	Yes
(not applicable)	finite embedded	No

theorem Ostrove2026.finite_unrestricted_tam :

(Fragments.Mixtec.SMPM.clauseProperties Fragments.Mixtec.SMPM.EmbeddedClauseType.finiteEmbedded).unrestrictedTAM = true

theorem Ostrove2026.tensed_restricted_tam :

(Fragments.Mixtec.SMPM.clauseProperties Fragments.Mixtec.SMPM.EmbeddedClauseType.tensedSubjunctive).unrestrictedTAM = false

theorem Ostrove2026.untensed_restricted_tam :

(Fragments.Mixtec.SMPM.clauseProperties Fragments.Mixtec.SMPM.EmbeddedClauseType.untensedSubjunctive).unrestrictedTAM = false

theorem Ostrove2026.finite_allows_noncoreferential :

(Fragments.Mixtec.SMPM.clauseProperties Fragments.Mixtec.SMPM.EmbeddedClauseType.finiteEmbedded).noncoreferentialSubject = true

theorem Ostrove2026.tensed_allows_noncoreferential :

(Fragments.Mixtec.SMPM.clauseProperties Fragments.Mixtec.SMPM.EmbeddedClauseType.tensedSubjunctive).noncoreferentialSubject = true

theorem Ostrove2026.untensed_no_noncoreferential :

(Fragments.Mixtec.SMPM.clauseProperties Fragments.Mixtec.SMPM.EmbeddedClauseType.untensedSubjunctive).noncoreferentialSubject = false

theorem Ostrove2026.untensed_restructuring :

(Fragments.Mixtec.SMPM.clauseProperties Fragments.Mixtec.SMPM.EmbeddedClauseType.untensedSubjunctive).restructuring = true

theorem Ostrove2026.tensed_no_restructuring :

(Fragments.Mixtec.SMPM.clauseProperties Fragments.Mixtec.SMPM.EmbeddedClauseType.tensedSubjunctive).restructuring = false

theorem Ostrove2026.finite_no_restructuring :

(Fragments.Mixtec.SMPM.clauseProperties Fragments.Mixtec.SMPM.EmbeddedClauseType.finiteEmbedded).restructuring = false

def Ostrove2026.smpmOCSignature :

Fragments.Mixtec.SMPM.EmbeddedClauseType → Minimalist.MinimalPronoun.OCSignature

OC signature for each SMPM clause type.

Untensed subjunctives show the full OC signature (§4):

Sloppy-only under VPE (33)
Exhaustive binding — no partial control (37)
Local c-commanding antecedent required (40, 44)

Tensed subjunctives and finite embedded clauses show none of these properties: they allow strict readings under VPE (30, 32), nonexhaustive binding (tensed subj., fn. 16), and non-local antecedents (43, 45).

Equations

Instances For

theorem Ostrove2026.untensed_is_OC :

(smpmOCSignature Fragments.Mixtec.SMPM.EmbeddedClauseType.untensedSubjunctive).isOC = true

theorem Ostrove2026.tensed_not_OC :

(smpmOCSignature Fragments.Mixtec.SMPM.EmbeddedClauseType.tensedSubjunctive).isOC = false

theorem Ostrove2026.finite_not_OC :

(smpmOCSignature Fragments.Mixtec.SMPM.EmbeddedClauseType.finiteEmbedded).isOC = false

def Ostrove2026.wurmbrandToSubjunctive :

Minimalist.Tense.InfinitivalTense.InfinitivalTenseClass → Option Fragments.Mixtec.SMPM.EmbeddedClauseType

SMPM's two subjunctive types correspond to @cite{wurmbrand-2014}'s infinitival tense classes. The mapping applies only to subjunctives — SMPM's finite embedded clauses are genuinely finite and fall outside Wurmbrand's infinitival classification.

futureIrrealis ↔ tensed subjunctive: future-oriented, non-OC
restructuring ↔ untensed subjunctive: dependent tense, OC

Note: Wurmbrand's propositional class (ECM/attitude infinitives like "believe Julia to be smart") has no SMPM correspondent. SMPM's finite embedded clauses have full TAM morphology and freely noncoreferential subjects — they are not infinitival.

Equations

Instances For

def Ostrove2026.wurmbrandHasOC :

Minimalist.Tense.InfinitivalTense.InfinitivalTenseClass → Bool

Whether a Wurmbrand class involves obligatory control.

Equations

Instances For

theorem Ostrove2026.wurmbrand_predicts_control_futureIrrealis :

Option.map (fun (x : Fragments.Mixtec.SMPM.EmbeddedClauseType) => (smpmOCSignature x).isOC) (wurmbrandToSubjunctive Minimalist.Tense.InfinitivalTense.InfinitivalTenseClass.futureIrrealis) = some (wurmbrandHasOC Minimalist.Tense.InfinitivalTense.InfinitivalTenseClass.futureIrrealis)

For the two Wurmbrand classes that have SMPM correspondents, the mapping correctly predicts control properties.

theorem Ostrove2026.wurmbrand_predicts_control_restructuring :

Option.map (fun (x : Fragments.Mixtec.SMPM.EmbeddedClauseType) => (smpmOCSignature x).isOC) (wurmbrandToSubjunctive Minimalist.Tense.InfinitivalTense.InfinitivalTenseClass.restructuring) = some (wurmbrandHasOC Minimalist.Tense.InfinitivalTense.InfinitivalTenseClass.restructuring)

theorem Ostrove2026.wurmbrand_propositional_no_correspondent :

wurmbrandToSubjunctive Minimalist.Tense.InfinitivalTense.InfinitivalTenseClass.propositional = none

Propositional infinitives have no SMPM correspondent — SMPM finite embedded clauses are genuinely finite, not infinitival.

def Ostrove2026.landauToSMPM :

Landau2015.LandauClauseClass → Fragments.Mixtec.SMPM.EmbeddedClauseType

SMPM clause types map onto @cite{landau-2004}'s finiteness scale. This is the framework the paper explicitly uses (p.8).

Landau class	SMPM clause type	OC?
C-subjunctive	untensed subjunctive	Yes
F-subjunctive	tensed subjunctive	No
finite	finite embedded	No

Equations

Instances For

def Ostrove2026.smpmLandauAgr :

Landau2015.LandauClauseClass → Bool

SMPM Agr status for each Landau clause class.

C-subjunctive (untensed): [−Agr] — no independent subject agreement
F-subjunctive (tensed): [+Agr] — allows noncoreferential subjects, which indicates independent agreement capability
Finite: [+Agr] — full agreement

Under the TTC's OC-NC generalization ((70) in @cite{landau-2015}), [+Agr] blocks logophoric control. This is why SMPM tensed subjunctives (F-subjunctives with [+Agr]) show no OC despite structurally permitting logophoric control.

Equations

Instances For

theorem Ostrove2026.landau_predicts_control (c : Landau2015.LandauClauseClass) :

(smpmOCSignature (landauToSMPM c)).isOC = c.hasOCWithAgr (smpmLandauAgr c)

The Landau classification predicts control properties for all three SMPM clause types, taking Agr status into account.

C-subjunctive [−Agr]: predicative OC (Agr-independent) → OC ✓
F-subjunctive [+Agr]: logophoric OC blocked by Agr → no OC ✓
Finite [+Agr]: no control tier → no OC ✓

def Ostrove2026.englishInventory :

Minimalist.MinimalPronoun.MinPronInventory Minimalist.MinimalPronoun.PronForm

English vocabulary items (94a–c).

Three items: null for controlled, reflexive for locally bound, pronoun elsewhere. English distinguishes all three non-free BVA contexts morphologically.

Equations

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

Instances For

def Ostrove2026.haitianInventory :

Minimalist.MinimalPronoun.MinPronInventory Minimalist.MinimalPronoun.PronForm

Haitian vocabulary items (96a–b).

Two items: null for controlled, pronoun elsewhere. Crucially LACKS a reflexive allomorph — reflexives and bound variables are both realized as pronouns (@cite{dechaine-manfredi-1994}).

Equations

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

Instances For

def Ostrove2026.smpmInventory :

Minimalist.MinimalPronoun.MinPronInventory Minimalist.MinimalPronoun.PronForm

SMPM vocabulary items (98a–b).

Two items: reflexive for locally bound, pronoun elsewhere. Crucially LACKS a null allomorph — controlled subjects and bound variables are both realized as overt clitic pronouns (=rà, =ñá, etc.).

Equations

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

Instances For

def Ostrove2026.quiegolaniInventory :

Minimalist.MinimalPronoun.MinPronInventory Minimalist.MinimalPronoun.PronForm

Quiegolani Zapotec: no context-specific items at all (@cite{black-1994}).

Everything — reflexives, controlled subjects, bound variables — surfaces as a single pronoun form (men). Total syncretism.

Equations

Ostrove2026.quiegolaniInventory = { items := [], elsewhere := Minimalist.MinimalPronoun.PronForm.pronoun }

Instances For

def Ostrove2026.buliInventory :

Minimalist.MinimalPronoun.MinPronInventory Minimalist.MinimalPronoun.PronForm

Büli vocabulary items (inferred from @cite{sulemana-2021}).

Like SMPM and Gã: lacks a null allomorph for controlled subjects. Overt PRO in nonfinite complementation.

Equations

Ostrove2026.buliInventory = { items := [], elsewhere := Minimalist.MinimalPronoun.PronForm.pronoun }

Instances For

theorem Ostrove2026.english_null_pro :

englishInventory.controlForm = Minimalist.MinimalPronoun.PronForm.null

English: controlled subjects are null (= silent PRO).

theorem Ostrove2026.smpm_overt_pro :

smpmInventory.controlForm = Minimalist.MinimalPronoun.PronForm.pronoun

SMPM: controlled subjects are overt pronouns (= overt PRO). This is the paper's central empirical observation.

theorem Ostrove2026.haitian_null_pro :

haitianInventory.controlForm = Minimalist.MinimalPronoun.PronForm.null

Haitian: controlled subjects are null.

theorem Ostrove2026.quiegolani_overt_pro :

quiegolaniInventory.controlForm = Minimalist.MinimalPronoun.PronForm.pronoun

Quiegolani Zapotec: controlled subjects are overt pronouns.

theorem Ostrove2026.buli_overt_pro :

buliInventory.controlForm = Minimalist.MinimalPronoun.PronForm.pronoun

Büli: controlled subjects are overt pronouns.

theorem Ostrove2026.english_has_reflexive :

englishInventory.realize Minimalist.MinimalPronoun.BVAContext.locallyBound = Minimalist.MinimalPronoun.PronForm.reflexive

English has reflexives distinct from pronouns.

theorem Ostrove2026.smpm_has_reflexive :

smpmInventory.realize Minimalist.MinimalPronoun.BVAContext.locallyBound = Minimalist.MinimalPronoun.PronForm.reflexive

SMPM has reflexives distinct from pronouns (mí + clitic).

theorem Ostrove2026.haitian_no_reflexive :

haitianInventory.realize Minimalist.MinimalPronoun.BVAContext.locallyBound = Minimalist.MinimalPronoun.PronForm.pronoun

Haitian lacks distinct reflexives — reflexives surface as pronouns.

def Ostrove2026.englishSyncretism :

Landau2015.BVASyncretism

Equations

Ostrove2026.englishSyncretism = Landau2015.syncretismFromInventory Ostrove2026.englishInventory "English"

Instances For

def Ostrove2026.quiegolaniSyncretism :

Landau2015.BVASyncretism

Equations

Ostrove2026.quiegolaniSyncretism = Landau2015.syncretismFromInventory Ostrove2026.quiegolaniInventory "Quiegolani Zapotec"

Instances For

def Ostrove2026.haitianSyncretism :

Landau2015.BVASyncretism

Equations

Ostrove2026.haitianSyncretism = Landau2015.syncretismFromInventory Ostrove2026.haitianInventory "Haitian"

Instances For

def Ostrove2026.smpmSyncretism :

Landau2015.BVASyncretism

Equations

Ostrove2026.smpmSyncretism = Landau2015.syncretismFromInventory Ostrove2026.smpmInventory "SMPM"

Instances For

theorem Ostrove2026.english_reflexive_distinct :

englishSyncretism.reflexiveEqReferential = false

theorem Ostrove2026.english_controlled_distinct :

englishSyncretism.controlledEqReferential = false

theorem Ostrove2026.english_boundvar_syncretic :

englishSyncretism.boundVarEqReferential = true

theorem Ostrove2026.quiegolani_reflexive_syncretic :

quiegolaniSyncretism.reflexiveEqReferential = true

theorem Ostrove2026.quiegolani_controlled_syncretic :

quiegolaniSyncretism.controlledEqReferential = true

theorem Ostrove2026.quiegolani_boundvar_syncretic :

quiegolaniSyncretism.boundVarEqReferential = true

theorem Ostrove2026.haitian_reflexive_syncretic :

haitianSyncretism.reflexiveEqReferential = true

theorem Ostrove2026.haitian_controlled_distinct :

haitianSyncretism.controlledEqReferential = false

theorem Ostrove2026.haitian_boundvar_syncretic :

haitianSyncretism.boundVarEqReferential = true

theorem Ostrove2026.smpm_reflexive_distinct :

smpmSyncretism.reflexiveEqReferential = false

theorem Ostrove2026.smpm_controlled_syncretic :

smpmSyncretism.controlledEqReferential = true

theorem Ostrove2026.smpm_boundvar_syncretic :

smpmSyncretism.boundVarEqReferential = true

def Ostrove2026.smpmCopyControlType :

Landau2015.CopyControlType

SMPM instantiates obligatory pronominal copy control: the controlled subject is always an overt clitic pronoun showing the full OC signature. This distinguishes SMPM from:

Full copy control (San Lucas Quievaní Zapotec): full DP copy
Logophoric pronominal (Gengbe, Mandarin): attitude reports only
Scope-sensitive pronominal (Italian, Hungarian): focus-triggered

Equations

Ostrove2026.smpmCopyControlType = Landau2015.CopyControlType.obligatoryPronominal

Instances For

theorem Ostrove2026.smpm_shows_oc :

(Landau2015.copyControlProfile smpmCopyControlType).showsOC = true

theorem Ostrove2026.smpm_not_attitude_only :

(Landau2015.copyControlProfile smpmCopyControlType).attitudeOnly = false

theorem Ostrove2026.smpm_no_scope_operator :

(Landau2015.copyControlProfile smpmCopyControlType).requiresScopeOperator = false

theorem Ostrove2026.smpm_copy_cannot_bear_focus :

(Landau2015.copyControlProfile smpmCopyControlType).copyCanBearFocus = false

Controlled subjects in SMPM cannot bear focus — they must be clitic pronouns, and clitics cannot bear focus (65, 67). This distinguishes SMPM from scope-sensitive pronominal copy control.

theorem Ostrove2026.smpm_controlled_must_be_clitic :

Fragments.Mixtec.SMPM.controlledSubjectMustBeClitic = true

The clitic requirement is derived from the fragment.

def Ostrove2026.smpmExemptProfile :

Landau2015.ExemptAnaphorProfile

SMPM exempt anaphor profile, derived from fragment data.

Exempt anaphors (reflexive forms used as possessors, outside Condition A domain) ARE available in SMPM (74) but CANNOT have quantified antecedents (75, 78).

Equations

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

Instances For

theorem Ostrove2026.smpm_has_exempt_anaphors :

smpmExemptProfile.hasExemptAnaphors = true

theorem Ostrove2026.smpm_no_quantified_exempt :

smpmExemptProfile.allowsQuantifiedAntecedent = false

def Ostrove2026.smpmExemptAvailableWithQuantifiedController :

Bool

The argument against movement (§6, pp.26–31):

Given: exempt anaphors cannot have quantified antecedents (78).

Movement analysis predicts: if the controller is quantified (e.g., "every dog"), the copy in embedded subject position IS the quantifier. An exempt anaphor in the embedded clause would need to be bound by this quantified copy → predicted UNAVAILABLE.

Base-generation analysis predicts: the pronoun in embedded subject position is a genuine pronoun (base-generated), not a copy of the quantifier. An exempt anaphor can take this pronoun as antecedent → predicted AVAILABLE.

SMPM data (86–87): exempt anaphors ARE available in untensed subjunctives with quantified controllers.

Tá'iin'iin tsǐnà kìxà [tsìi =rí ndò'ò mí =rí]. 'Each dog started to bite its own tail.'
Kò xíniñu'u ni'iin =rà bálí [kòni =rà táta mí =rà]. 'No boy needs to see his own father.'

This matches the base-generation prediction.

Equations

Ostrove2026.smpmExemptAvailableWithQuantifiedController = true

Instances For

theorem Ostrove2026.movement_incorrectly_predicts :

Landau2015.predictsExemptWithQuantifiedController Landau2015.ControlDerivation.movement = false

theorem Ostrove2026.basegeneration_correctly_predicts :

Landau2015.predictsExemptWithQuantifiedController Landau2015.ControlDerivation.baseGeneration = true

theorem Ostrove2026.smpm_supports_basegeneration :

smpmExemptAvailableWithQuantifiedController = Landau2015.predictsExemptWithQuantifiedController Landau2015.ControlDerivation.baseGeneration

def Ostrove2026.smpmProfile :

Phenomena.NullSubject.ProDropProfile

SMPM profile derived from fragment data and inventory.

Equations

Ostrove2026.smpmProfile = { allowsProDrop := Fragments.Mixtec.SMPM.allowsProDrop, hasOvertPRO := decide Ostrove2026.smpmInventory.hasOvertPRO }

Instances For

def Ostrove2026.englishProfile :

Phenomena.NullSubject.ProDropProfile

Equations

Ostrove2026.englishProfile = { allowsProDrop := false, hasOvertPRO := decide Ostrove2026.englishInventory.hasOvertPRO }

Instances For

def Ostrove2026.buliProfile :

Phenomena.NullSubject.ProDropProfile

Equations

Ostrove2026.buliProfile = { allowsProDrop := false, hasOvertPRO := decide Ostrove2026.buliInventory.hasOvertPRO }

Instances For

theorem Ostrove2026.smpm_satisfies_universal :

smpmProfile.Satisfies

theorem Ostrove2026.english_satisfies_universal :

englishProfile.Satisfies

theorem Ostrove2026.buli_satisfies_universal :

buliProfile.Satisfies

theorem Ostrove2026.smpm_classified :

smpmProfile.classify = Phenomena.NullSubject.Typology.overtPRONoProDrop

theorem Ostrove2026.english_classified :

englishProfile.classify = Phenomena.NullSubject.Typology.nullPRONoProDrop

theorem Ostrove2026.buli_classified :

buliProfile.classify = Phenomena.NullSubject.Typology.overtPRONoProDrop

def Ostrove2026.smpmToNoonan :

Fragments.Mixtec.SMPM.EmbeddedClauseType → Typology.Complementation.NoonanCompType

SMPM clause types map to @cite{noonan-2007}'s complement typology.

Finite embedded → indicative complement (unrestricted TAM)
Tensed subjunctive → subjunctive complement (irrealis only)
Untensed subjunctive → subjunctive complement (irrealis, with equi-deletion / obligatory coreference)

All three are "balanced" in Noonan's terms — SMPM lacks morphologically nonfinite predicates entirely.

Equations

Instances For

def Ostrove2026.smpmCTPClass :

Fragments.Mixtec.SMPM.EmbeddedClauseType → List Typology.Complementation.CTPClass

SMPM's CTP classes map to Noonan's CTP classes.

The paper's predicate lists (27a–c) align with Noonan's semantic classification:

Finite embedded (27a):

utterance: say (kà'àn), said (káchi), chat (ntatǔ'un)
propAttitude: think (ka'án), believe (nakanini)
commentative: be happy (kusijǐ ini), be sad (ntsi'i ini), regret (ntsiko ini)
knowledge: know (kòni), wonder (kuntàà ini)

Tensed subjunctive (27b):

desiderative: want (kòni), hope (ntatu), pray (nakwatu), agree (xiinka), refuse (xǐunka). 'Hate' (sǐso ini), 'be afraid' (iyì'bí), 'be scared' (kuntasí) are emotive predicates but select irrealis complements in SMPM, functioning like desideratives. 'Get the idea' (chikàà ini) is cognitive.

Untensed subjunctive (27c):

phasal: start (kìxà), finish (ntsi'i), stop (xikwīn), continue (kò xikwīn)
achievement: try (ntùkú), remember (nàkú'ún), forget (nantōso)
modal: need (xiniñu'u)
desiderative: like to (kutō)
knowledge: know how to (kòni xá kasa), learn how to (sakwā'a)
negative: not bother (kò ntaa)

Equations

One or more equations did not get rendered due to their size.
Ostrove2026.smpmCTPClass Fragments.Mixtec.SMPM.EmbeddedClauseType.tensedSubjunctive = [Typology.Complementation.CTPClass.desiderative]

Instances For

theorem Ostrove2026.desiderative_is_irrealis :

Typology.Complementation.ctpRealityStatus Typology.Complementation.CTPClass.desiderative = Typology.Complementation.RealityStatus.irrealis

Noonan's reality status predicts SMPM clause type selection.

Irrealis CTPs select subjunctive complements (tensed or untensed); realis CTPs select indicative (finite embedded) complements.

This holds for the core cases: desiderative (want, hope) is irrealis and selects tensed subjunctive; phasal (start, stop) is realis but selects untensed subjunctive — an apparent exception that reflects the restructuring/monoclausal nature of phasal predicates.

theorem Ostrove2026.achievement_is_irrealis :

Typology.Complementation.ctpRealityStatus Typology.Complementation.CTPClass.achievement = Typology.Complementation.RealityStatus.irrealis

theorem Ostrove2026.utterance_is_realis :

Typology.Complementation.ctpRealityStatus Typology.Complementation.CTPClass.utterance = Typology.Complementation.RealityStatus.realis

theorem Ostrove2026.propAttitude_is_realis :

Typology.Complementation.ctpRealityStatus Typology.Complementation.CTPClass.propAttitude = Typology.Complementation.RealityStatus.realis