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

[Sud16]

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 [Chi98], [Kri08], [Bor05], [rothstein-2010], [Nem05], [Li11]) 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 [Chi98]'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 [BK08], [BK14], [Doe13] 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 the composition section below; their full domain-of-definition machinery is not implemented here.

Classifier denotations (Sudo eq. 4)

[Sud16]

A classifier denotation in Sudo's framework: at each world w, the classifier takes a numeral n and an entity x, presupposes a sortal predicate P_w(x), and asserts that x is the join of n atomic P-parts.

Concretely, Sudo (2016, eq. 4): ⟦-rin⟧ = λw. λn. λx : *flower_w(x). |{y ⊑ x : flower_w(y)}| = n

This contrasts with the Chierchia / Little-Moroney-Royer framework in Semantics/Classifier.lean, where the classifier is a noun-side predicate transformer (E → Prop) → (E → Prop) that atomizes the noun denotation without reference to a numeral. The two views are different theoretical commitments.

Key types

• ClassifierDenot W E — sortal + counting predicates (intensional)
• ClassifierDenot.apply — Sudo's body: sortal_w(x) ∧ |{y ≤ x : counted_w(y)}| = n
• ClassifierDenot.ofSortal — atomic-sortal constructor (the common case)

Out of scope

Non-atomic classifiers like -kumi (pair) and -daasu (dozen) per Sudo (9a/b) require explicit mereological joins of disjoint pairs and are not expressible via ofSortal. A separate constructor will be added when the non-atomic case is needed.

structure Semantics.Classifier.ClassifierDenot (W : Type u) (E : Type v) [PartialOrder E] : Type (max u v)

A Sudo-style classifier denotation: at each world, a sortal presupposition plus a predicate whose ⊑-atomic parts of x are counted.

For atomic-sortal classifiers (the common case: -rin, -hiki, -nin, -mai, -hon, -ko, -tou), sortal = counted. For mensural classifiers like -hai (cupful), the relationship is more nuanced and handled by separate constructors.

• sortal : Intensional.Intension W (E → Prop)

  The sortal presupposition. ⟦-rin⟧ presupposes flower; ⟦-nin⟧ presupposes human; ⟦-hiki⟧ presupposes animal ∧ small.

• counted : Intensional.Intension W (E → Prop)

  The countable base whose atomic ⊑-parts of x are counted. For atomic-sortal classifiers, counted = sortal (see ofSortal).

noncomputable def Semantics.Classifier.atomCount {W : Type u} {E : Type v} [PartialOrder E] (P : Intensional.Intension W (E → Prop)) (w : W) (x : E) : ℕ

The atom-count measure: the number of ⊑-atomic P-parts of x in world w. Noncomputable (Set.ncard); this is the μ over which classifier counting is ordinary numeral comparison (Comparison.eq.over), and the same set the Sudo ∪/∩ operators (upNum/downNum) count.

Equations

• Semantics.Classifier.atomCount P w x = {y : E | y ≤ x ∧ P w y}.ncard

def Semantics.Classifier.ClassifierDenot.ofSortal {W : Type u} {E : Type v} [PartialOrder E] (P : Intensional.Intension W (E → Prop)) : ClassifierDenot W E

Construct an atomic-sortal classifier from a single predicate. The sortal and the counting base coincide — the standard case in Sudo (4) for -rin, (8a) for -nin, (8b) for -hiki (with the sortal being a conjunction small ∧ animal).

Equations

• Semantics.Classifier.ClassifierDenot.ofSortal P = { sortal := P, counted := P }

def Semantics.Classifier.ClassifierDenot.apply {W : Type u} {E : Type v} [PartialOrder E] (cl : ClassifierDenot W E) (w : W) (n : ℕ) (x : E) : Prop

The body of Sudo's denotation (eq. 4): apply cl w n x iff sortal_w(x) AND the count of x's ⊑-atomic counted-parts equals n.

The counting clause is the exact (=) case of the shared comparison-over-a-measure primitive Core.Order.Comparison.over, with the measure being the atom-count λx. |{y ⊑ x : counted_w(y)}| — classifier counting is numeral comparison with μ = atom-count, the same primitive measure phrases and bare cardinals use. (Set.ncard returns 0 on infinite sets; for natural-language counting the relevant sets are finite.)

Equations

• cl.apply w n x = (cl.sortal w x ∧ x ∈ Core.Order.Comparison.eq.over (Semantics.Classifier.atomCount cl.counted w) n)

@[simp]

theorem Semantics.Classifier.ClassifierDenot.ofSortal_sortal {W : Type u} {E : Type v} [PartialOrder E] (P : Intensional.Intension W (E → Prop)) : (ofSortal P).sortal = P

@[simp]

theorem Semantics.Classifier.ClassifierDenot.ofSortal_counted {W : Type u} {E : Type v} [PartialOrder E] (P : Intensional.Intension W (E → Prop)) : (ofSortal P).counted = P

theorem Semantics.Classifier.ClassifierDenot.apply_ofSortal {W : Type u} {E : Type v} [PartialOrder E] (P : Intensional.Intension W (E → Prop)) (w : W) (n : ℕ) (x : E) : (ofSortal P).apply w n x ↔ P w x ∧ {y : E | y ≤ x ∧ P w y}.ncard = n

For atomic-sortal classifiers, the body reduces to the join of the sortal presupposition and the cardinality constraint over P.

Numerals as type-n singular terms

[Sud16]

Sudo's central typed-semantic claim: in all natural languages, numerals denote singular terms of type n (an abstract numerical type). They are constant intensions λw_s. n (Sudo eq. 2):

⟦roku⟧ = ⟦six⟧ = λw_s. 6

In English (and other non-classifier languages), numerals can also be type-shifted to predicates/modifiers via a phonologically silent ∪-operator (Sudo eq. 10). In Japanese (and other obligatory-classifier languages), the ∪-operator is blocked by the lexical presence of classifiers (Chierchia 1998's Blocking Principle); numerals must combine with a classifier to acquire a predicative type.

The inverse ∩-operator maps certain properties back to type-n constants (Sudo eq. 24). Unlike ∪, ∩ has no overt counterpart in English or Japanese — it is freely available as a covert type-shift in both.

Architecture

NumeralIntens W is Intension W ℕ — a constant intension at a numeral value is a "type-n singular term" in Sudo's sense. The ∪/∩ operators specialized to numerals are defined in Composition.lean, where they combine with the classifier denotations from Defs.lean.

This file deliberately avoids committing to whether type n is "the naturals" ℕ, "the integers" ℤ, "abstract amounts" (Scontras 2014), or "kinds whose extension is a fixed cardinal" — Sudo's empirical arguments are agnostic about the deep ontology. We use ℕ for formalization convenience.

@[reducible, inline]

abbrev Semantics.Classifier.NumeralIntens (W : Type u) : Type u

A numeral intension: a function from worlds to natural-number meanings. [Sud16] (eq. 2) ⟦six⟧ = λw_s. 6 is a NumeralIntens W for any world type W.

Equations

• Semantics.Classifier.NumeralIntens W = Intensional.Intension W ℕ

def Semantics.Classifier.NumeralIntens.const {W : Type u} (n : ℕ) : NumeralIntens W

The rigid numeral intension: a numeral n denotes the constant function λw. n. This is Intension.rigid specialized to ℕ.

Equations

• Semantics.Classifier.NumeralIntens.const n = Intensional.Intension.rigid n

@[simp]

theorem Semantics.Classifier.NumeralIntens.const_apply {W : Type u} (n : ℕ) (w : W) : const n w = n

theorem Semantics.Classifier.NumeralIntens.const_isRigid {W : Type u} (n : ℕ) : Intensional.Intension.IsRigid (const n)

Every constant numeral intension is rigid. Sudo's empirical claim that numerals do not vary across worlds is the rigidity of NumeralIntens.const.

Composition rules: type-shifters and blocking

[Sud16] [Chi98]

The compositional apparatus that allows numerals (type ⟨s,n⟩) and classifier-modified numeral phrases (type ⟨s,⟨e,t⟩⟩ after classifier application) to combine with noun denotations.

Sudo's Three Type-Shifters

• ∪-operator (Sudo eq. 10): ∪(λw. n) = λw. λx. |{y ⊑ x : atomic_w(y)}| = n. Lifts a numeral intension ⟨s,n⟩ to a predicate ⟨s,⟨e,t⟩⟩ over entities with exactly n atomic parts.
• ∩-operator (Sudo eq. 24): the partial inverse of ∪. Maps certain properties back to numeral intensions.
• The composition rules ∪-Shifted PM (eq. 11), ∪-Shifted FA v1/v2 (eqs. 19a, 19b, 26a, 26b), and ∩-Shifted FA (eq. 26c) lift Heim & Kratzer's standard FA / PM by inserting ∪/∩ at type mismatches.

The Blocking Principle (Chierchia 1998, applied by Sudo 2016 §2.3)

The crucial cross-linguistic asymmetry is that Sudo's ∪-operator is blocked in Japanese by the presence of overt classifiers in the lexicon — but available in English, where there is no equivalent overt operator. This is Chierchia (1998)'s Blocking Principle applied to a phonologically silent type-shifter on numerals.

We formalize blocking as an UpAvailability enum derived from whether the language has classifiers in its lexicon. The downstream consequence — that predicative numerals like "The guests are twelve" (English ✓) vs "okyakusan-wa juu-ni-da" (Japanese ✗, Sudo eq. 15) — is then a corollary, not a stipulation.

Scope

This file defines the type signatures and the blocking machinery. The presupposition-tracking compositional rules (PM/FA with full domain-of-definition checking per Sudo eqs. 11/19/26) are out of scope for the first pass; they require partial-function plumbing that is peripheral to the cross-paper argument the file is meant to enable.

def Semantics.Classifier.upNum {W : Type u} {E : Type v} [PartialOrder E] (atomic : Intensional.Intension W (E → Prop)) (n : NumeralIntens W) : Intensional.Intension W (E → Prop)

Sudo's ∪-operator on numeral intensions (eq. 10): ∪(n)(w)(x) iff x has exactly n w atomic ⊑-parts according to the contextually-supplied atomicity predicate atomic.

In the type-theoretic semantics literature this is a type shift ⟨s,n⟩ → ⟨s,⟨e,t⟩⟩.

Equations

• Semantics.Classifier.upNum atomic n w x = (Semantics.Classifier.atomCount atomic w x = n w)

@[simp]

theorem Semantics.Classifier.upNum_apply {W : Type u} {E : Type v} [PartialOrder E] (atomic : Intensional.Intension W (E → Prop)) (n : NumeralIntens W) (w : W) (x : E) : upNum atomic n w x ↔ {y : E | y ≤ x ∧ atomic w y}.ncard = n w

noncomputable def Semantics.Classifier.downNum {W : Type u} {E : Type v} [PartialOrder E] (atomic P : Intensional.Intension W (E → Prop)) (w : W) : Option ℕ

Sudo's ∩-operator (eq. 24): a partial inverse of upNum. downNum P w returns the cardinality of atomic P-parts of any element of P w, packaged as a Option ℕ to model partiality (Sudo notes ∩ is only defined for "certain properties").

This is a placeholder signature; a fuller treatment would parameterize over a uniqueness-of-cardinality witness and would establish ∪ ∘ ∩ = id on the property image of ∪. Marked noncomputable because the inverse of an arbitrary intensional property is not constructively decidable.

Equations

• Semantics.Classifier.downNum atomic P w = if h : ∃ (x : E), P w x then some (Semantics.Classifier.atomCount atomic w h.choose) else none

inductive Semantics.Classifier.UpAvailability : Type

Whether the silent ∪-shift on numerals is available in a language.

Sudo (2016, §2.3) follows Chierchia (1998)'s Blocking Principle: a silent operator is blocked when there are overt lexical items playing the same role. In Japanese, the classifiers -rin/-hiki/-nin/... play the role ∪ would play (turning numerals into predicates), so ∪ is blocked. In English, no such overt items exist, so ∪ is available.

• available : UpAvailability

  No overt classifier blocks the silent ∪-operator (English-like).

• blocked : UpAvailability

  An overt classifier in the lexicon blocks ∪ (Japanese-like).

@[instance_reducible]

instance Semantics.Classifier.instDecidableEqUpAvailability : DecidableEq UpAvailability

Equations

• Semantics.Classifier.instDecidableEqUpAvailability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Classifier.instReprUpAvailability.repr : UpAvailability → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Semantics.Classifier.instReprUpAvailability : Repr UpAvailability

Equations

• Semantics.Classifier.instReprUpAvailability = { reprPrec := Semantics.Classifier.instReprUpAvailability.repr }

def Semantics.Classifier.upAvailability (hasOvertClassifiers : Bool) : UpAvailability

Derivation of UpAvailability from lexicon facts: ∪ is available iff the language has no classifiers in its lexicon.

This is not a stipulation about which languages allow predicative numerals — it is a derivation of that fact from the deeper Blocking Principle. Whether a particular language has classifiers is a fragment- level fact (Fragments.{Lang}.Classifiers.allClassifiers); whether predicative numerals are licit is a downstream consequence.

Equations

• Semantics.Classifier.upAvailability hasOvertClassifiers = if hasOvertClassifiers = true then Semantics.Classifier.UpAvailability.blocked else Semantics.Classifier.UpAvailability.available

@[simp]

theorem Semantics.Classifier.upAvailability_true : upAvailability true = UpAvailability.blocked

@[simp]

theorem Semantics.Classifier.upAvailability_false : upAvailability false = UpAvailability.available

theorem Semantics.Classifier.classifiers_block_up : upAvailability true = UpAvailability.blocked

A language with overt classifiers blocks the silent ∪-shift. The empirical content (Sudo eq. 15: "okyakusan-wa juu-ni-da" in Japanese) is a downstream consequence of this.

theorem Semantics.Classifier.no_classifiers_leave_up_available : upAvailability false = UpAvailability.available

A language without overt classifiers leaves the silent ∪-shift available. The empirical content (Sudo eq. 13: "The number of guests is twelve" in English) follows.

§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 Intensional.Defs.

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

@[instance_reducible]

instance Sudo2016.instDecidableEqEntity : DecidableEq Entity

Equations

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

@[instance_reducible]

instance Sudo2016.instReprEntity : Repr Entity

Equations

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

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✝

@[instance_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 : Intensional.Intension World (Entity → Prop)

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

bound_volume(x): sortal for -satsu.

Equations

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

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

round(x): sortal for -ko.

Equations

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

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

flat(x): sortal for -mai.

Equations

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

§3: Per-Classifier Denotations

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

def Sudo2016.sudoFormalized : List Japanese.Classifier

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

Equations

• Sudo2016.sudoFormalized = List.filter (fun (c : Japanese.Classifier) => (Sudo2016.japaneseSudoDenot c).isSome) 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 = !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 [Chi98]'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 Japanese.Classifier.nin ≠ japaneseSudoDenot 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 System). Sudo's view is now a first-class constructor of ClassifierStrategy (.sudoBlocking), so the disagreement with [Chi98] reduces to a single decidable inequality.

def Sudo2016.japaneseStrategy : NounCategorization.ClassifierStrategy

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

Equations

• Sudo2016.japaneseStrategy = NounCategorization.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 [LMR22]'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. System.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 : NounCategorization.System) : 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