Allotey (2021): Overt Pronouns of Infinitival Predicates of Gã

Formalizes [All21]: obligatory control into Gã irrealis ni-clauses requires an overt subject proclitic — null PRO is ungrammatical. The controlled clause is non-finite irrealis, not subjunctive (against [KD04], [Cam17], [Kor17]); the pronoun is a Spec-TP subject valued by Long Distance Agree across the weak C head ni ([Sza09], [Riz97]) and pronounced to host the obligatory irrealis high tone. The Movement Theory of Control ([Hor99]) does not extend to Gã, and [Sat19]'s left-periphery-bound pronoun only partly does. The verb-movement/negation diagnostics (§§5.5.5, 6.2, after [Pol89]) need phrase-structure substrate and are not formalized.

References

• D. Allotey, Overt Pronouns of Infinitival Predicates of Gã

OC by clause type

def Allotey2021.gaProfile (c : Ga.EmbeddedClauseType) : Control.Profile Landau2013.Clause74

The control profile of a Gã clause type, from its noncoreference flag (the derivation Ostrove2026.smpmProfile also uses).

Equations

• Allotey2021.gaProfile c = Landau2013.ofNoncoreferential (Ga.clauseProperties c).noncoreferentialSubject

theorem Allotey2021.obligatory_iff_not_isFinite (c : Ga.EmbeddedClauseType) : (gaProfile c).IsObligatory ↔ (Ga.clauseComplementizer c).isFinite = false

OC status is read off the complementizer's finiteness.

theorem Allotey2021.control_iff_selects_ni (v : Ga.CTP) : v ∈ Ga.gaCTPs → (Ga.EmbeddedClauseType.irrealisNi ∈ v.selects ↔ v.control ≠ ControlType.none)

A verb has a ni-frame exactly when it is a control verb (§§3.4–3.5, 5.5.1).

Table 2: the overt pronoun has the OC signature

inductive Allotey2021.Table2Row : Type

The eight rows of [All21]'s Table 2 ([Lan13]'s OC criteria, §§3.3–3.4).

• cCommandedByAntecedent : Table2Row

  Must be c-commanded by its antecedent (exx 45–46)

• longDistanceAntecedent : Table2Row

  Allows a long-distance antecedent (exx 47–49)

• sloppyOnly : Table2Row

  Sloppy reading only under ellipsis (exx 50–52)

• boundVariable : Table2Row

  Interpreted as a bound variable

• hasPhiFeatures : Table2Row

  Bears φ-features

• obligatoryDeSe : Table2Row

  Must be read de se (ex 53; [Chi90]'s diagnostic)

• subjectControl : Table2Row

  Occurs under subject control (exx 34–43)

• objectControl : Table2Row

  Occurs under object control (exx 54–59)

@[instance_reducible]

instance Allotey2021.instDecidableEqTable2Row : DecidableEq Table2Row

Equations

• Allotey2021.instDecidableEqTable2Row x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Allotey2021.instReprTable2Row : Repr Table2Row

Equations

• Allotey2021.instReprTable2Row = { reprPrec := Allotey2021.instReprTable2Row.repr }

def Allotey2021.instReprTable2Row.repr : Table2Row → ℕ → Std.Format

Equations

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

def Allotey2021.predictedColumn (prof : Control.Profile Landau2013.Clause74) (tier : Landau2015.Tier) (verbs : List Ga.CTP) : Table2Row → Bool

The Table 2 column predicted by a control signature, a tier, and a control-verb inventory: the antecedence and reading rows are the criteria the profile excludes (Profile.admits); de se is a tier property, not signature content ([Lan13] §1.3; [Chi90]) — the attitude-tier reading in the paper's subject-control test configuration (ex 53; communicative object control would give de te instead); φ-covariance is feature transmission under binding; the two control rows read the inventory.

Equations

• Allotey2021.predictedColumn prof tier verbs Allotey2021.Table2Row.cCommandedByAntecedent = !decide (Control.Diagnostic.nonCCommandingControl ∈ prof.admits)
• Allotey2021.predictedColumn prof tier verbs Allotey2021.Table2Row.longDistanceAntecedent = decide (Control.Diagnostic.longDistanceControl ∈ prof.admits)
• Allotey2021.predictedColumn prof tier verbs Allotey2021.Table2Row.sloppyOnly = !decide (Control.Diagnostic.strictEllipsis ∈ prof.admits)
• Allotey2021.predictedColumn prof tier verbs Allotey2021.Table2Row.boundVariable = !decide (Control.Diagnostic.strictUnderOnly ∈ prof.admits)
• Allotey2021.predictedColumn prof tier verbs Allotey2021.Table2Row.hasPhiFeatures = prof Landau2013.Clause74.boundVariable
• Allotey2021.predictedColumn prof tier verbs Allotey2021.Table2Row.obligatoryDeSe = tier.isAttitude
• Allotey2021.predictedColumn prof tier verbs Allotey2021.Table2Row.subjectControl = verbs.any fun (x : Ga.CTP) => x.control == ControlType.subjectControl
• Allotey2021.predictedColumn prof tier verbs Allotey2021.Table2Row.objectControl = verbs.any fun (x : Ga.CTP) => x.control == ControlType.objectControl

def Allotey2021.overtPronoun (d : Table2Row) : Bool

Table 2's observed overt-pronoun column (§§3.3.1–3.3.7, 3.4).

Equations

• Allotey2021.overtPronoun d = (d != Allotey2021.Table2Row.longDistanceAntecedent)

theorem Allotey2021.overt_pronoun_matches_pro : overtPronoun = predictedColumn (gaProfile Ga.EmbeddedClauseType.irrealisNi) Landau2015.Tier.logophoric Ga.gaCTPs

The observed column is what the ni-clause signature predicts over the attested inventory, on the logophoric tier of the attitude verbs the de se test uses (ex 53 'expect').

The irrealis marker across complement frames

Within the ni-frame the subject's irrealis tone is constant (exx 43, 89c–d, 100–103, 117a). Implicativity governs frame choice: an affirmative positive implicative entails its complement realized and alternates into a realis frame (exx 89a–b), where the marker is impossible (§§5.2.3, 5.3.5).

structure Allotey2021.MarkerDatum : Type

An attested complement configuration: matrix verb, complementizer (none for the bare frame of ex 89b), matrix polarity, marker.

• verb : Ga.CTP
• comp : Option Ga.Complementizer
• matrixAffirmative : Bool
• markerPresent : Bool

def Allotey2021.instDecidableEqMarkerDatum.decEq (x✝ x✝¹ : MarkerDatum) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Allotey2021.instDecidableEqMarkerDatum : DecidableEq MarkerDatum

Equations

• Allotey2021.instDecidableEqMarkerDatum = Allotey2021.instDecidableEqMarkerDatum.decEq

@[instance_reducible]

instance Allotey2021.instReprMarkerDatum : Repr MarkerDatum

Equations

• Allotey2021.instReprMarkerDatum = { reprPrec := Allotey2021.instReprMarkerDatum.repr }

def Allotey2021.instReprMarkerDatum.repr : MarkerDatum → ℕ → Std.Format

Equations

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

def Allotey2021.MarkerDatum.irrealisFrame (d : MarkerDatum) : Bool

Whether the datum's frame is the irrealis ni-clause.

Equations

• d.irrealisFrame = (d.comp == some Ga.Complementizer.ni)

def Allotey2021.irrealisMarkerData : List MarkerDatum

The attested marker data (exx 89a–d, 100, 102–103, 117a).

Equations

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

theorem Allotey2021.marker_iff_irrealis_frame (d : MarkerDatum) : d ∈ irrealisMarkerData → d.markerPresent = d.irrealisFrame

The marker tracks the clause frame, not the verb.

theorem Allotey2021.realis_frame_only_under_realization (d : MarkerDatum) : d ∈ irrealisMarkerData → d.irrealisFrame = false → d.verb.implicative = some Implicative.positive ∧ d.matrixAffirmative = true

A realis frame occurs only where the complement is entailed realized: under an affirmative positive implicative (§5.2.3).

Landau bridge

def Allotey2021.gaToLandau (c : Ga.EmbeddedClauseType) : Control.ClauseClass

Gã clause types on [Lan04a]'s finiteness scale, via ClauseClass.ofFiniteness — a scale position, not a mood claim: §5.2 argues these clauses are not subjunctives.

Equations

• Allotey2021.gaToLandau c = Control.ClauseClass.ofFiniteness (Ga.clauseProperties c).unrestrictedTAM (Ga.clauseProperties c).independentTense

theorem Allotey2021.ga_no_fSubjunctive (c : Ga.EmbeddedClauseType) : gaToLandau c ≠ Control.ClauseClass.fSubjunctive

No Gã clause type is a tensed-but-controlled F-subjunctive (contrast Studies/Ostrove2026.lean).

theorem Allotey2021.landau_predicts_control (c : Ga.EmbeddedClauseType) (agr : Bool) : (gaProfile c).IsObligatory ↔ (gaToLandau c).HasOC agr

The scale predicts the control facts for any Agr value: Gã lacks the one position that reads Agr, and has no φ-agreement anyway (§4.4, exx 79–81; §6.1).

Long-Distance Agree and CP strength

akɛ/kɛji head strong CPs, ni a weak CP ([Riz97], §5.5.1). Blocking is a [Kei20]-style horizon at the strong C head — clause size, not intervention (contrast Studies/Halpert2019.lean, whose blocking CP is a φ-goal).

def Allotey2021.clauseSpine (c : Ga.Complementizer) : List Minimalist.Cat

Projected heads of a c-headed complement: strong CPs project the full C-domain, the weak CP ni only Fin.

Equations

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

def Allotey2021.ldaProbe : Minimalist.Probe.Profile

The matrix φ-probe: a T-probe whose horizon is the strong C head.

Equations

• Allotey2021.ldaProbe = { probeHead := Minimalist.Cat.T, horizon := some Minimalist.Cat.C }

def Allotey2021.ldaReaches (c : Ga.Complementizer) : Bool

LDA reaches into a c-headed complement.

Equations

• Allotey2021.ldaReaches c = Allotey2021.ldaProbe.transparentToLabel (Allotey2021.clauseSpine c)

theorem Allotey2021.ldaReaches_eq_not_isFinite (c : Ga.Complementizer) : ldaReaches c = !c.isFinite

LDA crosses ni and is blocked by akɛ/kɛji.

theorem Allotey2021.ldaReaches_iff_obligatory (c : Ga.EmbeddedClauseType) : ldaReaches (Ga.clauseComplementizer c) = true ↔ (gaProfile c).IsObligatory

The probe reaches the embedded subject in exactly the OC clause types.

theorem Allotey2021.ni_projects_no_focus : Minimalist.Cat.Foc ∉ clauseSpine Ga.Complementizer.ni ∧ Minimalist.Cat.Foc ∈ clauseSpine Ga.Complementizer.ake

ni projects no focus field; the finite complementizers do (exx 107–108).

theorem Allotey2021.npi_patterns_with_lda (c : Ga.EmbeddedClauseType) : (Ga.clauseProperties c).npiTransparent = ldaReaches (Ga.clauseComplementizer c)

NPI licensing patterns with LDA (§5.5.3, exx 115–117).

Against the rival derivations

def Allotey2021.gaEmbeddedLexicalCopyAvailable : Bool

Gã forbids embedded lexical-DP copies (exx 42b, 64).

Equations

• Allotey2021.gaEmbeddedLexicalCopyAvailable = false

inductive Allotey2021.Ex42Item : Type

The occupants of ex 42b's two positions.

• ameele : Ex42Item

  the lexical matrix subject Ameele

• pronoun : Ex42Item

  the obligatory embedded proclitic

@[instance_reducible]

instance Allotey2021.instDecidableEqEx42Item : DecidableEq Ex42Item

Equations

• Allotey2021.instDecidableEqEx42Item x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Allotey2021.instReprEx42Item : Repr Ex42Item

Equations

• Allotey2021.instReprEx42Item = { reprPrec := Allotey2021.instReprEx42Item.repr }

def Allotey2021.instReprEx42Item.repr : Ex42Item → ℕ → Std.Format

Equations

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

def Allotey2021.ex42Dependency : SetRel (Fin 2) (Fin 2)

Ex 42b's control dependency: matrix controller position 0 to embedded subject position 1.

Equations

• Allotey2021.ex42Dependency = {(0, 1)}

def Allotey2021.ex42Occupant : Fin 2 → Ex42Item

The attested occupants: lexical Ameele controls the obligatory proclitic — never a lexical copy (exx 42b, 64).

Equations

• Allotey2021.ex42Occupant p = if p = 0 then Allotey2021.Ex42Item.ameele else Allotey2021.Ex42Item.pronoun

theorem Allotey2021.ga_refutes_movement : ¬Control.IsExhaustive ex42Occupant ex42Dependency

Movement is token identity, and ex 42b's occupants differ across the dependency — the Movement Theory of Control ([Hor99]) is refuted on the Gã configuration (§3.6.2): control is base-generated.

theorem Allotey2021.lexical_copy_ban_predicted : gaEmbeddedLexicalCopyAvailable = (Semantics.Composition.TypeShifting.ComplementDenotation.property == Semantics.Composition.TypeShifting.ComplementDenotation.proposition)

The lexical-copy ban is what [Lan24]'s (72) predicts (the lexical-subject generalization originates with [Gra15]): the ex 42b/64 matrix verb kai is an implicative — nonattitude, predicative tier — so its complement is property-denoting, and only propositional complements license a lexical subject. (The attitude verbs' ni-frame aligns too: kplɛnɔ 'agree' takes the lexical-subject subjunctive of ex 105.)

theorem Allotey2021.controlled_form_covaries : Ga.subjectProclitic Person.first Number.singular ≠ Ga.subjectProclitic Person.second Number.singular

The controlled form φ-covaries with its controller (exx 37–39), unlike [Sat19]'s form-invariant Ewe yè (§3.6.3).

Table 4: the irrealis marker's realization sites

inductive Allotey2021.IrrealisContext : Type

The five [−REALIS] contexts of Table 4.

• subjunctive : IrrealisContext
• imperative : IrrealisContext
• conditional : IrrealisContext
• future : IrrealisContext
• embeddedControl : IrrealisContext

@[instance_reducible]

instance Allotey2021.instDecidableEqIrrealisContext : DecidableEq IrrealisContext

Equations

• Allotey2021.instDecidableEqIrrealisContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Allotey2021.instReprIrrealisContext : Repr IrrealisContext

Equations

• Allotey2021.instReprIrrealisContext = { reprPrec := Allotey2021.instReprIrrealisContext.repr }

def Allotey2021.instReprIrrealisContext.repr : IrrealisContext → ℕ → Std.Format

Equations

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

structure Allotey2021.IrrealisRealization : Type

Realization sites of the irrealis marker: high tone on the subject, high tone on the verb, the vowel segment a.

• subjectTone : Bool
• verbTone : Bool
• vowelSegment : Bool

def Allotey2021.instDecidableEqIrrealisRealization.decEq (x✝ x✝¹ : IrrealisRealization) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Allotey2021.instDecidableEqIrrealisRealization : DecidableEq IrrealisRealization

Equations

• Allotey2021.instDecidableEqIrrealisRealization = Allotey2021.instDecidableEqIrrealisRealization.decEq

def Allotey2021.instReprIrrealisRealization.repr : IrrealisRealization → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Allotey2021.instReprIrrealisRealization : Repr IrrealisRealization

Equations

• Allotey2021.instReprIrrealisRealization = { reprPrec := Allotey2021.instReprIrrealisRealization.repr }

def Allotey2021.irrealisRealization : IrrealisContext → IrrealisRealization

Table 4 (exx 85–87 subjunctive; 93–94 imperative; 97 conditional; 95–96 future; 100–103 embedded control).

Equations

• Allotey2021.irrealisRealization Allotey2021.IrrealisContext.subjunctive = { subjectTone := true, verbTone := true, vowelSegment := true }
• Allotey2021.irrealisRealization Allotey2021.IrrealisContext.imperative = { subjectTone := true, verbTone := true, vowelSegment := true }
• Allotey2021.irrealisRealization Allotey2021.IrrealisContext.conditional = { subjectTone := false, verbTone := false, vowelSegment := true }
• Allotey2021.irrealisRealization Allotey2021.IrrealisContext.future = { subjectTone := false, verbTone := false, vowelSegment := true }
• Allotey2021.irrealisRealization Allotey2021.IrrealisContext.embeddedControl = { subjectTone := true, verbTone := false, vowelSegment := false }

theorem Allotey2021.control_realization_unique (c : IrrealisContext) : irrealisRealization c = irrealisRealization IrrealisContext.embeddedControl → c = IrrealisContext.embeddedControl

The embedded-control realization profile is unique among the five irrealis contexts.

theorem Allotey2021.control_not_subjunctive : irrealisRealization IrrealisContext.embeddedControl ≠ irrealisRealization IrrealisContext.subjunctive

The control clause lacks the subjunctive's doubled realization (§5.2.2, ex 88: *ná).

Deriving overt PRO

The control clause obligatorily realizes the irrealis tone on its subject, and a tone needs a segmental host (pp. 28, 45) — so the controlled subject cannot be silent.

def Minimalist.MinimalPronoun.PronForm.hostsTone : PronForm → Bool

A tonal exponent needs a segmental host; the null form has none.

Equations

• Minimalist.MinimalPronoun.PronForm.null.hostsTone = false
• Minimalist.MinimalPronoun.PronForm.pronoun.hostsTone = true
• Minimalist.MinimalPronoun.PronForm.reflexive.hostsTone = true

def Allotey2021.HostsControlTone (inv : Minimalist.MinimalPronoun.MinPronInventory Minimalist.MinimalPronoun.PronForm) : Prop

The controlled-subject form must host the obligatory irrealis tone (Table 4's embedded-control row).

Equations

• Allotey2021.HostsControlTone inv = ((Allotey2021.irrealisRealization Allotey2021.IrrealisContext.embeddedControl).subjectTone = true → inv.controlForm.hostsTone = true)

theorem Allotey2021.null_pro_impossible (inv : Minimalist.MinimalPronoun.MinPronInventory Minimalist.MinimalPronoun.PronForm) (h : inv.controlForm = Minimalist.MinimalPronoun.PronForm.null) : ¬HostsControlTone inv

Null PRO is impossible in Gã: a null controlled-subject form cannot host the irrealis tone.

Minimal pronoun inventory

def Allotey2021.gaInventory : Minimalist.MinimalPronoun.MinPronInventory Minimalist.MinimalPronoun.PronForm

Gã vocabulary items: reflexive when locally bound, pronoun elsewhere; no null item. (The reflexive item is required by [Ost26]'s syncretism row for Gã; UNVERIFIED — [All21] never discusses Gã reflexives, check [Cam17].)

Equations

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

theorem Allotey2021.ga_hostsControlTone : HostsControlTone gaInventory

The Gã inventory meets the tone-hosting requirement.

theorem Allotey2021.ga_overt_pro : gaInventory.controlForm = Minimalist.MinimalPronoun.PronForm.pronoun

Controlled subjects surface as overt proclitics: no null item exists, so the elsewhere pronoun applies.

theorem Allotey2021.ga_has_reflexive : gaInventory.realize Minimalist.MinimalPronoun.BVAContext.locallyBound = Minimalist.MinimalPronoun.PronForm.reflexive

The locally-bound context realizes the reflexive item.

Typological placement

def Allotey2021.gaToNoonan : Ga.EmbeddedClauseType → Complement.Coding

Gã complements in [Noo07]'s typology; .infinitive is §5.6's own term for the bare-root ni-complement.

Equations

• Allotey2021.gaToNoonan Ga.EmbeddedClauseType.finiteAke = Complement.Coding.indicative
• Allotey2021.gaToNoonan Ga.EmbeddedClauseType.finiteKeji = Complement.Coding.indicative
• Allotey2021.gaToNoonan Ga.EmbeddedClauseType.irrealisNi = Complement.Coding.infinitive

theorem Allotey2021.ni_complement_reduced : (gaToNoonan Ga.EmbeddedClauseType.irrealisNi).isReduced = true

The control complement is reduced (deranked) in Noonan's terms.

theorem Allotey2021.ga_satisfies_universal : gaInventory.OvertPROUniversal Ga.allowsProDrop

Gã instantiates [Ost26]'s universal: overt PRO and no pro-drop.