English Determiners

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

Quantifier lexicon with syntactic and semantic properties.

Main definitions

• QForce: quantificational force
• QuantEntry: unified lexical entry

inductive Fragments.English.Determiners.QForce : Type

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

instance Fragments.English.Determiners.instDecidableEqQForce : DecidableEq QForce

Equations

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

def Fragments.English.Determiners.instReprQForce.repr : QForce → ℕ → Std.Format

Equations

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

instance Fragments.English.Determiners.instReprQForce : Repr QForce

Equations

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

instance Fragments.English.Determiners.instBEqQForce : BEq QForce

Equations

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

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

Equations

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

inductive Fragments.English.Determiners.Monotonicity : Type

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

instance Fragments.English.Determiners.instDecidableEqMonotonicity : DecidableEq Monotonicity

Equations

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

instance Fragments.English.Determiners.instReprMonotonicity : Repr Monotonicity

Equations

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

def Fragments.English.Determiners.instReprMonotonicity.repr : Monotonicity → ℕ → Std.Format

Equations

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

instance Fragments.English.Determiners.instBEqMonotonicity : BEq Monotonicity

Equations

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

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

Equations

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

inductive Fragments.English.Determiners.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

instance Fragments.English.Determiners.instDecidableEqStrength : DecidableEq Strength

Equations

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

def Fragments.English.Determiners.instReprStrength.repr : Strength → ℕ → Std.Format

Equations

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

instance Fragments.English.Determiners.instReprStrength : Repr Strength

Equations

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

instance Fragments.English.Determiners.instBEqStrength : BEq Strength

Equations

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

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

Equations

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

structure Fragments.English.Determiners.QuantifierEntry : Type

Unified lexical entry for quantifiers/determiners.

• form : String
• qforce : QForce
• numberRestriction : Option Number
• allowsMass : Bool
• monotonicity : Monotonicity
• strength : Strength
• gqtThreshold : ℚ
• ptPrototype : ℚ
• ptSpread : ℚ

def Fragments.English.Determiners.instReprQuantifierEntry.repr : QuantifierEntry → ℕ → Std.Format

Equations

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

instance Fragments.English.Determiners.instReprQuantifierEntry : Repr QuantifierEntry

Equations

• Fragments.English.Determiners.instReprQuantifierEntry = { reprPrec := Fragments.English.Determiners.instReprQuantifierEntry.repr }

def Fragments.English.Determiners.instBEqQuantifierEntry.beq : QuantifierEntry → QuantifierEntry → Bool

Equations

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

instance Fragments.English.Determiners.instBEqQuantifierEntry : BEq QuantifierEntry

Equations

• Fragments.English.Determiners.instBEqQuantifierEntry = { beq := Fragments.English.Determiners.instBEqQuantifierEntry.beq }

def Fragments.English.Determiners.none_ : QuantifierEntry

Equations

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

def Fragments.English.Determiners.few : QuantifierEntry

Equations

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

def Fragments.English.Determiners.some_ : QuantifierEntry

Equations

• Fragments.English.Determiners.some_ = { form := "some", qforce := Fragments.English.Determiners.QForce.existential, allowsMass := true, ptPrototype := 1 / 3, ptSpread := 3 }

def Fragments.English.Determiners.half : QuantifierEntry

Equations

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

def Fragments.English.Determiners.most : QuantifierEntry

"most" - more than half

Equations

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

def Fragments.English.Determiners.all : QuantifierEntry

"all" - everything satisfies

Equations

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

def Fragments.English.Determiners.every : QuantifierEntry

"every" - universal, singular

Equations

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

def Fragments.English.Determiners.each : QuantifierEntry

"each" - universal, distributive

Equations

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

def Fragments.English.Determiners.many : QuantifierEntry

"many" - a large number

Equations

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

structure Fragments.English.Determiners.NumericalDetEntry : Type

Numerical determiner entry. Parameterized by threshold n. These are the class of determiners @cite{van-de-pol-etal-2023} show satisfy all three semantic universals (and have low MDL).

• form : String
• qforce : QForce
• monotonicity : Monotonicity
• threshold : ℕ

  The numerical threshold

def Fragments.English.Determiners.instReprNumericalDetEntry.repr : NumericalDetEntry → ℕ → Std.Format

Equations

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

instance Fragments.English.Determiners.instReprNumericalDetEntry : Repr NumericalDetEntry

Equations

• Fragments.English.Determiners.instReprNumericalDetEntry = { reprPrec := Fragments.English.Determiners.instReprNumericalDetEntry.repr }

def Fragments.English.Determiners.instBEqNumericalDetEntry.beq : NumericalDetEntry → NumericalDetEntry → Bool

Equations

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

instance Fragments.English.Determiners.instBEqNumericalDetEntry : BEq NumericalDetEntry

Equations

• Fragments.English.Determiners.instBEqNumericalDetEntry = { beq := Fragments.English.Determiners.instBEqNumericalDetEntry.beq }

def Fragments.English.Determiners.atLeast (n : ℕ) : NumericalDetEntry

"at least n" — upward monotone in scope, conservative, quantity

Equations

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

def Fragments.English.Determiners.atMost (n : ℕ) : NumericalDetEntry

"at most n" — downward monotone in scope, conservative, quantity

Equations

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

def Fragments.English.Determiners.exactlyN (n : ℕ) : NumericalDetEntry

"exactly n" — non-monotone (neither UE nor DE), conservative, quantity

Equations

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

def Fragments.English.Determiners.moreThan (n : ℕ) : NumericalDetEntry

"more than n" — upward monotone, conservative, quantity

Equations

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

def Fragments.English.Determiners.fewerThan (n : ℕ) : NumericalDetEntry

"fewer than n" — downward monotone, conservative, quantity

Equations

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

def Fragments.English.Determiners.the : QuantifierEntry

Equations

• Fragments.English.Determiners.the = { form := "the", qforce := Fragments.English.Determiners.QForce.definite, allowsMass := true, strength := Fragments.English.Determiners.Strength.strong }

def Fragments.English.Determiners.this : QuantifierEntry

Equations

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

def Fragments.English.Determiners.that : QuantifierEntry

Equations

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

def Fragments.English.Determiners.these : QuantifierEntry

Equations

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

def Fragments.English.Determiners.those : QuantifierEntry

Equations

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

def Fragments.English.Determiners.a : QuantifierEntry

Equations

• Fragments.English.Determiners.a = { form := "a", qforce := Fragments.English.Determiners.QForce.existential, numberRestriction := some Number.sg }

def Fragments.English.Determiners.an : QuantifierEntry

Equations

• Fragments.English.Determiners.an = { form := "an", qforce := Fragments.English.Determiners.QForce.existential, numberRestriction := some Number.sg }

def Fragments.English.Determiners.both : QuantifierEntry

"both" - universal dual, presupposes exactly 2. K&S (83a): [_Det each of the two] ⇒ both. Semantically: gqMeet of every and (the 2).

Equations

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

def Fragments.English.Determiners.neither : QuantifierEntry

"neither" - negative dual, presupposes exactly 2. K&S (83b): [_Det (not one) of the two] ⇒ neither. Semantically: outerNeg of both.

Equations

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

def Fragments.English.Determiners.allQuantifiers : List QuantifierEntry

All quantifier entries

Equations

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

def Fragments.English.Determiners.allDeterminers : List QuantifierEntry

All determiner entries (including definites)

Equations

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

def Fragments.English.Determiners.lookup (form : String) : Option QuantifierEntry

Lookup by form

Equations

• Fragments.English.Determiners.lookup form = List.find? (fun (d : Fragments.English.Determiners.QuantifierEntry) => d.form == form) Fragments.English.Determiners.allDeterminers

inductive Fragments.English.Determiners.QuantityWord : Type

The 6-word quantity scale used in @cite{van-tiel-franke-sauerland-2021}.

This is a projection of the full lexicon for quantity-focused analyses.

• none_ : QuantityWord
• few : QuantityWord
• some_ : QuantityWord
• half : QuantityWord
• most : QuantityWord
• all : QuantityWord

instance Fragments.English.Determiners.instReprQuantityWord : Repr QuantityWord

Equations

• Fragments.English.Determiners.instReprQuantityWord = { reprPrec := Fragments.English.Determiners.instReprQuantityWord.repr }

def Fragments.English.Determiners.instReprQuantityWord.repr : QuantityWord → ℕ → Std.Format

Equations

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

instance Fragments.English.Determiners.instDecidableEqQuantityWord : DecidableEq QuantityWord

Equations

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

instance Fragments.English.Determiners.instBEqQuantityWord : BEq QuantityWord

Equations

• Fragments.English.Determiners.instBEqQuantityWord = { beq := Fragments.English.Determiners.instBEqQuantityWord.beq }

def Fragments.English.Determiners.instBEqQuantityWord.beq : QuantityWord → QuantityWord → Bool

Equations

• Fragments.English.Determiners.instBEqQuantityWord.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.English.Determiners.instInhabitedQuantityWord.default : QuantityWord

Equations

• Fragments.English.Determiners.instInhabitedQuantityWord.default = Fragments.English.Determiners.QuantityWord.none_

instance Fragments.English.Determiners.instInhabitedQuantityWord : Inhabited QuantityWord

Equations

• Fragments.English.Determiners.instInhabitedQuantityWord = { default := Fragments.English.Determiners.instInhabitedQuantityWord.default }

instance Fragments.English.Determiners.instFintypeQuantityWord : Fintype QuantityWord

Equations

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

def Fragments.English.Determiners.QuantityWord.entry : QuantityWord → QuantifierEntry

Get the lexical entry for a quantity word

Equations

• Fragments.English.Determiners.QuantityWord.none_.entry = Fragments.English.Determiners.none_
• Fragments.English.Determiners.QuantityWord.few.entry = Fragments.English.Determiners.few
• Fragments.English.Determiners.QuantityWord.some_.entry = Fragments.English.Determiners.some_
• Fragments.English.Determiners.QuantityWord.half.entry = Fragments.English.Determiners.half
• Fragments.English.Determiners.QuantityWord.most.entry = Fragments.English.Determiners.most
• Fragments.English.Determiners.QuantityWord.all.entry = Fragments.English.Determiners.all

def Fragments.English.Determiners.QuantityWord.monotonicity (q : QuantityWord) : Monotonicity

Get monotonicity from the entry

Equations

• q.monotonicity = q.entry.monotonicity

def Fragments.English.Determiners.QuantityWord.gqtThreshold (n : ℕ) (q : QuantityWord) : ℕ

Get GQT threshold (scaled to domain size n)

Equations

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

def Fragments.English.Determiners.QuantityWord.ptPrototype (n : ℕ) (q : QuantityWord) : ℕ

Get PT prototype (scaled to domain size n)

Equations

• Fragments.English.Determiners.QuantityWord.ptPrototype n q = (q.entry.ptPrototype * ↑n).floor.toNat

def Fragments.English.Determiners.QuantityWord.ptSpread (q : QuantityWord) : ℚ

Get PT spread

Equations

• q.ptSpread = q.entry.ptSpread

def Fragments.English.Determiners.QuantityWord.toList : List QuantityWord

All quantity words as a list

Equations

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

structure Fragments.English.Determiners.Scale : Type

A Horn scale: ordered alternatives from weak to strong.

The key property: each item entails all weaker items.

• items : List QuantityWord

  Items from weakest to strongest

• name : String

  Name for display

def Fragments.English.Determiners.someAllScale : Scale

The ⟨some, all⟩ scale

Equations

• Fragments.English.Determiners.someAllScale = { items := [Fragments.English.Determiners.QuantityWord.some_, Fragments.English.Determiners.QuantityWord.all], name := "⟨some, all⟩" }

def Fragments.English.Determiners.someMostAllScale : Scale

The ⟨some, most, all⟩ scale

Equations

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

def Fragments.English.Determiners.Scale.alternatives (s : Scale) (x : QuantityWord) : List QuantityWord

Get alternatives (items strictly stronger than x)

Equations

• s.alternatives x = match List.dropWhile (fun (x_1 : Fragments.English.Determiners.QuantityWord) => x_1 != x) s.items with | [] => [] | head :: rest => rest

def Fragments.English.Determiners.Scale.weaker (s : Scale) (x y : QuantityWord) : Bool

Is x weaker than y on this scale?

Equations

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

def Fragments.English.Determiners.QuantityWord.gqtMeaning (n : ℕ) (q : QuantityWord) (t : Fin (n + 1)) : Bool

GQT meaning: binary truth based on threshold and monotonicity

Equations

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

def Fragments.English.Determiners.QuantityWord.gqtMeaningRat (n : ℕ) (q : QuantityWord) (t : Fin (n + 1)) : ℚ

GQT meaning as rational

Equations

• Fragments.English.Determiners.QuantityWord.gqtMeaningRat n q t = if Fragments.English.Determiners.QuantityWord.gqtMeaning n q t = true then 1 else 0

theorem Fragments.English.Determiners.QuantityWord.gqtMeaningRat_nonneg (n : ℕ) (q : QuantityWord) (t : Fin (n + 1)) : 0 ≤ gqtMeaningRat n q t

GQT meaning is always non-negative

def Fragments.English.Determiners.QuantityWord.ptMeaning (n : ℕ) (q : QuantityWord) (t : Fin (n + 1)) : ℚ

PT meaning: gradient truth based on distance from prototype

Equations

• Fragments.English.Determiners.QuantityWord.ptMeaning n q t = Fragments.English.Determiners.approxGaussian✝ ((↑↑t - ↑(Fragments.English.Determiners.QuantityWord.ptPrototype n q)) / q.ptSpread)

theorem Fragments.English.Determiners.QuantityWord.ptMeaning_nonneg (n : ℕ) (q : QuantityWord) (t : Fin (n + 1)) : 0 ≤ ptMeaning n q t

PT meaning is always non-negative

def Fragments.English.Determiners.QuantifierEntry.toWord (d : QuantifierEntry) : Word

Equations

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

Compositional Generalized Quantifier Semantics

The single source of truth for model-theoretic GQ denotations is Semantics.Lexical.Determiner.Quantifier. This section re-exports those denotations and connects them to the QuantityWord scale.

Thread map

From a QuantityWord you can reach:

• Compositional denotations: QuantityWord.gqDenotation → every_sem, some_sem, etc.
• Semantic universals (@cite{barwise-cooper-1981}): Conservative, ScopeUpwardMono, ScopeDownwardMono — all in Core.Quantification. Quantity, SatisfiesUniversals in Semantics.Lexical.Determiner.Quantifier
• Proved properties: every_conservative, some_scope_up, no_scope_down, etc.
• Duality operations (B&C §4.11): Core.Quantification.outerNeg, innerNeg, dualQ with outerNeg_up_to_down, outerNeg_down_to_up, innerNeg_up_to_down (C9)
• Strength (B&C Table II): Strength enum, Core.Quantification.IntersectionCondition, QSymmetric, RestrictorUpwardMono (persistence), intersection_conservative_symmetric (C5)
• Threshold semantics: QuantityWord.gqtMeaning (scalar GQT representation)
• Prototype semantics: QuantityWord.ptMeaning (gradient PT representation)
• RSA domains: RSA.Quantity (pragmatic reasoning over quantity scales)
• Monotonicity: Semantics.Entailment.Monotonicity (polarity)
• Complexity: Core.Conjectures.simplicity_explains_universals

inductive Fragments.English.Determiners.InferentialClass : Type

@cite{van-benthem-1984} §3.3: Inferential characterization of the Square of Opposition. Each corner is uniquely determined by its relational properties under CONSERV + QUANT + VAR*.

• inclusion: all — transitive + reflexive (⊆)
• overlap: some — symmetric + quasi-reflexive (∩ ≠ ∅)
• disjointness: no — symmetric + quasi-universal (∩ = ∅)
• nonInclusion: not all — almost-connected + irreflexive (⊄)

• inclusion : InferentialClass
• overlap : InferentialClass
• disjointness : InferentialClass
• nonInclusion : InferentialClass

instance Fragments.English.Determiners.instDecidableEqInferentialClass : DecidableEq InferentialClass

Equations

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

def Fragments.English.Determiners.instReprInferentialClass.repr : InferentialClass → ℕ → Std.Format

Equations

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

instance Fragments.English.Determiners.instReprInferentialClass : Repr InferentialClass

Equations

• Fragments.English.Determiners.instReprInferentialClass = { reprPrec := Fragments.English.Determiners.instReprInferentialClass.repr }

instance Fragments.English.Determiners.instBEqInferentialClass : BEq InferentialClass

Equations

• Fragments.English.Determiners.instBEqInferentialClass = { beq := Fragments.English.Determiners.instBEqInferentialClass.beq }

def Fragments.English.Determiners.instBEqInferentialClass.beq : InferentialClass → InferentialClass → Bool

Equations

• Fragments.English.Determiners.instBEqInferentialClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Fragments.English.Determiners.QuantityWord.inferentialClass : QuantityWord → Option InferentialClass

Map quantity words to their inferential class (Square of Opposition corner).

Equations

• Fragments.English.Determiners.QuantityWord.all.inferentialClass = some Fragments.English.Determiners.InferentialClass.inclusion
• Fragments.English.Determiners.QuantityWord.some_.inferentialClass = some Fragments.English.Determiners.InferentialClass.overlap
• Fragments.English.Determiners.QuantityWord.none_.inferentialClass = some Fragments.English.Determiners.InferentialClass.disjointness
• x✝.inferentialClass = none

def Fragments.English.Determiners.QuantityWord.doubleMono : QuantityWord → Option Core.Quantification.DoubleMono

Map quantity words to their double monotonicity type (@cite{van-benthem-1984} §4.2).

Equations

• Fragments.English.Determiners.QuantityWord.all.doubleMono = some Core.Quantification.DoubleMono.downUp
• Fragments.English.Determiners.QuantityWord.some_.doubleMono = some Core.Quantification.DoubleMono.upUp
• Fragments.English.Determiners.QuantityWord.none_.doubleMono = some Core.Quantification.DoubleMono.downDown
• x✝.doubleMono = none

def Fragments.English.Determiners.QuantityWord.gqDenotation (q : QuantityWord) (m : Semantics.Montague.Model) [Fintype m.Entity] : m.interpTy Semantics.Lexical.Determiner.Quantifier.Ty.det

Map quantity words to their canonical model-theoretic GQ denotation. These are the compositional (e→t) → ((e→t) → t) meanings from Montague/Barwise & Cooper, proved conservative and monotone in Semantics.Lexical.Determiner.Quantifier.

Equations

• Fragments.English.Determiners.QuantityWord.none_.gqDenotation m = Semantics.Lexical.Determiner.Quantifier.no_sem m
• Fragments.English.Determiners.QuantityWord.some_.gqDenotation m = Semantics.Lexical.Determiner.Quantifier.some_sem m
• Fragments.English.Determiners.QuantityWord.all.gqDenotation m = Semantics.Lexical.Determiner.Quantifier.every_sem m
• Fragments.English.Determiners.QuantityWord.most.gqDenotation m = Semantics.Lexical.Determiner.Quantifier.most_sem m
• Fragments.English.Determiners.QuantityWord.few.gqDenotation m = Semantics.Lexical.Determiner.Quantifier.few_sem m
• Fragments.English.Determiners.QuantityWord.half.gqDenotation m = Semantics.Lexical.Determiner.Quantifier.half_sem m

theorem Fragments.English.Determiners.every_mono_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : every.monotonicity = Monotonicity.increasing ∧ Core.Quantification.ScopeUpwardMono (Semantics.Lexical.Determiner.Quantifier.every_sem m)

Every: monotonicity metadata says .increasing and semantics is scope-↑.

theorem Fragments.English.Determiners.some_mono_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : some_.monotonicity = Monotonicity.increasing ∧ Core.Quantification.ScopeUpwardMono (Semantics.Lexical.Determiner.Quantifier.some_sem m)

Some: monotonicity metadata says .increasing and semantics is scope-↑.

theorem Fragments.English.Determiners.none_mono_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : none_.monotonicity = Monotonicity.decreasing ∧ Core.Quantification.ScopeDownwardMono (Semantics.Lexical.Determiner.Quantifier.no_sem m)

None: monotonicity metadata says .decreasing and semantics is scope-↓.

theorem Fragments.English.Determiners.all_mono_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : all.monotonicity = Monotonicity.increasing ∧ Core.Quantification.ScopeUpwardMono (Semantics.Lexical.Determiner.Quantifier.every_sem m)

All: monotonicity metadata says .increasing and semantics is scope-↑. (All and every share every_sem.)

theorem Fragments.English.Determiners.most_mono_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : most.monotonicity = Monotonicity.increasing ∧ Core.Quantification.ScopeUpwardMono (Semantics.Lexical.Determiner.Quantifier.most_sem m)

Most: monotonicity metadata says .increasing and semantics is scope-↑.

theorem Fragments.English.Determiners.few_mono_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : few.monotonicity = Monotonicity.decreasing ∧ Core.Quantification.ScopeDownwardMono (Semantics.Lexical.Determiner.Quantifier.few_sem m)

Few: monotonicity metadata says .decreasing and semantics is scope-↓.

theorem Fragments.English.Determiners.half_mono_bridge : half.monotonicity = Monotonicity.nonMonotone

Half: monotonicity metadata says .nonMonotone — half is neither scope-↑ nor scope-↓. Adding elements to S can flip half(R,S) either way.

theorem Fragments.English.Determiners.all_conservative_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : QuantityWord.all.gqDenotation m = Semantics.Lexical.Determiner.Quantifier.every_sem m ∧ Core.Quantification.Conservative (Semantics.Lexical.Determiner.Quantifier.every_sem m)

All maps to every_sem and every_sem is conservative.

theorem Fragments.English.Determiners.some_conservative_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : QuantityWord.some_.gqDenotation m = Semantics.Lexical.Determiner.Quantifier.some_sem m ∧ Core.Quantification.Conservative (Semantics.Lexical.Determiner.Quantifier.some_sem m)

Some maps to some_sem and some_sem is conservative.

theorem Fragments.English.Determiners.none_conservative_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : QuantityWord.none_.gqDenotation m = Semantics.Lexical.Determiner.Quantifier.no_sem m ∧ Core.Quantification.Conservative (Semantics.Lexical.Determiner.Quantifier.no_sem m)

None maps to no_sem and no_sem is conservative.

theorem Fragments.English.Determiners.most_conservative_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : QuantityWord.most.gqDenotation m = Semantics.Lexical.Determiner.Quantifier.most_sem m ∧ Core.Quantification.Conservative (Semantics.Lexical.Determiner.Quantifier.most_sem m)

Most maps to most_sem and most_sem is conservative.

theorem Fragments.English.Determiners.few_conservative_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : QuantityWord.few.gqDenotation m = Semantics.Lexical.Determiner.Quantifier.few_sem m ∧ Core.Quantification.Conservative (Semantics.Lexical.Determiner.Quantifier.few_sem m)

Few maps to few_sem and few_sem is conservative.

theorem Fragments.English.Determiners.half_conservative_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : QuantityWord.half.gqDenotation m = Semantics.Lexical.Determiner.Quantifier.half_sem m ∧ Core.Quantification.Conservative (Semantics.Lexical.Determiner.Quantifier.half_sem m)

Half maps to half_sem and half_sem is conservative.

theorem Fragments.English.Determiners.some_symmetry_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : some_.strength = Strength.weak ∧ Core.Quantification.QSymmetric (Semantics.Lexical.Determiner.Quantifier.some_sem m)

Some: weak (allows there-insertion) and symmetric.

theorem Fragments.English.Determiners.none_symmetry_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : none_.strength = Strength.weak ∧ Core.Quantification.QSymmetric (Semantics.Lexical.Determiner.Quantifier.no_sem m)

None: weak and symmetric.

theorem Fragments.English.Determiners.every_not_symmetric_bridge : every.strength = Strength.strong ∧ ¬Core.Quantification.QSymmetric (Semantics.Lexical.Determiner.Quantifier.every_sem Semantics.Montague.toyModel)

Every: strong and NOT symmetric.

def Fragments.English.Determiners.both_sem (m : Semantics.Montague.Model) [Fintype m.Entity] : m.interpTy Semantics.Lexical.Determiner.Quantifier.Ty.det

⟦both⟧(R)(S) = ⟦every⟧(R)(S) when |R|=2. For the general case, both = every restricted to exactly-2 restrictors. Simplified: on finite models, both(R,S) = every(R,S) ∧ |R|≥2.

Equations

• Fragments.English.Determiners.both_sem m R S = (Semantics.Lexical.Determiner.Quantifier.every_sem m R S && decide ({x : m.Entity | R x = true}.card ≥ 2))

def Fragments.English.Determiners.neither_sem (m : Semantics.Montague.Model) [Fintype m.Entity] : m.interpTy Semantics.Lexical.Determiner.Quantifier.Ty.det

⟦neither⟧ = outer negation of ⟦both⟧ (K&S (83b)). "Neither student passed" = "It's not the case that both students passed" when exactly 2 students exist. K&S: neither = (not one) of the two.

Equations

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

theorem Fragments.English.Determiners.both_conservative {m : Semantics.Montague.Model} [Fintype m.Entity] : Core.Quantification.Conservative (both_sem m)

both is conservative (follows from every_conservative + gqMeet closure).

theorem Fragments.English.Determiners.neither_conservative {m : Semantics.Montague.Model} [Fintype m.Entity] : Core.Quantification.Conservative (neither_sem m)

neither is conservative (follows from no_conservative + gqMeet closure).

theorem Fragments.English.Determiners.both_positive_strong_on_nonempty : both.strength = Strength.strong ∧ neither.strength = Strength.strong

K&S §3.2: both is positive strong — both(A,A) = true when |A|≥2.

theorem Fragments.English.Determiners.neither_decreasing : neither.monotonicity = Monotonicity.decreasing

K&S (26) at the fragment level: neither is scope-↓ (licenses NPIs). "Neither student saw any deer" — NPI "any" licensed.

theorem Fragments.English.Determiners.both_neither_mono_duality : both.monotonicity = Monotonicity.increasing ∧ neither.monotonicity = Monotonicity.decreasing

both/neither duality: both is increasing, neither is decreasing, mirroring every/no.

theorem Fragments.English.Determiners.every_laa_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : QuantityWord.all.gqDenotation m = Semantics.Lexical.Determiner.Quantifier.every_sem m ∧ Core.Quantification.LeftAntiAdditive (Semantics.Lexical.Determiner.Quantifier.every_sem m)

"Every"/"all" is left-anti-additive in the restrictor: every(A∪B, C) = every(A,C) ∧ every(B,C). This licenses strong NPIs in the restrictor of "every": "Everyone who ever lifted a finger..." Cross-ref: every_laa.

theorem Fragments.English.Determiners.none_laa_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : QuantityWord.none_.gqDenotation m = Semantics.Lexical.Determiner.Quantifier.no_sem m ∧ Core.Quantification.LeftAntiAdditive (Semantics.Lexical.Determiner.Quantifier.no_sem m) ∧ Core.Quantification.ScopeDownwardMono (Semantics.Lexical.Determiner.Quantifier.no_sem m)

"No"/"none" is left-anti-additive in the restrictor: no(A∪B, C) = no(A,C) ∧ no(B,C). Also scope-downward-monotone (licenses weak NPIs in scope). Cross-ref: no_laa, no_scope_down.

theorem Fragments.English.Determiners.all_inferential_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : QuantityWord.all.inferentialClass = some InferentialClass.inclusion ∧ Core.Quantification.QTransitive (Semantics.Lexical.Determiner.Quantifier.every_sem m) ∧ Core.Quantification.PositiveStrong (Semantics.Lexical.Determiner.Quantifier.every_sem m) ∧ Core.Quantification.QAntisymmetric (Semantics.Lexical.Determiner.Quantifier.every_sem m)

All: inferential class is inclusion, confirmed by relational properties. Van Benthem Thm 3.1.1: the ONLY reflexive antisymmetric quantifier.

theorem Fragments.English.Determiners.some_inferential_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : QuantityWord.some_.inferentialClass = some InferentialClass.overlap ∧ Core.Quantification.QSymmetric (Semantics.Lexical.Determiner.Quantifier.some_sem m) ∧ Core.Quantification.QuasiReflexive (Semantics.Lexical.Determiner.Quantifier.some_sem m)

Some: inferential class is overlap, confirmed by relational properties. Van Benthem Thm 3.3.2: the ONLY symmetric quasi-reflexive quantifier.

theorem Fragments.English.Determiners.none_inferential_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : QuantityWord.none_.inferentialClass = some InferentialClass.disjointness ∧ Core.Quantification.QSymmetric (Semantics.Lexical.Determiner.Quantifier.no_sem m) ∧ Core.Quantification.QuasiUniversal (Semantics.Lexical.Determiner.Quantifier.no_sem m)

None: inferential class is disjointness, confirmed by relational properties. Van Benthem Cor 3.3.3: the ONLY symmetric quasi-universal quantifier.

theorem Fragments.English.Determiners.all_doubleMono_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : QuantityWord.all.doubleMono = some Core.Quantification.DoubleMono.downUp ∧ Core.Quantification.RestrictorDownwardMono (Semantics.Lexical.Determiner.Quantifier.every_sem m) ∧ Core.Quantification.ScopeUpwardMono (Semantics.Lexical.Determiner.Quantifier.every_sem m)

All: double mono ↓MON↑ metadata matches semantic proof.

theorem Fragments.English.Determiners.some_doubleMono_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : QuantityWord.some_.doubleMono = some Core.Quantification.DoubleMono.upUp ∧ Core.Quantification.RestrictorUpwardMono (Semantics.Lexical.Determiner.Quantifier.some_sem m) ∧ Core.Quantification.ScopeUpwardMono (Semantics.Lexical.Determiner.Quantifier.some_sem m)

Some: double mono ↑MON↑ metadata matches semantic proof.

theorem Fragments.English.Determiners.none_doubleMono_bridge {m : Semantics.Montague.Model} [Fintype m.Entity] : QuantityWord.none_.doubleMono = some Core.Quantification.DoubleMono.downDown ∧ Core.Quantification.RestrictorDownwardMono (Semantics.Lexical.Determiner.Quantifier.no_sem m) ∧ Core.Quantification.ScopeDownwardMono (Semantics.Lexical.Determiner.Quantifier.no_sem m)

None: double mono ↓MON↓ metadata matches semantic proof.