Generalized quantifiers

This file defines generalized quantifier denotations and the properties of them that the theory of determiners studies. A generalized quantifier on a type α is a relation between two predicates on α, the restrictor and the scope, so GQ α is (α → Prop) → (α → Prop) → Prop and inherits the Boolean algebra of the Pi type. The properties are Barwise and Cooper's conservativity, monotonicity, symmetry and strength, Peters and Westerståhl's left monotonicity, smoothness and anti-additivity, van Benthem's relational properties and quantity invariance in the sense of Mostowski. The operations are the negations and the dual, the Boolean operations named for determiner conjunction and disjunction, and restriction by an adjective. The concrete denotations are in Quantification/Basic.lean, and the individuals and the type shifts they fix in Quantification/Individual.lean.

Main definitions

• GQ, GQ.Family, NP: quantifier denotations on a type, on every finite type, and of type ⟨1⟩.
• GQ.Conservative, GQ.ScopeMonotone, GQ.RestrictorMonotone, GQ.PositiveStrong: the properties of Barwise and Cooper; symmetry is Std.Symm.
• GQ.UpSEMon, GQ.Smooth, GQ.LeftAntiAdditive: the left monotonicities of Peters and Westerståhl.
• GQ.QuasiReflexive, GQ.Filtrating, GQ.QuantityInvariant: van Benthem's relational properties and quantity invariance.
• GQ.innerNeg, GQ.dual, GQ.adjRestrict: the operations; the outer negation, meet and join are the Boolean algebra's ᶜ, ⊓ and ⊔.
• NP.individual, NP.LivesOn: the Montague lift and the live-on property.

Implementation notes

Extension, the independence of a quantifier from the ambient universe, holds by construction, since a denotation is given on one type. A quantifier is a binary relation on predicates, so the classical relational properties are the core relation classes Std.Symm, IsTrans, Std.Antisymm, Std.Asymm and Std.Trichotomous applied to it, and the monotonicities are Monotone and Antitone of its sections. Decidability of the concrete denotations is recovered pointwise from [Fintype α] and decidable restrictor and scope.

References

• [BC81]
• [KS86]
• [Mos57]
• [Par87]
• [PW06]
• [vB84]

@[reducible, inline]

abbrev Quantifier.GQ (α : Type u_1) : Type u_1

A generalized quantifier denotation maps a restrictor and a scope to a proposition. Under the pointwise ordering of α → Prop it is a binary relation between predicates.

Equations

• Quantifier.GQ α = ((α → Prop) → (α → Prop) → Prop)

@[reducible, inline]

abbrev Quantifier.GQ.Family : Type (u + 1)

A determiner denotation given on every finite domain, the object from which a lexicon entry's available readings are drawn.

Equations

• Quantifier.GQ.Family = ((α : Type ?u.1) → [Fintype α] → Quantifier.GQ α)

@[reducible, inline]

abbrev Quantifier.NP (α : Type u_1) : Type u_1

A type ⟨1⟩ quantifier, the denotation of a noun phrase, is a property of properties, a quantifier proper in Barwise and Cooper's sense. It is definitionally Cont Prop α, the scope-taking continuation.

Equations

• Quantifier.NP α = ((α → Prop) → Prop)

Conservativity and monotonicity

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

A quantifier is conservative when Q(A, B) ↔ Q(A, A ∩ B), so that only the elements of the scope that are in the restrictor matter. Barwise and Cooper's universal says that every simple determiner denotes a conservative quantifier.

Equations

• q.Conservative = ∀ (R S : α → Prop), q R S ↔ q R fun (x : α) => R x ∧ S x

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

A quantifier is scope monotone when B ⊆ B' and Q(A, B) give Q(A, B'), that is, when every section q R is Monotone under the pointwise ordering.

Equations

• q.ScopeMonotone = ∀ (R : α → Prop), Monotone (q R)

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

A quantifier is scope antitone when B ⊆ B' and Q(A, B') give Q(A, B), that is, when every section q R is Antitone.

Equations

• q.ScopeAntitone = ∀ (R : α → Prop), Antitone (q R)

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

A quantifier satisfies the intersection condition when Q(A, B) depends only on A ∩ B.

Equations

• q.IntersectionCondition = ∀ (R S R' S' : α → Prop), (∀ (x : α), R x ∧ S x ↔ R' x ∧ S' x) → (q R S ↔ q R' S')

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

A quantifier is restrictor monotone, or persistent, when A ⊆ A' and Q(A, B) give Q(A', B), that is, when q · S is Monotone for every scope S.

Equations

• q.RestrictorMonotone = ∀ (S : α → Prop), Monotone fun (x : α → Prop) => q x S

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

A quantifier is restrictor antitone, or anti-persistent, when A ⊆ A' and Q(A', B) give Q(A, B), that is, when q · S is Antitone for every scope S.

Equations

• q.RestrictorAntitone = ∀ (S : α → Prop), Antitone fun (x : α → Prop) => q x S

Strength

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

A quantifier is positive strong when Q(A, A) holds for every A, as for every.

Equations

• q.PositiveStrong = ∀ (R : α → Prop), q R R

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

A quantifier is negative strong when Q(A, A) fails for every A, as for neither.

Equations

• q.NegativeStrong = ∀ (R : α → Prop), ¬q R R

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

A quantifier has the existential property when Q(A, B) ↔ Q(A ∩ B, ⊤), the property of the determiners felicitous in there-sentences.

Equations

• q.Existential = ∀ (R S : α → Prop), q R S ↔ q (fun (x : α) => R x ∧ S x) fun (x : α) => True

Left monotonicity and smoothness

Peters and Westerståhl's four left monotonicities enlarge or shrink the restrictor by elements inside or outside the scope. On the number triangle, with k = |A ∖ B| and m = |A ∩ B|, UpSEMon moves (k, m) to (k, m + 1), UpSWMon to (k + 1, m), DownNWMon moves (k, m + 1) to (k, m) and DownNEMon moves (k + 1, m) to (k, m).

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

A quantifier is ↑SE monotone when enlarging the restrictor by elements of the scope preserves it, so that A ⊆ A', A ∖ B = A' ∖ B and Q(A, B) give Q(A', B).

Equations

• q.UpSEMon = ∀ (R S R' : α → Prop), (∀ (x : α), R x → R' x) → (∀ (x : α), R' x → ¬S x → R x) → q R S → q R' S

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

A quantifier is ↑SW monotone when enlarging the restrictor by elements outside the scope preserves it, so that A ⊆ A', A ∩ B = A' ∩ B and Q(A, B) give Q(A', B).

Equations

• q.UpSWMon = ∀ (R S R' : α → Prop), (∀ (x : α), R x → R' x) → (∀ (x : α), R' x → S x → R x) → q R S → q R' S

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

A quantifier is ↓NW monotone when shrinking the restrictor by elements of the scope preserves it, so that A' ⊆ A, A ∖ B = A' ∖ B and Q(A, B) give Q(A', B).

Equations

• q.DownNWMon = ∀ (R S R' : α → Prop), (∀ (x : α), R' x → R x) → (∀ (x : α), R x → ¬S x → R' x) → q R S → q R' S

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

A quantifier is ↓NE monotone when shrinking the restrictor by elements outside the scope preserves it, so that A' ⊆ A, A ∩ B = A' ∩ B and Q(A, B) give Q(A', B).

Equations

• q.DownNEMon = ∀ (R S R' : α → Prop), (∀ (x : α), R' x → R x) → (∀ (x : α), R x → S x → R' x) → q R S → q R' S

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

A quantifier is smooth when it is ↓NE and ↑SE monotone; smooth quantifiers are scope-upward monotone.

Equations

• q.Smooth = (q.DownNEMon ∧ q.UpSEMon)

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

A quantifier is co-smooth when its inner negation is smooth, that is, when it is ↓NW and ↑SW monotone.

Equations

• q.CoSmooth = (q.DownNWMon ∧ q.UpSWMon)

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

A quantifier is left anti-additive when Q(A ∪ B, C) ↔ Q(A, C) ∧ Q(B, C).

Equations

• q.LeftAntiAdditive = ∀ (R R' S : α → Prop), q (fun (x : α) => R x ∨ R' x) S ↔ q R S ∧ q R' S

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

A quantifier is right anti-additive when Q(A, B ∪ C) ↔ Q(A, B) ∧ Q(A, C).

Equations

• q.RightAntiAdditive = ∀ (R S S' : α → Prop), (q R fun (x : α) => S x ∨ S' x) ↔ q R S ∧ q R S'

Relational properties

Van Benthem reads a quantifier as a relation between predicates and asks which relational properties it has. The classical ones are the core relation classes: all is IsTrans and Std.Antisymm, some and no are Std.Symm, and not all is Std.Trichotomous. The properties below are the ones the theory of quantifiers adds.

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

A quantifier is quasi-reflexive when Q(A, B) gives Q(A, A), as for some.

Equations

• q.QuasiReflexive = ∀ (A B : α → Prop), q A B → q A A

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

A quantifier is quasi-universal when Q(A, A) gives Q(A, B) for every B, as for no.

Equations

• q.QuasiUniversal = ∀ (A B : α → Prop), q A A → q A B

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

A quantifier is almost connected when Q(A, B) gives Q(A, C) or Q(C, B) for every C, which is the transitivity of its complement.

Equations

• q.AlmostConnected = ∀ (A B C : α → Prop), q A B → q A C ∨ q C B

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

A quantifier is circular when Q(A, B) and Q(B, C) give Q(C, A).

Equations

• q.Circular = ∀ (A B C : α → Prop), q A B → q B C → q C A

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

A quantifier is right continuous when Q(A, B₁), Q(A, B₂) and B₁ ⊆ B ⊆ B₂ give Q(A, B); every scope-monotone quantifier is right continuous.

Equations

• q.RightContinuous = ∀ (A B B₁ B₂ : α → Prop), (∀ (x : α), B₁ x → B x) → (∀ (x : α), B x → B₂ x) → q A B₁ → q A B₂ → q A B

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

A quantifier is scope-intersective when Q(A, B) and Q(A, C) give Q(A, B ∩ C).

Equations

• q.ScopeIntersective = ∀ (A B C : α → Prop), q A B → q A C → q A fun (x : α) => B x ∧ C x

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

A quantifier is filtrating when it is scope monotone and scope-intersective, so that its scopes at a fixed restrictor form a filter.

Equations

• q.Filtrating = (q.ScopeMonotone ∧ q.ScopeIntersective)

Invariance

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

A quantifier is quantity invariant when it is invariant under permutations of the domain, so that Q(A, B) depends only on the pattern of the two predicates and not on which elements satisfy them. This is Mostowski's permutation invariance for type ⟨1, 1⟩ quantifiers.

Equations

• q.QuantityInvariant = ∀ (A B A' B' : α → Prop) (f : α → α), Function.Bijective f → (∀ (x : α), A (f x) ↔ A' x) → (∀ (x : α), B (f x) ↔ B' x) → (q A B ↔ q A' B')

The Boolean algebra, the negations and the dual

The outer negation of a quantifier is its complement qᶜ, and determiner conjunction and disjunction are the meet f ⊓ g and join f ⊔ g of the Boolean algebra GQ α; the lemmas below are their pointwise normal forms.

@[simp]

theorem Quantifier.GQ.compl_apply {α : Type u_1} (q : GQ α) (R S : α → Prop) : qᶜ R S = ¬q R S

@[simp]

theorem Quantifier.GQ.inf_apply {α : Type u_1} (f g : GQ α) (R S : α → Prop) : (f ⊓ g) R S = (f R S ∧ g R S)

@[simp]

theorem Quantifier.GQ.sup_apply {α : Type u_1} (f g : GQ α) (R S : α → Prop) : (f ⊔ g) R S = (f R S ∨ g R S)

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

The inner negation of a quantifier, (Q~)(A, B) = Q(A, ¬ B).

Equations

• q.innerNeg R S = q R fun (x : α) => ¬S x

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

The dual of a quantifier, Q̌ = (Q~)ᶜ, so that the dual of every is some.

Equations

• q.dual = q.innerNegᶜ

Restriction

def Quantifier.GQ.adjRestrict {α : Type u_1} (q : GQ α) (adj : α → Prop) : GQ α

The restriction of a quantifier by an adjective or relative clause narrows the restrictor, so that tall student is student and tall.

Equations

• q.adjRestrict adj R S = q (fun (x : α) => R x ∧ adj x) S

Type ⟨1⟩ quantifiers

def Quantifier.NP.LivesOn {α : Type u_1} (Q : NP α) (A : α → Prop) : Prop

A type ⟨1⟩ quantifier lives on A when Q(B) ↔ Q(A ∩ B) for every B.

Equations

• Q.LivesOn A = ∀ (B : α → Prop), Q B ↔ Q fun (x : α) => A x ∧ B x

theorem Quantifier.GQ.Conservative.livesOn {α : Type u_1} {q : GQ α} (h : q.Conservative) (A : α → Prop) : NP.LivesOn (q A) A

A conservative quantifier lives on its restrictor.

def Quantifier.NP.individual {α : Type u_1} (a : α) : NP α

The Montague lift of an entity is the principal ultrafilter it generates, the type ⟨1⟩ quantifier of the properties it has; it is Partee's LIFT and the continuation pure.

Equations

• Quantifier.NP.individual a P = P a

theorem Quantifier.NP.individual_injective {α : Type u_1} : Function.Injective individual

The Montague lift is injective, since an entity is recovered from its principal ultrafilter.

theorem Quantifier.NP.individual_livesOn {α : Type u_1} {A : α → Prop} {a : α} (ha : A a) : (individual a).LivesOn A

The Montague lift of a member of A lives on A.

def Quantifier.NP.ident {α : Type u_1} (j : α) : α → Prop

The singleton property of an entity, ident j = {j}, whose lift is individual j.

Equations

• Quantifier.NP.ident j x✝ = (x✝ = j)

theorem Quantifier.NP.ident_injective {α : Type u_1} : Function.Injective ident