Concrete propositional generalized quantifiers

[BC81] [KS86] [PW06]

The three propositional GQs every_sem, some_sem, no_sem and the property proofs that don't need Fintype. Counting GQs (most_sem, few_sem, etc.) and their proofs live in Quantification.Counting.

Main declarations

• every_sem, some_sem, no_sem — the three propositional GQ denotations.
• SatisfiesUniversals — B&C universals: conservativity + monotonicity in scope.
• Conservativity/monotonicity/symmetry/intersectivity/duality/etc. proofs.

Denotations

def Quantification.every_sem {α : Type u_1} : GQ α

⟦every⟧ = λR.λS. ∀x. R(x) → S(x).

Equations

• Quantification.every_sem R S = ∀ (x : α), R x → S x

def Quantification.some_sem {α : Type u_1} : GQ α

⟦some⟧ = λR.λS. ∃x. R(x) ∧ S(x).

Equations

• Quantification.some_sem R S = ∃ (x : α), R x ∧ S x

def Quantification.no_sem {α : Type u_1} : GQ α

⟦no⟧ = λR.λS. ∀x. R(x) → ¬S(x).

Equations

• Quantification.no_sem R S = ∀ (x : α), R x → ¬S x

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

B&C semantic universals ([BC81]): conservativity plus monotonicity in scope. Convenience conjunction of three Core predicates.

Equations

• Quantification.SatisfiesUniversals q = (Quantification.Conservative q ∧ (Quantification.ScopeUpwardMono q ∨ Quantification.ScopeDownwardMono q))

Bijection invariance

theorem Quantification.forall_bij_inv {α : Type u_1} (f : α → α) (hBij : Function.Bijective f) (P : α → Prop) : (∀ (x : α), P x) ↔ ∀ (x : α), P (f x)

∀ x, P x is invariant under bijective substitution.

theorem Quantification.exists_bij_inv {α : Type u_1} (f : α → α) (hBij : Function.Bijective f) (P : α → Prop) : (∃ (x : α), P x) ↔ ∃ (x : α), P (f x)

∃ x, P x is invariant under bijective substitution.

Conservativity

theorem Quantification.every_conservative {α : Type u_1} : Conservative every_sem

theorem Quantification.some_conservative {α : Type u_1} : Conservative some_sem

theorem Quantification.no_conservative {α : Type u_1} : Conservative no_sem

Scope monotonicity

theorem Quantification.every_scope_up {α : Type u_1} : ScopeUpwardMono every_sem

theorem Quantification.some_scope_up {α : Type u_1} : ScopeUpwardMono some_sem

theorem Quantification.no_scope_down {α : Type u_1} : ScopeDownwardMono no_sem

Symmetry (P&W Ch.6)

theorem Quantification.some_symmetric {α : Type u_1} : QSymmetric some_sem

theorem Quantification.no_symmetric {α : Type u_1} : QSymmetric no_sem

Intersectivity (CONSERV + SYMM bridge)

theorem Quantification.some_intersective {α : Type u_1} : IntersectionCondition some_sem

theorem Quantification.no_intersective {α : Type u_1} : IntersectionCondition no_sem

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

theorem Quantification.every_laa {α : Type u_1} : LeftAntiAdditive every_sem

theorem Quantification.no_laa {α : Type u_1} : LeftAntiAdditive no_sem

theorem Quantification.no_raa {α : Type u_1} : RightAntiAdditive no_sem

theorem Quantification.laa_characterization {α : Type u_1} : LeftAntiAdditive every_sem ∧ LeftAntiAdditive no_sem

[PW06] Prop 13: the only non-trivial CONSERV, EXT, and ISOM quantifiers satisfying LAA are every and no (and A = ∅).

Duality square (B&C §4.11)

theorem Quantification.innerNeg_every_eq_no {α : Type u_1} : innerNeg every_sem = no_sem

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

theorem Quantification.dualQ_every_eq_some {α : Type u_1} : dualQ every_sem = some_sem

The dual of every is some: Q̌(every) = some.

theorem Quantification.outerNeg_some_eq_no {α : Type u_1} : outerNeg some_sem = no_sem

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

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

theorem Quantification.every_positive_strong {α : Type u_1} : PositiveStrong every_sem

theorem Quantification.no_negative_strong_nonempty {α : Type u_1} (R : α → Prop) (hR : ∃ (x : α), R x) : ¬no_sem R R

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

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

theorem Quantification.some_existential {α : Type u_1} : Existential some_sem

theorem Quantification.no_existential {α : Type u_1} : Existential no_sem

Relational properties ([vB84])

theorem Quantification.every_transitive {α : Type u_1} : QTransitive every_sem

theorem Quantification.every_antisymmetric {α : Type u_1} : QAntisymmetric every_sem

theorem Quantification.some_quasi_reflexive {α : Type u_1} : QuasiReflexive some_sem

theorem Quantification.no_quasi_universal {α : Type u_1} : QuasiUniversal no_sem

Double monotonicity classification ([vB84] §4.2)

theorem Quantification.every_restrictor_down {α : Type u_1} : RestrictorDownwardMono every_sem

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

theorem Quantification.some_restrictor_up {α : Type u_1} : RestrictorUpwardMono some_sem

theorem Quantification.no_restrictor_down {α : Type u_1} : RestrictorDownwardMono no_sem

theorem Quantification.every_doubleMono {α : Type u_1} : RestrictorDownwardMono every_sem ∧ ScopeUpwardMono every_sem

theorem Quantification.some_doubleMono {α : Type u_1} : RestrictorUpwardMono some_sem ∧ ScopeUpwardMono some_sem

theorem Quantification.no_doubleMono {α : Type u_1} : RestrictorDownwardMono no_sem ∧ ScopeDownwardMono no_sem

theorem Quantification.notAll_doubleMono {α : Type u_1} : RestrictorUpwardMono (outerNeg every_sem) ∧ ScopeDownwardMono (outerNeg every_sem)

theorem Quantification.every_filtrating {α : Type u_1} : Filtrating every_sem

Aristotelian square of opposition

The four Aristotelian relations among GQ denotations (every_sem, some_sem, no_sem, outerNeg every_sem) at a fixed restrictor R, where the corners are elements of the Pi-instance Boolean algebra (α → Prop) → Prop.

The contradictory diagonals are placed on the Aristotelian hub by construction: since outerNeg = ᶜ (Defs.outerNeg), every quantifier is Aristotelian.IsContradictory to its outer negation — isContradictory_outerNeg, which is just isCompl_compl — and the A–O and E–I diagonals are instances. The pointwise ↔-form theorems (every_contradicts_notEvery, no_contradicts_some) are the unfolded readings.

Contrariety and subalternation are not hub relations: they hold only under existential import (non-empty restrictor) and are |R|-sensitive — at a singleton R, every/no are contradictory, not contrary — so the unconditional IsContrary/IsSubaltern do not apply. They stay as the conditional theorems (a_e_contrary, subalternation_a_i, …), the faithful Aristotelian-vs-Boolean existential-import treatment.

theorem Quantification.every_contradicts_notEvery {α : Type u_1} (R S : α → Prop) : every_sem R S ↔ ¬outerNeg every_sem R S

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

theorem Quantification.no_contradicts_some {α : Type u_1} (R S : α → Prop) : no_sem R S ↔ ¬some_sem R S

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

theorem Quantification.a_e_contrary {α : Type u_1} (R S : α → Prop) : every_sem R S → no_sem R S → ∀ (x : α), ¬R x

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

theorem Quantification.subalternation_a_i {α : Type u_1} (R S : α → Prop) (hR : ∃ (x : α), R x) : every_sem R S → some_sem R S

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

theorem Quantification.subalternation_e_o {α : Type u_1} (R S : α → Prop) (hR : ∃ (x : α), R x) : no_sem R S → outerNeg every_sem R S

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

theorem Quantification.subcontrariety_i_o {α : Type u_1} (R S : α → Prop) (hR : ∃ (x : α), R x) : some_sem R S ∨ outerNeg every_sem R S

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

theorem Quantification.isContradictory_outerNeg {α : Type u_1} (q : GQ α) (R : α → Prop) : Aristotelian.IsContradictory (q R) (outerNeg q R)

Every quantifier is Aristotelian.IsContradictory to its outer negation: the Boolean complement law isCompl_compl on the Pi-instance Boolean algebra (α → Prop) → Prop (where outerNeg = ᶜ). The square's contradictory diagonals are instances — this is the "single home" for the diagonals, by construction rather than re-derivation.

theorem Quantification.every_satisfies_isContradictory_pointwise {α : Type u_1} (R : α → Prop) : Aristotelian.IsContradictory (every_sem R) (outerNeg every_sem R)

A–O diagonal: every and not-every are contradictory.

theorem Quantification.no_satisfies_isContradictory_pointwise {α : Type u_1} (R : α → Prop) : Aristotelian.IsContradictory (no_sem R) (some_sem R)

E–I diagonal: no and some are contradictory, since some = ~no.

Basic left monotonicities ([PW06] §5.5)

theorem Quantification.some_upSE {α : Type u_1} : UpSEMon some_sem

theorem Quantification.some_upSW {α : Type u_1} : UpSWMon some_sem

theorem Quantification.every_downNW {α : Type u_1} : DownNWMon every_sem

theorem Quantification.every_downNE {α : Type u_1} : DownNEMon every_sem

theorem Quantification.no_downNW {α : Type u_1} : DownNWMon no_sem

theorem Quantification.no_downNE {α : Type u_1} : DownNEMon no_sem

Smooth quantifiers ([PW06] §5.6)

theorem Quantification.some_downNE {α : Type u_1} : DownNEMon some_sem

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

theorem Quantification.some_smooth {α : Type u_1} : Smooth some_sem

theorem Quantification.every_upSE_direct {α : Type u_1} : UpSEMon every_sem

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

theorem Quantification.every_smooth {α : Type u_1} : Smooth every_sem

theorem Quantification.no_coSmooth_partial {α : Type u_1} : DownNWMon no_sem ∧ DownNEMon no_sem

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

learnability/complexity target by [vdPLvM+23])

theorem Quantification.some_satisfiesUniversals {α : Type u_1} : SatisfiesUniversals some_sem

theorem Quantification.every_satisfiesUniversals {α : Type u_1} : SatisfiesUniversals every_sem

theorem Quantification.no_satisfiesUniversals {α : Type u_1} : SatisfiesUniversals no_sem