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 Core.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 Phenomena.Agreement.Studies.Corbett2000.NumberValue : Type

Equations

• Phenomena.Agreement.Studies.Corbett2000.NumberValue = Core.Number.Category

structure Phenomena.Agreement.Studies.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)

instance Phenomena.Agreement.Studies.Corbett2000.instBEqNumberSystem : BEq NumberSystem

Equations

• Phenomena.Agreement.Studies.Corbett2000.instBEqNumberSystem = { beq := Phenomena.Agreement.Studies.Corbett2000.instBEqNumberSystem.beq }

def Phenomena.Agreement.Studies.Corbett2000.instBEqNumberSystem.beq : NumberSystem → NumberSystem → Bool

Equations

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

def Phenomena.Agreement.Studies.Corbett2000.NumberSystem.size (ns : NumberSystem) : ℕ

Number of values in the system.

Equations

• ns.size = ns.values.length

def Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.Corbett2000.englishNS : NumberSystem

English: obligatory sg–pl, no general number.

Equations

• Phenomena.Agreement.Studies.Corbett2000.englishNS = { name := "English", values := [Core.Number.Category.singular, Core.Number.Category.plural] }

def Phenomena.Agreement.Studies.Corbett2000.russianNS : NumberSystem

Russian: obligatory sg–pl, no general number.

Equations

• Phenomena.Agreement.Studies.Corbett2000.russianNS = { name := "Russian", values := [Core.Number.Category.singular, Core.Number.Category.plural] }

def Phenomena.Agreement.Studies.Corbett2000.upperSorbianNS : NumberSystem

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

Equations

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

def Phenomena.Agreement.Studies.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

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

def Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.Corbett2000.japaneseNS : NumberSystem

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

Equations

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

def Phenomena.Agreement.Studies.Corbett2000.pirahaNS : NumberSystem

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

Equations

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

def Phenomena.Agreement.Studies.Corbett2000.allNumberSystems : List NumberSystem

Equations

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

theorem Phenomena.Agreement.Studies.Corbett2000.english_two : englishNS.size = 2

theorem Phenomena.Agreement.Studies.Corbett2000.upperSorbian_three : upperSorbianNS.size = 3

theorem Phenomena.Agreement.Studies.Corbett2000.lihir_five : lihirNS.size = 5

theorem Phenomena.Agreement.Studies.Corbett2000.piraha_zero : pirahaNS.size = 0

theorem Phenomena.Agreement.Studies.Corbett2000.bayso_has_general : baysoNS.hasGeneral = true

theorem Phenomena.Agreement.Studies.Corbett2000.japanese_has_general : japaneseNS.hasGeneral = true

theorem Phenomena.Agreement.Studies.Corbett2000.english_no_general : englishNS.hasGeneral = false

theorem Phenomena.Agreement.Studies.Corbett2000.slovene_dual_facultative : sloveneNS.facultative.contains Core.Number.Category.dual = true

theorem Phenomena.Agreement.Studies.Corbett2000.larike_both_facultative : larikeNS.facultative.contains Core.Number.Category.dual = true ∧ larikeNS.facultative.contains Core.Number.Category.trial = true

def Phenomena.Agreement.Studies.Corbett2000.NumberSystem.trialImpliesDual (ns : NumberSystem) : Bool

Trial implies dual: no language has trial without dual.

Equations

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

def Phenomena.Agreement.Studies.Corbett2000.NumberSystem.dualImpliesPlural (ns : NumberSystem) : Bool

Dual implies plural.

Equations

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

def Phenomena.Agreement.Studies.Corbett2000.NumberSystem.pluralImpliesSingular (ns : NumberSystem) : Bool

Plural implies singular (unless the system is empty = no number).

Equations

• ns.pluralImpliesSingular = (!ns.values.contains Core.Number.Category.plural || ns.values.contains Core.Number.Category.singular || ns.values.isEmpty)

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

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

theorem Phenomena.Agreement.Studies.Corbett2000.all_plural_implies_singular : (allNumberSystems.all fun (x : NumberSystem) => x.pluralImpliesSingular) = true

inductive Phenomena.Agreement.Studies.Corbett2000.MarkingStatus : Type

Number marking status at a position on the Animacy Hierarchy.

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

instance Phenomena.Agreement.Studies.Corbett2000.instDecidableEqMarkingStatus : DecidableEq MarkingStatus

Equations

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

def Phenomena.Agreement.Studies.Corbett2000.instBEqMarkingStatus.beq : MarkingStatus → MarkingStatus → Bool

Equations

• Phenomena.Agreement.Studies.Corbett2000.instBEqMarkingStatus.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Agreement.Studies.Corbett2000.instBEqMarkingStatus : BEq MarkingStatus

Equations

• Phenomena.Agreement.Studies.Corbett2000.instBEqMarkingStatus = { beq := Phenomena.Agreement.Studies.Corbett2000.instBEqMarkingStatus.beq }

def Phenomena.Agreement.Studies.Corbett2000.instReprMarkingStatus.repr : MarkingStatus → ℕ → Std.Format

Equations

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

instance Phenomena.Agreement.Studies.Corbett2000.instReprMarkingStatus : Repr MarkingStatus

Equations

• Phenomena.Agreement.Studies.Corbett2000.instReprMarkingStatus = { reprPrec := Phenomena.Agreement.Studies.Corbett2000.instReprMarkingStatus.repr }

def Phenomena.Agreement.Studies.Corbett2000.MarkingStatus.toNat : MarkingStatus → ℕ

Numeric ordering: higher = more marking.

Equations

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

structure Phenomena.Agreement.Studies.Corbett2000.AnimacyNumberProfile : Type

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

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

  Marking status at each position on the hierarchy.

def Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.Corbett2000.englishAnimacy : AnimacyNumberProfile

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

Equations

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

def Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.Corbett2000.allAnimacyProfiles : List AnimacyNumberProfile

Equations

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

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

Constraints I and III hold for all profiled languages.

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

inductive Phenomena.Agreement.Studies.Corbett2000.AgreementType : Type

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

• syntactic : AgreementType
• semantic : AgreementType

instance Phenomena.Agreement.Studies.Corbett2000.instDecidableEqAgreementType : DecidableEq AgreementType

Equations

• Phenomena.Agreement.Studies.Corbett2000.instDecidableEqAgreementType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Agreement.Studies.Corbett2000.instBEqAgreementType : BEq AgreementType

Equations

• Phenomena.Agreement.Studies.Corbett2000.instBEqAgreementType = { beq := Phenomena.Agreement.Studies.Corbett2000.instBEqAgreementType.beq }

def Phenomena.Agreement.Studies.Corbett2000.instBEqAgreementType.beq : AgreementType → AgreementType → Bool

Equations

• Phenomena.Agreement.Studies.Corbett2000.instBEqAgreementType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Agreement.Studies.Corbett2000.instReprAgreementType.repr : AgreementType → ℕ → Std.Format

Equations

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

instance Phenomena.Agreement.Studies.Corbett2000.instReprAgreementType : Repr AgreementType

Equations

• Phenomena.Agreement.Studies.Corbett2000.instReprAgreementType = { reprPrec := Phenomena.Agreement.Studies.Corbett2000.instReprAgreementType.repr }

structure Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.Corbett2000.serboCroatDeca : AgreementProfile

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

Equations

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

def Phenomena.Agreement.Studies.Corbett2000.allAgreementProfiles : List AgreementProfile

Equations

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

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

The Agreement Hierarchy is respected by all profiled controllers.

theorem Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.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

instance Phenomena.Agreement.Studies.Corbett2000.instBEqControllerTargetSystem : BEq ControllerTargetSystem

Equations

• Phenomena.Agreement.Studies.Corbett2000.instBEqControllerTargetSystem = { beq := Phenomena.Agreement.Studies.Corbett2000.instBEqControllerTargetSystem.beq }

def Phenomena.Agreement.Studies.Corbett2000.instBEqControllerTargetSystem.beq : ControllerTargetSystem → ControllerTargetSystem → Bool

Equations

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

def Phenomena.Agreement.Studies.Corbett2000.ControllerTargetSystem.hasMismatch (ct : ControllerTargetSystem) : Bool

Whether controller and target systems differ in size.

Equations

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

def Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.Corbett2000.bayso_mismatch : baysoCT.hasMismatch = true

theorem Phenomena.Agreement.Studies.Corbett2000.hebrew_mismatch : hebrewCT.hasMismatch = true

theorem Phenomena.Agreement.Studies.Corbett2000.english_no_mismatch : englishCT.hasMismatch = false

structure Phenomena.Agreement.Studies.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 : Core.Prominence.AnimacyRank → List NumberValue

  Number values available at each hierarchy position

def Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.Corbett2000.englishIndiv : IndividuationProfile

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

Equations

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

def Phenomena.Agreement.Studies.Corbett2000.allIndividuationProfiles : List IndividuationProfile

Equations

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

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

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

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

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

inductive Phenomena.Agreement.Studies.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.

instance Phenomena.Agreement.Studies.Corbett2000.instDecidableEqResolutionStrategy : DecidableEq ResolutionStrategy

Equations

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

instance Phenomena.Agreement.Studies.Corbett2000.instBEqResolutionStrategy : BEq ResolutionStrategy

Equations

• Phenomena.Agreement.Studies.Corbett2000.instBEqResolutionStrategy = { beq := Phenomena.Agreement.Studies.Corbett2000.instBEqResolutionStrategy.beq }

def Phenomena.Agreement.Studies.Corbett2000.instBEqResolutionStrategy.beq : ResolutionStrategy → ResolutionStrategy → Bool

Equations

• Phenomena.Agreement.Studies.Corbett2000.instBEqResolutionStrategy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Agreement.Studies.Corbett2000.instReprResolutionStrategy : Repr ResolutionStrategy

Equations

• Phenomena.Agreement.Studies.Corbett2000.instReprResolutionStrategy = { reprPrec := Phenomena.Agreement.Studies.Corbett2000.instReprResolutionStrategy.repr }

def Phenomena.Agreement.Studies.Corbett2000.instReprResolutionStrategy.repr : ResolutionStrategy → ℕ → Std.Format

Equations

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

def Phenomena.Agreement.Studies.Corbett2000.NumberValue.semanticResolve (a b : NumberValue) : NumberValue

The result of resolving two number values under semantic resolution.

Equations

• Phenomena.Agreement.Studies.Corbett2000.NumberValue.semanticResolve Core.Number.Category.singular Core.Number.Category.singular = Core.Number.Category.plural
• Phenomena.Agreement.Studies.Corbett2000.NumberValue.semanticResolve Core.Number.Category.singular Core.Number.Category.dual = Core.Number.Category.trial
• Phenomena.Agreement.Studies.Corbett2000.NumberValue.semanticResolve Core.Number.Category.dual Core.Number.Category.singular = Core.Number.Category.trial
• a.semanticResolve b = Core.Number.Category.plural

theorem Phenomena.Agreement.Studies.Corbett2000.sg_sg_resolves_pl : NumberValue.semanticResolve Core.Number.Category.singular Core.Number.Category.singular = Core.Number.Category.plural

Semantic resolution: sg + sg → pl.

theorem Phenomena.Agreement.Studies.Corbett2000.sg_du_resolves_tri : NumberValue.semanticResolve Core.Number.Category.singular Core.Number.Category.dual = Core.Number.Category.trial

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

theorem Phenomena.Agreement.Studies.Corbett2000.animacy_rank_ordering_consistent : Core.Prominence.AnimacyRank.speaker.toNat > Core.Prominence.AnimacyRank.human.toNat ∧ Core.Prominence.AnimacyRank.human.toNat > Core.Prominence.AnimacyRank.higherAnimal.toNat ∧ Core.Prominence.AnimacyRank.higherAnimal.toNat > Core.Prominence.AnimacyRank.discreteInanimate.toNat

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

theorem Phenomena.Agreement.Studies.Corbett2000.english_matches_plurals_typology : englishNS.size = 2 ∧ englishNS.hasGeneral = false ∧ Plurals.Typology.english.occurrence = Plurals.Typology.PluralOccurrence.allNounsAlwaysObligatory

Bridge: English NumberSystem matches the PluralityProfile in Plurals.Typology — both record a 2-value obligatory system.

theorem Phenomena.Agreement.Studies.Corbett2000.japanese_general_vs_wals : japaneseNS.hasGeneral = true ∧ Plurals.Typology.japanese.coding = Plurals.Typology.PluralCoding.noPlural

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

theorem Phenomena.Agreement.Studies.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 Phenomena.Agreement.Studies.Corbett2000.NumberSystem.toNumberStage (ns : NumberSystem) : Typology.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 Phenomena.Agreement.Studies.Corbett2000.piraha_N1 : pirahaNS.toNumberStage = Typology.NumberStage.N1

theorem Phenomena.Agreement.Studies.Corbett2000.english_N2 : englishNS.toNumberStage = Typology.NumberStage.N2

theorem Phenomena.Agreement.Studies.Corbett2000.russian_N2 : russianNS.toNumberStage = Typology.NumberStage.N2

theorem Phenomena.Agreement.Studies.Corbett2000.japanese_N2 : japaneseNS.toNumberStage = Typology.NumberStage.N2

theorem Phenomena.Agreement.Studies.Corbett2000.upperSorbian_N3 : upperSorbianNS.toNumberStage = Typology.NumberStage.N3

theorem Phenomena.Agreement.Studies.Corbett2000.larike_N4 : larikeNS.toNumberStage = Typology.NumberStage.N4

theorem Phenomena.Agreement.Studies.Corbett2000.numberStage_consistent_with_size : pirahaNS.size = 0 ∧ pirahaNS.toNumberStage = Typology.NumberStage.N1 ∧ englishNS.size = 2 ∧ englishNS.toNumberStage = Typology.NumberStage.N2 ∧ upperSorbianNS.size = 3 ∧ upperSorbianNS.toNumberStage = Typology.NumberStage.N3 ∧ larikeNS.size = 4 ∧ larikeNS.toNumberStage = Typology.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 Phenomena.Agreement.Studies.Corbett2000.general_number_iff_bare_kind : (baysoNS.hasGeneral = true ∧ Semantics.Lexical.Noun.Kind.Chierchia1998.canDenoteKind Semantics.Lexical.Noun.Kind.Chierchia1998.NominalMapping.argOnly false = true) ∧ (japaneseNS.hasGeneral = true ∧ Semantics.Lexical.Noun.Kind.Chierchia1998.canDenoteKind Semantics.Lexical.Noun.Kind.Chierchia1998.NominalMapping.argOnly false = true) ∧ englishNS.hasGeneral = false ∧ Semantics.Lexical.Noun.Kind.Chierchia1998.canDenoteKind Semantics.Lexical.Noun.Kind.Chierchia1998.NominalMapping.predOnly false = 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) = true, which holds for argOnly and argAndPred but not predOnly.

inductive Phenomena.Agreement.Studies.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.

instance Phenomena.Agreement.Studies.Corbett2000.instDecidableEqPluralInterpretation : DecidableEq PluralInterpretation

Equations

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

def Phenomena.Agreement.Studies.Corbett2000.instBEqPluralInterpretation.beq : PluralInterpretation → PluralInterpretation → Bool

Equations

• Phenomena.Agreement.Studies.Corbett2000.instBEqPluralInterpretation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Agreement.Studies.Corbett2000.instBEqPluralInterpretation : BEq PluralInterpretation

Equations

• Phenomena.Agreement.Studies.Corbett2000.instBEqPluralInterpretation = { beq := Phenomena.Agreement.Studies.Corbett2000.instBEqPluralInterpretation.beq }

def Phenomena.Agreement.Studies.Corbett2000.instReprPluralInterpretation.repr : PluralInterpretation → ℕ → Std.Format

Equations

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

instance Phenomena.Agreement.Studies.Corbett2000.instReprPluralInterpretation : Repr PluralInterpretation

Equations

• Phenomena.Agreement.Studies.Corbett2000.instReprPluralInterpretation = { reprPrec := Phenomena.Agreement.Studies.Corbett2000.instReprPluralInterpretation.repr }

def Phenomena.Agreement.Studies.Corbett2000.PluralInterpretation.includesSingleton : PluralInterpretation → Bool

Inclusive plural includes singletons; exclusive does not.

Equations

• Phenomena.Agreement.Studies.Corbett2000.PluralInterpretation.inclusive.includesSingleton = true
• Phenomena.Agreement.Studies.Corbett2000.PluralInterpretation.exclusive.includesSingleton = false

theorem Phenomena.Agreement.Studies.Corbett2000.compositional_plural_is_inclusive : PluralInterpretation.inclusive.includesSingleton = true

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