Italian determiners

This file records the Italian determiner lexicon. The quantificational determiners are the carrier QuantityWord, whose masculine and feminine forms are QuantityWord.form and QuantityWord.feminine, the invariant ogni and qualche having one form, and whose members project to a Quantifier record and denote the readings the literature makes available for them, so ⟦QuantityWord.tutti⟧ is {every} and molti, like English many, denotes ∅. The definite article il, lo, la and plural i, gli, le is one syncretic definite over Schwarz's use types, the indefinite is un, uno, una, and the partitive del, dello, della and plural dei, degli, delle is the indefinite of mass nouns and plurals.

References

• [Sch09b]
• [Mor21]
• [Chi98]
• [dSS02]
• [Zei04]

Articles

The definite article il, lo, la and plural i, gli, le, one syncretic definite covering the [Sch09b] use types; the indefinite un, uno, una; and the partitive del, dello, della and plural dei, degli, delle, the indefinite of mass nouns and plurals.

def Italian.Determiners.definite (form : String) : Article

The definite article with the given form.

Equations

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

def Italian.Determiners.indefinite (form : String) : Article

The indefinite article with the given form.

Equations

• Italian.Determiners.indefinite form = { form := form, definiteness := Reference.Definiteness.indefinite, exponent := Determiner.Exponent.dedicatedMorpheme }

def Italian.Determiners.il : Article

Equations

• Italian.Determiners.il = Italian.Determiners.definite "il"

def Italian.Determiners.lo : Article

Equations

• Italian.Determiners.lo = Italian.Determiners.definite "lo"

def Italian.Determiners.la : Article

Equations

• Italian.Determiners.la = Italian.Determiners.definite "la"

def Italian.Determiners.i : Article

Equations

• Italian.Determiners.i = Italian.Determiners.definite "i"

def Italian.Determiners.gli : Article

Equations

• Italian.Determiners.gli = Italian.Determiners.definite "gli"

def Italian.Determiners.le : Article

Equations

• Italian.Determiners.le = Italian.Determiners.definite "le"

def Italian.Determiners.un : Article

Equations

• Italian.Determiners.un = Italian.Determiners.indefinite "un"

def Italian.Determiners.uno : Article

Equations

• Italian.Determiners.uno = Italian.Determiners.indefinite "uno"

def Italian.Determiners.una : Article

Equations

• Italian.Determiners.una = Italian.Determiners.indefinite "una"

def Italian.Determiners.del : Article

Equations

• Italian.Determiners.del = Italian.Determiners.indefinite "del"

def Italian.Determiners.dello : Article

Equations

• Italian.Determiners.dello = Italian.Determiners.indefinite "dello"

def Italian.Determiners.della : Article

Equations

• Italian.Determiners.della = Italian.Determiners.indefinite "della"

def Italian.Determiners.dei : Article

Equations

• Italian.Determiners.dei = Italian.Determiners.indefinite "dei"

def Italian.Determiners.degli : Article

Equations

• Italian.Determiners.degli = Italian.Determiners.indefinite "degli"

def Italian.Determiners.delle : Article

Equations

• Italian.Determiners.delle = Italian.Determiners.indefinite "delle"

def Italian.Determiners.allArticles : List Article

All Italian article entries.

Equations

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

Quantificational determiners

inductive Italian.Determiners.QuantityWord : Type

The quantificational determiners: ogni 'every', qualche 'some', nessuno 'no', tutti 'all', alcuni 'some', molti 'many' and pochi 'few'.

• ogni : QuantityWord
• qualche : QuantityWord
• nessuno : QuantityWord
• tutti : QuantityWord
• alcuni : QuantityWord
• molti : QuantityWord
• pochi : QuantityWord

@[instance_reducible]

instance Italian.Determiners.instDecidableEqQuantityWord : DecidableEq QuantityWord

Equations

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

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

Equations

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

@[instance_reducible]

instance Italian.Determiners.instReprQuantityWord : Repr QuantityWord

Equations

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

@[instance_reducible]

instance Italian.Determiners.instFintypeQuantityWord : Fintype QuantityWord

Equations

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

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

The masculine form, which is the citation form.

Equations

• Italian.Determiners.QuantityWord.ogni.form = "ogni"
• Italian.Determiners.QuantityWord.qualche.form = "qualche"
• Italian.Determiners.QuantityWord.nessuno.form = "nessuno"
• Italian.Determiners.QuantityWord.tutti.form = "tutti"
• Italian.Determiners.QuantityWord.alcuni.form = "alcuni"
• Italian.Determiners.QuantityWord.molti.form = "molti"
• Italian.Determiners.QuantityWord.pochi.form = "pochi"

def Italian.Determiners.QuantityWord.feminine : QuantityWord → String

The feminine form, which for the invariant ogni and qualche is the citation form.

Equations

• Italian.Determiners.QuantityWord.ogni.feminine = "ogni"
• Italian.Determiners.QuantityWord.qualche.feminine = "qualche"
• Italian.Determiners.QuantityWord.nessuno.feminine = "nessuna"
• Italian.Determiners.QuantityWord.tutti.feminine = "tutte"
• Italian.Determiners.QuantityWord.alcuni.feminine = "alcune"
• Italian.Determiners.QuantityWord.molti.feminine = "molte"
• Italian.Determiners.QuantityWord.pochi.feminine = "poche"

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

The grammatical number a word selects: the singular for ogni, qualche and nessuno, the plural for the rest.

Equations

• Italian.Determiners.QuantityWord.ogni.numberRestriction = some Number.singular
• Italian.Determiners.QuantityWord.qualche.numberRestriction = some Number.singular
• Italian.Determiners.QuantityWord.nessuno.numberRestriction = some Number.singular
• Italian.Determiners.QuantityWord.tutti.numberRestriction = some Number.plural
• Italian.Determiners.QuantityWord.alcuni.numberRestriction = some Number.plural
• Italian.Determiners.QuantityWord.molti.numberRestriction = some Number.plural
• Italian.Determiners.QuantityWord.pochi.numberRestriction = some Number.plural

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

The word as a determiner record.

Equations

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

def Italian.Determiners.QuantityWord.toList : List QuantityWord

All the words.

Equations

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

theorem Italian.Determiners.QuantityWord.feminine_eq_form_iff (w : QuantityWord) : w.feminine = w.form ↔ w = ogni ∨ w = qualche

Every word distinguishes its two forms or has one for both genders.

@[instance_reducible]

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

The readings available for a word. Ogni and tutti read as every, qualche and alcuni as Quantifier.GQ.some, and pochi as few; molti has no reading, its standard being contextual like that of English many. The n-word nessuno reads as no, a negative quantifier ([dSS02]), or as Quantifier.GQ.some, an indefinite whose negation the clause supplies ([Zei04]).

Equations

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

def Italian.Determiners.inventory : Determiner.Inventory

The Italian determiner inventory.

Equations

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

theorem Italian.Determiners.marking : inventory.markingStrategy = Reference.MarkingStrategy.generallyMarked

Italian derives the .generallyMarked [Mor21] cell.