Gã Fragment

[All21]

Language data for Gã (ISO: gaa), a Kwa (Niger-Congo) language spoken in Greater Accra, Ghana, covering what [All21] ("Overt Pronouns of Infinitival Predicates of Gã") needs for the obligatory-control facts: pronoun paradigm, TAM marking, complementizer inventory, and embedded clause typology.

Coverage

• Subject proclitics (person × number; the paper's Table 3)
• TAM prefixes (future, progressive, perfective) and the irrealis marker á, realized in embedded control clauses as high tone on the subject pronoun
• Complementizer inventory (akɛ, kɛji, ni) with finite vs. irrealis distinction; ni is optionally overt with some control verbs (tao 'want', [All21] ex 34) and obligatory with others (hiɛ-kã-nɔ 'hope', ex 35)
• Embedded clause typology (three-way: finiteAke, finiteKeji, irrealisNi)
• Pro-drop profile

Identifier policy

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

What is NOT covered (deliberately)

The verb-movement/negation-placement diagnostic ([All21]'s fifth non-finiteness argument, after [Pol89]: finite verbs raise past the suffixal negation -ee, -ŋ, -ko, while irrealis embedded clauses show a free preverbal negator ka, her exx 120–125). Formalizing the raising argument needs phrase-structure substrate beyond this fragment's clause-typology schema; the finiteness split it diagnoses is already carried by ClauseProperties.unrestrictedTAM.

Pronoun paradigm

def Ga.subjectProclitic : Person → Number → Option String

Subject proclitic forms (plain subjective series, [All21] Table 3), on the canonical person/number inventory; none for cells outside Gã's 3 × 2 paradigm. Not covered: the clipped past-tense 1SG variant ĩ and the impersonal subject pronoun a.

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 (ex 3a: e- for a 3SG controllee) — the embedded subject position cannot be silent. Merged with the irrealis marker á the 1SG proclitic surfaces as the portmanteau má (ex 34) rather than plain mi.

Equations

• Ga.subjectProclitic Person.first Number.singular = some "mi"
• Ga.subjectProclitic Person.second Number.singular = some "o"
• Ga.subjectProclitic Person.third Number.singular = some "e"
• Ga.subjectProclitic Person.first Number.plural = some "wɔ"
• Ga.subjectProclitic Person.second Number.plural = some "nyɛ"
• Ga.subjectProclitic Person.third Number.plural = some "amɛ"
• Ga.subjectProclitic x✝¹ x✝ = none

TAM marking

inductive Ga.TAM : Type

Prefixal TAM categories of the Gã verb (bare root = default past).

[All21] uses the future, progressive, and perfective prefixes to argue that embedded clauses introduced by akɛ and kɛji allow the full TAM paradigm (finite), while clauses introduced by ni prohibit tense/aspect marking of any kind and are restricted to irrealis (her exx 118–119, tense-restriction diagnostic).

• future : TAM

  Future prefix baa- (historically the ingressive deictic bà plus the irrealis marker á)

• progressive : TAM

  Progressive prefix mii-

• perfective : TAM

  Perfective prefix é- (high tone)

• irrealis : TAM

  Irrealis marker á: no independent verbal prefix in embedded control clauses; realized as high tone on the subject pronoun (portmanteau má for 1SG). True subjunctives double it — high tone on pronoun AND verb ([All21] Table 4).

@[instance_reducible]

instance Ga.instDecidableEqTAM : DecidableEq TAM

Equations

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

@[instance_reducible]

instance Ga.instReprTAM : Repr TAM

Equations

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

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.perfective prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Ga.TAM.perfective")).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✝

def Ga.TAM.exponent : TAM → Option String

Segmental exponent of a TAM category; none for the irrealis, whose marking in embedded control clauses is tonal (on the subject pronoun) rather than prefixal.

Equations

• Ga.TAM.future.exponent = some "baa-"
• Ga.TAM.progressive.exponent = some "mii-"
• Ga.TAM.perfective.exponent = some "é-"
• Ga.TAM.irrealis.exponent = none

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

Complementizers

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 (a weak CP: no focus fronting, no independent tense, [All21] exx 107–109). Optionally overt with some control verbs (tao 'want', ex 34) and obligatory with others (hiɛ-kã-nɔ 'hope', ex 35).

@[instance_reducible]

instance Ga.instDecidableEqComplementizer : DecidableEq Complementizer

Equations

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

@[instance_reducible]

instance Ga.instReprComplementizer : Repr Complementizer

Equations

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

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✝

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

Embedded clause typology

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

  The controlled irrealis ni-clause: irrealis only, obligatory coreference, OC. The complementizer ni itself may be optional or obligatory depending on the matrix verb; the irrealis tone marking and OC behavior are constant. NOT every ni-headed clause is of this type: ni also introduces true subjunctives with lexical subjects (Osa kplɛnɔ ni Taki á-tsɛ́ Momo, ex 105) and, with dwɛŋ 'think', finite low-tone complements (exx 110–111).

@[instance_reducible]

instance Ga.instDecidableEqEmbeddedClauseType : DecidableEq EmbeddedClauseType

Equations

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

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

Equations

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

@[instance_reducible]

instance Ga.instReprEmbeddedClauseType : Repr EmbeddedClauseType

Equations

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

structure Ga.ClauseProperties : Type

Properties distinguishing the three clause types.

• unrestrictedTAM : Bool

  All four TAM categories available

• independentTense : Bool

  Tense independent of the matrix clause ([Lan04a]'s [±T]): finite complements host past/progressive/future freely (exx 110–111), while ni-clauses have only "the tense of a possible future" and reject overt tense (exx 118–119).

• noncoreferentialSubject : Bool

  Noncoreferential embedded subject possible

• finiteComplementizer : Bool

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

• npiTransparent : Bool

  Matrix negation licenses an embedded NPI across this clause's boundary ([All21] §5.5.3: possible across ni, exx 117a–b; impossible across akɛ, exx 116a–b; kɛji unattested per-example but finite, so covered by her generalization that NPIs "cannot be licensed across borders of finite" clauses).

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

Equations

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

@[instance_reducible]

instance Ga.instDecidableEqClauseProperties : DecidableEq ClauseProperties

Equations

• Ga.instDecidableEqClauseProperties = Ga.instDecidableEqClauseProperties.decEq

@[instance_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

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

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

Typological profile

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