Sudo (2016) — The Semantic Role of Classifiers in Japanese

@cite{sudo-2016}

Yasutada Sudo. The Baltic International Yearbook of Cognition, Logic and Communication 11. DOI: 10.4148/1944-3676.1108

Central Claim

Sudo argues that what makes Japanese an obligatory classifier language is not the semantics of nouns (contra @cite{chierchia-1998}, @cite{krifka-2008}, @cite{borer-2005}, @cite{rothstein-2010}, @cite{nemoto-2005}, @cite{li-2011}) but the semantics of numerals. His core proposal:

1. In all natural languages, numerals denote singular terms of type n (constant intensions λw. n, modeled here by NumeralIntens.const).
2. Languages are equipped with a phonologically silent ∪-operator (Semantics.Classifier.upNum) that lifts numerals from type ⟨s,n⟩ to predicates of type ⟨s,⟨e,t⟩⟩.
3. Following @cite{chierchia-1998}'s Blocking Principle, ∪ is blocked in languages whose lexicon contains overt items playing the same role — namely classifiers. In Japanese the classifiers -rin, -hiki, -nin, -mai, -hon, -ko, ... are precisely such items, so ∪ is unavailable and predicative numerals like "okyakusan-wa juu-ni-da" (eq. 15) are ruled out.
4. The inverse ∩-operator (Semantics.Classifier.downNum) maps certain properties back to numeral intensions and has no overt counterpart in either English or Japanese, so it is freely available in both — explaining the well-formedness of Japanese type-n classifier phrases like "juu-ni-nin-da" (eq. 22a).

Cross-paper disagreement

NMP.japaneseStrategy = .forNoun (CLF atomizes a kind-denoting noun) and Sudo2016.japaneseStrategy = .sudoBlocking (CLF blocks the silent ∪-operator on numerals) commit to incompatible analyses of the same empirical fact (Japanese requires classifiers). The disagreement is proved structurally in sudo_disagrees_with_chierchia_on_japanese below and propagates to divergent empirical predictions through LMR's diagnostic battery (LittleMoroneyRoyer2022.predictionsOf).

What is formalized

• Per-classifier ClassifierDenot instances for the six core atomic-sortal classifiers Sudo cites or instantiates: -rin, -hiki, -nin, -mai, -hon, -ko.
• The four empirical paradigms (15)/(16)/(17a/b)/(22) at the level of the Sudo apparatus: predicative numerals require ∪, ∪ is blocked in Japanese by the presence of overt classifiers, ∩ is available so type-n classifier phrases compose.
• A cross-paper theorem locating the disagreement with the chierchia-1998 strategy assignment in the typology file.

Out of scope

• Non-atomic classifiers -kumi (pair) and -daasu (dozen) per Sudo (9a/b) require explicit mereological joins of disjoint pairs.
• Sudo's optional-classifier-language follow-up (Armenian, Hausa) per @cite{bale-khanjian-2008}, @cite{bale-khanjian-2014}, @cite{doetjes-2013} is left as a separate study file.
• The full presupposition-tracking ∪-Shifted FA / PM compositional rules (Sudo eqs. 11/19/26) are referenced via the type-shift signatures in Composition.lean; their full domain-of-definition machinery is not implemented here.

§1: Toy Domain

A minimal world type and entity domain sufficient to instantiate Sudo's sortal classifiers. The domain is intentionally small — Sudo's argument is type-theoretic, not data-driven.

@[reducible, inline]

abbrev Sudo2016.World : Type

The toy world type. Sudo's intensional analysis is parameterized over worlds; for the purposes of demonstrating type-shifts, a singleton world suffices. Real applications would parameterize over a richer World type from Core.Logic.Intensional.Frame.

Equations

• Sudo2016.World = Unit

inductive Sudo2016.Entity : Type

A toy entity domain: a person, a flower, an animal (small), and a book. Six core classifiers can be selectively defined over this minimal domain.

• hanako : Entity
• hana : Entity
• inu : Entity
• hon : Entity
• ringo : Entity
• kami : Entity

@[implicit_reducible]

instance Sudo2016.instDecidableEqEntity : DecidableEq Entity

Equations

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

def Sudo2016.instReprEntity.repr : Entity → ℕ → Std.Format

Equations

• Sudo2016.instReprEntity.repr Sudo2016.Entity.hanako prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Entity.hanako")).group prec✝
• Sudo2016.instReprEntity.repr Sudo2016.Entity.hana prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Entity.hana")).group prec✝
• Sudo2016.instReprEntity.repr Sudo2016.Entity.inu prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Entity.inu")).group prec✝
• Sudo2016.instReprEntity.repr Sudo2016.Entity.hon prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Entity.hon")).group prec✝
• Sudo2016.instReprEntity.repr Sudo2016.Entity.ringo prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Entity.ringo")).group prec✝
• Sudo2016.instReprEntity.repr Sudo2016.Entity.kami prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Entity.kami")).group prec✝

@[implicit_reducible]

instance Sudo2016.instReprEntity : Repr Entity

Equations

• Sudo2016.instReprEntity = { reprPrec := Sudo2016.instReprEntity.repr }

@[implicit_reducible]

instance Sudo2016.instPartialOrderEntity : PartialOrder Entity

Equations

• Sudo2016.instPartialOrderEntity = { le := fun (x y : Sudo2016.Entity) => x = y, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := Sudo2016.instPartialOrderEntity._proof_1, le_antisymm := ⋯ }

§2: Sortal Predicates

Each is a constant intension (rigid) over the toy domain. Named here (rather than inlined into japaneseSudoDenot) so that apply-computation theorems can reference them directly.

def Sudo2016.flowerIntens : Core.Intension World (Entity → Prop)

flower(x): sortal for -rin (Sudo eq. 4).

Equations

• Sudo2016.flowerIntens = Core.Intension.rigid fun (x : Sudo2016.Entity) => x = Sudo2016.Entity.hana

def Sudo2016.humanIntens : Core.Intension World (Entity → Prop)

human(x): sortal for -nin (Sudo eq. 8a).

Equations

• Sudo2016.humanIntens = Core.Intension.rigid fun (x : Sudo2016.Entity) => x = Sudo2016.Entity.hanako

def Sudo2016.smallAnimalIntens : Core.Intension World (Entity → Prop)

small_animal(x): sortal for -hiki (Sudo eq. 8b's atomic-sortal core).

Equations

• Sudo2016.smallAnimalIntens = Core.Intension.rigid fun (x : Sudo2016.Entity) => x = Sudo2016.Entity.inu

def Sudo2016.bookIntens : Core.Intension World (Entity → Prop)

bound_volume(x): sortal for -satsu.

Equations

• Sudo2016.bookIntens = Core.Intension.rigid fun (x : Sudo2016.Entity) => x = Sudo2016.Entity.hon

def Sudo2016.roundIntens : Core.Intension World (Entity → Prop)

round(x): sortal for -ko.

Equations

• Sudo2016.roundIntens = Core.Intension.rigid fun (x : Sudo2016.Entity) => x = Sudo2016.Entity.ringo

def Sudo2016.flatIntens : Core.Intension World (Entity → Prop)

flat(x): sortal for -mai.

Equations

• Sudo2016.flatIntens = Core.Intension.rigid fun (x : Sudo2016.Entity) => x = Sudo2016.Entity.kami

§3: Per-Classifier Denotations

The exhaustive map from Fragments.Japanese.Classifier to ClassifierDenot. Pattern matching on the typed inventory forces every classifier to either get a denotation or an explicit none for the deferred cases (mensural -hai/-shoku/-teki, non-atomic -kumi/-daasu, function-based classifiers without a sortal predicate over our toy domain). Adding a classifier to the fragment requires extending this match — the type checker catches missing cases, replacing the prior floating-def style.

def Sudo2016.japaneseSudoDenot : Fragments.Japanese.Classifier → Option (Semantics.Classifier.ClassifierDenot World Entity)

Atomic-sortal denotation builder for the six classifiers Sudo formalizes over our toy domain. none for classifiers we haven't formalized (most function-based ones, mensural ones, non-atomic group ones).

Equations

• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.rin = some (Semantics.Classifier.ClassifierDenot.ofSortal Sudo2016.flowerIntens)
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.nin = some (Semantics.Classifier.ClassifierDenot.ofSortal Sudo2016.humanIntens)
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.hiki = some (Semantics.Classifier.ClassifierDenot.ofSortal Sudo2016.smallAnimalIntens)
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.satsu = some (Semantics.Classifier.ClassifierDenot.ofSortal Sudo2016.bookIntens)
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.ko = some (Semantics.Classifier.ClassifierDenot.ofSortal Sudo2016.roundIntens)
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.mai = some (Semantics.Classifier.ClassifierDenot.ofSortal Sudo2016.flatIntens)
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.hai = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.shoku = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.teki = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.kumi = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.daasu = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.tsu = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.mei = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.tou = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.wa = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.hon = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.tsubu = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.sao = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.dai = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.kenBuilding = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.kenIncident = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.ki = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.ku = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.kyoku = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.mon = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.mune = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.seki = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.soku = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.soo = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.ten = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.toori = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.tsuu = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.kabu = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.furi = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.zen = none
• Sudo2016.japaneseSudoDenot Fragments.Japanese.Classifier.kyaku = none

def Sudo2016.sudoFormalized : List Fragments.Japanese.Classifier

The classifiers Sudo formalizes (the six atomic-sortal cases).

Equations

• Sudo2016.sudoFormalized = List.filter (fun (c : Fragments.Japanese.Classifier) => (Sudo2016.japaneseSudoDenot c).isSome) Fragments.Japanese.Classifier.all

theorem Sudo2016.six_classifiers_formalized : sudoFormalized.length = 6

Exactly six classifiers have a Sudo-style denotation in this file.

§4: Sudo's Paradigms (eqs. 15, 16, 17, 22)

The empirical contrast that motivates the analysis. Sudo's argument structure: (a) numerals can't predicate in Japanese (eq. 15); (b) adding a classifier rescues the predication (eq. 16); (c) the same pattern repeats with non-human classifiers (eq. 17). The numeral+classifier phrase is type-n by ∩ (eq. 22).

def Sudo2016.six : Semantics.Classifier.NumeralIntens World

The numeral six as a Sudo-style type-n singular term: λw. 6.

Equations

• Sudo2016.six = Semantics.Classifier.NumeralIntens.const 6

def Sudo2016.twelve : Semantics.Classifier.NumeralIntens World

The numeral twelve as a Sudo-style type-n singular term: λw. 12.

Equations

• Sudo2016.twelve = Semantics.Classifier.NumeralIntens.const 12

def Sudo2016.four : Semantics.Classifier.NumeralIntens World

The numeral four as a Sudo-style type-n singular term: λw. 4.

Equations

• Sudo2016.four = Semantics.Classifier.NumeralIntens.const 4

def Sudo2016.japaneseHasOvertClassifiers : Bool

Whether Japanese has overt classifiers in the lexicon. Derived from the Japanese fragment's classifier inventory being non-empty. Sudo's blocking argument depends on this fragment-level fact.

Equations

• Sudo2016.japaneseHasOvertClassifiers = !Fragments.Japanese.Classifier.all.isEmpty

§5: The Blocking Argument (Sudo §3)

Sudo eq. 15 (*kyoo-no okyakusan-wa juu-ni-da, intended: 'the guests today are twelve'): a predicative numeral is ungrammatical in Japanese, despite being grammatical in English (Rothstein 2013). Sudo derives this from @cite{chierchia-1998}'s Blocking Principle: the silent ∪-operator that would type-shift the numeral is unavailable in Japanese because classifiers in the lexicon already do that work.

theorem Sudo2016.japanese_blocks_upShift : Semantics.Classifier.upAvailability japaneseHasOvertClassifiers = Semantics.Classifier.UpAvailability.blocked

The ∪-shift on numerals is blocked in Japanese. This is a corollary of the Blocking Principle applied to the fragment-level fact that Japanese has classifiers.

theorem Sudo2016.predicative_numerals_blocked : Semantics.Classifier.upAvailability japaneseHasOvertClassifiers ≠ Semantics.Classifier.UpAvailability.available

Empirical content (Sudo eq. 15 → eq. 16): predicative numerals are out in Japanese; adding a classifier rescues the predication. This holds at the level of ∪-availability: the bare numeral has no shift to ⟨s,⟨e,t⟩⟩, so it cannot serve as a predicate.

§6: ∩ Is Available (Sudo §4, eq. 22)

Sudo eq. 22a (*kyoo-no okyakusan-no kazu-wa juu-ni-nin-da, 'the number of guests today is twelve'): a numeral+classifier phrase serves as a type-n singular term, identifying the cardinality 12. Sudo derives this from the ∩-operator, which has no overt counterpart in either English or Japanese, so it is freely available in both languages.

Note: The ∩-operator (downNum) has no overt classifier counterpart and is therefore not subject to the Blocking Principle. The empirical content is that numeral+classifier phrases can be type-n singular terms; no language-by-language stipulation is needed here.

§6b: apply-computation theorems (load-bearing denotations)

These theorems exercise the ClassifierDenot.apply body on concrete toy-domain inputs, demonstrating that japaneseSudoDenot denotations actually compute Sudo's eq. 4 / eq. 8 semantics rather than functioning as a typed-but-inert classification table.

theorem Sudo2016.nin_one_hanako : (Semantics.Classifier.ClassifierDenot.ofSortal humanIntens).apply () 1 Entity.hanako

Sudo eq. 8a applied at numeral 1 to .hanako: -nin recognises a single-human individual. The denotation (japaneseSudoDenot .nin) actually computes a true conjunction (sortal holds + count = 1).

theorem Sudo2016.rin_one_hana : (Semantics.Classifier.ClassifierDenot.ofSortal flowerIntens).apply () 1 Entity.hana

Sudo eq. 4 applied at numeral 1 to .hana: -rin recognises a single-flower individual.

theorem Sudo2016.hiki_one_inu : (Semantics.Classifier.ClassifierDenot.ofSortal smallAnimalIntens).apply () 1 Entity.inu

Sudo eq. 8b applied at numeral 1 to .inu: -hiki recognises a single small-animal individual.

theorem Sudo2016.nin_not_inu : ¬(Semantics.Classifier.ClassifierDenot.ofSortal humanIntens).apply () 1 Entity.inu

Sortal failure: -nin does not recognise the dog .inu as one human, because the human sortal presupposition fails on .inu. The first conjunct of apply is False.

theorem Sudo2016.nin_ne_hiki : japaneseSudoDenot Fragments.Japanese.Classifier.nin ≠ japaneseSudoDenot Fragments.Japanese.Classifier.hiki

The denotations of distinct atomic-sortal classifiers differ: -nin and -hiki carry incompatible sortal predicates, so substituting one for the other on a -nin-positive input contradicts.

§7: Sudo's Per-Language Strategy Assignment + Cross-Paper Engagement

Per-language strategy assignments live in study files (not as metadata on NounCategorizationSystem). Sudo's view is now a first-class constructor of ClassifierStrategy (.sudoBlocking), so the disagreement with @cite{chierchia-1998} reduces to a single decidable inequality.

def Sudo2016.japaneseStrategy : Typology.ClassifierStrategy

Sudo's strategy assignment for Japanese: classifier blocks the silent ∪-operator on numerals (Sudo §3, eqs. 15–16).

Equations

• Sudo2016.japaneseStrategy = Typology.ClassifierStrategy.sudoBlocking

theorem Sudo2016.sudo_disagrees_with_chierchia_on_japanese : japaneseStrategy ≠ NMP.japaneseStrategy

Sudo and Chierchia disagree about which strategy Japanese exhibits: Chierchia's analysis assigns .forNoun (CLF atomizes a kind-denoting noun); Sudo's assigns .sudoBlocking (CLF blocks the silent ∪-operator on numerals). The disagreement is structural, not editorial.

The two also disagree on the empirical predictions this generates under @cite{little-moroney-royer-2022}'s diagnostic battery — see LittleMoroneyRoyer2022.predictionsOf for the per-strategy profiles.

§8: Framework-applicability

Sudo's blocking-principle account (eqs. 10/15/16) presupposes that the target language has obligatory overt classifiers in the lexicon — that is what blocks the silent ∪-operator. NounCategorizationSystem.IsObligatory is the input-shape requirement; Sudo's framework applies iff it holds. Languages where numerals combine with bare nouns (no obligatory CL) do not provide the right input.

@[reducible, inline]

abbrev Sudo2016.frameworkApplies (cs : Typology.NounCategorizationSystem) : Prop

Sudo's framework applies to a language with classifier system cs iff cs.IsObligatory — the lexical input that Sudo's silent ∪-operator gets blocked by.

Equations

• Sudo2016.frameworkApplies cs = cs.IsObligatory