Properties of generalized quantifiers #
This file proves the general theorems about the properties of generalized quantifiers defined
in Quantification/Defs.lean. The negations and the dual reverse monotonicity and preserve
quantity invariance; conservativity and monotonicity are closed under the Boolean operations
and under adjectival restriction, as Keenan and Stavi show; and conservativity together with
symmetry or with the left monotonicities yields the characterizations of van Benthem and of
Peters and Westerståhl. Barwise and Cooper's theorems on type ⟨1⟩ quantifiers close the file.
References #
Duality Theorems #
Outer negation turns a scope-upward monotone quantifier into a scope-downward one.
Outer negation turns a scope-downward monotone quantifier into a scope-upward one.
Inner negation turns a scope-upward monotone quantifier into a scope-downward one.
Inner negation turns a scope-downward monotone quantifier into a scope-upward one.
Outer negation turns a restrictor-upward monotone quantifier into a restrictor-downward one.
Outer negation turns a restrictor-downward monotone quantifier into a restrictor-upward one.
QuantityInvariant closure #
Outer negation preserves quantity invariance.
Inner negation preserves quantity invariance.
Dual preserves QuantityInvariant.
Meet preserves QuantityInvariant.
Join preserves QuantityInvariant.
A conservative quantifier satisfying the intersection condition is symmetric (Barwise and Cooper's Theorem C5).
Scope-downward monotonicity is equivalent to scope-upward monotonicity of the inner negation (co-property characterization, P&W §3.2.4).
Conservativity, Symmetry, and Strength #
A conservative quantifier reads its scope only on the restrictor.
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.
Non-trivial symmetric quantifiers are not positive strong (P&W Ch.6 Fact 7).
Conservativity of a GQ is equivalent to its restricted quantifiers living on their restrictors (P&W §3.2.2).
A conservative quantifier's value at a restrictor depends only on the scope's meet with it.
Persistence → ↑_SE Mon.
Persistence → ↑_SW Mon.
Persistence ↔ ↑_SW Mon ∧ ↑_SE Mon ([PW06] Prop 6).
Anti-persistence → ↓_NW Mon.
Anti-persistence → ↓_NE Mon.
↓_NW Mon ∧ ↓_NE Mon → Anti-persistence.
Anti-persistence ↔ ↓_NW Mon ∧ ↓_NE Mon.
CONSERV ∧ Smooth → Mon↑ ([PW06] Prop 9).
CONSERV ∧ Std.Symm → ↑_SW Mon ∧ ↓_NE Mon ([PW06] Prop 7).
↑_SW Mon ∧ ↓_NE Mon → Std.Symm (under CONSERV).
A conservative quantifier is symmetric iff it satisfies ↑SW Mon and ↓NE Mon ([PW06]'s Prop 7).
Conservativity is closed under complement.
Conservativity is closed under meet.
Conservativity is closed under join.
The meet of two scope-upward monotone quantifiers is scope-upward monotone.
The meet of two scope-downward monotone quantifiers is scope-downward monotone.
The join of two scope-upward monotone quantifiers is scope-upward monotone.
An existential quantifier is conservative, so E-Det lies inside DDet ([KS86]).
The existential property is preserved under adjectival restriction, since an absolute adjective commutes with the meet of restrictor and scope ([KS86]'s PROP 16).
Conservativity is preserved under adjectival restriction.
Scope-upward monotonicity is preserved under adjectival restriction.
Scope-downward monotonicity is preserved under adjectival restriction.
Type ⟨1⟩ Theorems (P&W Ch.2-3) #
Montagovian individuals are upward closed (ultrafilter property).
Montagovian individuals are closed under intersection.
Under conservativity, inclusion is the only reflexive antisymmetric quantifier ([vB84]'s Theorem 3.1.1).
A conservative reflexive transitive quantifier is scope-upward monotone (Zwarts's theorem in [vB84]).
A conservative reflexive transitive quantifier is restrictor-antitone (Zwarts's theorem in [vB84]).
Under conservativity a scope-upward monotone quantifier is quasi-reflexive, the half of van Benthem's theorem on symmetric quantifiers that needs no symmetry.
Under conservativity a scope-downward monotone quantifier is quasi-universal, the half of van Benthem's theorem on symmetric quantifiers that needs no symmetry.
Right-monotone quantifiers are right-continuous.
A conservative irreflexive almost-connected quantifier is scope-antitone ([vB84]'s Theorem 4.1.2).
A conservative irreflexive almost-connected quantifier is restrictor-monotone ([vB84]'s Theorem 4.1.2).
Asymmetric quantifiers are negative-strong (irreflexive).
Asymmetric implies antisymmetric (vacuously).
Circular + symmetric → quasi-reflexive.
Circularity + reflexivity → symmetry.
Under conservativity, quantity invariance and asymmetry, Q(A, B) fails whenever A ∖ B
and B ∖ A have the same size ([PW06]'s Prop 6.59, fixed-domain version).
Under conservativity the only symmetric quasi-reflexive quantifier is overlap, that is some ([vB84]'s Corollary 3.3.2).
Under conservativity the only symmetric quasi-universal quantifier is disjointness, that is no ([vB84]'s Corollary 3.3.3).