Concrete propositional generalized quantifiers

This file defines the generalized quantifiers every, some, no and the Russellian the, whose truth conditions need no counting, and proves their conservativity, monotonicity, symmetry, duality and square-of-opposition properties. The properties checked are Barwise and Cooper's universals of conservativity and scope monotonicity, Keenan and Stavi's Boolean structure, and Peters and Westerståhl's left monotonicity and smoothness. The counting quantifiers such as most and few are in Quantification/Counting.lean.

Main definitions

• every, GQ.some, no, the: the propositional denotations.
• SatisfiesUniversals: conservativity together with monotonicity in the scope.
• square: the square of opposition of every, no, some and not every at a restrictor.

Main results

• every_eq_sInf_image, some_eq_sSup_image, no_eq_compl_sSup_image: the three determiners are the infimum, the supremum and the complement of the supremum of the scope over the restrictor.
• every_iff_le, no_iff_disjoint: the universal determiners are the pointwise order and disjointness on predicates.
• square_relations: with a non-empty restrictor the four stand in all six relations of the square, so its cells (Aristotelian.Square.cell) divide the scopes into those covering all of the restrictor, some but not all of it, and none of it.

References

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

Denotations

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

The universal determiner is λR λS. ∀x. R(x) → S(x).

Equations

• Quantifier.GQ.every R S = ∀ (x : α), R x → S x

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

The existential determiner is λR λS. ∃x. R(x) ∧ S(x).

Equations

• Quantifier.GQ.some R S = ∃ (x : α), R x ∧ S x

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

The negative determiner is λR λS. ∀x. R(x) → ¬S(x).

Equations

• Quantifier.GQ.no R S = ∀ (x : α), R x → ¬S x

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

The singular definite of [Rus05] in Montagovian form, λR λS. ∃x. ∀y. (R(y) ↔ y = x) ∧ S(x).

Equations

• Quantifier.GQ.the R S = ∃ (x : α), (∀ (y : α), R y ↔ y = x) ∧ S x

theorem Quantifier.GQ.the_iff {α : Type u_1} (R S : α → Prop) : the R S ↔ (∃! x : α, R x) ∧ ∀ (x : α), R x → S x

The definite asserts a unique restrictor element and applies the scope to it.

The order on predicates

theorem Quantifier.GQ.every_iff_le {α : Type u_1} {R S : α → Prop} : every R S ↔ R ≤ S

Every is the pointwise order on predicates, the standard formulation R ⊆ S.

theorem Quantifier.GQ.no_iff_le_compl {α : Type u_1} {R S : α → Prop} : no R S ↔ R ≤ Sᶜ

No is inclusion in the complement.

theorem Quantifier.GQ.no_iff_disjoint {α : Type u_1} {R S : α → Prop} : no R S ↔ Disjoint R S

No is disjointness of restrictor and scope.

@[instance_reducible]

instance Quantifier.GQ.instDecidableEvery {α : Type u_1} [Fintype α] {R S : α → Prop} [DecidablePred R] [DecidablePred S] : Decidable (every R S)

Equations

• Quantifier.GQ.instDecidableEvery = { decide := decide (∀ a ∈ Finset.univ, (fun (x : α) => R x → S x) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Quantifier.GQ.instDecidableSome {α : Type u_1} [Fintype α] {R S : α → Prop} [DecidablePred R] [DecidablePred S] : Decidable (GQ.some R S)

Equations

• Quantifier.GQ.instDecidableSome = { decide := decide (∃ a ∈ Finset.univ, (fun (x : α) => R x ∧ S x) a), reflects_decide := ⋯ }

@[instance_reducible]

instance Quantifier.GQ.instDecidableNo {α : Type u_1} [Fintype α] {R S : α → Prop} [DecidablePred R] [DecidablePred S] : Decidable (no R S)

Equations

• Quantifier.GQ.instDecidableNo = { decide := decide (∀ a ∈ Finset.univ, (fun (x : α) => R x → ¬S x) a), reflects_decide := ⋯ }

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

A quantifier satisfies Barwise and Cooper's semantic universals when it is conservative and either monotone or antitone in its scope.

Equations

• q.SatisfiesUniversals = (q.Conservative ∧ (q.ScopeMonotone ∨ q.ScopeAntitone))

Infima and suprema

At a restrictor R, every R S is the infimum of the values the scope takes on R, GQ.some R S their supremum, and no R S the complement of their supremum, so the three determiners are conjunction, disjunction and negative coordination over the restrictor.

theorem Quantifier.GQ.every_eq_sInf_image {α : Type u_1} (R S : α → Prop) : every R S = sInf (S '' {x : α | R x})

theorem Quantifier.GQ.some_eq_sSup_image {α : Type u_1} (R S : α → Prop) : GQ.some R S = sSup (S '' {x : α | R x})

theorem Quantifier.GQ.no_eq_compl_sSup_image {α : Type u_1} (R S : α → Prop) : no R S = (sSup (S '' {x : α | R x}))ᶜ

Conservativity

theorem Quantifier.GQ.conservative_every {α : Type u_1} : every.Conservative

theorem Quantifier.GQ.conservative_some {α : Type u_1} : GQ.some.Conservative

theorem Quantifier.GQ.conservative_no {α : Type u_1} : no.Conservative

Quantity invariance

theorem Quantifier.GQ.quantityInvariant_every {α : Type u_1} : every.QuantityInvariant

every is quantity invariant, since a bijection preserves ∀.

Scope monotonicity

theorem Quantifier.GQ.scopeMonotone_every {α : Type u_1} : every.ScopeMonotone

theorem Quantifier.GQ.scopeMonotone_some {α : Type u_1} : GQ.some.ScopeMonotone

theorem Quantifier.GQ.scopeAntitone_no {α : Type u_1} : no.ScopeAntitone

theorem Quantifier.GQ.scopeMonotone_the {α : Type u_1} : the.ScopeMonotone

theorem Quantifier.GQ.not_scopeAntitone_some {α : Type u_1} [Nonempty α] : ¬GQ.some.ScopeAntitone

On a nonempty domain some is not scope antitone, since some ⊤ ⊤ holds and some ⊤ ⊥ fails.

theorem Quantifier.GQ.not_scopeAntitone_every {α : Type u_1} [Nonempty α] : ¬every.ScopeAntitone

On a nonempty domain every is not scope antitone, since every ⊤ ⊤ holds and every ⊤ ⊥ fails.

theorem Quantifier.GQ.monotone_every {α : Type u_1} (R : α → Prop) : Monotone (every R)

every R is a monotone quantifier.

theorem Quantifier.GQ.monotone_some {α : Type u_1} (R : α → Prop) : Monotone (GQ.some R)

some R is a monotone quantifier.

theorem Quantifier.GQ.antitone_no {α : Type u_1} (R : α → Prop) : Antitone (no R)

no R is an antitone quantifier.

Symmetry (P&W Ch.6)

instance Quantifier.GQ.symm_some {α : Type u_1} : Std.Symm GQ.some

instance Quantifier.GQ.symm_no {α : Type u_1} : Std.Symm no

Intersectivity (CONSERV + SYMM bridge)

theorem Quantifier.GQ.intersectionCondition_some {α : Type u_1} : GQ.some.IntersectionCondition

theorem Quantifier.GQ.intersectionCondition_no {α : Type u_1} : no.IntersectionCondition

Left/right anti-additivity (P&W §5.8)

theorem Quantifier.GQ.leftAntiAdditive_every {α : Type u_1} : every.LeftAntiAdditive

theorem Quantifier.GQ.leftAntiAdditive_no {α : Type u_1} : no.LeftAntiAdditive

theorem Quantifier.GQ.rightAntiAdditive_no {α : Type u_1} : no.RightAntiAdditive

Duality square (B&C §4.11)

theorem Quantifier.GQ.innerNeg_every {α : Type u_1} : every.innerNeg = no

Inner negation maps every to no, since every ... not is no.

theorem Quantifier.GQ.dual_every {α : Type u_1} : every.dual = GQ.some

The dual of every is some.

theorem Quantifier.GQ.compl_some {α : Type u_1} : GQ.someᶜ = no

The outer negation of some is no, since negating existence gives universal negation.

Positive/negative strong (P&W Ch.6)

theorem Quantifier.GQ.positiveStrong_every {α : Type u_1} : every.PositiveStrong

theorem Quantifier.GQ.no_negative_strong_nonempty {α : Type u_1} (R : α → Prop) (hR : ∃ (x : α), R x) : ¬no R R

(no : GQ α) is negative strong on non-empty restrictors, no(A,A) being false for every non-empty A.

K&S existential det classification (§3.3, G3)

theorem Quantifier.GQ.existential_some {α : Type u_1} : GQ.some.Existential

theorem Quantifier.GQ.existential_no {α : Type u_1} : no.Existential

Relational properties ([vB84])

instance Quantifier.GQ.isTrans_every {α : Type u_1} : IsTrans (α → Prop) every

instance Quantifier.GQ.antisymm_every {α : Type u_1} : Std.Antisymm every

theorem Quantifier.GQ.quasiReflexive_some {α : Type u_1} : GQ.some.QuasiReflexive

theorem Quantifier.GQ.quasiUniversal_no {α : Type u_1} : no.QuasiUniversal

Double monotonicity classification ([vB84] §4.2)

theorem Quantifier.GQ.restrictorAntitone_every {α : Type u_1} : every.RestrictorAntitone

(every : GQ α) is restrictor-↓ (anti-persistent), by Zwarts's bridge from reflexivity, transitivity and conservativity to ↓MON.

theorem Quantifier.GQ.restrictorMonotone_some {α : Type u_1} : GQ.some.RestrictorMonotone

theorem Quantifier.GQ.restrictorAntitone_no {α : Type u_1} : no.RestrictorAntitone

theorem Quantifier.GQ.doubleMono_every {α : Type u_1} : every.RestrictorAntitone ∧ every.ScopeMonotone

theorem Quantifier.GQ.doubleMono_some {α : Type u_1} : GQ.some.RestrictorMonotone ∧ GQ.some.ScopeMonotone

theorem Quantifier.GQ.doubleMono_no {α : Type u_1} : no.RestrictorAntitone ∧ no.ScopeAntitone

theorem Quantifier.GQ.doubleMono_compl_every {α : Type u_1} : everyᶜ.RestrictorMonotone ∧ everyᶜ.ScopeAntitone

theorem Quantifier.GQ.scopeIntersective_every {α : Type u_1} : every.ScopeIntersective

Every is scope-intersective, and so filtrating.

theorem Quantifier.GQ.filtrating_every {α : Type u_1} : every.Filtrating

Aristotelian square of opposition

At a restrictor R, the denotations every R, no R, GQ.some R and everyᶜ R are the corners of a square in the Boolean algebra (α → Prop) → Prop. Outer negation is the Boolean complement, so the diagonals are contradictory at every restrictor. Contrariety, and with it the subalternations and subcontrariety, needs existential import: at an empty restrictor every and no both hold vacuously (a_e_contrary), and square_relations assumes a non-empty one.

def Quantifier.GQ.square {α : Type u_1} (R : α → Prop) : Aristotelian.Square ((α → Prop) → Prop)

At a restrictor R the four determiners form a square of opposition.

Equations

• Quantifier.GQ.square R = { A := Quantifier.GQ.every R, E := Quantifier.GQ.no R, I := Quantifier.GQ.some R, O := Quantifier.GQ.everyᶜ R }

theorem Quantifier.GQ.every_contradicts_notEvery {α : Type u_1} (R S : α → Prop) : every R S ↔ ¬everyᶜ R S

The A-form and the O-form are contradictories.

theorem Quantifier.GQ.no_contradicts_some {α : Type u_1} (R S : α → Prop) : no R S ↔ ¬GQ.some R S

The E-form and the I-form are contradictories.

theorem Quantifier.GQ.a_e_contrary {α : Type u_1} (R S : α → Prop) : every R S → no R S → ∀ (x : α), ¬R x

The A-form and the E-form both hold only when the restrictor is empty.

theorem Quantifier.GQ.square_relations {α : Type u_1} {R : α → Prop} (hR : ∃ (x : α), R x) : Aristotelian.SquareRelations (square R)

With a non-empty restrictor the four determiners stand in all six relations of the square.

theorem Quantifier.GQ.subalternation_a_i {α : Type u_1} (R S : α → Prop) (hR : ∃ (x : α), R x) : every R S → GQ.some R S

The A-form entails the I-form when the restrictor is nonempty.

Basic left monotonicities ([PW06] §5.5)

theorem Quantifier.GQ.upSE_some {α : Type u_1} : GQ.some.UpSEMon

theorem Quantifier.GQ.upSW_some {α : Type u_1} : GQ.some.UpSWMon

theorem Quantifier.GQ.downNW_every {α : Type u_1} : every.DownNWMon

theorem Quantifier.GQ.downNE_every {α : Type u_1} : every.DownNEMon

theorem Quantifier.GQ.downNW_no {α : Type u_1} : no.DownNWMon

theorem Quantifier.GQ.downNE_no {α : Type u_1} : no.DownNEMon

Smooth quantifiers ([PW06] §5.6)

theorem Quantifier.GQ.downNE_some {α : Type u_1} : GQ.some.DownNEMon

(GQ.some : GQ α) is ↓_NE Mon (direct proof).

theorem Quantifier.GQ.smooth_some {α : Type u_1} : GQ.some.Smooth

theorem Quantifier.GQ.upSE_every {α : Type u_1} : every.UpSEMon

(every : GQ α) is ↑_SE Mon (direct proof).

theorem Quantifier.GQ.smooth_every {α : Type u_1} : every.Smooth

theorem Quantifier.GQ.coSmooth_no {α : Type u_1} : no.CoSmooth

Satisfies universals: B&C's CONS + MON ([BC81]; used as a

learnability/complexity target by [vdPLvM+23])

theorem Quantifier.GQ.satisfiesUniversals_some {α : Type u_1} : GQ.some.SatisfiesUniversals

theorem Quantifier.GQ.satisfiesUniversals_every {α : Type u_1} : every.SatisfiesUniversals

theorem Quantifier.GQ.satisfiesUniversals_no {α : Type u_1} : no.SatisfiesUniversals