Generalized Quantifiers #

@cite{barwise-cooper-1981} @cite{keenan-stavi-1986} @cite{peters-westerstahl-2006} @cite{van-de-pol-etal-2023} @cite{mostowski-1957}

Determiners have type (e→t) → ((e→t) → t):

⟦every⟧ = λR.λS. ∀x. R(x) → S(x)
⟦some⟧ = λR.λS. ∃x. R(x) ∧ S(x)
⟦no⟧ = λR.λS. ¬∃x. R(x) ∧ S(x)

Semantic Universals #

Three properties conjectured to hold of all simple (lexicalized) determiners:

Conservativity: Q(A, B) ↔ Q(A, A ∩ B) — only the restrictor matters
Quantity (isomorphism closure): meaning depends only on cardinalities |A ∩ B|, |A \ B|, |B \ A|, |M \ (A ∪ B)|
Monotonicity: Q is either upward or downward monotone in scope

@cite{van-de-pol-etal-2023} show quantifiers satisfying these universals have shorter minimal description length, suggesting a simplicity bias explains the universals.

Organization #

Generic GQ properties: Core.Quantification — Conservative, ScopeUpwardMono, ScopeDownwardMono, outerNeg, innerNeg, dualQ, etc. (model-agnostic, Bool-valued)
Prop-valued GQ properties: Defined locally in this file for Prop-valued denotations (Conservative, ScopeUpwardMono, etc.)
Concrete denotations: every_sem, some_sem, etc. — Prop-valued, matching Denot .t = Prop
Counting quantifiers: most_sem, few_sem, etc. — use Finset.univ.filter for cardinality comparisons

source

def Semantics.Quantification.Quantifier.Ty.det :

Core.Logic.Intensional.Ty

Equations

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

Instances For

source

def Semantics.Quantification.Quantifier.SatisfiesUniversals {α : Type u_1} (q : Core.Quantification.GQ α) :

Prop

A GQ satisfies the Barwise & Cooper monotonicity universals (CONS plus monotone in scope in some direction). Convenience conjunction; Core has Conservative, ScopeUpwardMono, ScopeDownwardMono separately.

Equations

Semantics.Quantification.Quantifier.SatisfiesUniversals q = (Core.Quantification.Conservative q ∧ (Core.Quantification.ScopeUpwardMono q ∨ Core.Quantification.ScopeDownwardMono q))

Instances For

source

@[implicit_reducible]

instance Semantics.Quantification.Quantifier.decImpl {p q : Prop} [Decidable p] [Decidable q] :

Decidable (p → q)

Decidability of implication (not in Lean 4 core).

Equations

Semantics.Quantification.Quantifier.decImpl = if hp : p then if hq : q then isTrue ⋯ else isFalse ⋯ else isTrue ⋯

source

def Semantics.Quantification.Quantifier.count {α : Type} [Fintype α] (P : α → Prop) [DecidablePred P] :

ℕ

Count of elements satisfying a predicate, via Finset.univ.filter.

Equations

Semantics.Quantification.Quantifier.count P = (Finset.filter P Finset.univ).card

Instances For

source

def Semantics.Quantification.Quantifier.every_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] :

F.Denot Ty.det

Equations

Semantics.Quantification.Quantifier.every_sem F R S = ∀ (x : F.Entity), R x → S x

Instances For

source

def Semantics.Quantification.Quantifier.some_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] :

F.Denot Ty.det

Equations

Semantics.Quantification.Quantifier.some_sem F R S = ∃ (x : F.Entity), R x ∧ S x

Instances For

source

theorem Semantics.Quantification.Quantifier.A_eq_some_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] (domain : List F.Entity) (hComplete : ∀ (x : F.Entity), x ∈ domain) :

Composition.TypeShifting.A domain = some_sem F

Partee's A (existential closure) = Barwise & Cooper's ⟦some⟧. Both compute λR.λS. ∃x. R(x) ∧ S(x) over a finite domain. A takes the domain explicitly; some_sem uses ∃ over the entity type.

source

def Semantics.Quantification.Quantifier.no_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] :

F.Denot Ty.det

Equations

Semantics.Quantification.Quantifier.no_sem F R S = ∀ (x : F.Entity), R x → ¬S x

Instances For

source

noncomputable def Semantics.Quantification.Quantifier.most_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] :

F.Denot Ty.det

⟦most⟧(R)(S) = |R ∩ S| > |R \ S|

Equations

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

Instances For

source

noncomputable def Semantics.Quantification.Quantifier.few_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] :

F.Denot Ty.det

⟦few⟧(R)(S) = |R ∩ S| < |R \ S| — a minority of Rs are Ss. Dual of most_sem: few(R,S) ↔ ¬most(R,S) ∧ ¬half(R,S).

Equations

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

Instances For

source

noncomputable def Semantics.Quantification.Quantifier.half_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] :

F.Denot Ty.det

⟦half⟧(R)(S) = 2 * |R ∩ S| = |R| — exactly half of Rs are Ss.

Equations

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

Instances For

source

noncomputable def Semantics.Quantification.Quantifier.both_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] :

F.Denot Ty.det

⟦both⟧(R)(S) = ⟦every⟧(R)(S) ∧ |R| ≥ 2. K&S §2.3: both = every restricted to dual restrictors.

Equations

Semantics.Quantification.Quantifier.both_sem F R S = (Semantics.Quantification.Quantifier.every_sem F R S ∧ {x : F.Entity | R x}.card ≥ 2)

Instances For

source

noncomputable def Semantics.Quantification.Quantifier.neither_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] :

F.Denot Ty.det

⟦neither⟧ = gqMeet ⟦no⟧ (|R| ≥ 2) (K&S (83b)).

Equations

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

Instances For

source

noncomputable def Semantics.Quantification.Quantifier.at_least_n_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] (n : ℕ) :

F.Denot Ty.det

⟦at least n⟧(R)(S) = |R ∩ S| ≥ n

Equations

Semantics.Quantification.Quantifier.at_least_n_sem F n R S = ((Semantics.Quantification.Quantifier.count fun (x : F.Entity) => R x ∧ S x) ≥ n)

Instances For

source

noncomputable def Semantics.Quantification.Quantifier.at_most_n_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] (n : ℕ) :

F.Denot Ty.det

⟦at most n⟧(R)(S) = |R ∩ S| ≤ n

Equations

Semantics.Quantification.Quantifier.at_most_n_sem F n R S = ((Semantics.Quantification.Quantifier.count fun (x : F.Entity) => R x ∧ S x) ≤ n)

Instances For

source

noncomputable def Semantics.Quantification.Quantifier.exactly_n_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] (n : ℕ) :

F.Denot Ty.det

⟦exactly n⟧(R)(S) = |R ∩ S| = n

Equations

Semantics.Quantification.Quantifier.exactly_n_sem F n R S = ((Semantics.Quantification.Quantifier.count fun (x : F.Entity) => R x ∧ S x) = n)

Instances For

source

noncomputable def Semantics.Quantification.Quantifier.all_but_n_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] (n : ℕ) :

F.Denot Ty.det

⟦all but n⟧(R)(S) = |R \ S| = n — exactly n R-elements are non-S. Generalizes "every" (= all but 0). The exceptive counterpart of exactly_n_sem (which counts |R ∩ S| = n).

Equations

Semantics.Quantification.Quantifier.all_but_n_sem F n R S = ((Semantics.Quantification.Quantifier.count fun (x : F.Entity) => R x ∧ ¬S x) = n)

Instances For

source

noncomputable def Semantics.Quantification.Quantifier.between_n_m_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] (n k : ℕ) :

F.Denot Ty.det

⟦between n and k⟧(R)(S) = n ≤ |R ∩ S| ≤ k

Equations

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

Instances For

source

@[implicit_reducible]

instance Semantics.Quantification.Quantifier.instFintypeToyEntity :

Fintype Montague.ToyEntity

Equations

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

source

@[implicit_reducible]

instance Semantics.Quantification.Quantifier.instFintypeEntityToyModel :

Fintype Montague.toyModel.Entity

Bridge: toyModel.Entity = ToyEntity is definitional but opaque to instance search.

Equations

Semantics.Quantification.Quantifier.instFintypeEntityToyModel = inferInstance

source

def Semantics.Quantification.Quantifier.student_sem :

Montague.toyModel.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

Instances For

source

def Semantics.Quantification.Quantifier.person_sem :

Montague.toyModel.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

Instances For

source

def Semantics.Quantification.Quantifier.thing_sem :

Montague.toyModel.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

Semantics.Quantification.Quantifier.thing_sem x✝ = True

Instances For

source

@[implicit_reducible]

instance Semantics.Quantification.Quantifier.instDecidablePredDenotToyModelEStudent_sem :

DecidablePred student_sem

Equations

One or more equations did not get rendered due to their size.
Semantics.Quantification.Quantifier.instDecidablePredDenotToyModelEStudent_sem Semantics.Montague.ToyEntity.john = isTrue True.intro
Semantics.Quantification.Quantifier.instDecidablePredDenotToyModelEStudent_sem Semantics.Montague.ToyEntity.mary = isTrue True.intro

source

@[implicit_reducible]

instance Semantics.Quantification.Quantifier.instDecidablePredDenotToyModelEPerson_sem :

DecidablePred person_sem

Equations

One or more equations did not get rendered due to their size.
Semantics.Quantification.Quantifier.instDecidablePredDenotToyModelEPerson_sem Semantics.Montague.ToyEntity.john = isTrue True.intro
Semantics.Quantification.Quantifier.instDecidablePredDenotToyModelEPerson_sem Semantics.Montague.ToyEntity.mary = isTrue True.intro

source

@[implicit_reducible]

instance Semantics.Quantification.Quantifier.instDecidablePredDenotToyModelEThing_sem :

DecidablePred thing_sem

Equations

Semantics.Quantification.Quantifier.instDecidablePredDenotToyModelEThing_sem x✝ = isTrue trivial

source

theorem Semantics.Quantification.Quantifier.not_everyStudentSleeps :

¬every_sem Montague.toyModel student_sem Montague.ToyLexicon.sleeps_sem

Not every student sleeps (john sleeps but mary doesn't).

source

theorem Semantics.Quantification.Quantifier.someStudentSleeps :

some_sem Montague.toyModel student_sem Montague.ToyLexicon.sleeps_sem

Some student sleeps (john does).

source

theorem Semantics.Quantification.Quantifier.not_noStudentSleeps :

¬no_sem Montague.toyModel student_sem Montague.ToyLexicon.sleeps_sem

Not no student sleeps (john does).

source

theorem Semantics.Quantification.Quantifier.everyStudentLaughs :

every_sem Montague.toyModel student_sem Montague.ToyLexicon.laughs_sem

Every student laughs (john and mary both laugh).

source

theorem Semantics.Quantification.Quantifier.someStudentLaughs :

some_sem Montague.toyModel student_sem Montague.ToyLexicon.laughs_sem

Some student laughs.

source

theorem Semantics.Quantification.Quantifier.not_everyPersonSleeps :

¬every_sem Montague.toyModel person_sem Montague.ToyLexicon.sleeps_sem

Not every person sleeps.

source

theorem Semantics.Quantification.Quantifier.somePersonSleeps :

some_sem Montague.toyModel person_sem Montague.ToyLexicon.sleeps_sem

Some person sleeps.

source

theorem Semantics.Quantification.Quantifier.forall_bij_inv {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] (f : F.Entity → F.Entity) (hBij : Function.Bijective f) (P : F.Entity → Prop) :

(∀ (x : F.Entity), P x) ↔ ∀ (x : F.Entity), P (f x)

∀ x, P x is invariant under bijective substitution.

source

theorem Semantics.Quantification.Quantifier.exists_bij_inv {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] (f : F.Entity → F.Entity) (hBij : Function.Bijective f) (P : F.Entity → Prop) :

(∃ (x : F.Entity), P x) ↔ ∃ (x : F.Entity), P (f x)

∃ x, P x is invariant under bijective substitution.

source

theorem Semantics.Quantification.Quantifier.count_bij_inv {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] (f : F.Entity → F.Entity) (hBij : Function.Bijective f) {P : F.Entity → Prop} [DecidablePred P] :

count P = count (P ∘ f)

count P = count (P ∘ f) when f is a bijection.

source

theorem Semantics.Quantification.Quantifier.every_conservative {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

Core.Quantification.Conservative (every_sem F)

⟦every⟧ is conservative: ∀x. R(x) → S(x) iff ∀x. R(x) → (R(x) ∧ S(x)).

source

theorem Semantics.Quantification.Quantifier.some_conservative {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

Core.Quantification.Conservative (some_sem F)

⟦some⟧ is conservative: ∃x. R(x) ∧ S(x) iff ∃x. R(x) ∧ (R(x) ∧ S(x)).

source

theorem Semantics.Quantification.Quantifier.no_conservative {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

Core.Quantification.Conservative (no_sem F)

⟦no⟧ is conservative: ∀x. R(x) → ¬S(x) iff ∀x. R(x) → ¬(R(x) ∧ S(x)).

source

theorem Semantics.Quantification.Quantifier.most_conservative {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

Core.Quantification.Conservative (most_sem F)

⟦most⟧ is conservative: the R-elements in S are the R-elements in R∩S.

source

theorem Semantics.Quantification.Quantifier.few_conservative {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

Core.Quantification.Conservative (few_sem F)

⟦few⟧ is conservative: the R-elements in S are the R-elements in R∩S.

source

theorem Semantics.Quantification.Quantifier.half_conservative {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

Core.Quantification.Conservative (half_sem F)

⟦half⟧ is conservative: depends only on R ∩ S within R.

source

theorem Semantics.Quantification.Quantifier.both_conservative {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

Core.Quantification.Conservative (both_sem F)

⟦both⟧ is conservative (inherits from every_sem).

source

theorem Semantics.Quantification.Quantifier.neither_conservative {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

Core.Quantification.Conservative (neither_sem F)

⟦neither⟧ is conservative (inherits from no_sem).

source

theorem Semantics.Quantification.Quantifier.at_least_n_conservative {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] (n : ℕ) :

Core.Quantification.Conservative (at_least_n_sem F n)

⟦at least n⟧ is conservative: |R ∩ S| = |R ∩ (R ∩ S)|.

source

theorem Semantics.Quantification.Quantifier.at_most_n_conservative {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] (n : ℕ) :

Core.Quantification.Conservative (at_most_n_sem F n)

⟦at most n⟧ is conservative.

source

theorem Semantics.Quantification.Quantifier.exactly_n_conservative {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] (n : ℕ) :

Core.Quantification.Conservative (exactly_n_sem F n)

⟦exactly n⟧ is conservative.

source

theorem Semantics.Quantification.Quantifier.every_scope_up {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

Core.Quantification.ScopeUpwardMono (every_sem F)

⟦every⟧ is upward monotone in scope.

source

theorem Semantics.Quantification.Quantifier.some_scope_up {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

Core.Quantification.ScopeUpwardMono (some_sem F)

⟦some⟧ is upward monotone in scope.

source

theorem Semantics.Quantification.Quantifier.no_scope_down {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

Core.Quantification.ScopeDownwardMono (no_sem F)

⟦no⟧ is downward monotone in scope.

source

theorem Semantics.Quantification.Quantifier.few_scope_down {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

Core.Quantification.ScopeDownwardMono (few_sem F)

⟦few⟧ is downward monotone in scope: if S ⊆ S' and few(R,S'), then few(R,S). Fewer Ss among Rs means even fewer S-subsets.

source

theorem Semantics.Quantification.Quantifier.most_scope_up {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

Core.Quantification.ScopeUpwardMono (most_sem F)

⟦most⟧ is upward monotone in scope: if S ⊆ S' and most(R,S), then most(R,S'). |R∩S'| ≥ |R∩S| > |R\S| ≥ |R\S'|.

source

theorem Semantics.Quantification.Quantifier.some_eq_at_least_1 {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

some_sem F = at_least_n_sem F 1

⟦some⟧ = ⟦at least 1⟧: existential quantification is "at least one".

source

theorem Semantics.Quantification.Quantifier.pouterNeg_some_eq_no {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

Core.Quantification.outerNeg (some_sem F) = no_sem F

outerNeg ⟦some⟧ = ⟦no⟧: negating existence gives universal negation.

source

theorem Semantics.Quantification.Quantifier.at_most_eq_pouterNeg_at_least_succ {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] (n : ℕ) :

at_most_n_sem F n = Core.Quantification.outerNeg (at_least_n_sem F (n + 1))

⟦at most n⟧ = outerNeg ⟦at least n+1⟧: duality of lower and upper bounds. This is the counting quantifier instance of the Square of Opposition.

source

theorem Semantics.Quantification.Quantifier.no_eq_at_most_0 {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] :

no_sem F = at_most_n_sem F 0

⟦no⟧ = ⟦at most 0⟧. Derived algebraically: no = outerNeg(some) = outerNeg(at_least 1) = at_most 0.

source

theorem Semantics.Quantification.Quantifier.exactly_eq_meet_at_least_at_most {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] (n : ℕ) :

exactly_n_sem F n = Core.Quantification.gqMeet (at_least_n_sem F n) (at_most_n_sem F n)

⟦exactly n⟧ = ⟦at least n⟧ ⊓ ⟦at most n⟧ in the GQ lattice. "Exactly n" is the meet of a lower bound and an upper bound.

source

theorem Semantics.Quantification.Quantifier.at_least_n_scope_up {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] (n : ℕ) :

Core.Quantification.ScopeUpwardMono (at_least_n_sem F n)

⟦at least n⟧ is Mon↑ in scope: enlarging B cannot decrease |A ∩ B|.

source

theorem Semantics.Quantification.Quantifier.at_most_n_scope_down {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] (n : ℕ) :

Core.Quantification.ScopeDownwardMono (at_most_n_sem F n)

⟦at most n⟧ is Mon↓ in scope. Derived from duality: outerNeg flips Mon↑ to Mon↓, and at_most = outerNeg(at_least).

source

def Semantics.Quantification.Quantifier.Quantity {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] (q : Core.Quantification.GQ F.Entity) :

Prop

Quantity / Isomorphism closure: Q(A, B) depends only on the four cardinalities |A ∩ B|, |A \ B|, |B \ A|, |M \ (A ∪ B)|.

Equivalently: permuting the domain does not change the quantifier's truth value. This is the type ⟨1,1⟩ (binary) generalization of @cite{mostowski-1957}'s permutation invariance for type ⟨1⟩ (unary) quantifiers; the extension to binary determiners is due to @cite{van-benthem-1984} (building on Lindström 1966).

Equations

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

Instances For

source

theorem Semantics.Quantification.Quantifier.quantityInvariant_of_quantity {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] (q : Core.Quantification.GQ F.Entity) (hQ : Quantity q) :

Core.Quantification.QuantityInvariant q

Quantity → QuantityInvariant: cardinality-dependence implies bijection-invariance. TODO: proof requires adapting cell-bijection machinery to Prop predicates.

source

theorem Semantics.Quantification.Quantifier.quantity_of_quantityInvariant {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (q : Core.Quantification.GQ F.Entity) (hQ : Core.Quantification.QuantityInvariant q) :

Quantity q

QuantityInvariant → Quantity: bijection-invariance implies cardinality-dependence. TODO: proof requires adapting cell-bijection machinery to Prop predicates.

source

noncomputable def Semantics.Quantification.Quantifier.m_sem (F : Core.Logic.Intensional.Frame) [Fintype F.Entity] :

Core.Quantification.GQ F.Entity

A non-conservative quantifier for contrast: ⟦M⟧(A,B) = |A| > |B| (van de Pol et al.'s hypothetical counterpart to "most").

Equations

Semantics.Quantification.Quantifier.m_sem F R S = ((Semantics.Quantification.Quantifier.count fun (x : F.Entity) => R x) > Semantics.Quantification.Quantifier.count fun (x : F.Entity) => S x)

Instances For

source

theorem Semantics.Quantification.Quantifier.m_not_conservative :

¬Core.Quantification.Conservative (m_sem Montague.toyModel)

M is not conservative: it inspects B outside A.

source

theorem Semantics.Quantification.Quantifier.some_symmetric {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.QSymmetric (some_sem F)

⟦some⟧ is symmetric: ∃x.R(x)∧S(x) = ∃x.S(x)∧R(x).

source

theorem Semantics.Quantification.Quantifier.no_symmetric {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.QSymmetric (no_sem F)

⟦no⟧ is symmetric: ¬∃x.R(x)∧S(x) = ¬∃x.S(x)∧R(x).

source

theorem Semantics.Quantification.Quantifier.every_not_symmetric :

¬Core.Quantification.QSymmetric (every_sem Montague.toyModel)

⟦every⟧ is NOT symmetric. Witness: R=students, S=things (everything). every(students)(things)=true but every(things)(students)=false.

source

theorem Semantics.Quantification.Quantifier.some_intersective {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.IntersectionCondition (some_sem F)

⟦some⟧ is intersective (follows from CONSERV + SYMM).

source

theorem Semantics.Quantification.Quantifier.no_intersective {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.IntersectionCondition (no_sem F)

⟦no⟧ is intersective.

source

theorem Semantics.Quantification.Quantifier.every_laa {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.LeftAntiAdditive (every_sem F)

⟦every⟧ is left anti-additive: every(A∪B, C) = every(A,C) ∧ every(B,C).

source

theorem Semantics.Quantification.Quantifier.no_laa {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.LeftAntiAdditive (no_sem F)

⟦no⟧ is left anti-additive: no(A∪B, C) = no(A,C) ∧ no(B,C).

source

theorem Semantics.Quantification.Quantifier.no_raa {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.RightAntiAdditive (no_sem F)

⟦no⟧ is right anti-additive: no(A, B∪C) = no(A,B) ∧ no(A,C). "Nobody saw A-or-B" ↔ "Nobody saw A and nobody saw B". This licenses strong NPIs in scope: "Nobody lifted a finger."

source

theorem Semantics.Quantification.Quantifier.laa_characterization {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.LeftAntiAdditive (every_sem F) ∧ Core.Quantification.LeftAntiAdditive (no_sem F)

@cite{peters-westerstahl-2006} Prop 13: the only non-trivial CONSERV, EXT, and ISOM quantifiers satisfying LAA are every and no (and A = ∅).

source

theorem Semantics.Quantification.Quantifier.pinnerNeg_every_eq_no {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.innerNeg (every_sem F) = no_sem F

Inner negation maps every to no: every...not = no. ∀x. R(x) → ¬S(x) = ¬∃x. R(x) ∧ S(x).

source

theorem Semantics.Quantification.Quantifier.pdualQ_every_eq_some {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.dualQ (every_sem F) = some_sem F

The dual of every is some: Q̌(every) = some. ¬(∀x. R(x) → ¬S(x)) = ∃x. R(x) ∧ S(x).

source

theorem Semantics.Quantification.Quantifier.every_ext_spectator {F : Core.Logic.Intensional.Frame} (es : List F.Entity) (e : F.Entity) (R S : F.Entity → Bool) (hR : R e = false) :

((e :: es).all fun (x : F.Entity) => !R x || S x) = es.all fun (x : F.Entity) => !R x || S x

every_sem satisfies Extension: spectator elements (outside the restrictor) don't affect truth values.

source

theorem Semantics.Quantification.Quantifier.some_ext_spectator {F : Core.Logic.Intensional.Frame} (es : List F.Entity) (e : F.Entity) (R S : F.Entity → Bool) (hR : R e = false) :

((e :: es).any fun (x : F.Entity) => R x && S x) = es.any fun (x : F.Entity) => R x && S x

some_sem satisfies Extension.

source

theorem Semantics.Quantification.Quantifier.no_ext_spectator {F : Core.Logic.Intensional.Frame} (es : List F.Entity) (e : F.Entity) (R S : F.Entity → Bool) (hR : R e = false) :

((e :: es).all fun (x : F.Entity) => !R x || !S x) = es.all fun (x : F.Entity) => !R x || !S x

no_sem satisfies Extension.

source

theorem Semantics.Quantification.Quantifier.most_ext_spectator {F : Core.Logic.Intensional.Frame} (es : List F.Entity) (e : F.Entity) (R S : F.Entity → Bool) (hR : R e = false) :

List.filter (fun (x : F.Entity) => R x && S x) (e :: es) = List.filter (fun (x : F.Entity) => R x && S x) es ∧ List.filter (fun (x : F.Entity) => R x && !S x) (e :: es) = List.filter (fun (x : F.Entity) => R x && !S x) es

most_sem satisfies Extension: spectators don't enter either R∩S or R\S, so the cardinality comparison is unchanged.

source

theorem Semantics.Quantification.Quantifier.every_positive_strong {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.PositiveStrong (every_sem F)

every_sem is positive strong: every(A,A) = true for all A. Proof: R(x) → R(x) for all x.

source

theorem Semantics.Quantification.Quantifier.no_negative_strong_nonempty {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (R : F.Entity → Prop) (hR : ∃ (x : F.Entity), R x) :

¬no_sem F R R

no_sem is negative strong on non-empty restrictors: no(A,A) = false for all non-empty A.

source

theorem Semantics.Quantification.Quantifier.no_not_positive_strong :

¬Core.Quantification.PositiveStrong (no_sem Montague.toyModel)

no_sem is NOT positive strong: no(A,A) = false when A is non-empty. Counterexample: R = {john}.

source

theorem Semantics.Quantification.Quantifier.some_existential {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.Existential (some_sem F)

⟦some⟧ is existential (K&S G3): some(A,B) = some(A∩B, everything). some is natural in there-sentences: "There are some cats."

source

theorem Semantics.Quantification.Quantifier.no_existential {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.Existential (no_sem F)

⟦no⟧ is existential (K&S G3): no(A,B) = no(A∩B, everything).

source

theorem Semantics.Quantification.Quantifier.every_not_existential :

¬Core.Quantification.Existential (every_sem Montague.toyModel)

⟦every⟧ is NOT existential (K&S §3.3).

source

theorem Semantics.Quantification.Quantifier.most_not_existential :

¬Core.Quantification.Existential (most_sem Montague.toyModel)

⟦most⟧ is NOT existential (K&S §3.3).

source

theorem Semantics.Quantification.Quantifier.every_transitive {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.QTransitive (every_sem F)

⟦every⟧ is transitive: A ⊆ B and B ⊆ C implies A ⊆ C.

source

theorem Semantics.Quantification.Quantifier.every_antisymmetric {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.QAntisymmetric (every_sem F)

⟦every⟧ is antisymmetric: A ⊆ B and B ⊆ A implies A = B.

source

theorem Semantics.Quantification.Quantifier.some_quasi_reflexive {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.QuasiReflexive (some_sem F)

⟦some⟧ is quasi-reflexive: A∩B ≠ ∅ implies A∩A ≠ ∅ (i.e., A ≠ ∅).

source

theorem Semantics.Quantification.Quantifier.no_quasi_universal {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.QuasiUniversal (no_sem F)

⟦no⟧ is quasi-universal: A∩A = ∅ (i.e., A = ∅) implies A∩B = ∅ for all B.

source

theorem Semantics.Quantification.Quantifier.every_restrictor_down {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.RestrictorDownwardMono (every_sem F)

⟦every⟧ is restrictor-↓ (anti-persistent). Follows from Zwarts bridge: reflexive + transitive + CONSERV → ↓MON.

source

theorem Semantics.Quantification.Quantifier.some_restrictor_up {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.RestrictorUpwardMono (some_sem F)

⟦some⟧ is restrictor-↑ (persistent): A ⊆ A' and some(A,B) → some(A',B).

source

theorem Semantics.Quantification.Quantifier.no_restrictor_down {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.RestrictorDownwardMono (no_sem F)

⟦no⟧ is restrictor-↓ (anti-persistent): A ⊆ A' and no(A',B) → no(A,B).

source

theorem Semantics.Quantification.Quantifier.every_doubleMono {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.RestrictorDownwardMono (every_sem F) ∧ Core.Quantification.ScopeUpwardMono (every_sem F)

⟦every⟧ has double monotonicity ↓MON↑ (@cite{van-benthem-1984} §4.2).

source

theorem Semantics.Quantification.Quantifier.some_doubleMono {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.RestrictorUpwardMono (some_sem F) ∧ Core.Quantification.ScopeUpwardMono (some_sem F)

⟦some⟧ has double monotonicity ↑MON↑.

source

theorem Semantics.Quantification.Quantifier.no_doubleMono {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.RestrictorDownwardMono (no_sem F) ∧ Core.Quantification.ScopeDownwardMono (no_sem F)

⟦no⟧ has double monotonicity ↓MON↓.

source

theorem Semantics.Quantification.Quantifier.notAll_doubleMono {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.RestrictorUpwardMono (Core.Quantification.outerNeg (every_sem F)) ∧ Core.Quantification.ScopeDownwardMono (Core.Quantification.outerNeg (every_sem F))

outerNeg ⟦every⟧ (= "not all") has double monotonicity ↑MON↓.

source

theorem Semantics.Quantification.Quantifier.every_filtrating {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.Filtrating (every_sem F)

⟦every⟧ is filtrating: every(A,B) ∧ every(A,C) → every(A, B∩C).

The six theorems below establish the four Aristotelian relations among GQ denotations (every_sem, some_sem, no_sem, outerNeg every_sem) at fixed restrictor R. They work over Prop-valued predicates, while Core.Logic.Opposition.Aristotelian formulates the same relations over Bool-valued predicates. The two frameworks are mathematically equivalent but type-different; bridging them at the predicate level would require either a Prop-valued version of the Aristotelian relations or a Bool-coercion of the GQ machinery — both architectural decisions beyond this section's scope.

For consumers wanting to instantiate the abstract Square (W → Bool) from Core.Opposition.Square, pass decide-coerced versions of the GQ predicates. The downstream Phenomena/Quantification/Studies/BarwiseCooper1981.lean §8 duality theorems are the natural site to package this bridge.

source

theorem Semantics.Quantification.Quantifier.every_contradicts_notEvery {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (R S : F.Entity → Prop) :

every_sem F R S ↔ ¬Core.Quantification.outerNeg (every_sem F) R S

Contradiction (A vs O): the A-form and O-form are contradictories.

source

theorem Semantics.Quantification.Quantifier.no_contradicts_some {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (R S : F.Entity → Prop) :

no_sem F R S ↔ ¬some_sem F R S

Contradiction (E vs I): the E-form and I-form are contradictories.

source

theorem Semantics.Quantification.Quantifier.a_e_contrary {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (R S : F.Entity → Prop) :

every_sem F R S → no_sem F R S → ∀ (x : F.Entity), ¬R x

Contrariety (A ∧ E): the A-form and E-form can't both hold unless the restrictor is empty.

source

theorem Semantics.Quantification.Quantifier.subalternation_a_i {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (R S : F.Entity → Prop) (hR : ∃ (x : F.Entity), R x) :

every_sem F R S → some_sem F R S

Subalternation (A → I): the A-form entails the I-form when the restrictor is non-empty.

source

theorem Semantics.Quantification.Quantifier.subalternation_e_o {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (R S : F.Entity → Prop) (hR : ∃ (x : F.Entity), R x) :

no_sem F R S → Core.Quantification.outerNeg (every_sem F) R S

Subalternation (E → O): the E-form entails the O-form when the restrictor is non-empty.

source

theorem Semantics.Quantification.Quantifier.subcontrariety_i_o {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (R S : F.Entity → Prop) (hR : ∃ (x : F.Entity), R x) :

some_sem F R S ∨ Core.Quantification.outerNeg (every_sem F) R S

Subcontrariety (I ∨ O): the I-form and O-form can't both fail when the restrictor is non-empty.

source

theorem Semantics.Quantification.Quantifier.every_satisfies_isContradictory_pointwise {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (R : F.Entity → Prop) :

Core.Opposition.IsContradictory (every_sem F R) (Core.Quantification.outerNeg (every_sem F) R)

Bundled (Prop↔Bool gap closure demo): the canonical A↔O contradiction diagonal, packaged as Core.Opposition.IsContradictory over the Pi-instance Boolean algebra on (F.Entity → Prop) → Prop. For a fixed restrictor R, the GQ semantics every_sem F R and its outer-negation outerNeg (every_sem F) R are pointwise contradictory in the BA-generic sense.

This bundling demonstrates that Aristotelian.lean's polymorphic IsContradictory/IsSubaltern/etc. work uniformly on Prop-valued predicates (the GQ convention) and Bool-valued predicates (the Tessler convention), via Pi.instBooleanAlgebra for Prop and Bool respectively. The audit's "Prop↔Bool gap" is closed at the type level. Bundling theorems for the other 5 corners (E↔I, A∧E, A→I, E→O, I∨O) follow the same template.

source

theorem Semantics.Quantification.Quantifier.some_upSE {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.UpSEMon (some_sem F)

⟦some⟧ is ↑_SE Mon: adding elements of B to A preserves some(A,B).

source

theorem Semantics.Quantification.Quantifier.some_upSW {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.UpSWMon (some_sem F)

⟦some⟧ is ↑_SW Mon: adding elements outside B to A preserves some(A,B).

source

theorem Semantics.Quantification.Quantifier.every_downNW {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.DownNWMon (every_sem F)

⟦every⟧ is ↓_NW Mon: removing elements of B from A preserves every(A,B).

source

theorem Semantics.Quantification.Quantifier.every_downNE {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.DownNEMon (every_sem F)

⟦every⟧ is ↓_NE Mon: removing elements outside B from A preserves every(A,B).

source

theorem Semantics.Quantification.Quantifier.no_downNW {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.DownNWMon (no_sem F)

⟦no⟧ is ↓_NW Mon.

source

theorem Semantics.Quantification.Quantifier.no_downNE {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.DownNEMon (no_sem F)

⟦no⟧ is ↓_NE Mon.

source

theorem Semantics.Quantification.Quantifier.some_downNE {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.DownNEMon (some_sem F)

⟦some⟧ is ↓_NE Mon (direct proof). Removing non-S elements from A preserves ∃x.R(x)∧S(x) since the witness is in S.

source

theorem Semantics.Quantification.Quantifier.some_smooth {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.Smooth (some_sem F)

⟦some⟧ is smooth (↓_NE + ↑_SE).

source

theorem Semantics.Quantification.Quantifier.every_upSE_direct {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.UpSEMon (every_sem F)

⟦every⟧ is ↑_SE Mon (direct proof). Adding B-elements to A preserves ∀x.R(x)→S(x) since the new elements satisfy S.

source

theorem Semantics.Quantification.Quantifier.every_smooth {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.Smooth (every_sem F)

⟦every⟧ is smooth (↓_NE + ↑_SE).

source

theorem Semantics.Quantification.Quantifier.no_coSmooth_partial {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.DownNWMon (no_sem F) ∧ Core.Quantification.DownNEMon (no_sem F)

⟦no⟧ is co-smooth (↓_NW + ↑_SW). Follows from anti-persistence.

source

theorem Semantics.Quantification.Quantifier.most_downNE {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.DownNEMon (most_sem F)

⟦most⟧ is ↓_NE Mon (direct proof).

source

theorem Semantics.Quantification.Quantifier.most_upSE {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.UpSEMon (most_sem F)

⟦most⟧ is ↑_SE Mon (direct proof).

source

theorem Semantics.Quantification.Quantifier.most_smooth {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Core.Quantification.Smooth (most_sem F)

⟦most⟧ is smooth.

source

theorem Semantics.Quantification.Quantifier.at_least_n_restrictor_up {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n : ℕ) :

Core.Quantification.RestrictorUpwardMono (at_least_n_sem F n)

⟦at least n⟧ is persistent (Mon↑ in restrictor).

source

theorem Semantics.Quantification.Quantifier.at_least_n_downNE {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n : ℕ) :

Core.Quantification.DownNEMon (at_least_n_sem F n)

⟦at least n⟧ is ↓_NE Mon.

source

theorem Semantics.Quantification.Quantifier.at_least_n_smooth {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n : ℕ) :

Core.Quantification.Smooth (at_least_n_sem F n)

⟦at least n⟧ is smooth (↓_NE + ↑_SE).

source

theorem Semantics.Quantification.Quantifier.at_most_n_restrictor_down {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n : ℕ) :

Core.Quantification.RestrictorDownwardMono (at_most_n_sem F n)

⟦at most n⟧ is anti-persistent (Mon↓ in restrictor).

source

theorem Semantics.Quantification.Quantifier.at_most_n_coSmooth {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n : ℕ) :

Core.Quantification.CoSmooth (at_most_n_sem F n)

⟦at most n⟧ is co-smooth (↓_NW + ↑_SW).

source

theorem Semantics.Quantification.Quantifier.quantity_pouterNeg {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (q : Core.Quantification.GQ F.Entity) (h : Quantity q) :

Quantity (Core.Quantification.outerNeg q)

Quantity is closed under outerNeg.

source

theorem Semantics.Quantification.Quantifier.quantity_pgqMeet {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (q₁ q₂ : Core.Quantification.GQ F.Entity) (h₁ : Quantity q₁) (h₂ : Quantity q₂) :

Quantity (Core.Quantification.gqMeet q₁ q₂)

Quantity is closed under gqMeet.

source

theorem Semantics.Quantification.Quantifier.at_least_n_quantity {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n : ℕ) :

Quantity (at_least_n_sem F n)

⟦at least n⟧ satisfies Quantity: truth depends only on |A ∩ B|.

source

theorem Semantics.Quantification.Quantifier.at_most_n_quantity {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n : ℕ) :

Quantity (at_most_n_sem F n)

⟦at most n⟧ satisfies Quantity: truth depends only on |A ∩ B|.

source

theorem Semantics.Quantification.Quantifier.exactly_n_quantity {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n : ℕ) :

Quantity (exactly_n_sem F n)

⟦exactly n⟧ satisfies Quantity.

source

theorem Semantics.Quantification.Quantifier.some_quantity {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Quantity (some_sem F)

⟦some⟧ satisfies Quantity.

source

theorem Semantics.Quantification.Quantifier.no_quantity {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Quantity (no_sem F)

⟦no⟧ satisfies Quantity.

source

theorem Semantics.Quantification.Quantifier.every_quantity {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Quantity (every_sem F)

source

theorem Semantics.Quantification.Quantifier.most_quantity {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Quantity (most_sem F)

⟦most⟧ satisfies Quantity.

source

theorem Semantics.Quantification.Quantifier.few_quantity {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Quantity (few_sem F)

⟦few⟧ satisfies Quantity.

source

theorem Semantics.Quantification.Quantifier.half_quantity {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Quantity (half_sem F)

⟦half⟧ satisfies Quantity.

source

theorem Semantics.Quantification.Quantifier.some_satisfiesUniversals {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

SatisfiesUniversals (some_sem F)

⟦some⟧ satisfies CONSERV ∧ Mon↑.

source

theorem Semantics.Quantification.Quantifier.every_satisfiesUniversals {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

SatisfiesUniversals (every_sem F)

⟦every⟧ satisfies CONSERV ∧ Mon↑.

source

theorem Semantics.Quantification.Quantifier.no_satisfiesUniversals {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

SatisfiesUniversals (no_sem F)

⟦no⟧ satisfies CONSERV ∧ Mon↓.

source

theorem Semantics.Quantification.Quantifier.most_satisfiesUniversals {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

SatisfiesUniversals (most_sem F)

⟦most⟧ satisfies CONSERV ∧ Mon↑.

source

theorem Semantics.Quantification.Quantifier.few_satisfiesUniversals {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

SatisfiesUniversals (few_sem F)

⟦few⟧ satisfies CONSERV ∧ Mon↓.

source

theorem Semantics.Quantification.Quantifier.at_least_n_satisfiesUniversals {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n : ℕ) :

SatisfiesUniversals (at_least_n_sem F n)

⟦at least n⟧ satisfies CONSERV ∧ Mon↑.

source

theorem Semantics.Quantification.Quantifier.at_most_n_satisfiesUniversals {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n : ℕ) :

SatisfiesUniversals (at_most_n_sem F n)

⟦at most n⟧ satisfies CONSERV ∧ Mon↓.

source

theorem Semantics.Quantification.Quantifier.exactly_n_conservative_quantity {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n : ℕ) :

Core.Quantification.Conservative (exactly_n_sem F n)

⟦exactly n⟧ satisfies CONSERV (but not MON for n ≥ 1).

source

theorem Semantics.Quantification.Quantifier.all_but_0_eq_every {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

all_but_n_sem F 0 = every_sem F

⟦all but 0⟧ = ⟦every⟧: zero exceptions means universal.

source

theorem Semantics.Quantification.Quantifier.all_but_n_conservative {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n : ℕ) :

Core.Quantification.Conservative (all_but_n_sem F n)

⟦all but n⟧ is conservative.

source

theorem Semantics.Quantification.Quantifier.all_but_n_quantity {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n : ℕ) :

Quantity (all_but_n_sem F n)

⟦all but n⟧ satisfies Quantity.

source

theorem Semantics.Quantification.Quantifier.between_n_m_conservative {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n k : ℕ) :

Core.Quantification.Conservative (between_n_m_sem F n k)

⟦between n and k⟧ is conservative.

source

theorem Semantics.Quantification.Quantifier.between_n_m_quantity {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] (n k : ℕ) :

Quantity (between_n_m_sem F n k)

⟦between n and k⟧ satisfies Quantity.

source

def Semantics.Quantification.Quantifier.Proportional {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] (q : Core.Quantification.GQ F.Entity) :

Prop

Proportional: Q's truth value depends only on the ratio |A∩B|/|A\B|.

Equations

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

Instances For

source

theorem Semantics.Quantification.Quantifier.most_proportional {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Proportional (most_sem F)

⟦most⟧ is proportional.

source

theorem Semantics.Quantification.Quantifier.few_proportional {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Proportional (few_sem F)

⟦few⟧ is proportional.

source

theorem Semantics.Quantification.Quantifier.half_proportional {F : Core.Logic.Intensional.Frame} [Fintype F.Entity] [DecidableEq F.Entity] :

Proportional (half_sem F)

Generalized-Quantifier-Theoretic (GQT) meaning operator #

A parametric truth-conditional GQT operator: given a monotonicity direction and a numerical threshold, gqtMeaning returns the literal GQT denotation as a Bool over a finite "intersection-count" world. Used by quantity-implicature studies (e.g., van Tiel et al. 2021) that plug per-paper threshold parameters into the same GQT machinery.

source

def Semantics.Quantification.Quantifier.gqtMeaning (n : ℕ) (mono : Theories.Semantics.Quantification.Lexicon.Monotonicity) (θ : ℕ) (t : Fin (n + 1)) :

Bool

GQT meaning: at threshold θ, with monotonicity mono, in a domain of size n, is the count t true?

Equations

Semantics.Quantification.Quantifier.gqtMeaning n Theories.Semantics.Quantification.Lexicon.Monotonicity.increasing θ t = decide (↑t ≥ θ)
Semantics.Quantification.Quantifier.gqtMeaning n Theories.Semantics.Quantification.Lexicon.Monotonicity.decreasing θ t = decide (↑t ≤ θ)
Semantics.Quantification.Quantifier.gqtMeaning n Theories.Semantics.Quantification.Lexicon.Monotonicity.nonMonotone θ t = (↑t == θ)

Instances For

source

def Semantics.Quantification.Quantifier.gqtMeaningRat (n : ℕ) (mono : Theories.Semantics.Quantification.Lexicon.Monotonicity) (θ : ℕ) (t : Fin (n + 1)) :

ℚ

Rational version of gqtMeaning (1 if true, 0 if false).

Equations

Semantics.Quantification.Quantifier.gqtMeaningRat n mono θ t = if Semantics.Quantification.Quantifier.gqtMeaning n mono θ t = true then 1 else 0

Instances For

source

theorem Semantics.Quantification.Quantifier.gqtMeaningRat_nonneg (n : ℕ) (mono : Theories.Semantics.Quantification.Lexicon.Monotonicity) (θ : ℕ) (t : Fin (n + 1)) :

0 ≤ gqtMeaningRat n mono θ t

Open conjectures (van de Pol et al. 2023) #

TODO: Quantifiers satisfying the B&C semantic universals (conservativity, quantity, monotonicity) have strictly lower complexity (Lempel-Ziv on truth-table representations, or MDL in a language-of-thought grammar) than violators.

TODO: Among the three universals, monotonicity is the strongest predictor of complexity reduction; conservativity is intermediate; quantity shows a weaker but robust effect.

Both were previously stubbed in the deleted Core/Conjectures.lean. Formal content depends on choosing canonical complexity measures (LZ over Boolean truth tables; MDL over LoT grammars) and connecting them to the existing SatisfiesUniversals predicate.

Documentation

Linglib.Theories.Semantics.Quantification.Quantifier

Generalized Quantifiers #

Semantic Universals #

Organization #

Generalized-Quantifier-Theoretic (GQT) meaning operator #

Open conjectures (van de Pol et al. 2023) #