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, ka for the existential (dare-ka 'someone') and mo for the universal (dare-mo 'everyone', dono N mo 'every N'). The particles are the coordinators ka 'or' and mo 'and', and an indeterminate quantifier applies its particle's coordination to the values its scope takes on the restrictor, the supremum for ka and the infimum for mo, which are Quantifier.GQ.some and every (IndeterminateQuantifier.reading). The remaining quantifiers are words of their own, the carrier QuantityWord of subete 'all', hotondo 'most' and ryōhō 'both'. 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.indefinites: the indeterminate quantifiers, with the coordinators of Japanese.Coordination as their particles.
• Japanese.Determiners.QuantityWord: the quantifiers that are words of their own.
• Japanese.Determiners.inventory: the determiner inventory, quantifiers only.

References

• [Chi98]
• [KS17]
• [Shi06]

def Japanese.Determiners.dare_ka : IndeterminateQuantifier

Dare-ka is 'someone'.

Equations

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

def Japanese.Determiners.dare_mo : IndeterminateQuantifier

Dare-mo is 'everyone'.

Equations

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

def Japanese.Determiners.dono_N_mo : IndeterminateQuantifier

Dono N mo is 'every N'.

Equations

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

def Japanese.Determiners.nan_nin_ka : IndeterminateQuantifier

Nan-nin-ka is '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 IndeterminateQuantifier

indefinites lists 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 are 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 form of a word is its romanization.

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

A word's determiner record carries its form.

Equations

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

def Japanese.Determiners.QuantityWord.toList : List QuantityWord

toList lists every word.

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)

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 has quantifiers only, there being no articles.

Equations

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

theorem Japanese.Determiners.denote_dare_ka : Semantics.Denotes.denote dare_ka = {Quantifier.GQ.Family.some}

Dare-ka reads as Quantifier.GQ.some.

theorem Japanese.Determiners.denote_dare_mo : Semantics.Denotes.denote dare_mo = {Quantifier.GQ.Family.every}

Dare-mo reads as every.