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 Phenomena.Control.Studies.Ostrove2026.finite_unrestricted_tam :

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

theorem Phenomena.Control.Studies.Ostrove2026.tensed_restricted_tam :

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

theorem Phenomena.Control.Studies.Ostrove2026.untensed_restricted_tam :

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

theorem Phenomena.Control.Studies.Ostrove2026.finite_allows_noncoreferential :

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

theorem Phenomena.Control.Studies.Ostrove2026.tensed_allows_noncoreferential :

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

theorem Phenomena.Control.Studies.Ostrove2026.untensed_no_noncoreferential :

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

theorem Phenomena.Control.Studies.Ostrove2026.untensed_restructuring :

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

theorem Phenomena.Control.Studies.Ostrove2026.tensed_no_restructuring :

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

theorem Phenomena.Control.Studies.Ostrove2026.finite_no_restructuring :

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

def Phenomena.Control.Studies.Ostrove2026.smpmOCSignature :

Fragments.Mixtec.SMPM.ClauseType → Syntax.Minimalism.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 Phenomena.Control.Studies.Ostrove2026.untensed_is_OC :

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

theorem Phenomena.Control.Studies.Ostrove2026.tensed_not_OC :

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

theorem Phenomena.Control.Studies.Ostrove2026.finite_not_OC :

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

def Phenomena.Control.Studies.Ostrove2026.wurmbrandToSubjunctive :

Minimalism.Tense.InfinitivalTense.InfinitivalTenseClass → Option Fragments.Mixtec.SMPM.ClauseType

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 Phenomena.Control.Studies.Ostrove2026.wurmbrandHasOC :

Minimalism.Tense.InfinitivalTense.InfinitivalTenseClass → Bool

Whether a Wurmbrand class involves obligatory control.

Equations

Instances For

theorem Phenomena.Control.Studies.Ostrove2026.wurmbrand_predicts_control_futureIrrealis :

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

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

theorem Phenomena.Control.Studies.Ostrove2026.wurmbrand_predicts_control_restructuring :

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

theorem Phenomena.Control.Studies.Ostrove2026.wurmbrand_propositional_no_correspondent :

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

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

def Phenomena.Control.Studies.Ostrove2026.landauToSMPM :

Landau2015.LandauClauseClass → Fragments.Mixtec.SMPM.ClauseType

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 Phenomena.Control.Studies.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 Phenomena.Control.Studies.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 Phenomena.Control.Studies.Ostrove2026.englishInventory :

Syntax.Minimalism.MinimalPronoun.MinPronInventory Syntax.Minimalism.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 Phenomena.Control.Studies.Ostrove2026.haitianInventory :

Syntax.Minimalism.MinimalPronoun.MinPronInventory Syntax.Minimalism.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 Phenomena.Control.Studies.Ostrove2026.smpmInventory :

Syntax.Minimalism.MinimalPronoun.MinPronInventory Syntax.Minimalism.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 Phenomena.Control.Studies.Ostrove2026.quiegolaniInventory :

Syntax.Minimalism.MinimalPronoun.MinPronInventory Syntax.Minimalism.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

Phenomena.Control.Studies.Ostrove2026.quiegolaniInventory = { items := [], elsewhere := Syntax.Minimalism.MinimalPronoun.PronForm.pronoun }

Instances For

def Phenomena.Control.Studies.Ostrove2026.gaInventory :

Syntax.Minimalism.MinimalPronoun.MinPronInventory Syntax.Minimalism.MinimalPronoun.PronForm

Gã vocabulary items (inferred from @cite{allotey-2021}).

Like SMPM: lacks a null allomorph for controlled subjects. Overt PRO in complement clause obligatory control. One of three languages argued to have obligatory pronominal copy control.

Equations

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

Instances For

def Phenomena.Control.Studies.Ostrove2026.buliInventory :

Syntax.Minimalism.MinimalPronoun.MinPronInventory Syntax.Minimalism.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

Phenomena.Control.Studies.Ostrove2026.buliInventory = { items := [], elsewhere := Syntax.Minimalism.MinimalPronoun.PronForm.pronoun }

Instances For

theorem Phenomena.Control.Studies.Ostrove2026.english_null_pro :

englishInventory.controlForm = Syntax.Minimalism.MinimalPronoun.PronForm.null

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

theorem Phenomena.Control.Studies.Ostrove2026.smpm_overt_pro :

smpmInventory.controlForm = Syntax.Minimalism.MinimalPronoun.PronForm.pronoun

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

theorem Phenomena.Control.Studies.Ostrove2026.haitian_null_pro :

haitianInventory.controlForm = Syntax.Minimalism.MinimalPronoun.PronForm.null

Haitian: controlled subjects are null.

theorem Phenomena.Control.Studies.Ostrove2026.quiegolani_overt_pro :

quiegolaniInventory.controlForm = Syntax.Minimalism.MinimalPronoun.PronForm.pronoun

Quiegolani Zapotec: controlled subjects are overt pronouns.

theorem Phenomena.Control.Studies.Ostrove2026.ga_overt_pro :

gaInventory.controlForm = Syntax.Minimalism.MinimalPronoun.PronForm.pronoun

Gã: controlled subjects are overt pronouns.

theorem Phenomena.Control.Studies.Ostrove2026.buli_overt_pro :

buliInventory.controlForm = Syntax.Minimalism.MinimalPronoun.PronForm.pronoun

Büli: controlled subjects are overt pronouns.

theorem Phenomena.Control.Studies.Ostrove2026.english_has_reflexive :

englishInventory.realize Syntax.Minimalism.MinimalPronoun.BVAContext.locallyBound = Syntax.Minimalism.MinimalPronoun.PronForm.reflexive

English has reflexives distinct from pronouns.

theorem Phenomena.Control.Studies.Ostrove2026.smpm_has_reflexive :

smpmInventory.realize Syntax.Minimalism.MinimalPronoun.BVAContext.locallyBound = Syntax.Minimalism.MinimalPronoun.PronForm.reflexive

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

theorem Phenomena.Control.Studies.Ostrove2026.haitian_no_reflexive :

haitianInventory.realize Syntax.Minimalism.MinimalPronoun.BVAContext.locallyBound = Syntax.Minimalism.MinimalPronoun.PronForm.pronoun

Haitian lacks distinct reflexives — reflexives surface as pronouns.

def Phenomena.Control.Studies.Ostrove2026.englishSyncretism :

Landau2015.BVASyncretism

Equations

Phenomena.Control.Studies.Ostrove2026.englishSyncretism = Phenomena.Control.Studies.Landau2015.syncretismFromInventory Phenomena.Control.Studies.Ostrove2026.englishInventory "English"

Instances For

def Phenomena.Control.Studies.Ostrove2026.quiegolaniSyncretism :

Landau2015.BVASyncretism

Equations

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

Instances For

def Phenomena.Control.Studies.Ostrove2026.haitianSyncretism :

Landau2015.BVASyncretism

Equations

Phenomena.Control.Studies.Ostrove2026.haitianSyncretism = Phenomena.Control.Studies.Landau2015.syncretismFromInventory Phenomena.Control.Studies.Ostrove2026.haitianInventory "Haitian"

Instances For

def Phenomena.Control.Studies.Ostrove2026.smpmSyncretism :

Landau2015.BVASyncretism

Equations

Phenomena.Control.Studies.Ostrove2026.smpmSyncretism = Phenomena.Control.Studies.Landau2015.syncretismFromInventory Phenomena.Control.Studies.Ostrove2026.smpmInventory "SMPM"

Instances For

theorem Phenomena.Control.Studies.Ostrove2026.english_reflexive_distinct :

englishSyncretism.reflexiveEqReferential = false

theorem Phenomena.Control.Studies.Ostrove2026.english_controlled_distinct :

englishSyncretism.controlledEqReferential = false

theorem Phenomena.Control.Studies.Ostrove2026.english_boundvar_syncretic :

englishSyncretism.boundVarEqReferential = true

theorem Phenomena.Control.Studies.Ostrove2026.quiegolani_reflexive_syncretic :

quiegolaniSyncretism.reflexiveEqReferential = true

theorem Phenomena.Control.Studies.Ostrove2026.quiegolani_controlled_syncretic :

quiegolaniSyncretism.controlledEqReferential = true

theorem Phenomena.Control.Studies.Ostrove2026.quiegolani_boundvar_syncretic :

quiegolaniSyncretism.boundVarEqReferential = true

theorem Phenomena.Control.Studies.Ostrove2026.haitian_reflexive_syncretic :

haitianSyncretism.reflexiveEqReferential = true

theorem Phenomena.Control.Studies.Ostrove2026.haitian_controlled_distinct :

haitianSyncretism.controlledEqReferential = false

theorem Phenomena.Control.Studies.Ostrove2026.haitian_boundvar_syncretic :

haitianSyncretism.boundVarEqReferential = true

theorem Phenomena.Control.Studies.Ostrove2026.smpm_reflexive_distinct :

smpmSyncretism.reflexiveEqReferential = false

theorem Phenomena.Control.Studies.Ostrove2026.smpm_controlled_syncretic :

smpmSyncretism.controlledEqReferential = true

theorem Phenomena.Control.Studies.Ostrove2026.smpm_boundvar_syncretic :

smpmSyncretism.boundVarEqReferential = true

def Phenomena.Control.Studies.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

Phenomena.Control.Studies.Ostrove2026.smpmCopyControlType = Phenomena.Control.Studies.Landau2015.CopyControlType.obligatoryPronominal

Instances For

theorem Phenomena.Control.Studies.Ostrove2026.smpm_shows_oc :

(Landau2015.copyControlProfile smpmCopyControlType).showsOC = true

theorem Phenomena.Control.Studies.Ostrove2026.smpm_not_attitude_only :

(Landau2015.copyControlProfile smpmCopyControlType).attitudeOnly = false

theorem Phenomena.Control.Studies.Ostrove2026.smpm_no_scope_operator :

(Landau2015.copyControlProfile smpmCopyControlType).requiresScopeOperator = false

theorem Phenomena.Control.Studies.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 Phenomena.Control.Studies.Ostrove2026.smpm_controlled_must_be_clitic :

Fragments.Mixtec.SMPM.controlledSubjectMustBeClitic = true

The clitic requirement is derived from the fragment.

def Phenomena.Control.Studies.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 Phenomena.Control.Studies.Ostrove2026.smpm_has_exempt_anaphors :

smpmExemptProfile.hasExemptAnaphors = true

theorem Phenomena.Control.Studies.Ostrove2026.smpm_no_quantified_exempt :

smpmExemptProfile.allowsQuantifiedAntecedent = false

def Phenomena.Control.Studies.Ostrove2026.smpmExemptAvailableWithQuantifiedController :

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

Phenomena.Control.Studies.Ostrove2026.smpmExemptAvailableWithQuantifiedController = true

Instances For

theorem Phenomena.Control.Studies.Ostrove2026.movement_incorrectly_predicts :

Landau2015.predictsExemptWithQuantifiedController Landau2015.ControlDerivation.movement = false

theorem Phenomena.Control.Studies.Ostrove2026.basegeneration_correctly_predicts :

Landau2015.predictsExemptWithQuantifiedController Landau2015.ControlDerivation.baseGeneration = true

theorem Phenomena.Control.Studies.Ostrove2026.smpm_supports_basegeneration :

smpmExemptAvailableWithQuantifiedController = Landau2015.predictsExemptWithQuantifiedController Landau2015.ControlDerivation.baseGeneration

structure Phenomena.Control.Studies.Ostrove2026.ProDropProfile :

A language's pro-drop and overt-PRO profile.

@cite{ostrove-2026} (54): If a language requires the subject of obligatory control clauses (i.e., PRO) to be overt, then that language will not allow pro-drop.

This is a one-way implicational universal — non-pro-drop does not entail overt PRO (English is non-pro-drop but has null PRO).

language : String
allowsProDrop : Bool
hasOvertPRO : Bool

Instances For

def Phenomena.Control.Studies.Ostrove2026.instDecidableEqProDropProfile.decEq (x✝ x✝¹ : ProDropProfile) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

instance Phenomena.Control.Studies.Ostrove2026.instDecidableEqProDropProfile :

DecidableEq ProDropProfile

Equations

Phenomena.Control.Studies.Ostrove2026.instDecidableEqProDropProfile = Phenomena.Control.Studies.Ostrove2026.instDecidableEqProDropProfile.decEq

instance Phenomena.Control.Studies.Ostrove2026.instBEqProDropProfile :

BEq ProDropProfile

Equations

Phenomena.Control.Studies.Ostrove2026.instBEqProDropProfile = { beq := Phenomena.Control.Studies.Ostrove2026.instBEqProDropProfile.beq }

def Phenomena.Control.Studies.Ostrove2026.instBEqProDropProfile.beq :

ProDropProfile → ProDropProfile → Bool

Equations

One or more equations did not get rendered due to their size.
Phenomena.Control.Studies.Ostrove2026.instBEqProDropProfile.beq x✝¹ x✝ = false

Instances For

def Phenomena.Control.Studies.Ostrove2026.instReprProDropProfile.repr :

ProDropProfile → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Control.Studies.Ostrove2026.instReprProDropProfile :

Repr ProDropProfile

Equations

Phenomena.Control.Studies.Ostrove2026.instReprProDropProfile = { reprPrec := Phenomena.Control.Studies.Ostrove2026.instReprProDropProfile.repr }

def Phenomena.Control.Studies.Ostrove2026.satisfiesImplicational (p : ProDropProfile) :

The implicational universal: overt PRO → non-pro-drop.

Equations

Phenomena.Control.Studies.Ostrove2026.satisfiesImplicational p = (!p.hasOvertPRO || !p.allowsProDrop)

Instances For

def Phenomena.Control.Studies.Ostrove2026.hasOvertPRO (inv : Syntax.Minimalism.MinimalPronoun.MinPronInventory Syntax.Minimalism.MinimalPronoun.PronForm) :

Whether the inventory produces overt PRO (i.e., controlled form = pronoun).

Equations

Phenomena.Control.Studies.Ostrove2026.hasOvertPRO inv = (inv.controlForm == Syntax.Minimalism.MinimalPronoun.PronForm.pronoun)

Instances For

def Phenomena.Control.Studies.Ostrove2026.smpmProfile :

SMPM profile derived from fragment data and inventory.

Equations

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

Instances For

def Phenomena.Control.Studies.Ostrove2026.englishProfile :

Equations

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

Instances For

theorem Phenomena.Control.Studies.Ostrove2026.overt_pro_non_prodrop_satisfies (p : ProDropProfile) (h_overt : p.hasOvertPRO = true) (h_prodrop : p.allowsProDrop = false) :

satisfiesImplicational p = true

The universal is satisfied when overt PRO + non-pro-drop (consequent true).

theorem Phenomena.Control.Studies.Ostrove2026.null_pro_satisfies (p : ProDropProfile) (h_null : p.hasOvertPRO = false) :

satisfiesImplicational p = true

The universal is trivially satisfied when PRO is null (antecedent false).

theorem Phenomena.Control.Studies.Ostrove2026.smpm_satisfies_universal :

satisfiesImplicational smpmProfile = true

theorem Phenomena.Control.Studies.Ostrove2026.english_satisfies_universal :

satisfiesImplicational englishProfile = true

theorem Phenomena.Control.Studies.Ostrove2026.ga_satisfies_universal :

satisfiesImplicational { language := "Gã", allowsProDrop := false, hasOvertPRO := hasOvertPRO gaInventory } = true

theorem Phenomena.Control.Studies.Ostrove2026.buli_satisfies_universal :

satisfiesImplicational { language := "Büli", allowsProDrop := false, hasOvertPRO := hasOvertPRO buliInventory } = true

def Phenomena.Control.Studies.Ostrove2026.smpmToNoonan :

Fragments.Mixtec.SMPM.ClauseType → Complementation.Typology.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 Phenomena.Control.Studies.Ostrove2026.smpmCTPClass :

Fragments.Mixtec.SMPM.ClauseType → List Complementation.Typology.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.
Phenomena.Control.Studies.Ostrove2026.smpmCTPClass Fragments.Mixtec.SMPM.ClauseType.tensedSubjunctive = [Phenomena.Complementation.Typology.CTPClass.desiderative ]

Instances For

theorem Phenomena.Control.Studies.Ostrove2026.desiderative_is_irrealis :

Complementation.Typology.ctpRealityStatus Complementation.Typology.CTPClass.desiderative = Complementation.Typology.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 Phenomena.Control.Studies.Ostrove2026.achievement_is_irrealis :

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

theorem Phenomena.Control.Studies.Ostrove2026.utterance_is_realis :

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

theorem Phenomena.Control.Studies.Ostrove2026.propAttitude_is_realis :

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