Corbett (2000) — Number

[Cor00]

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, [SS74]): 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 [Chi98]'s Nominal Mapping Parameter.

Number Systems (Ch 2, §2.3)

def Corbett2000.englishNS : Number.System

English: obligatory sg–pl, no general number.

Equations

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

def Corbett2000.russianNS : Number.System

Russian: obligatory sg–pl, no general number.

Equations

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

def Corbett2000.upperSorbianNS : Number.System

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

Equations

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

def Corbett2000.baysoNS : Number.System

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 := [Number.singular, Number.paucal, Number.plural], hasGeneral := true }

def Corbett2000.sloveneNS : Number.System

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

Equations

• Corbett2000.sloveneNS = { name := "Slovene", values := [Number.singular, Number.dual, Number.plural], facultative := [Number.dual] }

def Corbett2000.larikeNS : Number.System

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

Equations

• Corbett2000.larikeNS = { name := "Larike", values := [Number.singular, Number.dual, Number.trial, Number.plural], facultative := [Number.dual, Number.trial] }

def Corbett2000.lihirNS : Number.System

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

Equations

• Corbett2000.lihirNS = { name := "Lihir", values := [Number.singular, Number.dual, Number.trial, Number.paucal, Number.plural] }

def Corbett2000.japaneseNS : Number.System

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

Equations

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

def Corbett2000.westernArmenianNS : Number.System

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 [BK14] 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 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 := [Number.singular, Number.plural], hasGeneral := true }

def Corbett2000.pirahaNS : Number.System

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

Equations

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

def Corbett2000.winnebagoNS : Number.System

Winnebago (Siouan): minimal–augmented, two values. {±minimal} only ([Har14a] Table 3).

Equations

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

def Corbett2000.rembarrnganS : Number.System

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

Equations

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

def Corbett2000.mebengokreNS : Number.System

Mebengokre (Jê): minimal–paucal–plural, three values. {±additive, ±minimal} ([Har14a] Table 3).

Equations

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

def Corbett2000.allNumberSystems : List Number.System

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 : Number.dual ∈ sloveneNS.facultative

theorem Corbett2000.larike_both_facultative : Number.dual ∈ larikeNS.facultative ∧ Number.trial ∈ larikeNS.facultative

theorem Corbett2000.all_trial_implies_dual (ns : Number.System) : ns ∈ allNumberSystems → ns.TrialImpliesDual

theorem Corbett2000.all_dual_implies_plural (ns : Number.System) : ns ∈ allNumberSystems → ns.DualImpliesPlural

theorem Corbett2000.all_plural_implies_singular_or_minimal (ns : Number.System) : ns ∈ allNumberSystems → ns.PluralImpliesSingularOrMinimal

theorem Corbett2000.all_augmented_implies_minimal (ns : Number.System) : ns ∈ allNumberSystems → ns.AugmentedImpliesMinimal

theorem Corbett2000.all_unitAug_implies_augmented (ns : Number.System) : ns ∈ allNumberSystems → ns.UnitAugImpliesAugmented

theorem Corbett2000.allNumberSystems_wellFormed (ns : Number.System) : ns ∈ allNumberSystems → ns.WellFormed

Every system the book records satisfies the full Table-1 universal set ([Har14a]) — all eleven implications, not only the five originally checked above.

Animacy Hierarchy and Number Marking (Ch 3)

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) : Prop

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

• p.RespectsConstraintI = ((∃ r ∈ Corbett2000.allRanks✝, (p.status r).toNat ≥ 2) → (p.status Features.Prominence.AnimacyRank.speaker).toNat ≥ 2)

def Corbett2000.AnimacyNumberProfile.RespectsConstraintIII (p : AnimacyNumberProfile) : Prop

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

Equations

• p.RespectsConstraintIII = ∀ r1 ∈ Corbett2000.allRanks✝, ∀ r2 ∈ Corbett2000.allRanks✝, r1.toNat ≤ r2.toNat ∨ (p.status r1).toNat ≥ (p.status r2).toNat

@[implicit_reducible]

instance Corbett2000.instDecidableRespectsConstraintI (p : AnimacyNumberProfile) : Decidable p.RespectsConstraintI

Equations

• Corbett2000.instDecidableRespectsConstraintI p = id inferInstance

@[implicit_reducible]

instance Corbett2000.instDecidableRespectsConstraintIII (p : AnimacyNumberProfile) : Decidable p.RespectsConstraintIII

Equations

• Corbett2000.instDecidableRespectsConstraintIII p = id inferInstance

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 (p : AnimacyNumberProfile) : p ∈ allAnimacyProfiles → p.RespectsConstraintI

Constraints I and III hold for all profiled languages.

theorem Corbett2000.constraint_iii_holds (p : AnimacyNumberProfile) : p ∈ allAnimacyProfiles → p.RespectsConstraintIII

The Agreement Hierarchy (Ch 6, §6.2)

inductive Corbett2000.AgreementControl : Type

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

Distinct from Agreement.AgreementType (grammatical vs. pronominal, [BN07]), 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 the targets where semantic (meaning-driven) agreement is available.

• controller : String

  Controller description

• semanticTargets : List Agreement.AgreementTarget

  Targets where semantic (meaning-driven) agreement is possible.

def Corbett2000.AgreementProfile.RespectsHierarchy (p : AgreementProfile) : Prop

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

Equations

• p.RespectsHierarchy = ∀ t1 ∈ Corbett2000.hierarchyPositions✝, ∀ t2 ∈ Corbett2000.hierarchyPositions✝, t1.rank ≤ t2.rank ∨ t1 ∉ p.semanticTargets ∨ t2 ∈ p.semanticTargets

@[implicit_reducible]

instance Corbett2000.instDecidableRespectsHierarchy (p : AgreementProfile) : Decidable p.RespectsHierarchy

Equations

• Corbett2000.instDecidableRespectsHierarchy p = id inferInstance

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

• Corbett2000.americanCommittee = { controller := "committee (American English)", semanticTargets := [Agreement.AgreementTarget.relativePronoun, Agreement.AgreementTarget.personalPronoun] }

def Corbett2000.serboCroatDeca : AgreementProfile

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

Equations

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

def Corbett2000.allAgreementProfiles : List AgreementProfile

Equations

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

theorem Corbett2000.agreement_hierarchy_holds (p : AgreementProfile) : p ∈ allAgreementProfiles → p.RespectsHierarchy

The Agreement Hierarchy is respected by all profiled controllers.

theorem Corbett2000.semantic_at_pronoun (p : AgreementProfile) : p ∈ allAgreementProfiles → Agreement.AgreementTarget.personalPronoun ∈ p.semanticTargets

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

theorem Corbett2000.no_attributive_only_semantic (p : AgreementProfile) : p ∈ allAgreementProfiles → Agreement.AgreementTarget.attributive ∈ p.semanticTargets → Agreement.AgreementTarget.personalPronoun ∈ p.semanticTargets

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

Controller–Target Mismatch (Ch 6, §6.1)

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 Number
• targetValues : List Number
• defaultNumber : Number

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

def Corbett2000.instDecidableEqControllerTargetSystem.decEq (x✝ x✝¹ : ControllerTargetSystem) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Corbett2000.instDecidableEqControllerTargetSystem : DecidableEq ControllerTargetSystem

Equations

• Corbett2000.instDecidableEqControllerTargetSystem = Corbett2000.instDecidableEqControllerTargetSystem.decEq

def Corbett2000.ControllerTargetSystem.HasMismatch (ct : ControllerTargetSystem) : Prop

Whether controller and target systems differ in size.

Equations

• ct.HasMismatch = (ct.controllerValues.length ≠ ct.targetValues.length)

@[implicit_reducible]

instance Corbett2000.instDecidableHasMismatch (ct : ControllerTargetSystem) : Decidable ct.HasMismatch

Equations

• Corbett2000.instDecidableHasMismatch ct = id inferInstance

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

• Corbett2000.baysoCT = { name := "Bayso", controllerValues := [Number.general, Number.singular, Number.paucal, Number.plural], targetValues := [Number.singular, Number.paucal, Number.plural] }

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

• Corbett2000.hebrewCT = { name := "Modern Hebrew", controllerValues := [Number.singular, Number.dual, Number.plural], targetValues := [Number.singular, Number.plural] }

def Corbett2000.englishCT : ControllerTargetSystem

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

Equations

• Corbett2000.englishCT = { name := "English", controllerValues := [Number.singular, Number.plural], targetValues := [Number.singular, Number.plural] }

theorem Corbett2000.bayso_mismatch : baysoCT.HasMismatch

theorem Corbett2000.hebrew_mismatch : hebrewCT.HasMismatch

theorem Corbett2000.english_no_mismatch : ¬englishCT.HasMismatch

The Individuation Hierarchy (Ch 4)

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 Number

  Number values available at each hierarchy position

• minorValues : List Number

  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) : Prop

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) : Prop

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

• p.RespectsMonotonicity = ∀ r1 ∈ Corbett2000.allRanks✝, ∀ r2 ∈ Corbett2000.allRanks✝, r1.toNat ≤ r2.toNat ∨ ∀ v ∈ p.valuesAt r2, v ∈ p.valuesAt r1

@[implicit_reducible]

instance Corbett2000.instDecidableRespectsConstraintII (p : IndividuationProfile) : Decidable p.RespectsConstraintII

Equations

• Corbett2000.instDecidableRespectsConstraintII p = id inferInstance

@[implicit_reducible]

instance Corbett2000.instDecidableRespectsMonotonicity (p : IndividuationProfile) : Decidable p.RespectsMonotonicity

Equations

• Corbett2000.instDecidableRespectsMonotonicity p = id inferInstance

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) => [Number.singular, Number.plural] }

def Corbett2000.allIndividuationProfiles : List IndividuationProfile

Equations

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

theorem Corbett2000.constraint_ii_holds (p : IndividuationProfile) : p ∈ allIndividuationProfiles → p.RespectsConstraintII

theorem Corbett2000.individuation_monotonicity_holds (p : IndividuationProfile) : p ∈ allIndividuationProfiles → p.RespectsMonotonicity

theorem Corbett2000.upperSorbian_split : Number.dual ∈ upperSorbianIndiv.valuesAt Features.Prominence.AnimacyRank.speaker ∧ Number.dual ∉ upperSorbianIndiv.valuesAt Features.Prominence.AnimacyRank.discreteInanimate

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

Resolution Rules for Conjoined Controllers (Ch 6, §6.3)

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 ⋯

@[implicit_reducible]

instance Corbett2000.instReprResolutionStrategy : Repr ResolutionStrategy

Equations

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

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

Equations

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

theorem Corbett2000.sg_sg_resolves_pl : englishNS.resolve Number.singular Number.singular = Number.plural

Semantic resolution in English ({sg, pl}): sg + sg → pl — the lattice-canonical dual coarsens to plural (Number.System.resolve, Features/Number/Resolve.lean).

theorem Corbett2000.sg_sg_resolves_du_with_dual : upperSorbianNS.resolve Number.singular Number.singular = Number.dual

In Upper Sorbian (which has dual), sg + sg resolves to dual: the lattice-canonical result survives uncoarsened ([Cor00] §6.3).

theorem Corbett2000.sg_du_resolves_pl_without_trial : englishNS.resolve Number.singular Number.dual = Number.plural

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

theorem Corbett2000.sg_du_resolves_tri_with_trial : larikeNS.resolve Number.singular Number.dual = Number.trial

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

Bridges to AnimacyRank, Fragment plurality profiles

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 ∧ English.pluralityProfile.occurrence = Morphology.Number.PluralOccurrence.allNounsAlwaysObligatory

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

theorem Corbett2000.japanese_general_vs_wals : japaneseNS.hasGeneral = true ∧ Japanese.pluralityProfile.coding = Morphology.Number.PluralCoding.noPlural

Bridge: Japanese general number in Corbett's analysis corresponds to the noPlural coding in 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.

Bridge to Cysouw Number.Stage

theorem Corbett2000.piraha_N1 : pirahaNS.toStage = Number.Stage.N1

theorem Corbett2000.english_N2 : englishNS.toStage = Number.Stage.N2

theorem Corbett2000.russian_N2 : russianNS.toStage = Number.Stage.N2

theorem Corbett2000.japanese_N2 : japaneseNS.toStage = Number.Stage.N2

theorem Corbett2000.upperSorbian_N3 : upperSorbianNS.toStage = Number.Stage.N3

theorem Corbett2000.larike_N4 : larikeNS.toStage = Number.Stage.N4

theorem Corbett2000.numberStage_consistent_with_size : pirahaNS.size = 0 ∧ pirahaNS.toStage = Number.Stage.N1 ∧ englishNS.size = 2 ∧ englishNS.toStage = Number.Stage.N2 ∧ upperSorbianNS.size = 3 ∧ upperSorbianNS.toStage = Number.Stage.N3 ∧ larikeNS.size = 4 ∧ larikeNS.toStage = Number.Stage.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.

Bridge to Chierchia (1998) Nominal Mapping Parameter

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.

Bridge to Link (1983) — Inclusive vs Exclusive Plural

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 ⋯

@[implicit_reducible]

instance Corbett2000.instReprPluralInterpretation : Repr PluralInterpretation

Equations

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

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

Equations

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

def Corbett2000.PluralInterpretation.IncludesSingleton : PluralInterpretation → Prop

Inclusive plural includes singletons; exclusive does not.

Equations

• Corbett2000.PluralInterpretation.inclusive.IncludesSingleton = True
• Corbett2000.PluralInterpretation.exclusive.IncludesSingleton = False

@[implicit_reducible]

instance Corbett2000.instDecidablePredPluralInterpretationIncludesSingleton : DecidablePred PluralInterpretation.IncludesSingleton

Equations

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

theorem Corbett2000.compositional_plural_is_inclusive : PluralInterpretation.inclusive.IncludesSingleton

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

Minor Number Constraints IV–VII (Ch 4)

def Corbett2000.IndividuationProfile.RespectsConstraintVII (p : IndividuationProfile) : Prop

Constraint VII ([Cor00] 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 = ∀ v ∈ p.minorValues, v = Number.dual ∨ v = Number.paucal

def Corbett2000.IndividuationProfile.RespectsConstraintIV (p : IndividuationProfile) : Prop

Constraint IV ([Cor00] 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

• p.RespectsConstraintIV = ∀ v ∈ p.minorValues, ∀ r1 ∈ Corbett2000.allRanks✝, ∀ r2 ∈ Corbett2000.allRanks✝, r1.toNat ≤ r2.toNat ∨ v ∉ p.valuesAt r2 ∨ v ∈ p.valuesAt r1

@[implicit_reducible]

instance Corbett2000.instDecidableRespectsConstraintVII (p : IndividuationProfile) : Decidable p.RespectsConstraintVII

Equations

• Corbett2000.instDecidableRespectsConstraintVII p = id inferInstance

@[implicit_reducible]

instance Corbett2000.instDecidableRespectsConstraintIV (p : IndividuationProfile) : Decidable p.RespectsConstraintIV

Equations

• Corbett2000.instDecidableRespectsConstraintIV p = id inferInstance

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 (p : IndividuationProfile) : p ∈ allIndividuationProfilesExtended → p.RespectsConstraintVII

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

theorem Corbett2000.constraint_iv_holds (p : IndividuationProfile) : p ∈ allIndividuationProfilesExtended → p.RespectsConstraintIV

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

theorem Corbett2000.constraint_ii_extended (p : IndividuationProfile) : p ∈ allIndividuationProfilesExtended → p.RespectsConstraintII

Constraint II also holds for the extended profile set.

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

Hebrew and Maltese duals are minor numbers.

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

theorem Corbett2000.no_minor_singular_or_plural (p : IndividuationProfile) : p ∈ allIndividuationProfilesExtended → Number.singular ∉ p.minorValues ∧ Number.plural ∉ p.minorValues

No language in our sample has minor singular or plural.

Default Number (Ch 6, §6.1.2)

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

• Corbett2000.tsezCT = { name := "Tsez", controllerValues := [Number.singular, Number.plural], targetValues := [Number.singular, Number.plural], defaultNumber := Number.plural }

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

English defaults to singular.

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

Tsez defaults to plural.

theorem Corbett2000.default_in_target_system (ct : ControllerTargetSystem) : ct ∈ [englishCT, baysoCT, hebrewCT, tsezCT] → ct.defaultNumber ∈ ct.targetValues

Default number is always in the target system.

Associative Plurals (Ch 5)

structure Corbett2000.AssociativePluralProfile : Type

Associative plural profile: "X and associates" constructions are constrained by animacy — they typically require human or animate controllers ([Cor00] 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.instDecidableEqAssociativePluralProfile : DecidableEq AssociativePluralProfile

Equations

• Corbett2000.instDecidableEqAssociativePluralProfile = Corbett2000.instDecidableEqAssociativePluralProfile.decEq

def Corbett2000.instDecidableEqAssociativePluralProfile.decEq (x✝ x✝¹ : AssociativePluralProfile) : Decidable (x✝ = x✝¹)

Equations

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

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 (p : AssociativePluralProfile) : p ∈ allAssociativeProfiles → p.minAnimacy.toNat ≥ Features.Prominence.AnimacyRank.human.toNat

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 Number.System), reflecting the interaction between the two.

Count/Mass × Number Interaction (Ch 7)

structure Corbett2000.CountMassNumberInteraction : Type

Count/mass interaction with number systems ([Cor00] 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 : Number.System

  Number system for count nouns

• massSystem : Number.System

  Number system for mass nouns (often smaller or empty)

@[implicit_reducible]

instance Corbett2000.instDecidableEqCountMassNumberInteraction : DecidableEq CountMassNumberInteraction

Equations

• Corbett2000.instDecidableEqCountMassNumberInteraction = Corbett2000.instDecidableEqCountMassNumberInteraction.decEq

def Corbett2000.instDecidableEqCountMassNumberInteraction.decEq (x✝ x✝¹ : CountMassNumberInteraction) : Decidable (x✝ = x✝¹)

Equations

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

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 (cm : CountMassNumberInteraction) : cm ∈ allCountMassInteractions → cm.massSystem.size ≤ cm.countSystem.size

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

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

Predicate Hierarchy Bridge

structure Corbett2000.PredicateHierarchyProfile : Type

A predicate-hierarchy profile records the sub-positions (verb, participle, adjective, noun) where semantic agreement is possible for a controller — e.g. Russian honorific vy.

• name : String
• semanticTargets : List Agreement.PredicateTarget

  Predicate sub-positions where semantic agreement is possible.

def Corbett2000.PredicateHierarchyProfile.RespectsHierarchy (p : PredicateHierarchyProfile) : Prop

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

Equations

• p.RespectsHierarchy = ∀ t1 ∈ Corbett2000.predicatePositions✝, ∀ t2 ∈ Corbett2000.predicatePositions✝, t1.rank ≥ t2.rank ∨ t1 ∉ p.semanticTargets ∨ t2 ∈ p.semanticTargets

@[implicit_reducible]

instance Corbett2000.instDecidableRespectsHierarchy_1 (p : PredicateHierarchyProfile) : Decidable p.RespectsHierarchy

Equations

• Corbett2000.instDecidableRespectsHierarchy_1 p = id inferInstance

def Corbett2000.russianHonorificVy : PredicateHierarchyProfile

Russian honorific vy 'you' (polite singular): grammatically plural but referring to one person, so semantic agreement = singular. Per [Cor00]'s Predicate Hierarchy data, the finite verb and participle keep syntactic (plural) agreement, while the long-form predicate adjective and the predicate noun take singular (semantic) agreement.

Equations

• Corbett2000.russianHonorificVy = { name := "Russian honorific vy (Predicate Hierarchy)", semanticTargets := [Agreement.PredicateTarget.adjective, Agreement.PredicateTarget.noun] }

theorem Corbett2000.russian_predicate_hierarchy_holds : russianHonorificVy.RespectsHierarchy

The Russian honorific-vy profile respects Predicate Hierarchy monotonicity.