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

This file formalizes Sudo's account of why Japanese numerals require classifiers: not the semantics of nouns, as for Chierchia and Krifka, but the semantics of numerals. Numerals in every language denote singular terms of type n, constant intensions (numeral, numeral_isRigid), which cannot modify or predicate on their own. A classifier turns such a term into a property: a sortal classifier presupposes the plural closure of its sortal predicate and counts the sortal atoms of its argument (Sortal.apply), the paper's (4) and (8), and a non-atomic classifier such as -kumi 'pair' counts non-overlapping groups of a fixed size (groupApply), so that four books form two pairs and never six (groupApply_card, four_books_two_pairs, four_books_not_six_pairs). Non-classifier languages reach the same properties through the silent ∪-operator, which maps a numeral to the property of having that many atomic parts (up); by the Blocking Principle its use is unavailable in a language whose lexicon has overt items with the same function, the classifiers. The ways a numeral becomes a predicate are therefore the ∪-operator where no classifier blocks it and an overt classifier otherwise (PredicateOf): with classifiers in the lexicon, as the Japanese fragment has (japanese_has_classifiers), every predicate use of a numeral goes through a classifier and carries its sortal presupposition (predicateOf_iff_of_hasClassifiers), the paper's contrast between the ungrammatical bare predicative numeral of (15) and its classifier-suffixed counterpart (16). The inverse ∩-operator maps a property of having a fixed number of atoms back to its numeral (IsDown, isDown_up), has no overt counterpart and so is available in Japanese, where it returns the type-n correlate of a numeral-plus-classifier phrase (isDown_sortal), the paper's (22) to (25). The blocking premise, that the Japanese lexicon has classifiers, is the fact Chierchia's typology records for Japanese, so the two accounts share their premise and part over what the classifier serves, the kind-denoting noun there and the type-n numeral here (predicateOf_iff_japanese).

Implementation notes

Type n is ℕ, and the paper's extension of the type-n domain to the correlates of classifier phrases is represented by stating ∩ relative to the classifier's sortal. The ∪-shifted composition rules (11), (19) and (26) are represented by the derivation relation PredicateOf rather than as rules with domain conditions, and the paper's observation that English numerals fail in some predicative constructions is not modelled. The witnesses use the set-based ontology of the plural algebra, an individual being its singleton and sum union, on which the atom count of a plurality is its cardinality (atomCount_finset).

References

• [Sud16]
• [Chi98]
• [Rot13]
• [Lin83]
• [HK98]
• [Kri08]

Numerals and classifiers

def Sudo2016.numeral {W : Type u_1} (n : ℕ) : W → ℕ

A numeral denotes a singular term of type n, the constant intension of the paper's (2).

Equations

• Sudo2016.numeral n x✝ = n

theorem Sudo2016.numeral_isRigid {W : Type u_1} (n : ℕ) : Reference.IsRigid (numeral n)

noncomputable def Sudo2016.atomCount {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (P : W → E → Prop) (w : W) (x : E) : ℕ

The number of atomic P-parts of x at a world.

Equations

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

@[reducible, inline]

abbrev Sudo2016.Sortal (W : Type u_3) (E : Type u_4) : Type (max u_3 u_4)

A sortal predicate of atoms, indexed by worlds, such as the metalanguage predicates flower and human of the paper's (4) and (8).

Equations

• Sudo2016.Sortal W E = (W → E → Prop)

noncomputable def Sudo2016.Sortal.apply {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (c : Sortal W E) (n : W → ℕ) (w : W) : E → SignType

A sortal classifier applied to a numeral, the paper's (4) and (7b), is at each world a trivalent property presupposing the plural closure of the sortal and asserting that the argument has the numeral's number of sortal atoms.

Equations

• c.apply n w = {x : E | Mereology.AlgClosure (c w) x}.indicator fun (x : E) => SignType.ofProp (Sudo2016.atomCount c w x = n w)

def Sudo2016.up {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (atomic : Sortal W E) (n : W → ℕ) : W → E → Prop

The ∪-operator of the paper's (10) maps a numeral to its property correlate, having that many atomic parts.

Equations

• Sudo2016.up atomic n w x = (Sudo2016.atomCount atomic w x = n w)

@[simp]

theorem Sudo2016.Sortal.apply_eq_zero_iff {W : Type u_1} {E : Type u_2} [SemilatticeSup E] {c : Sortal W E} {n : W → ℕ} {w : W} {x : E} : c.apply n w x = 0 ↔ ¬Mereology.AlgClosure (c w) x

A sortal classifier is undefined of what is not a plurality of its sortal.

@[simp]

theorem Sudo2016.Sortal.apply_eq_one_iff {W : Type u_1} {E : Type u_2} [SemilatticeSup E] {c : Sortal W E} {n : W → ℕ} {w : W} {x : E} : c.apply n w x = 1 ↔ Mereology.AlgClosure (c w) x ∧ up c n w x

The classifier's assertion is the ∪-correlate of the numeral counted over the sortal.

@[simp]

theorem Sudo2016.Sortal.apply_eq_neg_one_iff {W : Type u_1} {E : Type u_2} [SemilatticeSup E] {c : Sortal W E} {n : W → ℕ} {w : W} {x : E} : c.apply n w x = -1 ↔ Mereology.AlgClosure (c w) x ∧ ¬up c n w x

A sortal classifier is false of a plurality of its sortal with another number of atoms.

noncomputable def Sudo2016.modify {E : Type u_2} (P : E → SignType) (N : E → Prop) : E → SignType

Predicate Modification with a presupposed modifier, the paper's (6), conjoins the noun with the assertion and projects the presupposition.

Equations

• Sudo2016.modify P N x = (P x).meetWeak (SignType.ofProp (N x))

theorem Sudo2016.modify_sortal_ne_zero {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (c : Sortal W E) (n : W → ℕ) (w : W) {x : E} (h : Mereology.AlgClosure (c w) x) : modify (c.apply n w) (Mereology.AlgClosure (c w)) x ≠ 0

When the noun denotes the plural closure of the classifier's own sortal, the paper's (7c), the noun entails the presupposition, so the modified phrase is defined wherever the noun holds.

The ∩-operator

def Sudo2016.IsDown {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (atomic : Sortal W E) (P : W → E → Prop) (n : W → ℕ) : Prop

The property P is the ∪-correlate of the numeral n, so that ∩ maps it back to n, the paper's (24).

Equations

• Sudo2016.IsDown atomic P n = ∀ (w : W) (x : E), P w x ↔ Sudo2016.atomCount atomic w x = n w

theorem Sudo2016.isDown_up {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (atomic : Sortal W E) (n : W → ℕ) : IsDown atomic (up atomic n) n

theorem Sudo2016.IsDown.unique {W : Type u_1} {E : Type u_2} [SemilatticeSup E] {atomic : Sortal W E} {P : W → E → Prop} {n m : W → ℕ} (hn : IsDown atomic P n) (hm : IsDown atomic P m) (hsurj : ∀ (w : W), ∃ (x : E), atomCount atomic w x = n w) : n = m

∩ is a partial inverse, since a property with a type-n correlate has only one, provided every count is instantiated.

theorem Sudo2016.isDown_sortal {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (c : Sortal W E) (n : W → ℕ) (w : W) (x : E) : Mereology.AlgClosure (c w) x → (c.apply n w x = 1 ↔ atomCount c w x = n w)

A numeral-plus-classifier phrase has a type-n correlate relative to the classifier's sortal, the paper's (25), since on the plural closure of the sortal it is the property of having the numeral's number of sortal atoms. So ∩ applies in Japanese to juu-ni-nin and returns twelve.

Blocking

inductive Sudo2016.PredicateOf {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (hasClassifiers : Prop) (atomic : Sortal W E) (n : W → ℕ) : (W → E → Prop) → Prop

A numeral becomes a predicate by the silent ∪-operator, available only when no overt classifier is in the lexicon, or by an overt classifier, which adds its sortal presupposition.

• up {W : Type u_1} {E : Type u_2} [SemilatticeSup E] {hasClassifiers : Prop} {atomic : Sortal W E} {n : W → ℕ} (h : ¬hasClassifiers) : PredicateOf hasClassifiers atomic n (Sudo2016.up atomic n)
• classifier {W : Type u_1} {E : Type u_2} [SemilatticeSup E] {hasClassifiers : Prop} {atomic : Sortal W E} {n : W → ℕ} (c : Sortal W E) : PredicateOf hasClassifiers atomic n fun (w : W) (x : E) => c.apply n w x = 1

theorem Sudo2016.predicateOf_iff_of_hasClassifiers {W : Type u_1} {E : Type u_2} [SemilatticeSup E] {hasClassifiers : Prop} (h : hasClassifiers) (atomic : Sortal W E) (n : W → ℕ) (P : W → E → Prop) : PredicateOf hasClassifiers atomic n P ↔ ∃ (c : Sortal W E), P = fun (w : W) (x : E) => c.apply n w x = 1

With classifiers in the lexicon every predicate use of a numeral goes through a classifier and carries its sortal presupposition, the contrast of the paper's (15) and (16).

theorem Sudo2016.predicateOf_up {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (atomic : Sortal W E) (n : W → ℕ) : PredicateOf False atomic n (up atomic n)

Without classifiers the bare ∪-shift is available, the paper's (18) for English.

theorem Sudo2016.japanese_has_classifiers : Japanese.Classifiers.classifiers.Nonempty

The Japanese lexicon has classifiers, as the fragment records.

theorem Sudo2016.predicateOf_iff_japanese {W : Type u_1} {E : Type u_2} [SemilatticeSup E] (atomic : Sortal W E) (n : W → ℕ) (P : W → E → Prop) : PredicateOf Chierchia1998.Language.japanese.HasClassifiers atomic n P ↔ ∃ (c : Sortal W E), P = fun (w : W) (x : E) => c.apply n w x = 1

With the classifiers [Chi98]'s typology records for Japanese in the lexicon, every predicate use of a Japanese numeral goes through a classifier. The two accounts share the premise and part over what the classifier serves, the kind-denoting noun there and the type-n numeral here.

Witnesses on the set-based ontology

def Sudo2016.singletonSortal {α : Type u_1} (P : α → Prop) : Sortal Unit (Finset α)

The sortal predicate P of atoms lifted to pluralities, an individual being its singleton.

Equations

• Sudo2016.singletonSortal P x✝ y = ∃ (a : α), y = {a} ∧ P a

theorem Sudo2016.atomCount_finset {α : Type u_1} [DecidableEq α] (P : α → Prop) [DecidablePred P] (x : Finset α) : atomCount (singletonSortal P) () x = (Finset.filter P x).card

The atom count of a plurality is the number of its members satisfying the sortal.

theorem Sudo2016.singletonSortal_apply_ne_zero_iff {α : Type u_1} [DecidableEq α] (P : α → Prop) (n : Unit → ℕ) (x : Finset α) : (singletonSortal P).apply n () x ≠ 0 ↔ x.Nonempty ∧ ∀ a ∈ x, P a

On the set-based ontology a sortal classifier is defined exactly of a nonempty plurality of sortal individuals.

def Sudo2016.groupApply {α : Type u_1} [DecidableEq α] (k n : ℕ) (x : Finset α) : Prop

A non-atomic classifier counting groups of k atoms, the paper's (9), holds when the argument is the sum of n non-overlapping pluralities of k members each.

Equations

• Sudo2016.groupApply k n x = ∃ (s : Finset (Finset α)), s.card = n ∧ s.biUnion id = x ∧ (∀ y ∈ s, y.card = k) ∧ ∀ y ∈ s, ∀ z ∈ s, y ≠ z → Disjoint y z

theorem Sudo2016.groupApply_card {α : Type u_1} [DecidableEq α] {k n : ℕ} {x : Finset α} (h : groupApply k n x) : x.card = n * k

Non-overlap makes the count exact, so n groups of k have n * k atoms.

inductive Sudo2016.Ind : Type

The individuals of the witnesses are three flowers, two humans, and four books.

• f1 : Ind
• f2 : Ind
• f3 : Ind
• h1 : Ind
• h2 : Ind
• b1 : Ind
• b2 : Ind
• b3 : Ind
• b4 : Ind

@[instance_reducible]

instance Sudo2016.instDecidableEqInd : DecidableEq Ind

Equations

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

def Sudo2016.instReprInd.repr : Ind → ℕ → Std.Format

Equations

• Sudo2016.instReprInd.repr Sudo2016.Ind.f1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Ind.f1")).group prec✝
• Sudo2016.instReprInd.repr Sudo2016.Ind.f2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Ind.f2")).group prec✝
• Sudo2016.instReprInd.repr Sudo2016.Ind.f3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Ind.f3")).group prec✝
• Sudo2016.instReprInd.repr Sudo2016.Ind.h1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Ind.h1")).group prec✝
• Sudo2016.instReprInd.repr Sudo2016.Ind.h2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Ind.h2")).group prec✝
• Sudo2016.instReprInd.repr Sudo2016.Ind.b1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Ind.b1")).group prec✝
• Sudo2016.instReprInd.repr Sudo2016.Ind.b2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Ind.b2")).group prec✝
• Sudo2016.instReprInd.repr Sudo2016.Ind.b3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Ind.b3")).group prec✝
• Sudo2016.instReprInd.repr Sudo2016.Ind.b4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Sudo2016.Ind.b4")).group prec✝

@[instance_reducible]

instance Sudo2016.instReprInd : Repr Ind

Equations

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

def Sudo2016.Ind.flower : Ind → Prop

Equations

• Sudo2016.Ind.f1.flower = True
• Sudo2016.Ind.f2.flower = True
• Sudo2016.Ind.f3.flower = True
• x✝.flower = False

@[instance_reducible]

instance Sudo2016.instDecidablePredIndFlower : DecidablePred Ind.flower

Equations

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

def Sudo2016.rin : Sortal Unit (Finset Ind)

-rin counts flowers.

Equations

• Sudo2016.rin = Sudo2016.singletonSortal Sudo2016.Ind.flower

theorem Sudo2016.rin_three : rin.apply (numeral 3) () {Ind.f1, Ind.f2, Ind.f3} = 1 ∧ rin.apply (numeral 3) () {Ind.f1, Ind.f2} = -1

san-rin holds of three flowers, its presupposition met, and fails of two of them.

theorem Sudo2016.rin_not_human : rin.apply (numeral 1) () {Ind.h1} = 0

-rin does not count people, so its sortal presupposition fails of a human.

theorem Sudo2016.four_books_two_pairs : groupApply 2 2 {Ind.b1, Ind.b2, Ind.b3, Ind.b4}

Four books form two pairs, the paper's remark on (9).

theorem Sudo2016.four_books_not_six_pairs (x : Finset Ind) (hx : x.card = 4) : ¬groupApply 2 6 x

Four books never form six pairs, since overlapping pairs are not counted.