@cite{downing-1996} — Numeral Classifier Systems: The Case of Japanese

@cite{downing-1996} @cite{aikhenvald-2000} @cite{chierchia-1998}

Formalizes core contributions from Downing's monograph on Japanese numeral classifiers (Studies in Discourse and Grammar, vol. 4).

Two Central Hypotheses

Hypothesis 1 (Universal semantic trends): Classifier categories encode culturally significant categories defined by physical, functional, and social interaction. The choice of which features are exploited is culture-dependent.

Hypothesis 2 (Semantic supplementation): Classifiers systematically supplement the information carried by nouns — the classifier system provides categorization independent of and additional to the common noun system.

UNVERIFIED: chapter/section/table location references throughout this file were inherited from earlier formalization work and have not been cross-checked against the @cite{downing-1996} monograph. Specific cell counts in the frequency tables below should be treated as illustrative of the qualitative shape of the data, not as verbatim transcriptions.

Individuation Function

@cite{downing-1996} treats classifier phrases and plural markers as individuators. @cite{chierchia-1998}'s later Nominal Mapping Parameter provides a formal framework for this insight: in [+arg, -pred] languages, bare nouns denote kinds, and classifiers supply individuation for enumeration. The bridge to @cite{chierchia-1998} is a linglib contribution, not one Downing herself makes (Chierchia 1998 postdates this monograph). The strict NMP correlation has been challenged (e.g., Turkish has bare arguments without classifiers; Li 2013 argues Chinese nouns are not uniformly mass), but the core insight — that classifiers relate to individuation — is preserved in current work, with the mechanism (atomization vs. unitization) still debated.

Anaphoric Use

Classifier phrases (numeral + classifier without accompanying noun) serve as anaphoric devices in discourse, occupying a unique niche between zero anaphora (short range) and full lexical NPs (long range). Qualitative findings (UNVERIFIED specific percentages): 人 nin dominates the anaphoric distribution; numeral 2 dominates the numeral distribution; striking distance is intermediate between pronouns and full NPs.

Shape Dimensionality

Shape-based classifiers decompose along a 1D/2D/3D dimensionality axis per @cite{allan-1977}, formalized via Fragments.Japanese.Classifier.shapeDim.

Core Inventory

All 27 classifiers from Downing's core inventory (UNVERIFIED: claimed to be Table 1.1) are represented in the Japanese fragment (Fragments.Japanese.Classifier.core), including the homophonous 軒 kenBuilding / 件 kenIncident pair, the maritime size split (隻 seki / 艘 soo), and the two building classifiers (軒 kenBuilding / 棟 mune).

Frequency Distribution

UNVERIFIED: the n=500 corpus sample and specific cell counts below were inherited from prior formalization work and have not been verified against the monograph. The qualitative pattern they encode is well-attested (extreme Zipfian skew with 人 nin and つ tsu dominating; shape-based classifiers collectively outweigh function-based ones), but the precise numbers should be regarded as a placeholder until reconfirmed.

def Downing1996.shapeClassifiers : List Fragments.Japanese.Classifier

Shape-based classifiers in the Japanese inventory decompose into three dimensionality classes (Downing 1996, UNVERIFIED location).

Equations

• Downing1996.shapeClassifiers = List.filter (fun (c : Fragments.Japanese.Classifier) => decide (c.Encodes Typology.SemanticParameter.shape)) Fragments.Japanese.Classifier.all

theorem Downing1996.shape_classifier_count : shapeClassifiers.length ≥ 5

At least 5 classifiers in the inventory encode shape.

theorem Downing1996.all_dimensions_in_inventory : (shapeClassifiers.any fun (c : Fragments.Japanese.Classifier) => c.shapeDim == some Typology.ShapeDimension.oneD) = true ∧ (shapeClassifiers.any fun (c : Fragments.Japanese.Classifier) => c.shapeDim == some Typology.ShapeDimension.twoD) = true ∧ (shapeClassifiers.any fun (c : Fragments.Japanese.Classifier) => c.shapeDim == some Typology.ShapeDimension.threeD) = true

All three shape dimensions (1D, 2D, 3D) are attested.

theorem Downing1996.animacy_hierarchy_witnessed : Fragments.Japanese.Classifier.nin.Encodes Typology.SemanticParameter.humanness ∧ Fragments.Japanese.Classifier.mei.Encodes Typology.SemanticParameter.humanness ∧ Fragments.Japanese.Classifier.tou.Encodes Typology.SemanticParameter.animacy ∧ Fragments.Japanese.Classifier.hiki.Encodes Typology.SemanticParameter.animacy ∧ Fragments.Japanese.Classifier.tsu.IsDefault

The animacy hierarchy in Japanese classifiers: human (nin/mei) > large animal (tou) > small animal (hiki) > inanimate (tsu). Each level is distinguished by a distinct classifier.

theorem Downing1996.human_has_register_variant : Fragments.Japanese.Classifier.nin.Encodes Typology.SemanticParameter.humanness ∧ Fragments.Japanese.Classifier.mei.Encodes Typology.SemanticParameter.humanness ∧ Fragments.Japanese.Classifier.mei.Encodes Typology.SemanticParameter.register ∧ ¬Fragments.Japanese.Classifier.nin.Encodes Typology.SemanticParameter.register

The human classifier has a formal register variant (名 mei) marking formality/register of the speech act, unlike the neutral 人 nin. Note: this indexes register (formal vs casual) rather than socialStatus (honorific status of the referent — kin, age, social rank).

structure Downing1996.AnaphoricDistribution : Type

Distribution of classifiers in anaphoric examples (Downing 1996, UNVERIFIED location).

• classifier : Fragments.Japanese.Classifier
• count : ℕ

@[implicit_reducible]

instance Downing1996.instReprAnaphoricDistribution : Repr AnaphoricDistribution

Equations

• Downing1996.instReprAnaphoricDistribution = { reprPrec := Downing1996.instReprAnaphoricDistribution.repr }

def Downing1996.instReprAnaphoricDistribution.repr : AnaphoricDistribution → ℕ → Std.Format

Equations

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

def Downing1996.anaphoricClassifierData : List AnaphoricDistribution

UNVERIFIED: cell-precise counts (nin=48, tsu=4, hiki=2, wa=1) inherited from prior formalization. The qualitative claim — that the anaphoric distribution is dominated by -nin and skewed against the long tail — is well-attested; the precise counts have not been cross-checked.

Equations

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

theorem Downing1996.anaphoric_total : List.foldl (fun (x1 x2 : ℕ) => x1 + x2) 0 (List.map (fun (x : AnaphoricDistribution) => x.count) anaphoricClassifierData) = 55

UNVERIFIED: total anaphoric classifier examples = 55 (sum of cells in anaphoricClassifierData).

theorem Downing1996.nin_dominates_anaphoric : Option.map (fun (x : AnaphoricDistribution) => x.count) (List.find? (fun (x : AnaphoricDistribution) => x.classifier == Fragments.Japanese.Classifier.nin) anaphoricClassifierData) = some 48

UNVERIFIED specific count: 人 nin dominates anaphoric classifier use at 48/55 ≈ 87%. The dominance claim is qualitatively robust; the precise count is unverified.

structure Downing1996.NumeralDistribution : Type

Distribution of numerals in anaphoric classifier examples (Downing 1996, UNVERIFIED location). Numeral 1 is absent — explained by competition with zero anaphora.

• numeral : ℕ
• count : ℕ

@[implicit_reducible]

instance Downing1996.instReprNumeralDistribution : Repr NumeralDistribution

Equations

• Downing1996.instReprNumeralDistribution = { reprPrec := Downing1996.instReprNumeralDistribution.repr }

def Downing1996.instReprNumeralDistribution.repr : NumeralDistribution → ℕ → Std.Format

Equations

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

def Downing1996.anaphoricNumeralData : List NumeralDistribution

UNVERIFIED: cell-precise counts (n=2:41, n=3:12, n=4:1, n=5:1) inherited from prior formalization.

Equations

• Downing1996.anaphoricNumeralData = [{ numeral := 2, count := 41 }, { numeral := 3, count := 12 }, { numeral := 4, count := 1 }, { numeral := 5, count := 1 }]

theorem Downing1996.two_dominates_anaphoric : Option.map (fun (x : NumeralDistribution) => x.count) (List.find? (fun (x : NumeralDistribution) => x.numeral == 2) anaphoricNumeralData) = some 41

UNVERIFIED specific count: numeral 2 dominates anaphoric use at 41/55 ≈ 75%.

theorem Downing1996.one_absent_from_anaphoric : (anaphoricNumeralData.all fun (x : NumeralDistribution) => decide (x.numeral ≠ 1)) = true

Numeral 1 is absent from anaphoric classifier constructions. Explanation: 'one' + CL has low contrastive information potential and competes with zero anaphora.

theorem Downing1996.argOnly_has_classifiers : Fragments.Japanese.Nouns.japaneseMapping = Semantics.Kinds.NMP.NominalMapping.argOnly ∧ Aikhenvald2000.japanese.classifierType = Typology.ClassifierType.numeralClassifier

(UNVERIFIED location: Ch. 7) discusses classifier phrases as individuators. @cite{chierchia-1998}'s later linking hypothesis formalizes this: [+arg, -pred] languages have kind-denoting bare nouns and need classifiers for individuation. The strict correlation is contested (see module docstring), but the co-occurrence is robustly attested.

Witnessed by: Japanese is [+arg, -pred] AND has numeral classifiers.

theorem Downing1996.no_blocking_needs_classifiers : Fragments.Japanese.Nouns.japaneseBlocking.iotaBlocked = false ∧ Fragments.Japanese.Nouns.japaneseBlocking.existsBlocked = false ∧ Aikhenvald2000.japanese.classifierType = Typology.ClassifierType.numeralClassifier

In @cite{chierchia-1998}'s framework, [+arg, -pred] languages have no type-shift blocking (no articles), so bare nouns freely occur as arguments. Classifiers rather than articles provide individuation.

theorem Downing1996.classifiers_carry_individuation_info (c : Fragments.Japanese.Classifier) : ¬c.IsDefault → ¬c.IsMensural → c.encodes ≠ []

Non-default classifiers encode at least one semantic parameter, confirming they carry individuation-relevant information beyond mere enumeration. The default classifier つ is the only one that enumerates without individuating. Delegates to the structural theorem in Fragments.Japanese.Classifier.

inductive Downing1996.MorphemeCategoryRelation : Type

Seven recurrent semantic relations between the independent sense of the classifier morpheme and the classifier category. Six are from Downing 1996 (UNVERIFIED location: Ch. 5, Table 5.2); the seventh (sharedQuality) is attested in non-Japanese languages and noted by Downing as recurring cross-linguistically but absent in Japanese.

• identicalClass : MorphemeCategoryRelation

  Morpheme denotes a class identical/superordinate to the category. e.g., 件 ken 'matter' → classifier for incidents.

• partOfMembers : MorphemeCategoryRelation

  Morpheme denotes a part possessed by category members. e.g., 頭 tou 'head' → classifier for large animals.

• associatedAction : MorphemeCategoryRelation

  Morpheme denotes an action associated with category members. e.g., 通 tsuu 'to pass' → classifier for letters/documents.

• exemplar : MorphemeCategoryRelation

  Morpheme denotes an exemplar possessing the defining traits. e.g., 筋 suji 'sinew' → classifier for long, slender objects.

• creationAction : MorphemeCategoryRelation

  Morpheme denotes the action creating category members. e.g., 巻 maki 'to roll up' → classifier for scrolls.

• beneficiaryGoal : MorphemeCategoryRelation

  Morpheme denotes the beneficiary/goal of category activity. e.g., 足 soku 'foot' → classifier for pairs of footwear.

• sharedQuality : MorphemeCategoryRelation

  Morpheme independently represents a quality shared by members. e.g., Indonesian bentuk 'curved' → classifier for rings, wheels.

@[implicit_reducible]

instance Downing1996.instDecidableEqMorphemeCategoryRelation : DecidableEq MorphemeCategoryRelation

Equations

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

def Downing1996.instReprMorphemeCategoryRelation.repr : MorphemeCategoryRelation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Downing1996.instReprMorphemeCategoryRelation : Repr MorphemeCategoryRelation

Equations

• Downing1996.instReprMorphemeCategoryRelation = { reprPrec := Downing1996.instReprMorphemeCategoryRelation.repr }

structure Downing1996.MorphemeRelationWitness : Type

A witness pairing a classifier with its morpheme (UNVERIFIED location: Table 5.2)-category relation and the independent meaning of the morpheme.

• classifier : Fragments.Japanese.Classifier
• relation : MorphemeCategoryRelation
• independentMeaning : String

def Downing1996.instReprMorphemeRelationWitness.repr : MorphemeRelationWitness → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Downing1996.instReprMorphemeRelationWitness : Repr MorphemeRelationWitness

Equations

• Downing1996.instReprMorphemeRelationWitness = { reprPrec := Downing1996.instReprMorphemeRelationWitness.repr }

def Downing1996.table5_2_witnesses : List MorphemeRelationWitness

Concrete morpheme (UNVERIFIED location: Table 5.2)-category relation assignments for classifiers in our inventory. Each entry records the classifier, the relation type, and the independent lexical meaning of the morpheme that motivates the relation.

Equations

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

theorem Downing1996.four_relation_types_attested : (List.map (fun (x : MorphemeRelationWitness) => x.relation) table5_2_witnesses).eraseDups.length ≥ 4

At least four of the six Japanese-attested relation types are witnessed in the inventory (Types 1, 2, 3, 6).

theorem Downing1996.witnesses_in_inventory (w : MorphemeRelationWitness) : w ∈ table5_2_witnesses → w.classifier ∈ Fragments.Japanese.Classifier.all

All witnesses reference classifiers in our inventory. Trivial since Classifier.mem_all says every constructor is in all.

theorem Downing1996.sortal_dominance : (List.filter (fun (c : Fragments.Japanese.Classifier) => decide ¬decide c.IsMensural = true) Fragments.Japanese.Classifier.all).length > (List.filter (fun (c : Fragments.Japanese.Classifier) => decide c.IsMensural) Fragments.Japanese.Classifier.all).length

The Japanese classifier inventory includes both sortal and mensural classifiers, with sortal classifiers dominating.

theorem Downing1996.function_classifiers_numerous : (List.filter (fun (c : Fragments.Japanese.Classifier) => decide (c.Encodes Typology.SemanticParameter.function)) Fragments.Japanese.Classifier.all).length ≥ 8

Function-based classifiers are the largest semantic group, confirming Downing's observation that the system concentrates on interactionally significant categories.

theorem Downing1996.core_inventory_complete : Fragments.Japanese.Classifier.core.length = 27

The core inventory (UNVERIFIED location: Table 1.1) has exactly 27 classifiers.

theorem Downing1996.full_inventory_includes_core (c : Fragments.Japanese.Classifier) : c ∈ Fragments.Japanese.Classifier.core → c ∈ Fragments.Japanese.Classifier.all

Every core classifier is in the full inventory. Trivial by construction: all := core ++ extended ++ sudoAdditions.

theorem Downing1996.two_ken_classifiers : Fragments.Japanese.Classifier.kenBuilding.form = "軒" ∧ Fragments.Japanese.Classifier.kenIncident.form = "件" ∧ Fragments.Japanese.Classifier.kenBuilding.Encodes Typology.SemanticParameter.function ∧ Fragments.Japanese.Classifier.kenIncident.Encodes Typology.SemanticParameter.function

The core inventory distinguishes two homophonous ken classifiers: 軒 kenBuilding and 件 kenIncident — different kanji, different semantic domains.

theorem Downing1996.two_building_classifiers : Fragments.Japanese.Classifier.kenBuilding.gloss = "building" ∧ Fragments.Japanese.Classifier.mune.gloss = "building.roof"

Two building classifiers exist: 軒 kenBuilding (functional capacity — home/shop) and 棟 mune (roofed structure).

theorem Downing1996.maritime_size_split : Fragments.Japanese.Classifier.seki.gloss = "large.boat" ∧ Fragments.Japanese.Classifier.soo.gloss = "small.boat"

Two maritime classifiers exist: 隻 seki (large boats) and 艘 soo (small boats), paralleling the animacy size split (頭 tou / 匹 hiki).

structure Downing1996.FrequencyEntry : Type

Frequency data (UNVERIFIED location: Ch. 3, Table 3.1): raw counts of classifiers in a 500-form corpus sample (first 50 uses from each of five works of fiction + 250 forms from transcribed conversations and oral narrative).

• classifier : Fragments.Japanese.Classifier
• count : ℕ

@[implicit_reducible]

instance Downing1996.instReprFrequencyEntry : Repr FrequencyEntry

Equations

• Downing1996.instReprFrequencyEntry = { reprPrec := Downing1996.instReprFrequencyEntry.repr }

def Downing1996.instReprFrequencyEntry.repr : FrequencyEntry → ℕ → Std.Format

Equations

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

def Downing1996.frequencyData : List FrequencyEntry

UNVERIFIED: 17-cell frequency distribution claimed to be from Downing 1996's n=500 corpus sample. Cells inherited from prior formalization and not cross-checked against the monograph; the qualitative shape (extreme Zipfian skew, -nin and -tsu dominating, shape-based collectively outweighing function-based) is well-attested but the precise counts are placeholders.

Equations

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

theorem Downing1996.nin_most_frequent : Option.map (fun (x : FrequencyEntry) => x.count) (List.find? (fun (x : FrequencyEntry) => x.classifier == Fragments.Japanese.Classifier.nin) frequencyData) = some 201

人 nin is the single most frequent classifier (qualitatively robust). UNVERIFIED specific count: 201/500 ≈ 40%.

theorem Downing1996.nin_tsu_dominate : 201 + 115 = 316 ∧ 316 * 100 / 500 = 63

人 nin and つ tsu together dominate the distribution (qualitatively robust). UNVERIFIED specific arithmetic: 201 + 115 = 316 ≈ 63% of 500.

theorem Downing1996.top_five_dominate : have top5 := [201, 115, 32, 31, 31]; List.foldl (fun (x1 x2 : ℕ) => x1 + x2) 0 top5 = 410 ∧ 410 * 100 / 500 = 82

The top five classifiers (nin, tsu, hiki, hon, mai) account for the bulk of the distribution (Zipfian skew, qualitatively robust). UNVERIFIED specific arithmetic: top-5 sum = 410 ≈ 82% of 500.

theorem Downing1996.quality_over_kind_classifiers : 31 + 31 + 11 > 11

Quality classifiers (shape-based: hon, mai, ko) are collectively more frequent than any individual kind classifier (function-based like ken, dai). observes that "classifiers denoting categories united by a common shape ... are used relatively more often than most of the 'kind-based' classifiers."