Quantifier typology — shared enums

[Hor72] [BC81]

Theory-level descriptive enums for the typological classification of quantifiers/determiners, shared across language fragments and the studies that consume the textbook-consensus B&C Table II metadata. The lexical entry record is gone: a quantifier's lexical marking is now Syntax.Determiner.Quantifier (Syntax/Determiner/Basic.lean); these enums survive only as the typological labels that record metadata (force, monotonicity, weak/strong strength) reads off, and as the parameter type of the GQT gqtMeaning operator.

Main declarations

• QForce — quantificational force (universal, existential, …).
• Monotonicity — increasing / decreasing / non-monotone (typological label).
• Strength — weak / strong (Barwise & Cooper §4.3 Table II; weak determiners pass there is/are).

inductive Quantification.Lexicon.QForce : Type

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

@[implicit_reducible]

instance Quantification.Lexicon.instDecidableEqQForce : DecidableEq QForce

Equations

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

@[implicit_reducible]

instance Quantification.Lexicon.instReprQForce : Repr QForce

Equations

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

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

Equations

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

inductive Quantification.Lexicon.Monotonicity : Type

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

@[implicit_reducible]

instance Quantification.Lexicon.instDecidableEqMonotonicity : DecidableEq Monotonicity

Equations

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

@[implicit_reducible]

instance Quantification.Lexicon.instReprMonotonicity : Repr Monotonicity

Equations

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

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

Equations

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

inductive 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 Quantification.Lexicon.instDecidableEqStrength : DecidableEq Strength

Equations

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

@[implicit_reducible]

instance Quantification.Lexicon.instReprStrength : Repr Strength

Equations

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

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

Equations

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