Documentation

Linglib.Studies.Ostrove2026

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

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 ([Kra09b], [Saf14], [Lan15]): 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 [Lan04a]'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 #

[Wur14]'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 :

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

theorem Ostrove2026.tensed_restricted_tam :

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

theorem Ostrove2026.untensed_restricted_tam :

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

theorem Ostrove2026.finite_allows_noncoreferential :

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

theorem Ostrove2026.tensed_allows_noncoreferential :

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

theorem Ostrove2026.untensed_no_noncoreferential :

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

theorem Ostrove2026.untensed_restructuring :

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

theorem Ostrove2026.tensed_no_restructuring :

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

theorem Ostrove2026.finite_no_restructuring :

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

def Ostrove2026.smpmProfile (c : Mixtec.SMPM.EmbeddedClauseType) :

Control.Profile Landau2013.Clause74

The control signature of each SMPM clause type, from clauseProperties.noncoreferentialSubject via Landau2013.ofNoncoreferential — the same derivation Allotey2021.gaProfile uses for Gã.

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

Ostrove2026.smpmProfile c = Landau2013.ofNoncoreferential (Mixtec.SMPM.clauseProperties c).noncoreferentialSubject

Instances For

theorem Ostrove2026.untensed_is_OC :

(smpmProfile Mixtec.SMPM.EmbeddedClauseType.untensedSubjunctive).IsObligatory

theorem Ostrove2026.tensed_not_OC :

¬(smpmProfile Mixtec.SMPM.EmbeddedClauseType.tensedSubjunctive).IsObligatory

theorem Ostrove2026.finite_not_OC :

¬(smpmProfile Mixtec.SMPM.EmbeddedClauseType.finiteEmbedded).IsObligatory

def Ostrove2026.wurmbrandToSubjunctive :

Minimalist.InfinitivalTenseClass → Option Mixtec.SMPM.EmbeddedClauseType

SMPM's two subjunctive types correspond to [Wur14]'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.InfinitivalTenseClass → Bool

Whether a Wurmbrand class involves obligatory control.

Equations

Instances For

theorem Ostrove2026.wurmbrand_predicts_control (w : Minimalist.InfinitivalTenseClass) (c : Mixtec.SMPM.EmbeddedClauseType) :

c ∈ wurmbrandToSubjunctive w → ((smpmProfile c).IsObligatory ↔ wurmbrandHasOC w = true)

For the Wurmbrand classes with SMPM correspondents, the mapping correctly predicts control properties.

theorem Ostrove2026.wurmbrand_propositional_no_correspondent :

wurmbrandToSubjunctive Minimalist.InfinitivalTenseClass.propositional = none

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

def Ostrove2026.landauToSMPM :

Control.ClauseClass → Mixtec.SMPM.EmbeddedClauseType

SMPM clause types map onto [Lan04a]'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.smpmToLandau (c : Mixtec.SMPM.EmbeddedClauseType) :

Control.ClauseClass

The forward direction, derived from the fragment's TAM observables via ClauseClass.ofFiniteness (the same derivation as Allotey2021.gaToLandau).

Equations

Ostrove2026.smpmToLandau c = Control.ClauseClass.ofFiniteness (Mixtec.SMPM.clauseProperties c).unrestrictedTAM (Mixtec.SMPM.clauseProperties c).independentTense

Instances For

theorem Ostrove2026.smpmToLandau_landauToSMPM (c : Control.ClauseClass) :

smpmToLandau (landauToSMPM c) = c

The stipulated table landauToSMPM is a section of the derived classification: SMPM realizes every position of [Lan04a]'s scale (contrast Allotey2021.ga_no_fSubjunctive).

def Ostrove2026.smpmLandauAgr :

Control.ClauseClass → 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 [Lan15]), [+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 : Control.ClauseClass) :

(smpmProfile (landauToSMPM c)).IsObligatory ↔ c.HasOC (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 ([DM94]).

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 ([Bla94a]).

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 [Sul21]).

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 :

Minimalist.MinimalPronoun.BVASyncretism

Equations

Ostrove2026.englishSyncretism = Minimalist.MinimalPronoun.syncretismFromInventory Ostrove2026.englishInventory "English"

Instances For

def Ostrove2026.quiegolaniSyncretism :

Minimalist.MinimalPronoun.BVASyncretism

Equations

Ostrove2026.quiegolaniSyncretism = Minimalist.MinimalPronoun.syncretismFromInventory Ostrove2026.quiegolaniInventory "Quiegolani Zapotec"

Instances For

def Ostrove2026.haitianSyncretism :

Minimalist.MinimalPronoun.BVASyncretism

Equations

Ostrove2026.haitianSyncretism = Minimalist.MinimalPronoun.syncretismFromInventory Ostrove2026.haitianInventory "Haitian"

Instances For

def Ostrove2026.smpmSyncretism :

Minimalist.MinimalPronoun.BVASyncretism

Equations

Ostrove2026.smpmSyncretism = Minimalist.MinimalPronoun.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

inductive Ostrove2026.CopyControlType :

The paper's four-way typology of copy control (§5, its own coinage of all four labels). [PP06] supply the definition of copy control — an overt element in the controlled position — and attest three cases (Assamese, San Lucas Quiaviní Zapotec, Tongan), noting that the Zapotec and Assamese patterns are themselves obligatory control. The types split two ways: full-copy vs. pronominal copy control (CopyControlType.isPronominal), the latter three-way by trigger. What distinguishes the obligatory-pronominal type is unconditional overtness (CopyControlType.unconditionallyOvert) — the scope-sensitive type alternates with null PRO in the same OC configurations ((60)).

fullCopy : CopyControlType
Full copy: the controlled subject is a full DP copy of the controller (San Lucas Quiaviní Zapotec; Copala Triqui).
logophoricPronominal : CopyControlType
Logophoric pronominal: an overt pronoun, in attitude reports only (Gengbe, Mandarin — whose PRO status Li 2021 doubts, per the paper).
scopeSensitivePronominal : CopyControlType
Scope-sensitive pronominal: an overt pronoun triggered by scope-taking operators, alternating with null PRO otherwise (Italian, Hungarian, European Portuguese).
obligatoryPronominal : CopyControlType
Obligatory pronominal: an unconditionally overt pronoun in all control contexts (SMPM; Gã, [All21]; Bùlì, [Sul21]).

Instances For

@[instance_reducible]

instance Ostrove2026.instDecidableEqCopyControlType :

DecidableEq CopyControlType

Equations

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

@[instance_reducible]

instance Ostrove2026.instReprCopyControlType :

Repr CopyControlType

Equations

Ostrove2026.instReprCopyControlType = { reprPrec := Ostrove2026.instReprCopyControlType.repr }

def Ostrove2026.instReprCopyControlType.repr :

CopyControlType → ℕ → Std.Format

Equations

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

Instances For

def Ostrove2026.CopyControlType.isPronominal :

CopyControlType → Bool

The typology's first cut: pronominal vs. full-copy copy control.

Equations

Ostrove2026.CopyControlType.fullCopy.isPronominal = false
x✝.isPronominal = true

Instances For

def Ostrove2026.CopyControlType.unconditionallyOvert :

CopyControlType → Bool

The obligatory-pronominal type's distinguishing property: overtness is unconditional, not contingent on attitudehood or a scope trigger.

Equations

Ostrove2026.CopyControlType.obligatoryPronominal.unconditionallyOvert = true
x✝.unconditionallyOvert = false

Instances For

def Ostrove2026.smpmCopyControlType :

CopyControlType

SMPM instantiates obligatory pronominal copy control: the controlled subject is always an overt clitic pronoun showing the full OC signature. Controlled subjects cannot bear focus — they must be clitic pronouns, and clitics cannot bear focus ((65)/(67), smpm_controlled_must_be_clitic) — which separates SMPM from the scope-sensitive type.

Equations

Ostrove2026.smpmCopyControlType = Ostrove2026.CopyControlType.obligatoryPronominal

Instances For

theorem Ostrove2026.smpm_controlled_must_be_clitic (p : PersonalPronoun) :

p ∈ Mixtec.SMPM.strongSeries → ∀ s ∈ p.strength, Mixtec.SMPM.controlledSubjectStrength < s

The clitic requirement, derived from the fragment and routed through the Cardinaletti–Starke deficiency order: the required controlled-subject class is strictly more deficient than every entry of the non-clitic series ((67)).

theorem Ostrove2026.smpm_has_exempt_anaphors :

Mixtec.SMPM.exemptAnaphorsAsPossessors = true

Exempt anaphors (reflexive forms used as possessors, outside the Condition A domain) are available in SMPM (74).

theorem Ostrove2026.smpm_no_quantified_exempt :

Mixtec.SMPM.exemptAnaphorAllowsQuantifiedAntecedent = false

SMPM exempt anaphors cannot have quantified antecedents (75, 78).

inductive Ostrove2026.Ex86Item :

The occupants of the (86)–(87) configurations.

quantifierDP : Ex86Item
the quantified controller ('each dog', 'no boy')
pronoun : Ex86Item
the overt controlled clitic anteceding the exempt anaphor

Instances For

@[instance_reducible]

instance Ostrove2026.instDecidableEqEx86Item :

DecidableEq Ex86Item

Equations

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

@[instance_reducible]

instance Ostrove2026.instReprEx86Item :

Equations

Ostrove2026.instReprEx86Item = { reprPrec := Ostrove2026.instReprEx86Item.repr }

def Ostrove2026.instReprEx86Item.repr :

Ex86Item → ℕ → Std.Format

Equations

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

Instances For

def Ostrove2026.ex86Dependency :

SetRel (Fin 2) (Fin 2)

The (86)–(87) control dependency: quantified controller position 0 to embedded clitic position 1.

Equations

Ostrove2026.ex86Dependency = {(0, 1)}

Instances For

def Ostrove2026.ex86Occupant :

Fin 2 → Ex86Item

The attested occupants: exempt anaphors reject quantified antecedents ((78)), yet they are available in untensed subjunctives with quantified controllers ((86)–(87)) — so the embedded position holds a genuine referential pronoun, not a quantifier copy.

Equations

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

Instances For

theorem Ostrove2026.smpm_refutes_movement :

¬Control.IsExhaustive ex86Occupant ex86Dependency

Movement is token identity, and the (86)–(87) occupants differ across the dependency — movement is refuted (§6, pp. 26–31): SMPM control is base-generated.

theorem Ostrove2026.smpm_satisfies_universal :

smpmInventory.OvertPROUniversal Mixtec.SMPM.allowsProDrop

SMPM instantiates the universal: overt PRO and no pro-drop (the fragment's flag).

theorem Ostrove2026.english_satisfies_universal (proDrop : Bool) :

englishInventory.OvertPROUniversal proDrop

English satisfies the universal vacuously, whatever its pro-drop status: its PRO is null.

theorem Ostrove2026.buli_satisfies_universal :

buliInventory.OvertPROUniversal false

Büli instantiates the universal: overt PRO and no pro-drop.

def Ostrove2026.smpmToNoonan :

Mixtec.SMPM.EmbeddedClauseType → Complement.Coding

SMPM clause types map to [Noo07]'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 :

Mixtec.SMPM.EmbeddedClauseType → List 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

Instances For

theorem Ostrove2026.desiderative_is_irrealis :

ctpRealityStatus CTPClass.desiderative = 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 :

ctpRealityStatus CTPClass.achievement = RealityStatus.irrealis

theorem Ostrove2026.utterance_is_realis :

ctpRealityStatus CTPClass.utterance = RealityStatus.realis

theorem Ostrove2026.propAttitude_is_realis :

ctpRealityStatus CTPClass.propAttitude = RealityStatus.realis

[Ost26] groups SMPM with Gã ([All21]) and Büli ([Sul21]) as obligatory-pronominal copy control languages. The Gã fragment and study predate this paper, so the cross-language bridges live here (chronology: the later paper draws the comparison), consuming Studies/Allotey2021.lean.

def Ostrove2026.gaCopyControlType :

CopyControlType

Gã instantiates obligatory pronominal copy control: the controlled subject of an irrealis ni-clause is always an overt subject proclitic showing the full OC signature ([All21]).

Equations

Ostrove2026.gaCopyControlType = Ostrove2026.CopyControlType.obligatoryPronominal

Instances For

theorem Ostrove2026.ga_same_copy_type_as_smpm :

gaCopyControlType = smpmCopyControlType

Gã and SMPM occupy the same copy-control cell.

def Ostrove2026.gaSyncretism :

Minimalist.MinimalPronoun.BVASyncretism

Gã syncretism row, derived from the Allotey2021 inventory: reflexive ×, controlled =, bound variable = .

Equations

Ostrove2026.gaSyncretism = Minimalist.MinimalPronoun.syncretismFromInventory Allotey2021.gaInventory "Gã"

Instances For

theorem Ostrove2026.ga_syncretism_matches_smpm :

(gaSyncretism.reflexiveEqReferential, gaSyncretism.controlledEqReferential, gaSyncretism.boundVarEqReferential) = (smpmSyncretism.reflexiveEqReferential, smpmSyncretism.controlledEqReferential, smpmSyncretism.boundVarEqReferential)

Gã patterns with SMPM in the syncretism typology: distinct reflexive, but controlled subjects and bound variables syncretic with the referential pronoun.

theorem Ostrove2026.ga_patterns_with_smpm :

Allotey2021.gaInventory.controlForm = smpmInventory.controlForm ∧ Ga.allowsProDrop = Mixtec.SMPM.allowsProDrop

Gã sits in the same cell of the overt-PRO / pro-drop typology as SMPM: identical controlled-subject realization, identical pro-drop status.

theorem Ostrove2026.ga_deranked_where_smpm_balanced :

(Allotey2021.gaToNoonan Ga.EmbeddedClauseType.irrealisNi).isReduced = true ∧ ∀ (c : Mixtec.SMPM.EmbeddedClauseType), (smpmToNoonan c).isReduced = false

Where the two overt-PRO languages part ways in [Noo07]'s typology: SMPM's complements are all balanced (finite or subjunctive), while Gã's control complement is a deranked bare-root infinitive.