Gã Fragment

@cite{allotey-2021}

Language data for Gã (ISO: gaa), a Kwa (Niger-Congo) language spoken in Greater Accra, Ghana. The data here covers what is needed to formalize the obligatory control facts in @cite{allotey-2021}: pronoun paradigm, TAM marking, complementizer inventory, and embedded clause typology.

Coverage

• Pronoun paradigm (subject proclitics, person × number)
• TAM prefixes (future, progressive, perfect) and irrealis tone
• Complementizer inventory (akɛ, kɛji, ni) with finite vs. irrealis distinction; ni is recorded as optionally-overt because @cite{allotey-2021} ex 34 shows it dropping in some controlled clauses while ex 35–38 show it obligatorily present
• Embedded clause typology (three-way: finiteAke, finiteKeji, irrealisNi)
• Pro-drop / overt-subject profile

Identifier policy

Lean 4 does not accept the IPA characters ɛ (U+025B) or ŋ (U+014B) as identifier characters. Constructor and definition names use the plain Latin orthography (ake, keji, nye, kpleno, kpang), while the IPA form is preserved in the corresponding String value.

What is NOT covered (deliberately)

Verbal negation morphology and the V-to-T raising claim. Both rely on independent morphological argumentation (@cite{pollock-1989}'s diagnostic requires a free Neg head; Gã -ee and -ko appear suffixal) that is orthogonal to the OC story.

inductive Fragments.Ga.Person : Type

• first : Person
• second : Person
• third : Person

@[implicit_reducible]

instance Fragments.Ga.instDecidableEqPerson : DecidableEq Person

Equations

• Fragments.Ga.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Ga.instReprPerson.repr : Person → ℕ → Std.Format

Equations

• Fragments.Ga.instReprPerson.repr Fragments.Ga.Person.first prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fragments.Ga.Person.first")).group prec✝
• Fragments.Ga.instReprPerson.repr Fragments.Ga.Person.second prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fragments.Ga.Person.second")).group prec✝
• Fragments.Ga.instReprPerson.repr Fragments.Ga.Person.third prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fragments.Ga.Person.third")).group prec✝

@[implicit_reducible]

instance Fragments.Ga.instReprPerson : Repr Person

Equations

• Fragments.Ga.instReprPerson = { reprPrec := Fragments.Ga.instReprPerson.repr }

inductive Fragments.Ga.Number : Type

• sg : Number
• pl : Number

@[implicit_reducible]

instance Fragments.Ga.instDecidableEqNumber : DecidableEq Number

Equations

• Fragments.Ga.instDecidableEqNumber x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Ga.instReprNumber : Repr Number

Equations

• Fragments.Ga.instReprNumber = { reprPrec := Fragments.Ga.instReprNumber.repr }

def Fragments.Ga.instReprNumber.repr : Number → ℕ → Std.Format

Equations

• Fragments.Ga.instReprNumber.repr Fragments.Ga.Number.sg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fragments.Ga.Number.sg")).group prec✝
• Fragments.Ga.instReprNumber.repr Fragments.Ga.Number.pl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fragments.Ga.Number.pl")).group prec✝

def Fragments.Ga.subjectProclitic : Person → Number → String

Subject proclitic forms.

Gã subject pronouns are proclitics on the inflected verb. In @cite{allotey-2021}'s OC examples, the embedded subject of a controlled ni-clause is realized as an overt subject proclitic (e.g., e- for 3SG controllees) — the embedded subject position cannot be silent.

Equations

• Fragments.Ga.subjectProclitic Fragments.Ga.Person.first Fragments.Ga.Number.sg = "mi"
• Fragments.Ga.subjectProclitic Fragments.Ga.Person.second Fragments.Ga.Number.sg = "o"
• Fragments.Ga.subjectProclitic Fragments.Ga.Person.third Fragments.Ga.Number.sg = "e"
• Fragments.Ga.subjectProclitic Fragments.Ga.Person.first Fragments.Ga.Number.pl = "wɔ"
• Fragments.Ga.subjectProclitic Fragments.Ga.Person.second Fragments.Ga.Number.pl = "nyɛ"
• Fragments.Ga.subjectProclitic Fragments.Ga.Person.third Fragments.Ga.Number.pl = "amɛ"

inductive Fragments.Ga.TAM : Type

Prefixal TAM categories of the Gã verb.

@cite{allotey-2021} uses the future, progressive, and perfect prefixes to argue that embedded clauses introduced by akɛ and kɛji allow the full TAM paradigm (finite), while clauses introduced by ni are restricted to irrealis (no future, progressive, or perfect prefix).

• future : TAM

  Future prefix baa-

• progressive : TAM

  Progressive prefix mii-

• perfect : TAM

  Perfect prefix é- (high tone)

• irrealis : TAM

  Irrealis: no overt prefix; marked by stem high tone (á)

@[implicit_reducible]

instance Fragments.Ga.instDecidableEqTAM : DecidableEq TAM

Equations

• Fragments.Ga.instDecidableEqTAM x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Ga.instReprTAM : Repr TAM

Equations

• Fragments.Ga.instReprTAM = { reprPrec := Fragments.Ga.instReprTAM.repr }

def Fragments.Ga.instReprTAM.repr : TAM → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Ga.instReprTAM.repr Fragments.Ga.TAM.future prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fragments.Ga.TAM.future")).group prec✝
• Fragments.Ga.instReprTAM.repr Fragments.Ga.TAM.perfect prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fragments.Ga.TAM.perfect")).group prec✝
• Fragments.Ga.instReprTAM.repr Fragments.Ga.TAM.irrealis prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Fragments.Ga.TAM.irrealis")).group prec✝

def Fragments.Ga.TAM.exponent : TAM → String

Equations

• Fragments.Ga.TAM.future.exponent = "baa-"
• Fragments.Ga.TAM.progressive.exponent = "mii-"
• Fragments.Ga.TAM.perfect.exponent = "é-"
• Fragments.Ga.TAM.irrealis.exponent = "á"

def Fragments.Ga.TAM.isFinite : TAM → Bool

Whether this TAM is part of the unrestricted (finite) paradigm.

Per @cite{allotey-2021}, finite embedded clauses (introduced by akɛ or kɛji) freely host any of the four TAM categories; ni-clauses are restricted to .irrealis.

Equations

• Fragments.Ga.TAM.irrealis.isFinite = false
• x✝.isFinite = true

inductive Fragments.Ga.Complementizer : Type

The three complementizers @cite{allotey-2021} discusses.

• ake : Complementizer

  akɛ — finite complementizer for declarative complements (typically utterance and propositional attitude verbs)

• keji : Complementizer

  kɛji — finite complementizer for conditional and conditional-like complements

• ni : Complementizer

  ni — irrealis complementizer; introduces controlled clauses. Allotey ex 34 shows ni is optional in some controlled clauses while ex 35–38 show it obligatorily present.

@[implicit_reducible]

instance Fragments.Ga.instDecidableEqComplementizer : DecidableEq Complementizer

Equations

• Fragments.Ga.instDecidableEqComplementizer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Ga.instReprComplementizer : Repr Complementizer

Equations

• Fragments.Ga.instReprComplementizer = { reprPrec := Fragments.Ga.instReprComplementizer.repr }

def Fragments.Ga.instReprComplementizer.repr : Complementizer → ℕ → Std.Format

Equations

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

def Fragments.Ga.Complementizer.form : Complementizer → String

Equations

• Fragments.Ga.Complementizer.ake.form = "akɛ"
• Fragments.Ga.Complementizer.keji.form = "kɛji"
• Fragments.Ga.Complementizer.ni.form = "ni"

def Fragments.Ga.Complementizer.isFinite : Complementizer → Bool

Whether the complementizer projects a finite (full-TAM) clause.

Equations

• Fragments.Ga.Complementizer.ni.isFinite = false
• x✝.isFinite = true

inductive Fragments.Ga.EmbeddedClauseType : Type

Three embedded clause types in Gã, distinguished by complementizer and TAM properties (@cite{allotey-2021}).

Note: Gã irrealisNi clauses always carry an OVERT subject proclitic in controlled contexts — there is no null-PRO option. The OC properties hold of this overt-subject configuration.

• finiteAke : EmbeddedClauseType

  Finite akɛ-clause: full TAM, free subject reference, no OC

• finiteKeji : EmbeddedClauseType

  Finite kɛji-clause: full TAM, free subject reference, no OC

• irrealisNi : EmbeddedClauseType

  Irrealis ni-clause: irrealis only, obligatory coreference, OC. The complementizer ni itself may be optional (Allotey ex 34) or obligatory (ex 35–38) depending on the matrix verb; the irrealis tone marking and OC behavior are constant.

@[implicit_reducible]

instance Fragments.Ga.instDecidableEqEmbeddedClauseType : DecidableEq EmbeddedClauseType

Equations

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

@[implicit_reducible]

instance Fragments.Ga.instReprEmbeddedClauseType : Repr EmbeddedClauseType

Equations

• Fragments.Ga.instReprEmbeddedClauseType = { reprPrec := Fragments.Ga.instReprEmbeddedClauseType.repr }

def Fragments.Ga.instReprEmbeddedClauseType.repr : EmbeddedClauseType → ℕ → Std.Format

Equations

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

structure Fragments.Ga.ClauseProperties : Type

Properties distinguishing the three clause types.

• unrestrictedTAM : Bool

  All four TAM categories available

• noncoreferentialSubject : Bool

  Noncoreferential embedded subject possible

• finiteComplementizer : Bool

  Selects one of the finite complementizers (akɛ, kɛji)

def Fragments.Ga.instDecidableEqClauseProperties.decEq (x✝ x✝¹ : ClauseProperties) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Fragments.Ga.instDecidableEqClauseProperties : DecidableEq ClauseProperties

Equations

• Fragments.Ga.instDecidableEqClauseProperties = Fragments.Ga.instDecidableEqClauseProperties.decEq

@[implicit_reducible]

instance Fragments.Ga.instReprClauseProperties : Repr ClauseProperties

Equations

• Fragments.Ga.instReprClauseProperties = { reprPrec := Fragments.Ga.instReprClauseProperties.repr }

def Fragments.Ga.instReprClauseProperties.repr : ClauseProperties → ℕ → Std.Format

Equations

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

def Fragments.Ga.clauseProperties : EmbeddedClauseType → ClauseProperties

Equations

• Fragments.Ga.clauseProperties Fragments.Ga.EmbeddedClauseType.finiteAke = { unrestrictedTAM := true, noncoreferentialSubject := true, finiteComplementizer := true }
• Fragments.Ga.clauseProperties Fragments.Ga.EmbeddedClauseType.finiteKeji = { unrestrictedTAM := true, noncoreferentialSubject := true, finiteComplementizer := true }
• Fragments.Ga.clauseProperties Fragments.Ga.EmbeddedClauseType.irrealisNi = { unrestrictedTAM := false, noncoreferentialSubject := false, finiteComplementizer := false }

def Fragments.Ga.clauseComplementizer : EmbeddedClauseType → Complementizer

Equations

• Fragments.Ga.clauseComplementizer Fragments.Ga.EmbeddedClauseType.finiteAke = Fragments.Ga.Complementizer.ake
• Fragments.Ga.clauseComplementizer Fragments.Ga.EmbeddedClauseType.finiteKeji = Fragments.Ga.Complementizer.keji
• Fragments.Ga.clauseComplementizer Fragments.Ga.EmbeddedClauseType.irrealisNi = Fragments.Ga.Complementizer.ni

theorem Fragments.Ga.complementizer_isFinite_eq_finiteFlag (c : EmbeddedClauseType) : (clauseComplementizer c).isFinite = (clauseProperties c).finiteComplementizer

def Fragments.Ga.allowsProDrop : Bool

Gã does NOT allow null pronominal subjects in matrix clauses: every clause requires an overt subject proclitic (@cite{allotey-2021}).

Equations

• Fragments.Ga.allowsProDrop = false

def Fragments.Ga.basicWordOrder : String

Gã has SVO basic order.

Equations

• Fragments.Ga.basicWordOrder = "SVO"

def Fragments.Ga.controlledSubjectMustBeOvert : Bool

Controlled subjects in irrealisNi clauses must be OVERT proclitics (@cite{allotey-2021}'s central empirical observation). Null PRO is ungrammatical in this position.

Equations

• Fragments.Ga.controlledSubjectMustBeOvert = true