Italian Determiners (Quantifiers)

Quantifier lexicon with syntactic and semantic properties, following the QuantifierEntry pattern from Fragments/English/Determiners.lean but extended with gender/number agreement for Italian.

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

inductive Fragments.Italian.Determiners.QForce : Type

Quantificational force.

• universal : QForce
• existential : QForce
• negative : QForce
• proportional : QForce

instance Fragments.Italian.Determiners.instDecidableEqQForce : DecidableEq QForce

Equations

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

instance Fragments.Italian.Determiners.instReprQForce : Repr QForce

Equations

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

def Fragments.Italian.Determiners.instReprQForce.repr : QForce → Nat → Std.Format

Equations

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

instance Fragments.Italian.Determiners.instBEqQForce : BEq QForce

Equations

• Fragments.Italian.Determiners.instBEqQForce = { beq := Fragments.Italian.Determiners.instBEqQForce.beq }

def Fragments.Italian.Determiners.instBEqQForce.beq : QForce → QForce → Bool

Equations

• Fragments.Italian.Determiners.instBEqQForce.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

inductive Fragments.Italian.Determiners.Monotonicity : Type

Monotonicity in the scope argument.

• increasing : Monotonicity
• decreasing : Monotonicity
• nonMonotone : Monotonicity

instance Fragments.Italian.Determiners.instDecidableEqMonotonicity : DecidableEq Monotonicity

Equations

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

instance Fragments.Italian.Determiners.instReprMonotonicity : Repr Monotonicity

Equations

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

def Fragments.Italian.Determiners.instReprMonotonicity.repr : Monotonicity → Nat → Std.Format

Equations

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

def Fragments.Italian.Determiners.instBEqMonotonicity.beq : Monotonicity → Monotonicity → Bool

Equations

• Fragments.Italian.Determiners.instBEqMonotonicity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Italian.Determiners.instBEqMonotonicity : BEq Monotonicity

Equations

• Fragments.Italian.Determiners.instBEqMonotonicity = { beq := Fragments.Italian.Determiners.instBEqMonotonicity.beq }

inductive Fragments.Italian.Determiners.Strength : Type

Weak/strong classification.

• weak : Strength
• strong : Strength

instance Fragments.Italian.Determiners.instDecidableEqStrength : DecidableEq Strength

Equations

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

instance Fragments.Italian.Determiners.instReprStrength : Repr Strength

Equations

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

def Fragments.Italian.Determiners.instReprStrength.repr : Strength → Nat → Std.Format

Equations

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

def Fragments.Italian.Determiners.instBEqStrength.beq : Strength → Strength → Bool

Equations

• Fragments.Italian.Determiners.instBEqStrength.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Italian.Determiners.instBEqStrength : BEq Strength

Equations

• Fragments.Italian.Determiners.instBEqStrength = { beq := Fragments.Italian.Determiners.instBEqStrength.beq }

inductive Fragments.Italian.Determiners.Gender : Type

Gender for agreement.

• masc : Gender
• fem : Gender

instance Fragments.Italian.Determiners.instDecidableEqGender : DecidableEq Gender

Equations

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

instance Fragments.Italian.Determiners.instReprGender : Repr Gender

Equations

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

def Fragments.Italian.Determiners.instReprGender.repr : Gender → Nat → Std.Format

Equations

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

def Fragments.Italian.Determiners.instBEqGender.beq : Gender → Gender → Bool

Equations

• Fragments.Italian.Determiners.instBEqGender.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Fragments.Italian.Determiners.instBEqGender : BEq Gender

Equations

• Fragments.Italian.Determiners.instBEqGender = { beq := Fragments.Italian.Determiners.instBEqGender.beq }

structure Fragments.Italian.Determiners.ItalianQuantifierEntry : Type

Italian quantifier entry with gender/number agreement.

• form : String
• qforce : QForce
• monotonicity : Monotonicity
• strength : Strength
• gender : Option Gender

  Gender agreement (none = invariant)

• number : Option Number

  Number restriction

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

Equations

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

instance Fragments.Italian.Determiners.instReprItalianQuantifierEntry : Repr ItalianQuantifierEntry

Equations

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

def Fragments.Italian.Determiners.instBEqItalianQuantifierEntry.beq : ItalianQuantifierEntry → ItalianQuantifierEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Fragments.Italian.Determiners.instBEqItalianQuantifierEntry.beq x✝¹ x✝ = false

instance Fragments.Italian.Determiners.instBEqItalianQuantifierEntry : BEq ItalianQuantifierEntry

Equations

• Fragments.Italian.Determiners.instBEqItalianQuantifierEntry = { beq := Fragments.Italian.Determiners.instBEqItalianQuantifierEntry.beq }

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 := Fragments.Italian.Determiners.QForce.existential, number := 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 = QForce.universal ∧ ogni.monotonicity = Monotonicity.increasing ∧ ogni.strength = Strength.strong

ogni is universal, increasing, and strong.

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

nessuno is negative and decreasing.

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

tutti is universal, increasing, and strong.

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

qualche is existential and increasing.

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

pochi is proportional and decreasing.

theorem Fragments.Italian.Determiners.nessuno_nessuna_gender : nessuno.gender = some Gender.masc ∧ nessuna.gender = some Gender.fem ∧ 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 Gender.masc ∧ tutte.gender = some Gender.fem ∧ tutti.qforce = tutte.qforce

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