Verbal Number and Pluractionality

@cite{corbett-2000}

Verbal number — number marking on the verb that quantifies over events rather than participants (@cite{corbett-2000} Ch 8). Languages like Hausa, Chechen, and Navajo mark number directly on the verb stem, often via suppletion (distinct stems for singular vs plural).

Key distinctions:

• Participant agreement: verb agrees with subject/object number (typical Indo-European pattern, not "verbal number" proper)
• Event plurality / pluractionality: the verb's own event argument is pluralized — repeated, distributed, or intensified action
• Mixed: both patterns co-exist (e.g. Georgian)

WALS 80A Bridge

WALS Feature 80A records verbal number and suppletion across 193 languages. 159 have no verbal number; 34 have singular-plural pairs (with or without suppletion); 7 have sg-du-pl triples.

inductive VerbalNumber.VerbalNumberType : Type

Whether verbal number is participant agreement, event plurality, or both.

• participantAgreement : VerbalNumberType

  Verb agrees with subject/object number (most Indo-European). Not "verbal number" in the strict Corbett sense.

• eventPlurality : VerbalNumberType

  Verb's own event argument is pluralized. The verb stem changes to encode repeated, distributed, or intensified action.

• mixed : VerbalNumberType

  Both patterns co-exist in the language.

@[implicit_reducible]

instance VerbalNumber.instDecidableEqVerbalNumberType : DecidableEq VerbalNumberType

Equations

• VerbalNumber.instDecidableEqVerbalNumberType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance VerbalNumber.instReprVerbalNumberType : Repr VerbalNumberType

Equations

• VerbalNumber.instReprVerbalNumberType = { reprPrec := VerbalNumber.instReprVerbalNumberType.repr }

def VerbalNumber.instReprVerbalNumberType.repr : VerbalNumberType → ℕ → Std.Format

Equations

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

structure VerbalNumber.VerbalNumberProfile : Type

Profile for a language's verbal number system.

• name : String
• type : VerbalNumberType
• hasSuppletion : Bool

  Whether the language uses suppletion (distinct stems for sg/pl).

• verbValues : List Features.Number.Category

  Number values distinguished on the verb.

@[implicit_reducible]

instance VerbalNumber.instBEqVerbalNumberProfile : BEq VerbalNumberProfile

Equations

• VerbalNumber.instBEqVerbalNumberProfile = { beq := VerbalNumber.instBEqVerbalNumberProfile.beq }

def VerbalNumber.instBEqVerbalNumberProfile.beq : VerbalNumberProfile → VerbalNumberProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• VerbalNumber.instBEqVerbalNumberProfile.beq x✝¹ x✝ = false

def VerbalNumber.hausa : VerbalNumberProfile

Hausa: event plurality with suppletive verb stems. tàfi 'go (sg)' / tàka 'go (pl)'.

Equations

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

def VerbalNumber.chechen : VerbalNumberProfile

Chechen: event plurality with suppletion. Verb pairs encode singular vs plural action.

Equations

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

def VerbalNumber.navajo : VerbalNumberProfile

Navajo: event plurality, sg-du-pl verb stems (one of the richer systems). Three-way suppletion: łtsooz 'flat object lies (sg)' / łtsos '(du)' / łtsoos '(pl)'.

Equations

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

def VerbalNumber.georgian : VerbalNumberProfile

Georgian: mixed system — participant agreement on some verbs, event plurality on others.

Equations

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

def VerbalNumber.allVerbalNumberProfiles : List VerbalNumberProfile

Equations

• VerbalNumber.allVerbalNumberProfiles = [VerbalNumber.hausa, VerbalNumber.chechen, VerbalNumber.navajo, VerbalNumber.georgian]

theorem VerbalNumber.event_plural_has_sg_pl : (allVerbalNumberProfiles.all fun (p : VerbalNumberProfile) => p.type == VerbalNumberType.participantAgreement || p.verbValues.contains Features.Number.Category.singular && p.verbValues.contains Features.Number.Category.plural) = true

Languages with event plurality always have at least sg and pl.

theorem VerbalNumber.navajo_three_values : navajo.verbValues.length = 3

Navajo is the only 3-value system in our sample.

theorem VerbalNumber.verbal_dual_implies_sg_pl : (allVerbalNumberProfiles.all fun (p : VerbalNumberProfile) => !p.verbValues.contains Features.Number.Category.dual || p.verbValues.contains Features.Number.Category.singular && p.verbValues.contains Features.Number.Category.plural) = true

The implicational universal holds: dual verbal number implies singular and plural are also distinguished.

def VerbalNumber.VerbalNumberProfile.toWALS80A (p : VerbalNumberProfile) : Data.WALS.F80A.VerbalNumberAndSuppletion

Map a VerbalNumberProfile to the corresponding WALS 80A category.

Equations

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

theorem VerbalNumber.hausa_wals : hausa.toWALS80A = Data.WALS.F80A.VerbalNumberAndSuppletion.singularPluralPairsSuppletion

Hausa maps to singular-plural pairs with suppletion.

theorem VerbalNumber.navajo_wals : navajo.toWALS80A = Data.WALS.F80A.VerbalNumberAndSuppletion.singularDualPluralTriplesSuppletion

Navajo maps to sg-du-pl triples with suppletion.

theorem VerbalNumber.wals_majority_no_verbal_number : (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F80A.VerbalNumberAndSuppletion) => x.value == Data.WALS.F80A.VerbalNumberAndSuppletion.none) Data.WALS.F80A.allData).length > (List.filter (fun (x : Data.WALS.Datapoint Data.WALS.F80A.VerbalNumberAndSuppletion) => x.value != Data.WALS.F80A.VerbalNumberAndSuppletion.none) Data.WALS.F80A.allData).length

WALS 80A confirms that the majority of languages lack verbal number.