Composition Rules for Sudo (2016)

@cite{sudo-2016} @cite{chierchia-1998}

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 : Core.Intension W (E → Prop)) (n : NumeralIntens W) : Core.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 = ({y : E | y ≤ x ∧ atomic w y}.ncard = n w)

@[simp]

theorem Semantics.Classifier.upNum_apply {W : Type u} {E : Type v} [PartialOrder E] (atomic : Core.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 : Core.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 {y : E | y ≤ h.choose ∧ atomic w y}.ncard 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).

@[implicit_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.

@[implicit_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.