Indeterminate quantifiers

An indeterminate quantifier is built from an indeterminate pronoun, an interrogative, and a particle that is also a coordinator of the language. Japanese dare-ka 'someone' and dare-mo 'everyone' combine dare 'who' with ka 'or' and mo 'and', and Latin quisque 'each' combines quis 'who' with the enclitic -que 'and'. A coordinator has a quantifier use when an indeterminate quantifier of its language has it as its particle. What the quantifier denotes is IndeterminateQuantifier.reading, in Semantics/Quantification/IndeterminateQuantifier.lean.

Main definitions

• IndeterminateQuantifier: an indeterminate and a particle, with the classifier between them where there is one.
• IndeterminateQuantifier.form, IndeterminateQuantifier.toQuantifier: its citation form and its determiner record.

References

• [KS17]
• [MS16a]

structure IndeterminateQuantifier : Type

An indeterminate quantifier is an indeterminate pronoun with a particle that is a coordinator of the language, and the classifier between them where there is one.

• indeterminate : InterrogativePronoun

  The indeterminate pronoun.

• particle : Coordinator

  The particle, a coordinator of the language.

• classifier : Option Classifier

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

@[instance_reducible]

instance instDecidableEqIndeterminateQuantifier : DecidableEq IndeterminateQuantifier

Equations

• instDecidableEqIndeterminateQuantifier = instDecidableEqIndeterminateQuantifier.decEq

def instDecidableEqIndeterminateQuantifier.decEq (x✝ x✝¹ : IndeterminateQuantifier) : Decidable (x✝ = x✝¹)

Equations

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

def IndeterminateQuantifier.form (q : IndeterminateQuantifier) : String

The citation form joins the indeterminate, its classifier and the particle by hyphens, and puts the particle of a determiner, such as Japanese dono 'which', after the noun the determiner takes.

Equations

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

def IndeterminateQuantifier.toQuantifier (q : IndeterminateQuantifier) : Quantifier

An indeterminate quantifier's determiner record carries its form.

Equations

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