Japanese Quantifier Fragment

Japanese quantifiers differ from English in three key ways:

1. Floating quantifiers: gakusei-ga san-nin kita (students-NOM three-CL came)
2. Wh-indeterminates: dare-ka (who-Q = someone), dare-mo (who-∀ = everyone)
3. No articles — bare nouns are ambiguous (generic/definite/indefinite)

Key typological properties:

• Particle-based force: -ka (existential), -mo (universal), -demo (free choice)
• Floating quantifiers interact with case marking for scope
• Conservativity expected to hold (universal)
• Negative concord via -mo...nai: dare-mo...nai = nobody

structure Fragments.Japanese.Determiners.JapaneseQuantEntry : Type

Japanese quantifier entry. Extends the English pattern with indeterminate/particle morphology and floating quantifier properties.

• form : String

  Kana/kanji form

• romaji : String

  Rōmaji romanization

• gloss : String

  English gloss

• qforce : English.Determiners.QForce

  Quantificational force

• monotonicity : English.Determiners.Monotonicity

  Monotonicity

• strength : English.Determiners.Strength

  Weak/strong

• particle : Option String

  Quantificational particle (ka/mo/demo) if built from indeterminate

• floats : Bool

  Whether this quantifier can float (appear separated from its NP)

• requiresNegation : Bool

  Whether this quantifier requires clausemate negation (negative concord)

• indeterminate : Option String

  The wh-indeterminate base (e.g., "dare" for dare-ka/dare-mo)

def Fragments.Japanese.Determiners.instReprJapaneseQuantEntry.repr : JapaneseQuantEntry → ℕ → Std.Format

Equations

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

instance Fragments.Japanese.Determiners.instReprJapaneseQuantEntry : Repr JapaneseQuantEntry

Equations

• Fragments.Japanese.Determiners.instReprJapaneseQuantEntry = { reprPrec := Fragments.Japanese.Determiners.instReprJapaneseQuantEntry.repr }

def Fragments.Japanese.Determiners.instBEqJapaneseQuantEntry.beq : JapaneseQuantEntry → JapaneseQuantEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Japanese.Determiners.instBEqJapaneseQuantEntry.beq x✝¹ x✝ = false

instance Fragments.Japanese.Determiners.instBEqJapaneseQuantEntry : BEq JapaneseQuantEntry

Equations

• Fragments.Japanese.Determiners.instBEqJapaneseQuantEntry = { beq := Fragments.Japanese.Determiners.instBEqJapaneseQuantEntry.beq }

def Fragments.Japanese.Determiners.subete : JapaneseQuantEntry

すべて subete "all" — universal, increasing, strong. すべての学生 subete-no gakusei "all students"

Equations

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

def Fragments.Japanese.Determiners.dono_N_mo : JapaneseQuantEntry

どのNも dono_N_mo "every N" — universal, increasing, strong. Built from wh-indeterminate dono + particle mo. どの学生も dono gakusei mo "every student"

Equations

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

def Fragments.Japanese.Determiners.dare_ka : JapaneseQuantEntry

誰か dare_ka "someone" — existential, increasing, weak. Built from wh-indeterminate dare + particle ka.

Equations

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

def Fragments.Japanese.Determiners.dare_mo : JapaneseQuantEntry

誰も dare_mo "everyone / nobody" — universal (affirmative) or negative universal (with clausemate negation: dare-mo...nai). @cite{shimoyama-2006}: -mo is Hamblin universal over indeterminate set.

Equations

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

def Fragments.Japanese.Determiners.nan_nin_ka : JapaneseQuantEntry

何人か nan_nin_ka "several people" — existential numeral+CL+ka. Floating quantifier: 学生が何人か来た gakusei-ga nan-nin-ka kita.

Equations

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

def Fragments.Japanese.Determiners.hotondo : JapaneseQuantEntry

ほとんど hotondo "most/almost all" — proportional, increasing, strong.

Equations

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

def Fragments.Japanese.Determiners.ryoho : JapaneseQuantEntry

両方 ryōhō "both" — universal dual, strong. 両方の学生 ryōhō-no gakusei "both students". Presupposes exactly two referents (like English "both"). K&S: both = every restricted to dual sets.

Equations

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

def Fragments.Japanese.Determiners.allQuantifiers : List JapaneseQuantEntry

Equations

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

def Fragments.Japanese.Determiners.lookup (romaji : String) : Option JapaneseQuantEntry

Equations

• Fragments.Japanese.Determiners.lookup romaji = List.find? (fun (e : Fragments.Japanese.Determiners.JapaneseQuantEntry) => e.romaji == romaji) Fragments.Japanese.Determiners.allQuantifiers

theorem Fragments.Japanese.Determiners.dare_ka_indeterminate : dare_ka.indeterminate = some "dare" ∧ dare_ka.particle = some "ka"

dare-ka is built from indeterminate dare + particle ka.

theorem Fragments.Japanese.Determiners.dare_mo_indeterminate : dare_mo.indeterminate = some "dare" ∧ dare_mo.particle = some "mo"

dare-mo is built from indeterminate dare + particle mo.

theorem Fragments.Japanese.Determiners.particle_force_shift : dare_ka.qforce = English.Determiners.QForce.existential ∧ dare_mo.qforce = English.Determiners.QForce.universal

Particle shift: same indeterminate base, different force. ka → existential, mo → universal.

theorem Fragments.Japanese.Determiners.nan_nin_ka_floats : nan_nin_ka.floats = true

nan-nin-ka floats.

theorem Fragments.Japanese.Determiners.ryoho_universal_strong : ryoho.qforce = English.Determiners.QForce.universal ∧ ryoho.strength = English.Determiners.Strength.strong

ryōhō is universal and strong (like English "both").

theorem Fragments.Japanese.Determiners.fragment_size : allQuantifiers.length = 7

Fragment has 7 entries.