Corbett (2000) — Number

@cite{corbett-2000}

Formalizes the core typological framework from:

Corbett, G. G. (2000). Number. Cambridge Textbooks in Linguistics. Cambridge University Press.

Core Contributions

1. Number value inventory (Ch 2): includes general number — a form outside the number system, non-committal as to cardinality (Bayso lúban 'lion(s)', Japanese inu 'dog(s)', Arabic collectives). Values are classified as determinate (fixed cardinality: singular=1, dual=2, trial=3) vs indeterminate (contextually variable: paucal, greater plural).

2. Number system typology (§2.3): implicational universals constrain which systems are possible — trial → dual → plural → singular.

3. Animacy Hierarchy constraints (Ch 3, @cite{smith-stark-1974}): the likelihood of number being distinguished decreases monotonically from speaker toward inanimate. Connects to AnimacyRank in Features.Prominence.

4. The Agreement Hierarchy (Ch 6, §6.2): for controllers permitting alternative agreement, semantic agreement increases monotonically along attributive < predicate < relative pronoun < personal pronoun.

5. Controller–target mismatch (§6.1): controller and target may have different number systems (Bayso: 4 controller values, 3 target forms).

6. Individuation Hierarchy (Ch 4): integrates the animacy hierarchy with number value inventories. Higher animacy positions can sustain richer number systems. Constraint II: if trial exists at position X, dual exists at X and all higher positions.

7. Resolution rules (Ch 6, §6.3): when conjoined controllers disagree in number, resolution is either semantic (referent sum: sg + sg → pl) or syntactic (nearest conjunct agreement).

8. Semantics of number (Ch 7): inclusive vs exclusive plural interpretation. Link's *P gives the inclusive reading (≥ 1); exclusive (≥ 2) is derived by scalar implicature. General number semantics connects to @cite{chierchia-1998}'s Nominal Mapping Parameter.

@[reducible, inline]

abbrev Corbett2000.NumberValue : Type

Equations

• Corbett2000.NumberValue = Features.Number.Category

structure Corbett2000.NumberSystem : Type

A number system specifies the values available in a language, which are obligatory vs facultative, and whether general number exists.

• name : String
• values : List NumberValue

  Values available within the number system

• hasGeneral : Bool

  Whether the language has general number (a form outside the system)

• facultative : List NumberValue

  Values whose use is optional (facultative)

def Corbett2000.instBEqNumberSystem.beq : NumberSystem → NumberSystem → Bool

Equations

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

@[implicit_reducible]

instance Corbett2000.instBEqNumberSystem : BEq NumberSystem

Equations

• Corbett2000.instBEqNumberSystem = { beq := Corbett2000.instBEqNumberSystem.beq }

def Corbett2000.NumberSystem.size (ns : NumberSystem) : ℕ

Number of values in the system.

Equations

• ns.size = ns.values.length

def Corbett2000.NumberSystem.isObligatory (ns : NumberSystem) (v : NumberValue) : Bool

Whether a value is obligatory (present and not facultative).

Equations

• ns.isObligatory v = (ns.values.contains v && !ns.facultative.contains v)

def Corbett2000.englishNS : NumberSystem

English: obligatory sg–pl, no general number.

Equations

• Corbett2000.englishNS = { name := "English", values := [Features.Number.Category.singular, Features.Number.Category.plural] }

def Corbett2000.russianNS : NumberSystem

Russian: obligatory sg–pl, no general number.

Equations

• Corbett2000.russianNS = { name := "Russian", values := [Features.Number.Category.singular, Features.Number.Category.plural] }

def Corbett2000.upperSorbianNS : NumberSystem

Upper Sorbian: sg–dual–pl, all obligatory.

Equations

• Corbett2000.upperSorbianNS = { name := "Upper Sorbian", values := [Features.Number.Category.singular, Features.Number.Category.dual, Features.Number.Category.plural] }

def Corbett2000.baysoNS : NumberSystem

Bayso (Cushitic): sg–paucal–pl within the system; general form lúban 'lion(s)' exists outside it. Four controller values total.

Equations

• Corbett2000.baysoNS = { name := "Bayso", values := [Features.Number.Category.singular, Features.Number.Category.paucal, Features.Number.Category.plural], hasGeneral := true }

def Corbett2000.sloveneNS : NumberSystem

Slovene: sg–dual–pl, but the dual is facultative (plural substitutes).

Equations

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

def Corbett2000.larikeNS : NumberSystem

Larike (Central Moluccan): sg–dual–trial–pl, dual and trial both facultative (plural can substitute for either).

Equations

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

def Corbett2000.lihirNS : NumberSystem

Lihir (Oceanic): sg–dual–trial–paucal–pl, five values — the richest well-documented system.

Equations

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

def Corbett2000.japaneseNS : NumberSystem

Japanese: sg–pl within the system, but general number exists (bare inu 'dog(s)' is non-committal).

Equations

• Corbett2000.japaneseNS = { name := "Japanese", values := [Features.Number.Category.singular, Features.Number.Category.plural], hasGeneral := true }

def Corbett2000.westernArmenianNS : NumberSystem

Western Armenian (ISO hyw): singular–plural within the system, but general number exists for singular indefinites (bare dəgha "boy" can refer to one or more boys). Per @cite{bale-khanjian-2014} eqs. 3 and 9: ⟦dəgha⟧ contains both singular individuals and groups; only plural dəgha-ner is strictly ≥2. The general-number reading is blocked in definite contexts via syntactic-complexity competition with the same-complexity plural alternative — see Phenomena/Plurals/Studies/BaleKhanjian2014.lean. Korean (Kim 2005) and Turkish (Bliss 2004) pattern alike per BK 2014 §2.3 and fn 14.

Equations

• Corbett2000.westernArmenianNS = { name := "Western Armenian", values := [Features.Number.Category.singular, Features.Number.Category.plural], hasGeneral := true }

def Corbett2000.pirahaNS : NumberSystem

Pirahã (Mura): no number category at all.

Equations

• Corbett2000.pirahaNS = { name := "Pirahã", values := [] }

def Corbett2000.winnebagoNS : NumberSystem

Winnebago (Siouan): minimal–augmented, two values. {±minimal} only (@cite{harbour-2014} Table 3).

Equations

• Corbett2000.winnebagoNS = { name := "Winnebago", values := [Features.Number.Category.minimal, Features.Number.Category.augmented] }

def Corbett2000.rembarrnganS : NumberSystem

Rembarrnga (Australian): minimal–unit augmented–augmented, three values. {±minimal*} — feature recursion on [±minimal] without [±atomic] (@cite{harbour-2014} Table 3).

Equations

• Corbett2000.rembarrnganS = { name := "Rembarrnga", values := [Features.Number.Category.minimal, Features.Number.Category.unitAugmented, Features.Number.Category.augmented] }

def Corbett2000.mebengokreNS : NumberSystem

Mebengokre (Jê): minimal–paucal–plural, three values. {±additive, ±minimal} (@cite{harbour-2014} Table 3).

Equations

• Corbett2000.mebengokreNS = { name := "Mebengokre", values := [Features.Number.Category.minimal, Features.Number.Category.paucal, Features.Number.Category.plural] }

def Corbett2000.allNumberSystems : List NumberSystem

Equations

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

theorem Corbett2000.english_two : englishNS.size = 2

theorem Corbett2000.upperSorbian_three : upperSorbianNS.size = 3

theorem Corbett2000.lihir_five : lihirNS.size = 5

theorem Corbett2000.piraha_zero : pirahaNS.size = 0

theorem Corbett2000.bayso_has_general : baysoNS.hasGeneral = true

theorem Corbett2000.japanese_has_general : japaneseNS.hasGeneral = true

theorem Corbett2000.western_armenian_has_general : westernArmenianNS.hasGeneral = true

theorem Corbett2000.english_no_general : englishNS.hasGeneral = false

theorem Corbett2000.slovene_dual_facultative : sloveneNS.facultative.contains Features.Number.Category.dual = true

theorem Corbett2000.larike_both_facultative : larikeNS.facultative.contains Features.Number.Category.dual = true ∧ larikeNS.facultative.contains Features.Number.Category.trial = true

def Corbett2000.NumberSystem.trialImpliesDual (ns : NumberSystem) : Bool

Trial implies dual: no language has trial without dual.

Equations

• ns.trialImpliesDual = (!ns.values.contains Features.Number.Category.trial || ns.values.contains Features.Number.Category.dual)

def Corbett2000.NumberSystem.dualImpliesPlural (ns : NumberSystem) : Bool

Dual implies plural.

Equations

• ns.dualImpliesPlural = (!ns.values.contains Features.Number.Category.dual || ns.values.contains Features.Number.Category.plural)

def Corbett2000.NumberSystem.pluralImpliesSingularOrMinimal (ns : NumberSystem) : Bool

Plural implies singular or minimal (@cite{harbour-2014} Table 1: PL → SG/MIN). Plural requires a "base" category — either singular (from [±atomic]) or minimal (from [±minimal]).

Equations

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

def Corbett2000.NumberSystem.augmentedImpliesMinimal (ns : NumberSystem) : Bool

Augmented implies minimal (@cite{harbour-2014} Table 1: AUG → MIN).

Equations

• ns.augmentedImpliesMinimal = (!ns.values.contains Features.Number.Category.augmented || ns.values.contains Features.Number.Category.minimal)

def Corbett2000.NumberSystem.unitAugImpliesAugmented (ns : NumberSystem) : Bool

Unit augmented implies augmented (@cite{harbour-2014} Table 1: U.AUG → AUG).

Equations

• ns.unitAugImpliesAugmented = (!ns.values.contains Features.Number.Category.unitAugmented || ns.values.contains Features.Number.Category.augmented)

theorem Corbett2000.all_trial_implies_dual : (allNumberSystems.all fun (x : NumberSystem) => x.trialImpliesDual) = true

theorem Corbett2000.all_dual_implies_plural : (allNumberSystems.all fun (x : NumberSystem) => x.dualImpliesPlural) = true

theorem Corbett2000.all_plural_implies_singular_or_minimal : (allNumberSystems.all fun (x : NumberSystem) => x.pluralImpliesSingularOrMinimal) = true

theorem Corbett2000.all_augmented_implies_minimal : (allNumberSystems.all fun (x : NumberSystem) => x.augmentedImpliesMinimal) = true

theorem Corbett2000.all_unitAug_implies_augmented : (allNumberSystems.all fun (x : NumberSystem) => x.unitAugImpliesAugmented) = true

inductive Corbett2000.MarkingStatus : Type

Number marking status at a position on the Animacy Hierarchy.

• obligatory : MarkingStatus
• optional : MarkingStatus
• absent : MarkingStatus

@[implicit_reducible]

instance Corbett2000.instDecidableEqMarkingStatus : DecidableEq MarkingStatus

Equations

• Corbett2000.instDecidableEqMarkingStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Corbett2000.instReprMarkingStatus : Repr MarkingStatus

Equations

• Corbett2000.instReprMarkingStatus = { reprPrec := Corbett2000.instReprMarkingStatus.repr }

def Corbett2000.instReprMarkingStatus.repr : MarkingStatus → ℕ → Std.Format

Equations

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

def Corbett2000.MarkingStatus.toNat : MarkingStatus → ℕ

Numeric ordering: higher = more marking.

Equations

• Corbett2000.MarkingStatus.obligatory.toNat = 2
• Corbett2000.MarkingStatus.optional.toNat = 1
• Corbett2000.MarkingStatus.absent.toNat = 0

structure Corbett2000.AnimacyNumberProfile : Type

An animacy–number profile records marking status at each hierarchy position for a particular language.

• name : String
• status : Features.Prominence.AnimacyRank → MarkingStatus

  Marking status at each position on the hierarchy.

def Corbett2000.AnimacyNumberProfile.respectsConstraintI (p : AnimacyNumberProfile) : Bool

Constraint I (Corbett Ch 3): the sg–pl distinction must affect a top segment of the hierarchy. If any position has obligatory marking, then the topmost position (speaker) does too.

Equations

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

def Corbett2000.AnimacyNumberProfile.respectsConstraintIII (p : AnimacyNumberProfile) : Bool

Constraint III (Corbett Ch 3): as we move rightward along the hierarchy, the likelihood of number being distinguished decreases monotonically — no intervening increase.

Equations

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

def Corbett2000.englishAnimacy : AnimacyNumberProfile

English: obligatory everywhere (regular split at the bottom).

Equations

• Corbett2000.englishAnimacy = { name := "English", status := fun (x : Features.Prominence.AnimacyRank) => Corbett2000.MarkingStatus.obligatory }

def Corbett2000.kannadaAnimacy : AnimacyNumberProfile

Kannada (Dravidian): obligatory for humans, optional for non-human animates, absent for inanimates.

Equations

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

def Corbett2000.slaveAnimacy : AnimacyNumberProfile

Slave (Athabaskan): obligatory for humans and kin, absent below.

Equations

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

def Corbett2000.allAnimacyProfiles : List AnimacyNumberProfile

Equations

• Corbett2000.allAnimacyProfiles = [Corbett2000.englishAnimacy, Corbett2000.kannadaAnimacy, Corbett2000.slaveAnimacy]

theorem Corbett2000.constraint_i_holds : (allAnimacyProfiles.all fun (x : AnimacyNumberProfile) => x.respectsConstraintI) = true

Constraints I and III hold for all profiled languages.

theorem Corbett2000.constraint_iii_holds : (allAnimacyProfiles.all fun (x : AnimacyNumberProfile) => x.respectsConstraintIII) = true

inductive Corbett2000.AgreementControl : Type

Whether agreement is determined by morphological form (syntactic) or by referential meaning (semantic).

Distinct from Core.AgreementType (grammatical vs. pronominal, @cite{bickel-nichols-2001}), which is about whether the agreement marker has referential autonomy. This type is about what controls agreement — the formal features of the controller or its semantic content.

• syntactic : AgreementControl
• semantic : AgreementControl

@[implicit_reducible]

instance Corbett2000.instDecidableEqAgreementControl : DecidableEq AgreementControl

Equations

• Corbett2000.instDecidableEqAgreementControl x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Corbett2000.instReprAgreementControl : Repr AgreementControl

Equations

• Corbett2000.instReprAgreementControl = { reprPrec := Corbett2000.instReprAgreementControl.repr }

def Corbett2000.instReprAgreementControl.repr : AgreementControl → ℕ → Std.Format

Equations

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

structure Corbett2000.AgreementProfile : Type

An agreement profile for a controller type records whether semantic agreement is available at each target position.

• controller : String

  Controller description

• semanticPossible : Core.AgreementTarget → Bool

  Whether semantic (meaning-driven) agreement is possible at each target

def Corbett2000.AgreementProfile.respectsHierarchy (p : AgreementProfile) : Bool

The Agreement Hierarchy monotonicity constraint: once semantic agreement becomes possible at a target, it remains possible at all targets further right (= lower Core.AgreementTarget.rank) on the hierarchy.

Equations

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

def Corbett2000.britishCommittee : AgreementProfile

British English committee: syntactic only in attributive position; semantic agreement possible in predicate, relative pronoun, and personal pronoun.

Equations

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

def Corbett2000.americanCommittee : AgreementProfile

American English committee: semantic agreement rare in predicate, but available in relative and personal pronoun.

Equations

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

def Corbett2000.serboCroatDeca : AgreementProfile

Serbo-Croatian deca 'children': morphologically feminine singular, semantically plural. Semantic agreement available everywhere.

Equations

• Corbett2000.serboCroatDeca = { controller := "deca 'children' (Serbo-Croatian)", semanticPossible := fun (x : Core.AgreementTarget) => true }

def Corbett2000.allAgreementProfiles : List AgreementProfile

Equations

• Corbett2000.allAgreementProfiles = [Corbett2000.britishCommittee, Corbett2000.americanCommittee, Corbett2000.serboCroatDeca]

theorem Corbett2000.agreement_hierarchy_holds : (allAgreementProfiles.all fun (x : AgreementProfile) => x.respectsHierarchy) = true

The Agreement Hierarchy is respected by all profiled controllers.

theorem Corbett2000.semantic_at_pronoun : (allAgreementProfiles.all fun (x : AgreementProfile) => x.semanticPossible Core.AgreementTarget.personalPronoun) = true

Once semantic agreement reaches the personal pronoun (rightmost), it is necessarily available there for all our controllers.

theorem Corbett2000.no_attributive_only_semantic : (allAgreementProfiles.all fun (p : AgreementProfile) => !p.semanticPossible Core.AgreementTarget.attributive || p.semanticPossible Core.AgreementTarget.personalPronoun) = true

No controller has semantic agreement only at the attributive position (the leftmost) without also having it further right — this would violate the monotonicity constraint.

structure Corbett2000.ControllerTargetSystem : Type

Controller and target may operate with different number systems. The target system is typically a subset of the controller system.

• name : String
• controllerValues : List NumberValue
• targetValues : List NumberValue
• defaultNumber : NumberValue

  Number appearing when controller lacks specification (§6.1.2). Most languages default to singular; Tsez defaults to plural.

def Corbett2000.instBEqControllerTargetSystem.beq : ControllerTargetSystem → ControllerTargetSystem → Bool

Equations

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

@[implicit_reducible]

instance Corbett2000.instBEqControllerTargetSystem : BEq ControllerTargetSystem

Equations

• Corbett2000.instBEqControllerTargetSystem = { beq := Corbett2000.instBEqControllerTargetSystem.beq }

def Corbett2000.ControllerTargetSystem.hasMismatch (ct : ControllerTargetSystem) : Bool

Whether controller and target systems differ in size.

Equations

• ct.hasMismatch = (ct.controllerValues.length != ct.targetValues.length)

def Corbett2000.baysoCT : ControllerTargetSystem

Bayso: 4 controller values (general, singular, paucal, plural), but only 3 target agreement forms. General and singular trigger the same agreement on the verb.

Equations

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

def Corbett2000.hebrewCT : ControllerTargetSystem

Modern Hebrew: 3 controller values (sg, dual, pl), but only 2 target agreement values — dual and plural trigger the same verb agreement.

Equations

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

def Corbett2000.englishCT : ControllerTargetSystem

English: 2 controller values, 2 target values (matched).

Equations

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

theorem Corbett2000.bayso_mismatch : baysoCT.hasMismatch = true

theorem Corbett2000.hebrew_mismatch : hebrewCT.hasMismatch = true

theorem Corbett2000.english_no_mismatch : englishCT.hasMismatch = false

structure Corbett2000.IndividuationProfile : Type

An individuation profile records which number values are available at each position on the animacy hierarchy. Languages may have split number systems where pronouns sustain a richer inventory than nouns.

• name : String
• valuesAt : Features.Prominence.AnimacyRank → List NumberValue

  Number values available at each hierarchy position

• minorValues : List NumberValue

  Minor number values: restricted to a closed class of nouns (e.g., Hebrew dual for body-part nouns, Maltese dual). Constraints IV–VII govern the distribution of minor numbers.

def Corbett2000.IndividuationProfile.respectsConstraintII (p : IndividuationProfile) : Bool

Constraint II (Corbett Ch 4): if trial exists at position X, then dual exists at X and at all positions higher on the animacy hierarchy.

Equations

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

def Corbett2000.IndividuationProfile.respectsMonotonicity (p : IndividuationProfile) : Bool

Monotonicity: number value inventories never grow as we move rightward (down) the hierarchy. If a value exists at position X, it exists at all higher positions.

Equations

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

def Corbett2000.upperSorbianIndiv : IndividuationProfile

Upper Sorbian: sg–dual–pl in pronouns and some nouns, but dual absent in lower animacy positions where only sg–pl remains.

Equations

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

def Corbett2000.lihirIndiv : IndividuationProfile

Lihir (Oceanic): full sg–du–tri–pauc–pl in pronouns, reduced inventory in lower positions.

Equations

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

def Corbett2000.englishIndiv : IndividuationProfile

English: uniform sg–pl at all positions (no split).

Equations

• Corbett2000.englishIndiv = { name := "English", valuesAt := fun (x : Features.Prominence.AnimacyRank) => [Features.Number.Category.singular, Features.Number.Category.plural] }

def Corbett2000.allIndividuationProfiles : List IndividuationProfile

Equations

• Corbett2000.allIndividuationProfiles = [Corbett2000.upperSorbianIndiv, Corbett2000.lihirIndiv, Corbett2000.englishIndiv]

theorem Corbett2000.constraint_ii_holds : (allIndividuationProfiles.all fun (x : IndividuationProfile) => x.respectsConstraintII) = true

theorem Corbett2000.individuation_monotonicity_holds : (allIndividuationProfiles.all fun (x : IndividuationProfile) => x.respectsMonotonicity) = true

theorem Corbett2000.upperSorbian_split : (upperSorbianIndiv.valuesAt Features.Prominence.AnimacyRank.speaker).contains Features.Number.Category.dual = true ∧ (upperSorbianIndiv.valuesAt Features.Prominence.AnimacyRank.discreteInanimate).contains Features.Number.Category.dual = false

Upper Sorbian pronouns have dual but lower animacy positions do not — a genuine split number system.

inductive Corbett2000.ResolutionStrategy : Type

When conjoined NPs disagree in number, the language must resolve which number value appears on the agreement target.

• semantic : ResolutionStrategy

  Semantic resolution: sum the referents. sg + sg → pl because the conjunction denotes a plurality.

• closestConjunct : ResolutionStrategy

  Syntactic resolution: the nearest (closest) conjunct to the target determines agreement, regardless of the other conjunct's number.

@[implicit_reducible]

instance Corbett2000.instDecidableEqResolutionStrategy : DecidableEq ResolutionStrategy

Equations

• Corbett2000.instDecidableEqResolutionStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Corbett2000.instReprResolutionStrategy.repr : ResolutionStrategy → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Corbett2000.instReprResolutionStrategy : Repr ResolutionStrategy

Equations

• Corbett2000.instReprResolutionStrategy = { reprPrec := Corbett2000.instReprResolutionStrategy.repr }

def Corbett2000.NumberValue.semanticResolve (a b : NumberValue) : NumberValue

The result of resolving two number values under semantic resolution.

Note: this function produces .trial for sg + du unconditionally. In languages without trial, the result is meaningless — use semanticResolveIn for language-sensitive resolution.

Equations

• Corbett2000.NumberValue.semanticResolve Features.Number.Category.singular Features.Number.Category.singular = Features.Number.Category.plural
• Corbett2000.NumberValue.semanticResolve Features.Number.Category.singular Features.Number.Category.dual = Features.Number.Category.trial
• Corbett2000.NumberValue.semanticResolve Features.Number.Category.dual Features.Number.Category.singular = Features.Number.Category.trial
• a.semanticResolve b = Features.Number.Category.plural

def Corbett2000.NumberValue.semanticResolveIn (ns : NumberSystem) (a b : NumberValue) : NumberValue

Language-sensitive semantic resolution: if the raw result is not in the language's number system, fall back to plural.

Equations

• Corbett2000.NumberValue.semanticResolveIn ns a b = if ns.values.contains (a.semanticResolve b) = true then a.semanticResolve b else Features.Number.Category.plural

theorem Corbett2000.sg_sg_resolves_pl : NumberValue.semanticResolve Features.Number.Category.singular Features.Number.Category.singular = Features.Number.Category.plural

Semantic resolution: sg + sg → pl.

theorem Corbett2000.sg_du_resolves_tri : NumberValue.semanticResolve Features.Number.Category.singular Features.Number.Category.dual = Features.Number.Category.trial

Semantic resolution: sg + du → tri (in languages with trial).

theorem Corbett2000.sg_du_resolves_pl_without_trial : NumberValue.semanticResolveIn englishNS Features.Number.Category.singular Features.Number.Category.dual = Features.Number.Category.plural

In languages without trial, sg + du resolves to pl.

theorem Corbett2000.sg_du_resolves_tri_with_trial : NumberValue.semanticResolveIn larikeNS Features.Number.Category.singular Features.Number.Category.dual = Features.Number.Category.trial

In Larike (which has trial), sg + du keeps trial.

theorem Corbett2000.animacy_rank_ordering_consistent : Features.Prominence.AnimacyRank.speaker.toNat > Features.Prominence.AnimacyRank.human.toNat ∧ Features.Prominence.AnimacyRank.human.toNat > Features.Prominence.AnimacyRank.higherAnimal.toNat ∧ Features.Prominence.AnimacyRank.higherAnimal.toNat > Features.Prominence.AnimacyRank.discreteInanimate.toNat

Bridge: AnimacyRank monotonicity constraint is consistent with the animacy hierarchy defined in Features.Prominence. The ranking used here agrees with the ranking there: speaker (8) > ... > nondiscrete (0).

theorem Corbett2000.english_matches_plurals_typology : englishNS.size = 2 ∧ englishNS.hasGeneral = false ∧ Fragments.English.pluralityProfile.occurrence = Typology.PluralOccurrence.allNounsAlwaysObligatory

Bridge: English NumberSystem matches the English plurality profile in Fragments.English.Plurals — both record a 2-value obligatory system.

theorem Corbett2000.japanese_general_vs_wals : japaneseNS.hasGeneral = true ∧ Fragments.Japanese.pluralityProfile.coding = Typology.PluralCoding.noPlural

Bridge: Japanese general number in Corbett's analysis corresponds to the noPlural coding in Fragments.Japanese.Plurals. WALS and Corbett describe the same facts differently: WALS says "no nominal plural," Corbett says "general number exists (form outside the system)."

theorem Corbett2000.bayso_general_with_system : baysoNS.hasGeneral = true ∧ baysoNS.size = 3

Bridge: Bayso's general number explains its "no nominal plural" appearance — it's not that number is absent, but that the general form stands outside the number system.

def Corbett2000.NumberSystem.toNumberStage (ns : NumberSystem) : Features.Number.NumberStage

Map a Corbett NumberSystem to Cysouw's NumberStage hierarchy by counting the number of non-general values in the system.

• 0–1 values → N1 (undifferentiated)
• 2 values → N2 (basic sg/pl opposition)
• 3 values (has dual or paucal) → N3
• 4+ values → N4

Equations

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

theorem Corbett2000.piraha_N1 : pirahaNS.toNumberStage = Features.Number.NumberStage.N1

theorem Corbett2000.english_N2 : englishNS.toNumberStage = Features.Number.NumberStage.N2

theorem Corbett2000.russian_N2 : russianNS.toNumberStage = Features.Number.NumberStage.N2

theorem Corbett2000.japanese_N2 : japaneseNS.toNumberStage = Features.Number.NumberStage.N2

theorem Corbett2000.upperSorbian_N3 : upperSorbianNS.toNumberStage = Features.Number.NumberStage.N3

theorem Corbett2000.larike_N4 : larikeNS.toNumberStage = Features.Number.NumberStage.N4

theorem Corbett2000.numberStage_consistent_with_size : pirahaNS.size = 0 ∧ pirahaNS.toNumberStage = Features.Number.NumberStage.N1 ∧ englishNS.size = 2 ∧ englishNS.toNumberStage = Features.Number.NumberStage.N2 ∧ upperSorbianNS.size = 3 ∧ upperSorbianNS.toNumberStage = Features.Number.NumberStage.N3 ∧ larikeNS.size = 4 ∧ larikeNS.toNumberStage = Features.Number.NumberStage.N4

Corbett's implicational hierarchy (trial → dual → plural → singular) is consistent with Cysouw's N-stages: a system at stage Nₖ has exactly k number oppositions, matching size = k for k ≤ 4.

theorem Corbett2000.general_number_iff_bare_kind : (baysoNS.hasGeneral = true ∧ Semantics.Kinds.NMP.CanDenoteKind Semantics.Kinds.NMP.NominalMapping.argOnly False) ∧ (japaneseNS.hasGeneral = true ∧ Semantics.Kinds.NMP.CanDenoteKind Semantics.Kinds.NMP.NominalMapping.argOnly False) ∧ englishNS.hasGeneral = false ∧ ¬Semantics.Kinds.NMP.CanDenoteKind Semantics.Kinds.NMP.NominalMapping.predOnly False

Corbett's general number languages are those where bare nouns can denote kinds without a determiner — exactly Chierchia's [+arg] languages.

If a language has general number (a form outside the number system, non- committal to cardinality), bare NPs can serve as arguments. This corresponds to CanDenoteKind mapping (hasD := false), which holds for argOnly and argAndPred but not predOnly.

inductive Corbett2000.PluralInterpretation : Type

The inclusive/exclusive ambiguity of plurals (Corbett Ch 7).

Link's *P (star/plural closure) gives the inclusive interpretation: *P(x) holds for atoms AND their sums, so "dogs" denotes ≥ 1 dogs. The exclusive interpretation (≥ 2 dogs) is not a separate semantic primitive — it arises by scalar implicature from the singular alternative.

This is modeled here as a parameter on plural interpretation. The compositional semantics (Link1983.star) always delivers inclusive; pragmatics narrows to exclusive.

• inclusive : PluralInterpretation

  ≥ 1: Link's *P, closed under join. The singular is included.

• exclusive : PluralInterpretation

  ≥ 2: derived by scalar implicature. The singular is excluded.

@[implicit_reducible]

instance Corbett2000.instDecidableEqPluralInterpretation : DecidableEq PluralInterpretation

Equations

• Corbett2000.instDecidableEqPluralInterpretation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Corbett2000.instReprPluralInterpretation.repr : PluralInterpretation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Corbett2000.instReprPluralInterpretation : Repr PluralInterpretation

Equations

• Corbett2000.instReprPluralInterpretation = { reprPrec := Corbett2000.instReprPluralInterpretation.repr }

def Corbett2000.PluralInterpretation.includesSingleton : PluralInterpretation → Bool

Inclusive plural includes singletons; exclusive does not.

Equations

• Corbett2000.PluralInterpretation.inclusive.includesSingleton = true
• Corbett2000.PluralInterpretation.exclusive.includesSingleton = false

theorem Corbett2000.compositional_plural_is_inclusive : PluralInterpretation.inclusive.includesSingleton = true

The compositional (pre-pragmatic) interpretation is always inclusive.

theorem Corbett2000.numberResolveIn_eq_semanticResolveIn (a b : NumberValue) : Minimalist.Agreement.CoordinateResolution.numberResolveIn englishNS.values a b = some (NumberValue.semanticResolveIn englishNS a b)

Corbett's semanticResolveIn agrees with the lattice-grounded numberResolveIn for any system containing .plural.

numberResolveIn computes the canonical lattice join (sg+sg→du) then coarsens to the target system. semanticResolveIn computes semantic summation (sg+sg→pl) then coarsens. For {sg,pl} systems, these agree because the coarsening step absorbs the difference (du→pl = pl→pl).

def Corbett2000.IndividuationProfile.respectsConstraintVII (p : IndividuationProfile) : Bool

Constraint VII (@cite{corbett-2000} Ch 4): only dual and paucal can be minor numbers. Singular and plural cannot be minor — they are the core of any number system.

Equations

• p.respectsConstraintVII = p.minorValues.all fun (v : Corbett2000.NumberValue) => v == Features.Number.Category.dual || v == Features.Number.Category.paucal

def Corbett2000.IndividuationProfile.respectsConstraintIV (p : IndividuationProfile) : Bool

Constraint IV (@cite{corbett-2000} Ch 4): if a minor number exists at some animacy position, it must also exist at all higher positions. Minor numbers obey the same monotonicity as full number values.

Equations

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

def Corbett2000.hebrewIndiv : IndividuationProfile

Modern Hebrew: minor dual restricted to body-part nouns and a few lexicalized time expressions. The dual is a closed class (Constraint V), found only among human/body-part nouns.

Equations

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

def Corbett2000.malteseIndiv : IndividuationProfile

Maltese: minor dual, also restricted to a small set of nouns (body parts and time expressions, e.g. idejn 'two hands').

Equations

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

def Corbett2000.allIndividuationProfilesExtended : List IndividuationProfile

Equations

• Corbett2000.allIndividuationProfilesExtended = [Corbett2000.upperSorbianIndiv, Corbett2000.lihirIndiv, Corbett2000.englishIndiv, Corbett2000.hebrewIndiv, Corbett2000.malteseIndiv]

theorem Corbett2000.constraint_vii_holds : (allIndividuationProfilesExtended.all fun (x : IndividuationProfile) => x.respectsConstraintVII) = true

Constraint VII holds for all profiles (only dual/paucal are minor).

theorem Corbett2000.constraint_iv_holds : (allIndividuationProfilesExtended.all fun (x : IndividuationProfile) => x.respectsConstraintIV) = true

Constraint IV holds for all profiles (minor number monotonicity).

theorem Corbett2000.constraint_ii_extended : (allIndividuationProfilesExtended.all fun (x : IndividuationProfile) => x.respectsConstraintII) = true

Constraint II also holds for the extended profile set.

theorem Corbett2000.hebrew_minor_dual : hebrewIndiv.minorValues = [Features.Number.Category.dual]

Hebrew and Maltese duals are minor numbers.

theorem Corbett2000.maltese_minor_dual : malteseIndiv.minorValues = [Features.Number.Category.dual]

theorem Corbett2000.no_minor_singular_or_plural : (allIndividuationProfilesExtended.all fun (p : IndividuationProfile) => !p.minorValues.contains Features.Number.Category.singular && !p.minorValues.contains Features.Number.Category.plural) = true

No language in our sample has minor singular or plural.

def Corbett2000.tsezCT : ControllerTargetSystem

Tsez (Northeast Caucasian): when the controller lacks a number specification, the default agreement target form is plural — opposite to most languages.

Equations

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

theorem Corbett2000.english_default_singular : englishCT.defaultNumber = Features.Number.Category.singular

English defaults to singular.

theorem Corbett2000.tsez_default_plural : tsezCT.defaultNumber = Features.Number.Category.plural

Tsez defaults to plural.

theorem Corbett2000.default_in_target_system : ([englishCT, baysoCT, hebrewCT, tsezCT].all fun (ct : ControllerTargetSystem) => ct.targetValues.contains ct.defaultNumber) = true

Default number is always in the target system.

structure Corbett2000.AssociativePluralProfile : Type

Associative plural profile: "X and associates" constructions are constrained by animacy — they typically require human or animate controllers (@cite{corbett-2000} Ch 5).

• name : String
• minAnimacy : Features.Prominence.AnimacyRank

  Minimum animacy rank for associative plural use

• sameAsAdditive : Bool

  Whether the associative marker is identical to the additive plural

@[implicit_reducible]

instance Corbett2000.instBEqAssociativePluralProfile : BEq AssociativePluralProfile

Equations

• Corbett2000.instBEqAssociativePluralProfile = { beq := Corbett2000.instBEqAssociativePluralProfile.beq }

def Corbett2000.instBEqAssociativePluralProfile.beq : AssociativePluralProfile → AssociativePluralProfile → Bool

Equations

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

def Corbett2000.hungarianAssoc : AssociativePluralProfile

Hungarian: associative -ék, dedicated form (not the additive plural), restricted to human referents.

Equations

• Corbett2000.hungarianAssoc = { name := "Hungarian", minAnimacy := Features.Prominence.AnimacyRank.human, sameAsAdditive := false }

def Corbett2000.japaneseAssoc : AssociativePluralProfile

Japanese: associative -tachi, distinct from additive plural (none on common nouns), human-restricted.

Equations

• Corbett2000.japaneseAssoc = { name := "Japanese", minAnimacy := Features.Prominence.AnimacyRank.human, sameAsAdditive := false }

def Corbett2000.turkishAssoc : AssociativePluralProfile

Turkish: associative -ler (same as additive plural), available for human referents.

Equations

• Corbett2000.turkishAssoc = { name := "Turkish", minAnimacy := Features.Prominence.AnimacyRank.human, sameAsAdditive := true }

def Corbett2000.allAssociativeProfiles : List AssociativePluralProfile

Equations

• Corbett2000.allAssociativeProfiles = [Corbett2000.hungarianAssoc, Corbett2000.japaneseAssoc, Corbett2000.turkishAssoc]

theorem Corbett2000.associative_requires_human : (allAssociativeProfiles.all fun (p : AssociativePluralProfile) => decide (p.minAnimacy.toNat ≥ Features.Prominence.AnimacyRank.human.toNat)) = true

Associative plurals in our sample all require at least human animacy.

theorem Corbett2000.japanese_associative_with_general : japaneseNS.hasGeneral = true ∧ japaneseAssoc.sameAsAdditive = false

Bridge: Japanese has both associative plural (here) and general number (from the NumberSystem), reflecting the interaction between the two.

structure Corbett2000.CountMassNumberInteraction : Type

Count/mass interaction with number systems (@cite{corbett-2000} Ch 7).

Mass nouns resist plural morphology; count nouns take it freely. The count/mass distinction interacts with the animacy hierarchy: higher animacy positions are more likely to be count (and thus support richer number distinctions).

• name : String
• countNounsInflect : Bool

  Does the language require count nouns to inflect for number?

• massNounsInflect : Bool

  Does the language allow mass nouns to inflect for number?

• countSystem : NumberSystem

  Number system for count nouns

• massSystem : NumberSystem

  Number system for mass nouns (often smaller or empty)

def Corbett2000.instBEqCountMassNumberInteraction.beq : CountMassNumberInteraction → CountMassNumberInteraction → Bool

Equations

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

@[implicit_reducible]

instance Corbett2000.instBEqCountMassNumberInteraction : BEq CountMassNumberInteraction

Equations

• Corbett2000.instBEqCountMassNumberInteraction = { beq := Corbett2000.instBEqCountMassNumberInteraction.beq }

def Corbett2000.englishCountMass : CountMassNumberInteraction

English: count nouns inflect obligatorily, mass nouns do not (*furnitures, *informations).

Equations

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

def Corbett2000.japaneseCountMass : CountMassNumberInteraction

Japanese: neither count nor mass nouns inflect for number (general number covers both).

Equations

• Corbett2000.japaneseCountMass = { name := "Japanese", countNounsInflect := false, massNounsInflect := false, countSystem := Corbett2000.japaneseNS, massSystem := Corbett2000.japaneseNS }

def Corbett2000.allCountMassInteractions : List CountMassNumberInteraction

Equations

• Corbett2000.allCountMassInteractions = [Corbett2000.englishCountMass, Corbett2000.japaneseCountMass]

theorem Corbett2000.mass_never_richer_than_count : (allCountMassInteractions.all fun (cm : CountMassNumberInteraction) => decide (cm.massSystem.size ≤ cm.countSystem.size)) = true

Mass noun systems are never richer than count noun systems.

theorem Corbett2000.english_count_mass_asymmetry : englishCountMass.countNounsInflect = true ∧ englishCountMass.massNounsInflect = false

In English, count nouns inflect but mass nouns do not.

theorem Corbett2000.japanese_count_mass_uniform : (japaneseCountMass.countSystem == japaneseCountMass.massSystem) = true

Bridge to Chierchia (1998): Japanese general number languages treat count and mass nouns identically — both get the same number system.

structure Corbett2000.PredicateHierarchyProfile : Type

Russian: predicate adjectives agree in gender/number, but past-tense verbs also do — illustrating the Predicate Hierarchy within the agreement target position.

• name : String
• semanticPossible : Core.PredicateTarget → Bool

  Whether semantic agreement is available at each predicate sub-position

def Corbett2000.PredicateHierarchyProfile.respectsHierarchy (p : PredicateHierarchyProfile) : Bool

The Predicate Hierarchy monotonicity constraint: once semantic agreement becomes possible at a sub-position, it remains possible at all higher positions.

Equations

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

def Corbett2000.russianDecaPredHier : PredicateHierarchyProfile

Russian deca ('children'): semantic agreement on predicate adjective and noun, but not on finite verb. Participial agreement follows adjective.

Equations

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

theorem Corbett2000.russian_predicate_hierarchy_holds : russianDecaPredHier.respectsHierarchy = true

The Russian Predicate Hierarchy profile respects monotonicity.