Quantifier lexicon — shared structure

@cite{horn-1972} @cite{barwise-cooper-1981}

A theory-level structure for quantifier lexical entries shared across language fragments. Carries only descriptive lexical-typological data — per-paper model parameters (GQT thresholds, PT prototypes, …) live in the study files that commit to specific values.

Fields

• form — surface form
• qforce — quantificational force (universal, existential, …)
• numberRestriction — none (number-neutral), or some .sg/.pl/.du (a single grammatical number; .du covers items like English both and French les deux whose meaning composition uses the dual core concept @cite{jeretic-bassi-gonzalez-yatsushiro-meyer-sauerland-2025})
• allowsMass — accepts mass NPs?
• monotonicity — increasing / decreasing / non-monotone (typological label)
• strength — weak / strong (Barwise & Cooper §4.3 Table II; weak determiners pass there is/are)

inductive Theories.Semantics.Quantification.Lexicon.QForce : Type

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

@[implicit_reducible]

instance Theories.Semantics.Quantification.Lexicon.instDecidableEqQForce : DecidableEq QForce

Equations

• Theories.Semantics.Quantification.Lexicon.instDecidableEqQForce x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Theories.Semantics.Quantification.Lexicon.instReprQForce.repr : QForce → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Theories.Semantics.Quantification.Lexicon.instReprQForce : Repr QForce

Equations

• Theories.Semantics.Quantification.Lexicon.instReprQForce = { reprPrec := Theories.Semantics.Quantification.Lexicon.instReprQForce.repr }

inductive Theories.Semantics.Quantification.Lexicon.Monotonicity : Type

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

@[implicit_reducible]

instance Theories.Semantics.Quantification.Lexicon.instDecidableEqMonotonicity : DecidableEq Monotonicity

Equations

• Theories.Semantics.Quantification.Lexicon.instDecidableEqMonotonicity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Theories.Semantics.Quantification.Lexicon.instReprMonotonicity : Repr Monotonicity

Equations

• Theories.Semantics.Quantification.Lexicon.instReprMonotonicity = { reprPrec := Theories.Semantics.Quantification.Lexicon.instReprMonotonicity.repr }

def Theories.Semantics.Quantification.Lexicon.instReprMonotonicity.repr : Monotonicity → ℕ → Std.Format

Equations

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

inductive Theories.Semantics.Quantification.Lexicon.Strength : Type

Weak/strong classification (B&C §4.3, Table II). Weak determiners allow there-insertion: "There are some cats." Strong determiners don't: "*There is every cat."

• weak : Strength
• strong : Strength

@[implicit_reducible]

instance Theories.Semantics.Quantification.Lexicon.instDecidableEqStrength : DecidableEq Strength

Equations

• Theories.Semantics.Quantification.Lexicon.instDecidableEqStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Theories.Semantics.Quantification.Lexicon.instReprStrength : Repr Strength

Equations

• Theories.Semantics.Quantification.Lexicon.instReprStrength = { reprPrec := Theories.Semantics.Quantification.Lexicon.instReprStrength.repr }

def Theories.Semantics.Quantification.Lexicon.instReprStrength.repr : Strength → ℕ → Std.Format

Equations

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

structure Theories.Semantics.Quantification.Lexicon.QuantifierEntry : Type

Unified lexical entry for quantifiers/determiners.

• form : String
• qforce : QForce
• numberRestriction : Option Number
• allowsMass : Bool
• monotonicity : Monotonicity
• strength : Strength

@[implicit_reducible]

instance Theories.Semantics.Quantification.Lexicon.instReprQuantifierEntry : Repr QuantifierEntry

Equations

• Theories.Semantics.Quantification.Lexicon.instReprQuantifierEntry = { reprPrec := Theories.Semantics.Quantification.Lexicon.instReprQuantifierEntry.repr }

def Theories.Semantics.Quantification.Lexicon.instReprQuantifierEntry.repr : QuantifierEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Theories.Semantics.Quantification.Lexicon.instBEqQuantifierEntry : BEq QuantifierEntry

Equations

• Theories.Semantics.Quantification.Lexicon.instBEqQuantifierEntry = { beq := Theories.Semantics.Quantification.Lexicon.instBEqQuantifierEntry.beq }

def Theories.Semantics.Quantification.Lexicon.instBEqQuantifierEntry.beq : QuantifierEntry → QuantifierEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• Theories.Semantics.Quantification.Lexicon.instBEqQuantifierEntry.beq x✝¹ x✝ = false

def Theories.Semantics.Quantification.Lexicon.instDecidableEqQuantifierEntry.decEq (x✝ x✝¹ : QuantifierEntry) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Theories.Semantics.Quantification.Lexicon.instDecidableEqQuantifierEntry : DecidableEq QuantifierEntry

Equations

• Theories.Semantics.Quantification.Lexicon.instDecidableEqQuantifierEntry = Theories.Semantics.Quantification.Lexicon.instDecidableEqQuantifierEntry.decEq

def Theories.Semantics.Quantification.Lexicon.QuantifierEntry.toWord (d : QuantifierEntry) : Word

Project the lexical entry to a Core Word: form, category DET, and number features inherited from numberRestriction.

Equations

• d.toWord = { form := d.form, cat := UD.UPOS.DET, features := { number := d.numberRestriction } }