Gã Fragment

[All21]

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 [All21]: 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 [All21] 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 ([Pol89]'s diagnostic requires a free Neg head; Gã -ee and -ko appear suffixal) that is orthogonal to the OC story.

inductive Ga.Person : Type

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

@[implicit_reducible]

instance Ga.instDecidableEqPerson : DecidableEq Person

Equations

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

@[implicit_reducible]

instance Ga.instReprPerson : Repr Person

Equations

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

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

Equations

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

def Ga.Person.toPerson : Person → _root_.Person

Ga's three-way person in the canonical inventory.

Equations

• Ga.Person.first.toPerson = Person.first
• Ga.Person.second.toPerson = Person.second
• Ga.Person.third.toPerson = Person.third

inductive Ga.Number : Type

• sg : Number
• pl : Number

@[implicit_reducible]

instance Ga.instDecidableEqNumber : DecidableEq Number

Equations

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

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

Equations

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

@[implicit_reducible]

instance Ga.instReprNumber : Repr Number

Equations

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

def Ga.Number.toNumber : Number → _root_.Number

Ga's two-value system in the canonical inventory.

Equations

• Ga.Number.sg.toNumber = Number.singular
• Ga.Number.pl.toNumber = Number.plural

def Ga.subjectProclitic : Person → Number → String

Subject proclitic forms.

Gã subject pronouns are proclitics on the inflected verb. In [All21]'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

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

inductive Ga.TAM : Type

Prefixal TAM categories of the Gã verb.

[All21] 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 Ga.instDecidableEqTAM : DecidableEq TAM

Equations

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

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

Equations

• Ga.instReprTAM.repr Ga.TAM.future prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ga.TAM.future")).group prec✝
• Ga.instReprTAM.repr Ga.TAM.progressive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ga.TAM.progressive")).group prec✝
• Ga.instReprTAM.repr Ga.TAM.perfect prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ga.TAM.perfect")).group prec✝
• Ga.instReprTAM.repr Ga.TAM.irrealis prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ga.TAM.irrealis")).group prec✝

@[implicit_reducible]

instance Ga.instReprTAM : Repr TAM

Equations

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

def Ga.TAM.exponent : TAM → String

Equations

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

def Ga.TAM.isFinite : TAM → Bool

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

Per [All21], finite embedded clauses (introduced by akɛ or kɛji) freely host any of the four TAM categories; ni-clauses are restricted to .irrealis.

Equations

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

inductive Ga.Complementizer : Type

The three complementizers [All21] 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 Ga.instDecidableEqComplementizer : DecidableEq Complementizer

Equations

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

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

Equations

• Ga.instReprComplementizer.repr Ga.Complementizer.ake prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ga.Complementizer.ake")).group prec✝
• Ga.instReprComplementizer.repr Ga.Complementizer.keji prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ga.Complementizer.keji")).group prec✝
• Ga.instReprComplementizer.repr Ga.Complementizer.ni prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ga.Complementizer.ni")).group prec✝

@[implicit_reducible]

instance Ga.instReprComplementizer : Repr Complementizer

Equations

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

def Ga.Complementizer.form : Complementizer → String

Equations

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

def Ga.Complementizer.isFinite : Complementizer → Bool

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

Equations

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

inductive Ga.EmbeddedClauseType : Type

Three embedded clause types in Gã, distinguished by complementizer and TAM properties ([All21]).

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 Ga.instDecidableEqEmbeddedClauseType : DecidableEq EmbeddedClauseType

Equations

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

@[implicit_reducible]

instance Ga.instReprEmbeddedClauseType : Repr EmbeddedClauseType

Equations

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

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

Equations

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

structure 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)

@[implicit_reducible]

instance Ga.instDecidableEqClauseProperties : DecidableEq ClauseProperties

Equations

• Ga.instDecidableEqClauseProperties = Ga.instDecidableEqClauseProperties.decEq

def 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 Ga.instReprClauseProperties : Repr ClauseProperties

Equations

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

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

Equations

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

def Ga.clauseProperties : EmbeddedClauseType → ClauseProperties

Equations

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

def Ga.clauseComplementizer : EmbeddedClauseType → Complementizer

Equations

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

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

def Ga.allowsProDrop : Bool

Gã does NOT allow null pronominal subjects in matrix clauses: every clause requires an overt subject proclitic ([All21]).

Equations

• Ga.allowsProDrop = false

def Ga.basicWordOrder : String

Gã has SVO basic order.

Equations

• Ga.basicWordOrder = "SVO"

def Ga.controlledSubjectMustBeOvert : Bool

Controlled subjects in irrealisNi clauses must be OVERT proclitics ([All21]'s central empirical observation). Null PRO is ungrammatical in this position.

Equations

• Ga.controlledSubjectMustBeOvert = true