Czech determiner inventory

Czech has neither a definite nor an indefinite article, so its inventory holds only the demonstrative ten and the quantificational determiners, and it falls in the unmarked cell of Moroney's typology of definiteness marking. The quantificational determiners are the carrier QuantityWord, whose words project to Quantifier records and denote the readings the literature makes available for them. Two of them are polarity sensitive, the concord item žádný 'no' and the positive polarity item nějaký 'some', and their entries in PolarityItems.lean take their forms from here.

Implementation notes

• Žádný has two readings. On de Swart's analysis of n-words as negative quantifiers, negative concord being their resumptive interpretation, it reads as no. On Zeijlstra's, which Staňková and Šimík adopt for Czech, it is a non-negative indefinite whose negation the clause's negative operator contributes, and it reads as some.
• WALS codes Czech with a two-way distance contrast, ten 'neutral / proximal' against onen 'contrastive'. Only ten is entered, as distance-neutral; the contrastive deixis of onen has no counterpart among participant sets.

References

• [Die13b]
• [Mor21]
• [dS10]
• [Zei04]
• [SS25]

def Czech.Determiners.ten : DemonstrativeDeterminer

ten 'that, the' is the distance-neutral demonstrative, so it covers every participant set.

Equations

• Czech.Determiners.ten = { form := "ten", deixis := Finset.univ }

inductive Czech.Determiners.QuantityWord : Type

The quantificational determiners are každý 'every', žádný 'no', nějaký 'some' and některý 'some, certain'.

• kazdy : QuantityWord
• zadny : QuantityWord
• nejaky : QuantityWord
• nektery : QuantityWord

@[instance_reducible]

instance Czech.Determiners.instDecidableEqQuantityWord : DecidableEq QuantityWord

Equations

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

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

Equations

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

@[instance_reducible]

instance Czech.Determiners.instReprQuantityWord : Repr QuantityWord

Equations

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

@[instance_reducible]

instance Czech.Determiners.instFintypeQuantityWord : Fintype QuantityWord

Equations

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

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

The surface form.

Equations

• Czech.Determiners.QuantityWord.kazdy.form = "každý"
• Czech.Determiners.QuantityWord.zadny.form = "žádný"
• Czech.Determiners.QuantityWord.nejaky.form = "nějaký"
• Czech.Determiners.QuantityWord.nektery.form = "některý"

def Czech.Determiners.QuantityWord.numberRestriction : QuantityWord → Option Number

The grammatical number a word selects, which only každý fixes, to the singular.

Equations

• Czech.Determiners.QuantityWord.kazdy.numberRestriction = some Number.singular
• x✝.numberRestriction = none

def Czech.Determiners.QuantityWord.selectsMass : QuantityWord → Bool

Whether a word selects mass nouns, which žádný and nějaký do.

Equations

• Czech.Determiners.QuantityWord.zadny.selectsMass = true
• Czech.Determiners.QuantityWord.nejaky.selectsMass = true
• Czech.Determiners.QuantityWord.kazdy.selectsMass = false
• Czech.Determiners.QuantityWord.nektery.selectsMass = false

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

The word as a determiner record.

Equations

• w.toQuantifier = { form := w.form, numberRestriction := w.numberRestriction, selectsMass := w.selectsMass }

def Czech.Determiners.QuantityWord.toList : List QuantityWord

All the words.

Equations

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

@[instance_reducible]

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

The readings available for a word. Každý reads as every, žádný as no or as Quantifier.GQ.some, and nějaký and některý as Quantifier.GQ.some, the partitive specificity of některý being no part of its truth conditions.

Equations

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

def Czech.Determiners.inventory : Determiner.Inventory

The Czech determiners are the demonstrative and the quantifiers, with no article.

Equations

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

theorem Czech.Determiners.marking : inventory.markingStrategy = Reference.MarkingStrategy.unmarked

Czech derives the .unmarked Moroney cell.