Japanese quantifiers

Japanese has no articles, and most of its quantifiers are built from an indeterminate pronoun of Japanese.Pronouns (dare 'who', dono 'which', nan- 'how many') and a particle: with ka the phrase is existential (dare-ka 'someone'), with mo universal (dare-mo 'everyone', dono N mo 'every N'), the particles being the coordinators ka 'or' and mo 'and', so that the force of the phrase is the Boolean operation of its particle. The remaining quantifiers are words of their own, the carrier QuantityWord of subete 'all', hotondo 'most' and ryōhō 'both'. Both carriers denote the readings available for their members, an indeterminate quantifier reading by the force of its particle. Numeral quantifiers such as nan-nin-ka 'several people' float away from their noun phrase, and dare-mo under clausemate negation is the negative indefinite of Fragments/Japanese/PolarityItems.lean.

Main definitions

• Japanese.Determiners.Indefinite — the quantifiers an indeterminate and a particle form, with the force Indefinite.force of the particle
• Japanese.Determiners.QuantityWord — the quantifiers that are words of their own
• Japanese.Determiners.inventory — the determiner inventory, quantifiers only

References

• [chierchia-1998]
• [kratzer-shimoyama-2002]
• [shimoyama-2006]

def Japanese.Determiners.particleForce (p : Coordinator) : Quantifier.Lexicon.QForce

The force a particle gives an indeterminate: existential for the disjunction ka and universal for the conjunction mo.

Equations

• Japanese.Determiners.particleForce p = match p.role with | Coordinator.Role.disjunctive => Quantifier.Lexicon.QForce.existential | x => Quantifier.Lexicon.QForce.universal

structure Japanese.Determiners.Indefinite : Type

A quantifier built from an indeterminate and a particle, with the classifier between them where there is one.

• indeterminate : InterrogativePronoun

  The indeterminate.

• particle : Coordinator

  The particle, ka or mo.

• classifier : Option Classifier

  The classifier after the indeterminate, as in nan-nin-ka.

def Japanese.Determiners.instDecidableEqIndefinite.decEq (x✝ x✝¹ : Indefinite) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Japanese.Determiners.instDecidableEqIndefinite : DecidableEq Indefinite

Equations

• Japanese.Determiners.instDecidableEqIndefinite = Japanese.Determiners.instDecidableEqIndefinite.decEq

def Japanese.Determiners.Indefinite.form (q : Indefinite) : String

The form: the indeterminate, its classifier and the particle joined by hyphens, and for the determiner dono the particle after the noun the determiner takes.

Equations

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

def Japanese.Determiners.Indefinite.force (q : Indefinite) : Quantifier.Lexicon.QForce

The force of the quantifier, that of its particle.

Equations

• q.force = Japanese.Determiners.particleForce q.particle

def Japanese.Determiners.Indefinite.toQuantifier (q : Indefinite) : Quantifier

The quantifier as a determiner entry.

Equations

• q.toQuantifier = { form := q.form }

@[instance_reducible]

instance Japanese.Determiners.Indefinite.instDenotesSetFamily : Semantics.Denotes Indefinite (Set Quantifier.GQ.Family)

The reading available for an indeterminate quantifier is that of its particle's force, Quantifier.GQ.some for the disjunction ka and every for the conjunction mo.

Equations

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

def Japanese.Determiners.dare_ka : Indefinite

dare-ka 'someone'.

Equations

• Japanese.Determiners.dare_ka = { indeterminate := Japanese.Pronouns.dare, particle := Japanese.Coordination.ka }

def Japanese.Determiners.dare_mo : Indefinite

dare-mo 'everyone'.

Equations

• Japanese.Determiners.dare_mo = { indeterminate := Japanese.Pronouns.dare, particle := Japanese.Coordination.mo }

def Japanese.Determiners.dono_N_mo : Indefinite

dono N mo 'every N'.

Equations

• Japanese.Determiners.dono_N_mo = { indeterminate := Japanese.Pronouns.dono, particle := Japanese.Coordination.mo }

def Japanese.Determiners.nan_nin_ka : Indefinite

nan-nin-ka 'several people', with the classifier -nin.

Equations

• Japanese.Determiners.nan_nin_ka = { indeterminate := Japanese.Pronouns.nan, particle := Japanese.Coordination.ka, classifier := some Japanese.Classifiers.nin }

def Japanese.Determiners.indefinites : List Indefinite

The indeterminate quantifiers.

Equations

• Japanese.Determiners.indefinites = [Japanese.Determiners.dare_ka, Japanese.Determiners.dare_mo, Japanese.Determiners.dono_N_mo, Japanese.Determiners.nan_nin_ka]

inductive Japanese.Determiners.QuantityWord : Type

The quantifiers that are words of their own: subete 'all', hotondo 'most' and ryōhō 'both'.

• subete : QuantityWord
• hotondo : QuantityWord
• ryoho : QuantityWord

@[instance_reducible]

instance Japanese.Determiners.instDecidableEqQuantityWord : DecidableEq QuantityWord

Equations

• Japanese.Determiners.instDecidableEqQuantityWord x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Japanese.Determiners.instReprQuantityWord.repr : QuantityWord → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Japanese.Determiners.instReprQuantityWord : Repr QuantityWord

Equations

• Japanese.Determiners.instReprQuantityWord = { reprPrec := Japanese.Determiners.instReprQuantityWord.repr }

@[instance_reducible]

instance Japanese.Determiners.instFintypeQuantityWord : Fintype QuantityWord

Equations

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

def Japanese.Determiners.QuantityWord.form : QuantityWord → String

The romanized form.

Equations

• Japanese.Determiners.QuantityWord.subete.form = "subete"
• Japanese.Determiners.QuantityWord.hotondo.form = "hotondo"
• Japanese.Determiners.QuantityWord.ryoho.form = "ryōhō"

def Japanese.Determiners.QuantityWord.toQuantifier (w : QuantityWord) : Quantifier

The word as a determiner record.

Equations

• w.toQuantifier = { form := w.form }

def Japanese.Determiners.QuantityWord.toList : List QuantityWord

All the words.

Equations

• Japanese.Determiners.QuantityWord.toList = [Japanese.Determiners.QuantityWord.subete, Japanese.Determiners.QuantityWord.hotondo, Japanese.Determiners.QuantityWord.ryoho]

@[instance_reducible]

noncomputable instance Japanese.Determiners.QuantityWord.instDenotesSetFamily : Semantics.Denotes QuantityWord (Set Quantifier.GQ.Family)

The readings available for a word: subete reads as every, hotondo as most and ryōhō as both.

Equations

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

def Japanese.Determiners.inventory : Determiner.Inventory

The determiner inventory: quantifiers only, there being no articles.

Equations

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

theorem Japanese.Determiners.Indefinite.force_eq_universal_iff (q : Indefinite) : q.force = Quantifier.Lexicon.QForce.universal ↔ q.particle.role ≠ Coordinator.Role.disjunctive

The universal indeterminates are the ones not built on the disjunction.