Grammatical number

Number is Corbett's inventory of number values, the vocabulary in which number systems, agreement, resolution and the semantics of number are stated. A value is determinate when its cardinality boundary is fixed, as for the singular, dual and trial, and the general, a form noncommittal to cardinality, lies outside the number system. The Universal Dependencies tags that corpora annotate (Morphology/Word/UD.lean) lack the general, minimal, augmented and unit augmented values and add inverse, collective and count categories. The quadral is excluded, Corbett reanalysing apparent quadrals (Sursurunga, Tangga) as paucals.

A number system is the set of values a language has. The implicational universals that constrain which sets occur are claims of the papers that state them, proved there of the systems each theory generates. The substrate keeps what cardinality decides, whether the determinate values of a system form an initial segment, which number resolution needs.

Main definitions

• Number: the number values.
• Number.System: a language's number values, which of them are facultative, and whether it has general number.
• Number.System.DeterminateInitial: the determinate values are an initial segment.

Implementation notes

Harbour's implicational universals and the order his features induce on the values are in Studies/Harbour2014.lean, the feature decomposition of the singular, dual and plural is in Semantics/Plurality/NumberFeatures.lean, and coordinate resolution in Syntax/Number/Resolve.lean.

References

• [Cor00]
• [Har14a]
• [Gri18]

inductive Number : Type

The grammatical number values are those of [Cor00]'s typology.

• general : Number

  The general is noncommittal to cardinality and lies outside the number system (Bayso lúban 'lion(s)', Japanese inu 'dog(s)'). It is a form of a noun that has number, unlike a noncountable noun, which lacks the contrast ([Gri18], Studies/Grimm2018.lean).

• singular : Number

  The singular denotes exactly one individual, [+atomic, +minimal].

• dual : Number

  The dual denotes exactly two, [−atomic, +minimal].

• trial : Number

  The trial denotes exactly three, recursive [+minimal] on the plural region.

• paucal : Number

  The paucal denotes a few, with an indeterminate boundary, [−additive].

• plural : Number

  The plural denotes more than one, the residual value, [−atomic] or [+additive].

• greaterPaucal : Number

  The greater paucal is indeterminate and larger than the paucal, [−additive +additive], a second bounded region above the paucal.

• greaterPlural : Number

  The greater plural denotes abundance, [+additive] above a high cut.

• minimal : Number

  The minimal is [+minimal] without [±atomic], covering atoms and minimal non-atoms alike, unlike the singular.

• augmented : Number

  The augmented is [−minimal] without [±atomic], the complement of the minimal.

• unitAugmented : Number

  The unit augmented is recursive [+minimal] on the augmented region, the minimal non-minimal, unlike the dual.

• globalPlural : Number

  The global plural denotes every instance in the domain of discourse, the cut of [±additive] at the top of the lattice, tentative in [Har14a].

@[instance_reducible]

instance instDecidableEqNumber : DecidableEq Number

Equations

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

def instReprNumber.repr : Number → ℕ → Std.Format

Equations

• instReprNumber.repr Number.general prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.general")).group prec✝
• instReprNumber.repr Number.singular prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.singular")).group prec✝
• instReprNumber.repr Number.dual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.dual")).group prec✝
• instReprNumber.repr Number.trial prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.trial")).group prec✝
• instReprNumber.repr Number.paucal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.paucal")).group prec✝
• instReprNumber.repr Number.plural prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.plural")).group prec✝
• instReprNumber.repr Number.greaterPaucal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.greaterPaucal")).group prec✝
• instReprNumber.repr Number.greaterPlural prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.greaterPlural")).group prec✝
• instReprNumber.repr Number.minimal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.minimal")).group prec✝
• instReprNumber.repr Number.augmented prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.augmented")).group prec✝
• instReprNumber.repr Number.unitAugmented prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.unitAugmented")).group prec✝
• instReprNumber.repr Number.globalPlural prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Number.globalPlural")).group prec✝

@[instance_reducible]

instance instReprNumber : Repr Number

Equations

• instReprNumber = { reprPrec := instReprNumber.repr }

@[instance_reducible]

instance instFintypeNumber : Fintype Number

Equations

• instFintypeNumber = { elems := { val := ↑Number.enumList, nodup := Number.enumList_nodup }, complete := instFintypeNumber._proof_1 }

Classification predicates

def Number.isDeterminate : Number → Prop

A number value is determinate when its cardinality boundary is fixed. The minimal and unit augmented are not, since they depend on the composition of the group.

Equations

• Number.singular.isDeterminate = True
• Number.dual.isDeterminate = True
• Number.trial.isDeterminate = True
• x✝.isDeterminate = False

@[instance_reducible]

instance Number.instDecidablePredIsDeterminate : DecidablePred isDeterminate

Equations

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

def Number.exactCard : Number → Option ℕ

A determinate value's referent has an exact cardinality, one for the singular, two for the dual and three for the trial; the other values have none.

Equations

• Number.singular.exactCard = some 1
• Number.dual.exactCard = some 2
• Number.trial.exactCard = some 3
• x✝.exactCard = none

def Number.fromCard : ℕ → Number

fromCard n is the determinate value of cardinality n, and the residual plural from four on, the greater plural being a value of abundance rather than of four or more.

Equations

• Number.fromCard 1 = Number.singular
• Number.fromCard 2 = Number.dual
• Number.fromCard 3 = Number.trial
• Number.fromCard x✝ = Number.plural

Number systems

structure Number.System : Type

A number system records the values available in a language, which of them are facultative, and whether the language has general number ([Cor00] §2.3).

• values : Finset Number

  The values available within the number system.

• hasGeneral : Bool

  Whether the language has general number, a form outside the system.

• facultative : Finset Number

  The facultative values, whose use is optional.

def Number.instDecidableEqSystem.decEq (x✝ x✝¹ : System) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Number.instDecidableEqSystem : DecidableEq System

Equations

• Number.instDecidableEqSystem = Number.instDecidableEqSystem.decEq

def Number.System.DeterminateInitial (ns : System) : Prop

A system's determinate values are an initial segment of the singular, dual and trial when, with the value of a cardinality, it has the value of every smaller positive one, as the dual requires the singular and the trial the dual ([Har14a] Table 1).

Equations

• ns.DeterminateInitial = ∀ v ∈ ns.values, ∀ m ∈ Finset.Icc 1 (v.exactCard.getD 0), Number.fromCard m ∈ ns.values

@[instance_reducible]

instance Number.System.instDecidablePredDeterminateInitial : DecidablePred DeterminateInitial

Equations

• x✝.instDecidablePredDeterminateInitial = id inferInstance