Generalized Quantifier Properties — Theorems #

@cite{barwise-cooper-1981} @cite{keenan-stavi-1986} @cite{peters-westerstahl-2006} @cite{van-benthem-1984} @cite{van-benthem-1986} @cite{icard-2012}

Theorems about GQ properties: duality, conservativity/symmetry/strength, left monotonicity and smoothness, Boolean closure, type ⟨1⟩ theorems, van Benthem characterization, and entailment-signature bridge.

source

theorem Core.Quantification.outerNeg_up_to_down {α : Type u_1} (q : GQ α) (h : ScopeUpwardMono q) :

ScopeDownwardMono (outerNeg q)

Outer negation reverses scope monotonicity: mon↑ → mon↓. B&C Theorem C9.

source

theorem Core.Quantification.outerNeg_down_to_up {α : Type u_1} (q : GQ α) (h : ScopeDownwardMono q) :

ScopeUpwardMono (outerNeg q)

Outer negation reverses scope monotonicity: mon↓ → mon↑. B&C Theorem C9.

source

theorem Core.Quantification.innerNeg_up_to_down {α : Type u_1} (q : GQ α) (h : ScopeUpwardMono q) :

ScopeDownwardMono (innerNeg q)

Inner negation reverses scope monotonicity: mon↑ → mon↓ (B&C §4.11).

source

theorem Core.Quantification.innerNeg_down_to_up {α : Type u_1} (q : GQ α) (h : ScopeDownwardMono q) :

ScopeUpwardMono (innerNeg q)

Inner negation reverses scope monotonicity: mon↓ → mon↑ (B&C §4.11).

source

theorem Core.Quantification.outerNeg_restrictorUp_to_down {α : Type u_1} (q : GQ α) (h : RestrictorUpwardMono q) :

RestrictorDownwardMono (outerNeg q)

Outer negation reverses restrictor monotonicity: mon↑ → mon↓.

source

theorem Core.Quantification.outerNeg_restrictorDown_to_up {α : Type u_1} (q : GQ α) (h : RestrictorDownwardMono q) :

RestrictorUpwardMono (outerNeg q)

Outer negation reverses restrictor monotonicity: mon↓ → mon↑.

source

theorem Core.Quantification.outerNeg_involution {α : Type u_1} (q : GQ α) :

outerNeg (outerNeg q) = q

Outer negation is involutive: ~~Q = Q. (Uses propositional extensionality.)

source

theorem Core.Quantification.innerNeg_involution {α : Type u_1} (q : GQ α) :

innerNeg (innerNeg q) = q

Inner negation is involutive: Q~~ = Q. (Uses propositional extensionality.)

source

theorem Core.Quantification.dualQ_involution {α : Type u_1} (q : GQ α) :

dualQ (dualQ q) = q

Dual is involutive: Q̌̌ = Q.

source

theorem Core.Quantification.quantityInvariant_outerNeg {α : Type u_1} (q : GQ α) (h : QuantityInvariant q) :

QuantityInvariant (outerNeg q)

Outer negation preserves QuantityInvariant: if Q is bijection-invariant, so is ~Q.

source

theorem Core.Quantification.quantityInvariant_innerNeg {α : Type u_1} (q : GQ α) (h : QuantityInvariant q) :

QuantityInvariant (innerNeg q)

Inner negation preserves QuantityInvariant: if Q is bijection-invariant, so is Q~.

source

theorem Core.Quantification.quantityInvariant_dualQ {α : Type u_1} (q : GQ α) (h : QuantityInvariant q) :

QuantityInvariant (dualQ q)

Dual preserves QuantityInvariant.

source

theorem Core.Quantification.quantityInvariant_gqMeet {α : Type u_1} (f g : GQ α) (hf : QuantityInvariant f) (hg : QuantityInvariant g) :

QuantityInvariant (gqMeet f g)

Meet preserves QuantityInvariant.

source

theorem Core.Quantification.intersection_conservative_symmetric {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hInt : IntersectionCondition q) :

QSymmetric q

Conservative + intersection condition → symmetric (B&C Theorem C5). Proof: by conservativity Q(A,B) = Q(A, A∩B) and Q(B,A) = Q(B, B∩A); both have the same restrictor∩scope = A∩B, so intersection condition equates them.

source

theorem Core.Quantification.co_property_mono {α : Type u_1} (q : GQ α) :

ScopeDownwardMono q ↔ ScopeUpwardMono (innerNeg q)

Scope-downward monotonicity is equivalent to scope-upward monotonicity of the inner negation (co-property characterization, P&W §3.2.4).

source

theorem Core.Quantification.conserv_symm_iff_int {α : Type u_1} (q : GQ α) (hCons : Conservative q) :

QSymmetric q ↔ IntersectionCondition q

Under conservativity, symmetric ↔ intersective (P&W Ch.6 Fact 1). This is the single most important bridge theorem — it explains why weak determiners allow there-insertion.

source

theorem Core.Quantification.symm_not_positive_strong {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hSym : QSymmetric q) (hNontrivF : ∃ (R : α → Prop) (S : α → Prop), ¬q R S) :

¬PositiveStrong q

Non-trivial symmetric quantifiers are not positive strong (P&W Ch.6 Fact 7).

source

theorem Core.Quantification.conservative_iff_livesOn {α : Type u_1} (q : GQ α) :

Conservative q ↔ ∀ (A : α → Prop), LivesOn (restrict q A) A

Conservativity of a GQ is equivalent to its restricted quantifiers living on their restrictors (P&W §3.2.2).

source

theorem Core.Quantification.extension_trivial {α : Type u_1} (q : GQ α) :

Extension q

Every GQ α satisfies Extension: the representation is universe-free.

source

theorem Core.Quantification.vanBenthem_cons_ext {α : Type u_1} (q : GQ α) :

Extension q → (Conservative q ↔ ∀ (A : α → Prop), LivesOn (restrict q A) A)

@cite{van-benthem-1984}: Under Extension (free for GQ α), Conservativity is equivalent to LivesOn — the restricted quantifier depends only on elements of its restrictor.

source

theorem Core.Quantification.restrictorUpMono_to_upSE {α : Type u_1} (q : GQ α) (h : RestrictorUpwardMono q) :

UpSEMon q

Persistence → ↑_SE Mon.

source

theorem Core.Quantification.restrictorUpMono_to_upSW {α : Type u_1} (q : GQ α) (h : RestrictorUpwardMono q) :

UpSWMon q

Persistence → ↑_SW Mon.

source

theorem Core.Quantification.upSW_upSE_to_restrictorUpMono {α : Type u_1} (q : GQ α) (hSW : UpSWMon q) (hSE : UpSEMon q) :

RestrictorUpwardMono q

↑_SW Mon ∧ ↑_SE Mon → Persistence (@cite{peters-westerstahl-2006} Prop 6).

source

theorem Core.Quantification.persistent_iff_upSW_and_upSE {α : Type u_1} (q : GQ α) :

RestrictorUpwardMono q ↔ UpSWMon q ∧ UpSEMon q

Persistence ↔ ↑_SW Mon ∧ ↑_SE Mon (@cite{peters-westerstahl-2006} Prop 6).

source

theorem Core.Quantification.restrictorDownMono_to_downNW {α : Type u_1} (q : GQ α) (h : RestrictorDownwardMono q) :

DownNWMon q

Anti-persistence → ↓_NW Mon.

source

theorem Core.Quantification.restrictorDownMono_to_downNE {α : Type u_1} (q : GQ α) (h : RestrictorDownwardMono q) :

DownNEMon q

Anti-persistence → ↓_NE Mon.

source

theorem Core.Quantification.downNW_downNE_to_restrictorDownMono {α : Type u_1} (q : GQ α) (hNW : DownNWMon q) (hNE : DownNEMon q) :

RestrictorDownwardMono q

↓_NW Mon ∧ ↓_NE Mon → Anti-persistence.

source

theorem Core.Quantification.anti_persistent_iff_downNW_and_downNE {α : Type u_1} (q : GQ α) :

RestrictorDownwardMono q ↔ DownNWMon q ∧ DownNEMon q

Anti-persistence ↔ ↓_NW Mon ∧ ↓_NE Mon.

source

theorem Core.Quantification.outerNeg_upSE_to_downNW {α : Type u_1} (q : GQ α) (h : UpSEMon q) :

DownNWMon (outerNeg q)

Outer negation reverses ↑_SE to ↓_NW (@cite{peters-westerstahl-2006} Prop 8a).

source

theorem Core.Quantification.outerNeg_downNW_to_upSE {α : Type u_1} (q : GQ α) (h : DownNWMon q) :

UpSEMon (outerNeg q)

Outer negation reverses ↓_NW to ↑_SE.

source

theorem Core.Quantification.outerNeg_upSW_to_downNE {α : Type u_1} (q : GQ α) (h : UpSWMon q) :

DownNEMon (outerNeg q)

Outer negation reverses ↑_SW to ↓_NE.

source

theorem Core.Quantification.outerNeg_downNE_to_upSW {α : Type u_1} (q : GQ α) (h : DownNEMon q) :

UpSWMon (outerNeg q)

Outer negation reverses ↓_NE to ↑_SW.

source

theorem Core.Quantification.innerNeg_downNE_to_downNW {α : Type u_1} (q : GQ α) (h : DownNEMon q) :

DownNWMon (innerNeg q)

Inner negation switches ↓_NE ↔ ↓_NW (@cite{peters-westerstahl-2006} Prop 8b).

source

theorem Core.Quantification.innerNeg_downNW_to_downNE {α : Type u_1} (q : GQ α) (h : DownNWMon q) :

DownNEMon (innerNeg q)

Inner negation switches ↓_NW ↔ ↓_NE.

source

theorem Core.Quantification.innerNeg_upSE_to_upSW {α : Type u_1} (q : GQ α) (h : UpSEMon q) :

UpSWMon (innerNeg q)

Inner negation switches ↑_SE ↔ ↑_SW.

source

theorem Core.Quantification.innerNeg_upSW_to_upSE {α : Type u_1} (q : GQ α) (h : UpSWMon q) :

UpSEMon (innerNeg q)

Inner negation switches ↑_SW ↔ ↑_SE.

source

theorem Core.Quantification.smooth_iff_outerNeg_coSmooth {α : Type u_1} (q : GQ α) :

Smooth q ↔ CoSmooth (outerNeg q)

Smooth ↔ outer negation is co-smooth (@cite{peters-westerstahl-2006} Prop 8a).

source

theorem Core.Quantification.smooth_iff_innerNeg_coSmooth {α : Type u_1} (q : GQ α) :

Smooth q ↔ CoSmooth (innerNeg q)

Smooth ↔ inner negation is co-smooth (@cite{peters-westerstahl-2006} Prop 8b).

source

theorem Core.Quantification.smooth_conservative_scopeUpMono {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hSmooth : Smooth q) :

ScopeUpwardMono q

CONSERV ∧ Smooth → Mon↑ (@cite{peters-westerstahl-2006} Prop 9).

source

theorem Core.Quantification.symmetric_to_upSW_downNE {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hSym : QSymmetric q) :

UpSWMon q ∧ DownNEMon q

CONSERV ∧ QSymmetric → ↑_SW Mon ∧ ↓_NE Mon (@cite{peters-westerstahl-2006} Prop 7).

source

theorem Core.Quantification.upSW_downNE_to_symmetric {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hUpSW : UpSWMon q) (hDownNE : DownNEMon q) :

QSymmetric q

↑_SW Mon ∧ ↓_NE Mon → QSymmetric (under CONSERV).

source

theorem Core.Quantification.symmetric_iff_upSW_downNE {α : Type u_1} (q : GQ α) (hCons : Conservative q) :

QSymmetric q ↔ UpSWMon q ∧ DownNEMon q

@cite{peters-westerstahl-2006} Prop 7: a CONSERV type ⟨1,1⟩ quantifier is symmetric iff it satisfies ↑_SW Mon and ↓_NE Mon.

source

theorem Core.Quantification.conservative_outerNeg {α : Type u_1} (q : GQ α) (h : Conservative q) :

Conservative (outerNeg q)

Conservativity is closed under complement.

source

theorem Core.Quantification.conservative_gqMeet {α : Type u_1} (f g : GQ α) (hf : Conservative f) (hg : Conservative g) :

Conservative (gqMeet f g)

Conservativity is closed under meet.

source

theorem Core.Quantification.conservative_gqJoin {α : Type u_1} (f g : GQ α) (hf : Conservative f) (hg : Conservative g) :

Conservative (gqJoin f g)

Conservativity is closed under join.

source

theorem Core.Quantification.outerNeg_gqJoin {α : Type u_1} (f g : GQ α) :

outerNeg (gqJoin f g) = gqMeet (outerNeg f) (outerNeg g)

K&S (26): complement distributes over join via de Morgan.

source

theorem Core.Quantification.outerNeg_gqMeet {α : Type u_1} (f g : GQ α) :

outerNeg (gqMeet f g) = gqJoin (outerNeg f) (outerNeg g)

K&S (26): complement distributes over meet via de Morgan.

source

theorem Core.Quantification.scopeUpMono_gqMeet {α : Type u_1} (f g : GQ α) (hf : ScopeUpwardMono f) (hg : ScopeUpwardMono g) :

ScopeUpwardMono (gqMeet f g)

K&S PROP 6: Meet of scope-↑ functions is scope-↑.

source

theorem Core.Quantification.scopeDownMono_gqMeet {α : Type u_1} (f g : GQ α) (hf : ScopeDownwardMono f) (hg : ScopeDownwardMono g) :

ScopeDownwardMono (gqMeet f g)

K&S PROP 6: Meet of scope-↓ functions is scope-↓.

source

theorem Core.Quantification.scopeUpMono_gqJoin {α : Type u_1} (f g : GQ α) (hf : ScopeUpwardMono f) (hg : ScopeUpwardMono g) :

ScopeUpwardMono (gqJoin f g)

K&S PROP 6: Join of scope-↑ functions is scope-↑.

source

theorem Core.Quantification.conservative_adjRestrict {α : Type u_1} (q : GQ α) (adj : α → Prop) (h : Conservative q) :

Conservative (adjRestrict q adj)

K&S PROP 3: Conservativity is preserved under adjectival restriction.

source

theorem Core.Quantification.scopeUpMono_adjRestrict {α : Type u_1} (q : GQ α) (adj : α → Prop) (h : ScopeUpwardMono q) :

ScopeUpwardMono (adjRestrict q adj)

K&S PROP 5: Scope-upward monotonicity is preserved under adjectival restriction.

source

theorem Core.Quantification.scopeDownMono_adjRestrict {α : Type u_1} (q : GQ α) (adj : α → Prop) (h : ScopeDownwardMono q) :

ScopeDownwardMono (adjRestrict q adj)

K&S PROP 5: Scope-downward monotonicity is preserved under adjectival restriction.

source

theorem Core.Quantification.individual_upward_closed {α : Type u_1} (a : α) (P P' : α → Prop) (h : ∀ (x : α), P x → P' x) :

individual a P → individual a P'

Montagovian individuals are upward closed (ultrafilter property).

source

theorem Core.Quantification.individual_meet_closed {α : Type u_1} (a : α) (P Q : α → Prop) :

individual a P → individual a Q → individual a fun (x : α) => P x ∧ Q x

Montagovian individuals are closed under intersection.

source

theorem Core.Quantification.vanBenthem_refl_antisym_is_inclusion {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hRefl : PositiveStrong q) (hAnti : QAntisymmetric q) (A B : α → Prop) :

q A B ↔ ∀ (x : α), A x → B x

@cite{van-benthem-1984} Theorem 3.1.1: Under conservativity, inclusion (⊆) is the only reflexive antisymmetric quantifier.

source

theorem Core.Quantification.zwarts_refl_trans_scopeUp {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hRefl : PositiveStrong q) (hTrans : QTransitive q) :

ScopeUpwardMono q

@cite{van-benthem-1984} Thm 4.1.1 (Zwarts): reflexive + transitive → MON↑.

source

theorem Core.Quantification.zwarts_refl_trans_restrictorDown {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hRefl : PositiveStrong q) (hTrans : QTransitive q) :

RestrictorDownwardMono q

@cite{van-benthem-1984} Thm 4.1.1 (Zwarts): reflexive + transitive → ↓MON.

source

theorem Core.Quantification.zwarts_sym_scopeUp_quasiRefl {α : Type u_1} (q : GQ α) (hCons : Conservative q) (_hSym : QSymmetric q) (hUp : ScopeUpwardMono q) :

QuasiReflexive q

@cite{van-benthem-1984} Thm 4.1.3 (Zwarts): for symmetric quantifiers, scope-↑ implies quasi-reflexive, under CONSERV.

source

theorem Core.Quantification.zwarts_sym_scopeDown_quasiUniv {α : Type u_1} (q : GQ α) (hCons : Conservative q) (_hSym : QSymmetric q) (hDown : ScopeDownwardMono q) :

QuasiUniversal q

@cite{van-benthem-1984} Thm 4.1.3 (Zwarts): for symmetric quantifiers, scope-↓ implies quasi-universal, under CONSERV.

source

theorem Core.Quantification.scopeUpMono_rightContinuous {α : Type u_1} (q : GQ α) (h : ScopeUpwardMono q) :

RightContinuous q

Right-monotone quantifiers are right-continuous.

source

theorem Core.Quantification.irrefl_almostConn_scopeDown {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hIrrefl : NegativeStrong q) (hAC : AlmostConnected q) :

ScopeDownwardMono q

@cite{van-benthem-1984} Thm 4.1.2: irreflexive + almost-connected → MON↓.

source

theorem Core.Quantification.irrefl_almostConn_restrictorUp {α : Type u_1} (q : GQ α) (hCons : Conservative q) (hIrrefl : NegativeStrong q) (hAC : AlmostConnected q) :

RestrictorUpwardMono q

@cite{van-benthem-1984} Thm 4.1.2: irreflexive + almost-connected → ↑MON.

source

theorem Core.Quantification.asymmetric_irreflexive {α : Type u_1} (q : GQ α) (hAsym : QAsymmetric q) :

QIrreflexive q

Asymmetric quantifiers are irreflexive.

source

theorem Core.Quantification.asymmetric_antisymmetric {α : Type u_1} (q : GQ α) (hAsym : QAsymmetric q) :

QAntisymmetric q

Asymmetric implies antisymmetric (vacuously).

source

theorem Core.Quantification.circular_symmetric_quasiRefl {α : Type u_1} (q : GQ α) (hSym : QSymmetric q) (hCirc : QCircular q) :

QuasiReflexive q

Circular + symmetric → quasi-reflexive.

source

theorem Core.Quantification.circular_reflexive_symmetric {α : Type u_1} (q : GQ α) (hCirc : QCircular q) (hPS : PositiveStrong q) :

QSymmetric q

Circularity + reflexivity → symmetry.

source

theorem Core.Quantification.isom_asymmetric_eq_diff {α : Type u_1} [Fintype α] [DecidableEq α] (q : GQ α) (hCons : Conservative q) (hIsom : QuantityInvariant q) (hAsym : QAsymmetric q) {A B : α → Prop} [DecidablePred A] [DecidablePred B] (hCard : Fintype.card { x : α // A x ∧ ¬B x } = Fintype.card { x : α // B x ∧ ¬A x }) :

¬q A B

@cite{peters-westerstahl-2006} Prop 6.59 (fixed-domain version): Under CONSERV + ISOM + asymmetry, ¬Q(A,B) whenever |A \ B| = |B \ A|.

source

theorem Core.Quantification.vanBenthem_symm_quasiRefl_is_overlap {α : Type u_1} [Fintype α] [DecidableEq α] (q : GQ α) (hCons : Conservative q) (hSym : QSymmetric q) (hQR : QuasiReflexive q) (hWitT : ∃ (x : α), q (fun (y : α) => y = x) fun (y : α) => y = x) (hWitF : ∃ (A : α → Prop), ¬q A A) (hIso : QuantityInvariant q) (A B : α → Prop) :

q A B ↔ ∃ (x : α), A x ∧ B x

@cite{van-benthem-1984} Cor 3.3.2: Under conservativity, the ONLY symmetric quasi-reflexive quantifier is overlap (= "some").

source

theorem Core.Quantification.vanBenthem_symm_quasiUniv_is_disjointness {α : Type u_1} [Fintype α] [DecidableEq α] (q : GQ α) (hCons : Conservative q) (hSym : QSymmetric q) (hQU : QuasiUniversal q) (hWitF : ∃ (x : α), ¬q (fun (y : α) => y = x) fun (y : α) => y = x) (hWitT : ∃ (A : α → Prop), q A A) (hIso : QuantityInvariant q) (A B : α → Prop) :