Italian Determiners (Quantifiers)

Quantifier lexicon with syntactic and semantic properties. Reuses the shared QuantifierEntry from Theories/Semantics/Quantification/Lexicon.lean and extends it with gender agreement.

Italian quantifiers agree in gender and/or number with their NP:

• ogni (every): invariant, singular
• qualche (some): invariant, singular
• nessuno/nessuna (no): gender-variable, singular, negative concord
• tutti/tutte (all): gender-variable, plural
• alcuni/alcune (some): gender-variable, plural
• molti/molte (many): gender-variable, plural
• pochi/poche (few): gender-variable, plural

structure Fragments.Italian.Determiners.ItalianQuantifierEntryextends Theories.Semantics.Quantification.Lexicon.QuantifierEntry : Type

Italian quantifier entry: shared QuantifierEntry + gender.

• form : String
• qforce : QForce
• numberRestriction : Option Number
• allowsMass : Bool
• monotonicity : Monotonicity
• strength : Strength
• gender : Option Features.SurfaceGender

  Gender agreement (none = invariant)

@[implicit_reducible]

instance Fragments.Italian.Determiners.instReprItalianQuantifierEntry : Repr ItalianQuantifierEntry

Equations

• Fragments.Italian.Determiners.instReprItalianQuantifierEntry = { reprPrec := Fragments.Italian.Determiners.instReprItalianQuantifierEntry.repr }

def Fragments.Italian.Determiners.instReprItalianQuantifierEntry.repr : ItalianQuantifierEntry → ℕ → Std.Format

Equations

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

def Fragments.Italian.Determiners.ogni : ItalianQuantifierEntry

ogni — every (invariant, singular, universal).

Equations

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

def Fragments.Italian.Determiners.qualche : ItalianQuantifierEntry

qualche — some (invariant, singular, existential).

Equations

• Fragments.Italian.Determiners.qualche = { form := "qualche", qforce := Theories.Semantics.Quantification.Lexicon.QForce.existential, numberRestriction := some Number.sg }

def Fragments.Italian.Determiners.nessuno : ItalianQuantifierEntry

nessuno — no one (masculine, singular, negative concord).

Equations

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

def Fragments.Italian.Determiners.nessuna : ItalianQuantifierEntry

nessuna — no one (feminine, singular, negative concord).

Equations

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

def Fragments.Italian.Determiners.tutti : ItalianQuantifierEntry

tutti — all (masculine, plural, universal).

Equations

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

def Fragments.Italian.Determiners.tutte : ItalianQuantifierEntry

tutte — all (feminine, plural, universal).

Equations

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

def Fragments.Italian.Determiners.alcuni : ItalianQuantifierEntry

alcuni — some (masculine, plural, existential).

Equations

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

def Fragments.Italian.Determiners.alcune : ItalianQuantifierEntry

alcune — some (feminine, plural, existential).

Equations

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

def Fragments.Italian.Determiners.molti : ItalianQuantifierEntry

molti — many (masculine, plural, proportional).

Equations

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

def Fragments.Italian.Determiners.molte : ItalianQuantifierEntry

molte — many (feminine, plural, proportional).

Equations

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

def Fragments.Italian.Determiners.pochi : ItalianQuantifierEntry

pochi — few (masculine, plural, proportional, decreasing).

Equations

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

def Fragments.Italian.Determiners.poche : ItalianQuantifierEntry

poche — few (feminine, plural, proportional, decreasing).

Equations

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

def Fragments.Italian.Determiners.allQuantifiers : List ItalianQuantifierEntry

All Italian quantifier entries.

Equations

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

def Fragments.Italian.Determiners.lookup (form : String) : Option ItalianQuantifierEntry

Lookup by form.

Equations

• Fragments.Italian.Determiners.lookup form = List.find? (fun (q : Fragments.Italian.Determiners.ItalianQuantifierEntry) => q.form == form) Fragments.Italian.Determiners.allQuantifiers

theorem Fragments.Italian.Determiners.ogni_universal : ogni.qforce = Theories.Semantics.Quantification.Lexicon.QForce.universal ∧ ogni.monotonicity = Theories.Semantics.Quantification.Lexicon.Monotonicity.increasing ∧ ogni.strength = Theories.Semantics.Quantification.Lexicon.Strength.strong

ogni is universal, increasing, and strong.

theorem Fragments.Italian.Determiners.nessuno_negative : nessuno.qforce = Theories.Semantics.Quantification.Lexicon.QForce.negative ∧ nessuno.monotonicity = Theories.Semantics.Quantification.Lexicon.Monotonicity.decreasing

nessuno is negative and decreasing.

theorem Fragments.Italian.Determiners.tutti_universal : tutti.qforce = Theories.Semantics.Quantification.Lexicon.QForce.universal ∧ tutti.monotonicity = Theories.Semantics.Quantification.Lexicon.Monotonicity.increasing ∧ tutti.strength = Theories.Semantics.Quantification.Lexicon.Strength.strong

tutti is universal, increasing, and strong.

theorem Fragments.Italian.Determiners.qualche_existential : qualche.qforce = Theories.Semantics.Quantification.Lexicon.QForce.existential ∧ qualche.monotonicity = Theories.Semantics.Quantification.Lexicon.Monotonicity.increasing

qualche is existential and increasing.

theorem Fragments.Italian.Determiners.pochi_decreasing : pochi.qforce = Theories.Semantics.Quantification.Lexicon.QForce.proportional ∧ pochi.monotonicity = Theories.Semantics.Quantification.Lexicon.Monotonicity.decreasing

pochi is proportional and decreasing.

theorem Fragments.Italian.Determiners.nessuno_nessuna_gender : nessuno.gender = some Features.SurfaceGender.masculine ∧ nessuna.gender = some Features.SurfaceGender.feminine ∧ nessuno.qforce = nessuna.qforce

Gender agreement: nessuno/nessuna are masculine/feminine forms of the same quantifier.

theorem Fragments.Italian.Determiners.tutti_tutte_gender : tutti.gender = some Features.SurfaceGender.masculine ∧ tutte.gender = some Features.SurfaceGender.feminine ∧ tutti.qforce = tutte.qforce

Gender agreement: tutti/tutte are masculine/feminine forms of the same quantifier.