Counting generalized quantifiers

The counting quantifiers most, few, half, both, neither, at least n, at most n, exactly n, all but n and between n and k hold of A and B according to |A \ B| and |A ∩ B| alone, so each is the quantifier of a set of points on van Benthem's tree of numbers. Defined that way they are conservative and permutation invariant by construction, and their monotonicity, smoothness and proportionality are read off the tree. Sizes are Set.ncard, which asks for no decidability. On a finite type with decidable arguments each quantifier is decidable through the Finset count of each size, so a concrete case closes by decide. A quantifier restricted to a finite set s of individuals is the quantifier with restrictor x ∈ s ∧ A x.

Main definitions

• Quantifier.NumberTree.most, Quantifier.NumberTree.atLeast, …: the trees of the counting quantifiers, with Quantifier.NumberTree.threshold for a proportion of the restrictor.
• Quantifier.GQ.most, Quantifier.GQ.atLeast, …: their quantifiers.
• Quantifier.GQ.Proportional: dependence on the ratio of |A ∩ B| to |A \ B|.

Main results

• Quantifier.GQ.smooth_most, Quantifier.GQ.proportional_most: most is smooth and proportional.
• Quantifier.NumberTree.thresholdGt_one_two: more than half is most.
• Quantifier.GQ.not_existential_most, Quantifier.GQ.not_monotone_half: most is not existential, and half is monotone in its scope in neither direction.

References

• [BC81]
• [KS86]
• [PW06]
• [vB84]
• [vdPLvM+23]

The trees of the counting quantifiers

def Quantifier.NumberTree.most : NumberTree

Most holds when more of A lies inside B than outside it.

Equations

• Quantifier.NumberTree.most a b = (a < b)

def Quantifier.NumberTree.few : NumberTree

Few holds when less of A lies inside B than outside it.

Equations

• Quantifier.NumberTree.few a b = (b < a)

def Quantifier.NumberTree.half : NumberTree

Half holds when as much of A lies inside B as outside it.

Equations

• Quantifier.NumberTree.half a b = (a = b)

def Quantifier.NumberTree.both : NumberTree

Both holds when A has two members, both in B.

Equations

• Quantifier.NumberTree.both a b = (a = 0 ∧ b = 2)

def Quantifier.NumberTree.neither : NumberTree

Neither holds when A has two members, neither in B.

Equations

• Quantifier.NumberTree.neither a b = (a = 2 ∧ b = 0)

def Quantifier.NumberTree.atLeast (n : ℕ) : NumberTree

At least n holds when at least n members of A lie in B.

Equations

• Quantifier.NumberTree.atLeast n x✝ b = (n ≤ b)

def Quantifier.NumberTree.atMost (n : ℕ) : NumberTree

At most n holds when at most n members of A lie in B.

Equations

• Quantifier.NumberTree.atMost n x✝ b = (b ≤ n)

def Quantifier.NumberTree.exactly (n : ℕ) : NumberTree

Exactly n holds when exactly n members of A lie in B.

Equations

• Quantifier.NumberTree.exactly n x✝ b = (b = n)

def Quantifier.NumberTree.allBut (n : ℕ) : NumberTree

All but n holds when exactly n members of A lie outside B.

Equations

• Quantifier.NumberTree.allBut n a x✝ = (a = n)

def Quantifier.NumberTree.between (n k : ℕ) : NumberTree

Between n and k holds when between n and k members of A lie in B.

Equations

• Quantifier.NumberTree.between n k x✝ b = (n ≤ b ∧ b ≤ k)

def Quantifier.NumberTree.threshold (n d : ℕ) : NumberTree

The threshold n / d holds when at least that proportion of A lies in B.

Equations

• Quantifier.NumberTree.threshold n d = Quantifier.NumberTree.ofSizes fun (x p : ℕ) => n * p ≤ d * x

def Quantifier.NumberTree.thresholdGt (n d : ℕ) : NumberTree

The strict threshold n / d holds when more than that proportion of A lies in B.

Equations

• Quantifier.NumberTree.thresholdGt n d = Quantifier.NumberTree.ofSizes fun (x p : ℕ) => n * p < d * x

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatMost : DecidableRel NumberTree.most

Equations

• Quantifier.NumberTree.instDecidableRelNatMost a b = a.decLt b

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatFew : DecidableRel NumberTree.few

Equations

• Quantifier.NumberTree.instDecidableRelNatFew a b = b.decLt a

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatHalf : DecidableRel NumberTree.half

Equations

• Quantifier.NumberTree.instDecidableRelNatHalf a b = a.decEq b

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatBoth : DecidableRel NumberTree.both

Equations

• Quantifier.NumberTree.instDecidableRelNatBoth a b = { decide := decide (a = 0) && decide (b = 2), reflects_decide := ⋯ }

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatNeither : DecidableRel NumberTree.neither

Equations

• Quantifier.NumberTree.instDecidableRelNatNeither a b = { decide := decide (a = 2) && decide (b = 0), reflects_decide := ⋯ }

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatAtLeast (n : ℕ) : DecidableRel (NumberTree.atLeast n)

Equations

• Quantifier.NumberTree.instDecidableRelNatAtLeast n x✝ b = n.decLe b

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatAtMost (n : ℕ) : DecidableRel (NumberTree.atMost n)

Equations

• Quantifier.NumberTree.instDecidableRelNatAtMost n x✝ b = b.decLe n

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatExactly (n : ℕ) : DecidableRel (NumberTree.exactly n)

Equations

• Quantifier.NumberTree.instDecidableRelNatExactly n x✝ b = b.decEq n

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatAllBut (n : ℕ) : DecidableRel (NumberTree.allBut n)

Equations

• Quantifier.NumberTree.instDecidableRelNatAllBut n a x✝ = a.decEq n

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatBetween (n k : ℕ) : DecidableRel (NumberTree.between n k)

Equations

• Quantifier.NumberTree.instDecidableRelNatBetween n k x✝ b = { decide := decide (n ≤ b) && decide (b ≤ k), reflects_decide := ⋯ }

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatThreshold (n d : ℕ) : DecidableRel (threshold n d)

Equations

• Quantifier.NumberTree.instDecidableRelNatThreshold n d a b = { decide := (n * (a + b)).ble (d * b), reflects_decide := ⋯ }

@[instance_reducible]

instance Quantifier.NumberTree.instDecidableRelNatThresholdGt (n d : ℕ) : DecidableRel (thresholdGt n d)

Equations

• Quantifier.NumberTree.instDecidableRelNatThresholdGt n d a b = { decide := (n * (a + b)).succ.ble (d * b), reflects_decide := ⋯ }

theorem Quantifier.NumberTree.innerNeg_most : NumberTree.most.innerNeg = NumberTree.few

theorem Quantifier.NumberTree.innerNeg_both : NumberTree.both.innerNeg = NumberTree.neither

theorem Quantifier.NumberTree.compl_atLeast_succ (n : ℕ) : (NumberTree.atLeast (n + 1))ᶜ = NumberTree.atMost n

theorem Quantifier.NumberTree.atLeast_inf_atMost (n : ℕ) : NumberTree.atLeast n ⊓ NumberTree.atMost n = NumberTree.exactly n

theorem Quantifier.NumberTree.thresholdGt_one_two : thresholdGt 1 2 = NumberTree.most

More than half is most.

theorem Quantifier.NumberTree.scopeMonotone_most : NumberTree.most.ScopeMonotone

theorem Quantifier.NumberTree.scopeAntitone_few : NumberTree.few.ScopeAntitone

theorem Quantifier.NumberTree.scopeMonotone_atLeast (n : ℕ) : (NumberTree.atLeast n).ScopeMonotone

theorem Quantifier.NumberTree.scopeAntitone_atMost (n : ℕ) : (NumberTree.atMost n).ScopeAntitone

theorem Quantifier.NumberTree.scopeMonotone_threshold (n d : ℕ) : (threshold n d).ScopeMonotone

Proportionality

def Quantifier.NumberTree.Proportional (q : NumberTree) : Prop

A tree is proportional when on nonempty rows it depends only on the ratio of b to a.

Equations

• q.Proportional = ∀ (a b a' b' : ℕ), 0 < a + b → 0 < a' + b' → b * a' = b' * a → (q a b ↔ q a' b')

theorem Quantifier.NumberTree.Proportional.innerNeg {q : NumberTree} (h : q.Proportional) : q.innerNeg.Proportional

theorem Quantifier.NumberTree.proportional_most : NumberTree.most.Proportional

theorem Quantifier.NumberTree.proportional_few : NumberTree.few.Proportional

theorem Quantifier.NumberTree.proportional_half : NumberTree.half.Proportional

The counting quantifiers

def Quantifier.GQ.most {α : Type u_1} : GQ α

Most A are B when more of the A are B than are not.

Equations

• Quantifier.GQ.most = Quantifier.NumberTree.most.toGQ

def Quantifier.GQ.few {α : Type u_1} : GQ α

Few A are B when fewer of the A are B than are not, the inner negation of most.

Equations

• Quantifier.GQ.few = Quantifier.NumberTree.few.toGQ

def Quantifier.GQ.half {α : Type u_1} : GQ α

Half the A are B when as many of the A are B as are not.

Equations

• Quantifier.GQ.half = Quantifier.NumberTree.half.toGQ

def Quantifier.GQ.both {α : Type u_1} : GQ α

Both is every on a restrictor of two, Keenan and Stavi's each of the two.

Equations

• Quantifier.GQ.both = Quantifier.NumberTree.both.toGQ

def Quantifier.GQ.neither {α : Type u_1} : GQ α

Neither is no on a restrictor of two, Keenan and Stavi's not one of the two.

Equations

• Quantifier.GQ.neither = Quantifier.NumberTree.neither.toGQ

def Quantifier.GQ.atLeast {α : Type u_1} (n : ℕ) : GQ α

At least n A are B when n ≤ |A ∩ B|.

Equations

• Quantifier.GQ.atLeast n = (Quantifier.NumberTree.atLeast n).toGQ

def Quantifier.GQ.atMost {α : Type u_1} (n : ℕ) : GQ α

At most n A are B when |A ∩ B| ≤ n.

Equations

• Quantifier.GQ.atMost n = (Quantifier.NumberTree.atMost n).toGQ

def Quantifier.GQ.exactly {α : Type u_1} (n : ℕ) : GQ α

Exactly n A are B when |A ∩ B| = n.

Equations

• Quantifier.GQ.exactly n = (Quantifier.NumberTree.exactly n).toGQ

def Quantifier.GQ.allBut {α : Type u_1} (n : ℕ) : GQ α

All but n A are B when |A \ B| = n.

Equations

• Quantifier.GQ.allBut n = (Quantifier.NumberTree.allBut n).toGQ

def Quantifier.GQ.between {α : Type u_1} (n k : ℕ) : GQ α

Between n and k A are B when n ≤ |A ∩ B| ≤ k.

Equations

• Quantifier.GQ.between n k = (Quantifier.NumberTree.between n k).toGQ

@[instance_reducible]

instance Quantifier.GQ.instDecidableMost {α : Type u_1} [Fintype α] (A B : α → Prop) [DecidablePred A] [DecidablePred B] : Decidable (most A B)

Equations

• Quantifier.GQ.instDecidableMost A B = Quantifier.NumberTree.toGQ.decidable Quantifier.NumberTree.most A B

@[instance_reducible]

instance Quantifier.GQ.instDecidableFew {α : Type u_1} [Fintype α] (A B : α → Prop) [DecidablePred A] [DecidablePred B] : Decidable (few A B)

Equations

• Quantifier.GQ.instDecidableFew A B = Quantifier.NumberTree.toGQ.decidable Quantifier.NumberTree.few A B

@[instance_reducible]

instance Quantifier.GQ.instDecidableHalf {α : Type u_1} [Fintype α] (A B : α → Prop) [DecidablePred A] [DecidablePred B] : Decidable (half A B)

Equations

• Quantifier.GQ.instDecidableHalf A B = Quantifier.NumberTree.toGQ.decidable Quantifier.NumberTree.half A B

@[instance_reducible]

instance Quantifier.GQ.instDecidableBoth {α : Type u_1} [Fintype α] (A B : α → Prop) [DecidablePred A] [DecidablePred B] : Decidable (both A B)

Equations

• Quantifier.GQ.instDecidableBoth A B = Quantifier.NumberTree.toGQ.decidable Quantifier.NumberTree.both A B

@[instance_reducible]

instance Quantifier.GQ.instDecidableNeither {α : Type u_1} [Fintype α] (A B : α → Prop) [DecidablePred A] [DecidablePred B] : Decidable (neither A B)

Equations

• Quantifier.GQ.instDecidableNeither A B = Quantifier.NumberTree.toGQ.decidable Quantifier.NumberTree.neither A B

@[instance_reducible]

instance Quantifier.GQ.instDecidableAtLeast {α : Type u_1} [Fintype α] (A B : α → Prop) [DecidablePred A] [DecidablePred B] (n : ℕ) : Decidable (atLeast n A B)

Equations

• Quantifier.GQ.instDecidableAtLeast A B n = Quantifier.NumberTree.toGQ.decidable (Quantifier.NumberTree.atLeast n) A B

@[instance_reducible]

instance Quantifier.GQ.instDecidableAtMost {α : Type u_1} [Fintype α] (A B : α → Prop) [DecidablePred A] [DecidablePred B] (n : ℕ) : Decidable (atMost n A B)

Equations

• Quantifier.GQ.instDecidableAtMost A B n = Quantifier.NumberTree.toGQ.decidable (Quantifier.NumberTree.atMost n) A B

@[instance_reducible]

instance Quantifier.GQ.instDecidableExactly {α : Type u_1} [Fintype α] (A B : α → Prop) [DecidablePred A] [DecidablePred B] (n : ℕ) : Decidable (exactly n A B)

Equations

• Quantifier.GQ.instDecidableExactly A B n = Quantifier.NumberTree.toGQ.decidable (Quantifier.NumberTree.exactly n) A B

@[instance_reducible]

instance Quantifier.GQ.instDecidableAllBut {α : Type u_1} [Fintype α] (A B : α → Prop) [DecidablePred A] [DecidablePred B] (n : ℕ) : Decidable (allBut n A B)

Equations

• Quantifier.GQ.instDecidableAllBut A B n = Quantifier.NumberTree.toGQ.decidable (Quantifier.NumberTree.allBut n) A B

@[instance_reducible]

instance Quantifier.GQ.instDecidableBetween {α : Type u_1} [Fintype α] (A B : α → Prop) [DecidablePred A] [DecidablePred B] (n k : ℕ) : Decidable (between n k A B)

Equations

• Quantifier.GQ.instDecidableBetween A B n k = Quantifier.NumberTree.toGQ.decidable (Quantifier.NumberTree.between n k) A B

theorem Quantifier.GQ.most_apply {α : Type u_1} {A B : α → Prop} : most A B ↔ {x : α | A x ∧ ¬B x}.ncard < {x : α | A x ∧ B x}.ncard

theorem Quantifier.GQ.few_apply {α : Type u_1} {A B : α → Prop} : few A B ↔ {x : α | A x ∧ B x}.ncard < {x : α | A x ∧ ¬B x}.ncard

theorem Quantifier.GQ.half_apply {α : Type u_1} {A B : α → Prop} : half A B ↔ {x : α | A x ∧ ¬B x}.ncard = {x : α | A x ∧ B x}.ncard

theorem Quantifier.GQ.atLeast_apply {α : Type u_1} {A B : α → Prop} {n : ℕ} : atLeast n A B ↔ n ≤ {x : α | A x ∧ B x}.ncard

theorem Quantifier.GQ.atMost_apply {α : Type u_1} {A B : α → Prop} {n : ℕ} : atMost n A B ↔ {x : α | A x ∧ B x}.ncard ≤ n

theorem Quantifier.GQ.exactly_apply {α : Type u_1} {A B : α → Prop} {n : ℕ} : exactly n A B ↔ {x : α | A x ∧ B x}.ncard = n

theorem Quantifier.GQ.conservative_most {α : Type u_1} : most.Conservative

theorem Quantifier.GQ.conservative_atLeast {α : Type u_1} (n : ℕ) : (atLeast n).Conservative

theorem Quantifier.GQ.conservative_exactly {α : Type u_1} (n : ℕ) : (exactly n).Conservative

Identities

theorem Quantifier.GQ.atMost_eq_compl_atLeast_succ {α : Type u_1} (n : ℕ) : atMost n = (atLeast (n + 1))ᶜ

theorem Quantifier.GQ.exactly_eq_atLeast_inf_atMost {α : Type u_1} (n : ℕ) : exactly n = atLeast n ⊓ atMost n

theorem Quantifier.GQ.every_eq_toGQ_all {α : Type u_1} [Finite α] : every = NumberTree.all.toGQ

On a finite universe every is the quantifier of the tree's all.

theorem Quantifier.GQ.no_eq_toGQ_no {α : Type u_1} [Finite α] : no = NumberTree.no.toGQ

On a finite universe no is the quantifier of the tree's no.

theorem Quantifier.GQ.some_eq_atLeast_one {α : Type u_1} [Finite α] : GQ.some = atLeast 1

On a finite universe some is at least one.

theorem Quantifier.GQ.no_eq_atMost_zero {α : Type u_1} [Finite α] : no = atMost 0

theorem Quantifier.GQ.allBut_zero_eq_every {α : Type u_1} [Finite α] : allBut 0 = every

Monotonicity

theorem Quantifier.GQ.scopeMonotone_most {α : Type u_1} [Finite α] : most.ScopeMonotone

theorem Quantifier.GQ.scopeAntitone_few {α : Type u_1} [Finite α] : few.ScopeAntitone

theorem Quantifier.GQ.scopeMonotone_atLeast {α : Type u_1} [Finite α] (n : ℕ) : (atLeast n).ScopeMonotone

theorem Quantifier.GQ.scopeAntitone_atMost {α : Type u_1} [Finite α] (n : ℕ) : (atMost n).ScopeAntitone

theorem Quantifier.GQ.monotone_atLeast {α : Type u_1} [Finite α] (n : ℕ) (A : α → Prop) : Monotone (atLeast n A)

theorem Quantifier.GQ.antitone_atMost {α : Type u_1} [Finite α] (n : ℕ) (A : α → Prop) : Antitone (atMost n A)

theorem Quantifier.GQ.not_scopeAntitone_most {α : Type u_1} [Finite α] [Nonempty α] : ¬most.ScopeAntitone

On a nonempty finite universe most is not scope antitone, since most ⊤ ⊤ holds and most ⊤ ⊥ fails.

theorem Quantifier.GQ.restrictorMonotone_atLeast {α : Type u_1} [Finite α] (n : ℕ) : (atLeast n).RestrictorMonotone

theorem Quantifier.GQ.restrictorAntitone_atMost {α : Type u_1} [Finite α] (n : ℕ) : (atMost n).RestrictorAntitone

Smoothness

theorem Quantifier.GQ.downNE_most {α : Type u_1} [Finite α] : most.DownNEMon

theorem Quantifier.GQ.upSE_most {α : Type u_1} [Finite α] : most.UpSEMon

theorem Quantifier.GQ.smooth_most {α : Type u_1} [Finite α] : most.Smooth

theorem Quantifier.GQ.smooth_atLeast {α : Type u_1} [Finite α] (n : ℕ) : (atLeast n).Smooth

theorem Quantifier.GQ.coSmooth_atMost {α : Type u_1} [Finite α] (n : ℕ) : (atMost n).CoSmooth

Proportionality

def Quantifier.GQ.Proportional {α : Type u_1} (q : GQ α) : Prop

A quantifier is proportional when on nonempty restrictors its truth depends only on the ratio of |A ∩ B| to |A \ B|.

Equations

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

theorem Quantifier.NumberTree.Proportional.toGQ {α : Type u_1} {q : NumberTree} (h : q.Proportional) : q.toGQ.Proportional

The quantifier of a proportional tree is proportional.

theorem Quantifier.GQ.proportional_most {α : Type u_1} : most.Proportional

theorem Quantifier.GQ.proportional_few {α : Type u_1} : few.Proportional

theorem Quantifier.GQ.proportional_half {α : Type u_1} : half.Proportional

Counterexamples on small universes

The proportional quantifiers fail Existential, the condition for felicity in there-sentences, although Barwise and Cooper's Table II labels few and half weak: their truth depends on |A \ B|, not just on |A ∩ B|. Few already fails it on one individual, most and half on two.

theorem Quantifier.GQ.not_existential_most : ¬most.Existential

Most fails Existential, by A = ⊤ and B = {0} on two individuals.

theorem Quantifier.GQ.not_existential_few : ¬few.Existential

Few fails Existential, by A = ⊤ and B = ∅ on one individual.

theorem Quantifier.GQ.not_existential_half : ¬half.Existential

Half fails Existential, by A = ⊤ and B = {0} on two individuals.

theorem Quantifier.GQ.not_restrictorMonotone_most : ¬most.RestrictorMonotone

Most is not persistent: enlarging the restrictor from {0} to {0, 2} loses the majority for B = {0}.

theorem Quantifier.GQ.not_symm_most : ¬Std.Symm most

Most is not symmetric, by A = {0} and B = {0, 1}.

theorem Quantifier.GQ.not_scopeMonotone_half : ¬half.ScopeMonotone

Half is not scope monotone: with A = {0, 1}, half A {0} holds and half A A fails.

theorem Quantifier.GQ.not_scopeAntitone_half : ¬half.ScopeAntitone

Half is not scope antitone: with A = {0, 1}, half A {0} holds and half A ∅ fails.

theorem Quantifier.GQ.not_monotone_half : ¬half.ScopeMonotone ∧ ¬half.ScopeAntitone

Half is non-monotone in its scope, neither monotone nor antitone ([vdPLvM+23]).

theorem Quantifier.GQ.not_monotone_exactly {α : Type u_1} [Fintype α] {n : ℕ} (h : n < Fintype.card α) : ¬Monotone (exactly n fun (x : α) => True)

Over a domain of more than n individuals, exactly n is not monotone in its scope.

theorem Quantifier.GQ.not_antitone_exactly {α : Type u_1} [Fintype α] {n : ℕ} (hn : n ≠ 0) (h : n ≤ Fintype.card α) : ¬Antitone (exactly n fun (x : α) => True)

Over a domain of at least n individuals, n positive, exactly n is not antitone in its scope.

theorem Quantifier.GQ.both_fin2 : both (fun (x : Fin 2) => True) fun (x : Fin 2) => True

Both holds of a restrictor of two and fails of one of three.

theorem Quantifier.GQ.not_both_fin3 : ¬both (fun (x : Fin 3) => True) fun (x : Fin 3) => True

theorem Quantifier.GQ.most_singleton_iff {α : Type u_1} (j : α) (B : α → Prop) : most (fun (x : α) => x = j) B ↔ B j

On a singleton restrictor most is the scope's value at the singleton.

The families of the canonical denotations

Each canonical denotation given on every finite domain, the readings a lexicon entry draws on.

def Quantifier.GQ.Family.every : Family

Family.every is every on every finite domain.

Equations

• Quantifier.GQ.Family.every x✝¹ = Quantifier.GQ.every

def Quantifier.GQ.Family.some : Family

Family.some is GQ.some on every finite domain.

Equations

• Quantifier.GQ.Family.some x✝¹ = Quantifier.GQ.some

def Quantifier.GQ.Family.no : Family

Family.no is no on every finite domain.

Equations

• Quantifier.GQ.Family.no x✝¹ = Quantifier.GQ.no

def Quantifier.GQ.Family.most : Family

Family.most is most on every finite domain.

Equations

• Quantifier.GQ.Family.most x✝¹ = Quantifier.GQ.most

def Quantifier.GQ.Family.few : Family

Family.few is few on every finite domain.

Equations

• Quantifier.GQ.Family.few x✝¹ = Quantifier.GQ.few

def Quantifier.GQ.Family.half : Family

Family.half is half on every finite domain.

Equations

• Quantifier.GQ.Family.half x✝¹ = Quantifier.GQ.half

def Quantifier.GQ.Family.both : Family

Family.both is both on every finite domain.

Equations

• Quantifier.GQ.Family.both x✝¹ = Quantifier.GQ.both

def Quantifier.GQ.Family.neither : Family

Family.neither is neither on every finite domain.

Equations

• Quantifier.GQ.Family.neither x✝¹ = Quantifier.GQ.neither

def Quantifier.GQ.Family.atLeast (n : ℕ) : Family

Family.atLeast n is atLeast n on every finite domain.

Equations

• Quantifier.GQ.Family.atLeast n x✝¹ = Quantifier.GQ.atLeast n

def Quantifier.GQ.Family.exactly (n : ℕ) : Family

Family.exactly n is exactly n on every finite domain.

Equations

• Quantifier.GQ.Family.exactly n x✝¹ = Quantifier.GQ.exactly n

theorem Quantifier.GQ.Family.some_ne_every : some ≠ every

some and every are different families, since on an empty restrictor every holds and some fails.

theorem Quantifier.GQ.Family.some_ne_no : some ≠ no

some and no are different families, since on a one-element domain some ⊤ ⊤ holds and no ⊤ ⊤ fails.

@[simp]

theorem Quantifier.GQ.Family.compl_some : someᶜ = no

@[simp]

theorem Quantifier.GQ.Family.compl_no : noᶜ = some