Generalized Quantifier Definitions

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

Model-agnostic property definitions, operations, and type shifts for generalized quantifier denotations.

A GQ denotation is a function (α → Prop) → (α → Prop) → Prop mapping a restrictor and a scope to a proposition. The properties defined here (conservativity, monotonicity, duality, intersection condition, symmetry) are purely logical — they hold at the predicate level and require no model infrastructure. Decidability is recovered pointwise via [Fintype α] + [DecidablePred R] + [DecidablePred S] for the concrete denotations defined in Semantics.Quantification.Quantifier.

The theory-specific module Semantics.Quantification.Quantifier defines concrete denotations (every_sem, some_sem, etc.) and proves they satisfy these properties.

Contents

• §1 Property definitions: all predicates on GQs, grouped by source
• §2 Operations: duality, Boolean algebra, type shifts
• §3 Mathlib bridge: connection to Monotone/Antitone

@[reducible, inline]

abbrev Core.Quantification.GQ (α : Type u_1) : Type u_1

Generalized quantifier denotation: restrictor → scope → proposition.

Under the Pi-of-Prop ordering (α → Prop ordered by pointwise implication), a GQ is just a binary relation between predicates.

Equations

• Core.Quantification.GQ α = ((α → Prop) → (α → Prop) → Prop)

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

Conservativity: Q(A, B) ↔ Q(A, A ∩ B).

Only the elements of B that are also in A matter for the quantifier's truth value. Also called "lives on" (B&C) or "intersectivity". All simple (lexicalized) determiners are conservative.

Equations

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

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

Scope-upward-monotone: if B ⊆ B' and Q(A,B), then Q(A,B').

Under the Pi-of-Prop ordering this is exactly ∀ R, Monotone (q R) (see scopeUpMono_iff_monotone). This connects to Semantics.Entailment.Polarity.IsUpwardEntailing = Monotone.

Equations

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

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

Scope-downward-monotone: if B ⊆ B' and Q(A,B'), then Q(A,B).

Equivalent to ∀ R, Antitone (q R) (see scopeDownMono_iff_antitone).

Equations

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

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

Intersection condition: Q(A,B) depends only on A∩B. B&C §4.8, p.189.

Equations

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

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

Symmetric: Q(A,B) ↔ Q(B,A). B&C p.210; equivalent to intersection condition by Theorem C5.

Equations

• Core.Quantification.QSymmetric q = ∀ (R S : α → Prop), q R S ↔ q S R

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

Restrictor-upward-monotone (persistent): if A ⊆ A' then Q(A,B) → Q(A',B). Linked to weak determiners and there-insertion. B&C §4.9, p.193.

Equations

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

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

Restrictor-downward-monotone (anti-persistent).

Equations

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

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

Positive strong: Q(A,A) for all A. P&W Ch.6: "every", "most", "the".

Equations

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

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

Negative strong: ¬Q(A,A) for all A. "Neither".

Equations

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

def Core.Quantification.Extension {α : Type u_1} (_q : GQ α) : Prop

Extension (EXT): Q(A,B) depends only on A and B, not on the ambient universe M. In model-theoretic GQ theory (where Q^M takes a universe), EXT must be stated as an additional axiom. For GQ α, EXT holds trivially since there is no universe parameter — it's a design theorem.

Significance: EXT + CONS characterize "well-behaved" determiners. See vanBenthem_cons_ext.

Reference: Peters & Westerståhl Ch.4 Def 4.1.

Equations

• Core.Quantification.Extension _q = True

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

Second conservativity: Q(A,B) ↔ Q(A∩B, B). P&W Ch.6.

Equations

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

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

Existential property: Q(A,B) ↔ Q(A∩B, everything). P&W Ch.6. Characterizes determiners that are felicitous in there-sentences.

Equations

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

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

↑_SE Mon (@cite{peters-westerstahl-2006} §5.5): Q(A,B) & A⊆A' & A\B=A'\B → Q(A',B). On the number triangle: if Q(k,m) then Q(k',m) for k' ≥ k. Enlarging A by adding elements of B preserves Q.

Equations

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

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

↑_SW Mon (@cite{peters-westerstahl-2006} §5.5): Q(A,B) & A⊆A' & A∩B=A'∩B → Q(A',B). On the number triangle: if Q(k,m) then Q(k,m') for m' ≥ m. Enlarging A by adding elements outside B preserves Q. This is property (p) from P&W §5.2: half of the EXT condition.

Equations

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

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

↓_NW Mon (@cite{peters-westerstahl-2006} §5.5): Q(A,B) & A'⊆A & A\B=A'\B → Q(A',B). On the number triangle: if Q(k,m) then Q(k',m) for k' ≤ k. Shrinking A by removing elements of B preserves Q.

Equations

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

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

↓_NE Mon (@cite{peters-westerstahl-2006} §5.5): Q(A,B) & A'⊆A & A∩B=A'∩B → Q(A',B). On the number triangle: if Q(k,m) then Q(k,m') for m' ≤ m. Shrinking A by removing elements outside B preserves Q.

Equations

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

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

Smooth (@cite{peters-westerstahl-2006} §5.6): Q is ↓_NE Mon and ↑_SE Mon. Smooth quantifiers are Mon↑ (Prop 9). Under ISOM, smooth quantifiers have smooth monotonicity functions f where f(n) ≤ f(n+1) ≤ f(n)+1 (Prop 10). Most natural language Mon↑ determiners are smooth: all proportional quantifiers, "some", "all", "most", etc.

Equations

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

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

Co-smooth (@cite{peters-westerstahl-2006} §5.6): Q's inner negation is smooth. Equivalently, ↓_NW Mon and ↑_SW Mon. "no" and "fewer than half" are co-smooth.

Equations

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

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

Left anti-additive: Q(A∪B, C) ↔ Q(A,C) ∧ Q(B,C). P&W §5.9.

Equations

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

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

Right anti-additive: Q(A, B∪C) ↔ Q(A,B) ∧ Q(A,C). P&W §5.9.

Equations

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

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

Transitive: Q(A,B) ∧ Q(B,C) → Q(A,C). @cite{van-benthem-1984} §3.1. "all" is the prime transitive quantifier (inclusion is transitive).

Equations

• Core.Quantification.QTransitive q = ∀ (A B C : α → Prop), q A B → q B C → q A C

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

Antisymmetric: Q(A,B) ∧ Q(B,A) → A = B (extensionally). @cite{van-benthem-1984} §3.1: "all" (inclusion) is antisymmetric.

Equations

• Core.Quantification.QAntisymmetric q = ∀ (A B : α → Prop), q A B → q B A → A = B

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

Linear (connected): Q(A,B) ∨ Q(B,A) for all A, B. @cite{van-benthem-1984} §3.1: "not all" (non-inclusion) is linear.

Equations

• Core.Quantification.QLinear q = ∀ (A B : α → Prop), q A B ∨ q B A

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

Quasi-reflexive: Q(A,B) → Q(A,A). @cite{van-benthem-1984} §3.1. "some" is quasi-reflexive: overlap implies non-emptiness.

Equations

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

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

Quasi-universal: Q(A,A) → Q(A,B) for all B. @cite{van-benthem-1984} §3.1. "no" is quasi-universal: if A∩A = ∅ then A∩B = ∅ for all B.

Equations

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

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

Almost-connected: Q(A,B) → Q(A,C) ∨ Q(C,B) for all C. @cite{van-benthem-1984} §3.1: equivalent to transitivity of ¬Q. "not all" is almost-connected.

Equations

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

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

Asymmetric: Q(A,B) → ¬Q(B,A). @cite{peters-westerstahl-2006} Ch 6.4. Strictly stronger than antisymmetric: antisymmetry allows Q(A,B) ∧ Q(B,A) when A = B; asymmetry forbids it entirely. Under CONSERV + ISOM, no non-trivial quantifier is asymmetric (P&W Ch 6.4).

Equations

• Core.Quantification.QAsymmetric q = ∀ (A B : α → Prop), q A B → ¬q B A

@[reducible, inline]

abbrev Core.Quantification.QReflexive {α : Type u_1} (q : GQ α) : Prop

Reflexive (relational vocabulary): Q(A,A) for all A. Definitionally equal to PositiveStrong; included for relational vocabulary alignment with @cite{peters-westerstahl-2006} Ch 6.4 and @cite{van-benthem-1984}.

Equations

• Core.Quantification.QReflexive q = Core.Quantification.PositiveStrong q

@[reducible, inline]

abbrev Core.Quantification.QIrreflexive {α : Type u_1} (q : GQ α) : Prop

Irreflexive (relational vocabulary): ¬Q(A,A) for all A. Definitionally equal to NegativeStrong; included for relational vocabulary alignment with @cite{peters-westerstahl-2006} Ch 6.4.

Equations

• Core.Quantification.QIrreflexive q = Core.Quantification.NegativeStrong q

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

Circular: Q(A,B) ∧ Q(B,C) → Q(C,A). @cite{peters-westerstahl-2006} Ch 6.4. No natural language quantifier is non-trivially circular (under CONSERV + ISOM). Together with transitivity, circularity forces quasi-reflexivity.

Equations

• Core.Quantification.QCircular q = ∀ (A B C : α → Prop), q A B → q B C → q C A

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

VAR (Variety): Q is non-trivial — it both accepts and rejects some pair. @cite{van-benthem-1984} §2: rules out degenerate quantifiers like "at least 2" on singleton domains. Used as hypothesis in most uniqueness theorems.

Equations

• Core.Quantification.Variety q = ((∃ (A : α → Prop) (B : α → Prop), q A B) ∧ ∃ (A : α → Prop) (B : α → Prop), ¬q A B)

inductive Core.Quantification.DoubleMono : Type

Double monotonicity type (@cite{van-benthem-1984} §4.2). The logical Square of Opposition maps to four double-monotonicity types: all = ↓MON↑, some = ↑MON↑, no = ↓MON↓, not all = ↑MON↓.

• upUp : DoubleMono
• downUp : DoubleMono
• upDown : DoubleMono
• downDown : DoubleMono

@[implicit_reducible]

instance Core.Quantification.instDecidableEqDoubleMono : DecidableEq DoubleMono

Equations

• Core.Quantification.instDecidableEqDoubleMono x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Quantification.instReprDoubleMono : Repr DoubleMono

Equations

• Core.Quantification.instReprDoubleMono = { reprPrec := Core.Quantification.instReprDoubleMono.repr }

def Core.Quantification.instReprDoubleMono.repr : DoubleMono → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def Core.Quantification.DoubleMono.toProjectionType : DoubleMono → Duality.ProjectionType

Restrictor monotonicity determines projection type for embedded trivalent content (@cite{ramotowska-marty-romoli-santorio-2025}).

Restrictor-↓ (every, no) = conjunctive/strong = fragile under gaps. Restrictor-↑ (some, not-every) = disjunctive/weak = robust under gaps.

This is the monotonicity-theoretic explanation of why quantifier STRENGTH (not polarity) determines truth-value judgments for counterfactuals and other trivalent phenomena.

Equations

• Core.Quantification.DoubleMono.downUp.toProjectionType = Core.Duality.ProjectionType.conjunctive
• Core.Quantification.DoubleMono.downDown.toProjectionType = Core.Duality.ProjectionType.conjunctive
• Core.Quantification.DoubleMono.upUp.toProjectionType = Core.Duality.ProjectionType.disjunctive
• Core.Quantification.DoubleMono.upDown.toProjectionType = Core.Duality.ProjectionType.disjunctive

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

Right continuity (CONT): if Q(A,B₁) and Q(A,B₂) hold and B₁ ⊆ B ⊆ B₂, then Q(A,B). @cite{van-benthem-1984} §4.3: all right-monotone quantifiers are continuous. "precisely one" is continuous but non-monotone.

Equations

• Core.Quantification.RightContinuous q = ∀ (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 Core.Quantification.Filtrating {α : Type u_1} (q : GQ α) : Prop

Filtrating: Q(A,B) ∧ Q(A,C) → Q(A, B∩C). @cite{van-benthem-1984} Thm 4.4.2: "all" is the only filtrating quantifier (under VAR*). This is because filtrating ↔ filter (closure under ∩), and only the principal filter at A (= inclusion) satisfies CONSERV.

Equations

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

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

MU1: All simple (lexicalized) determiners are monotone in scope. @cite{peters-westerstahl-2006} §5.8 Universal 1.

Equations

• Core.Quantification.MU1 q = (Core.Quantification.ScopeUpwardMono q ∨ Core.Quantification.ScopeDownwardMono q)

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

MU2: All simple determiners are monotone in at least one restrictor direction. @cite{peters-westerstahl-2006} §5.8 Universal 2.

Equations

• Core.Quantification.MU2 q = (Core.Quantification.RestrictorUpwardMono q ∨ Core.Quantification.RestrictorDownwardMono q)

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

MU3: All simple Mon↑ determiners are smooth. @cite{peters-westerstahl-2006} §5.8 Universal 3.

Equations

• Core.Quantification.MU3 q = (Core.Quantification.ScopeUpwardMono q → Core.Quantification.Smooth q)

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

MU4: All simple Mon↓ determiners are co-smooth. @cite{peters-westerstahl-2006} §5.8 Universal 4.

Equations

• Core.Quantification.MU4 q = (Core.Quantification.ScopeDownwardMono q → Core.Quantification.CoSmooth q)

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

QUANT (Isomorphism closure): Q is invariant under permutations of the domain. Model-agnostic version: Q(A,B) depends only on the pointwise pattern, not on which specific elements satisfy A and B.

This is the type ⟨1,1⟩ (binary) generalization of @cite{mostowski-1957}'s permutation invariance. Mostowski's original condition applies to type ⟨1⟩ (unary) quantifiers; the extension to binary determiners is due to @cite{van-benthem-1984} (building on Lindström 1966).

The model-specific version in Semantics.Quantification.Quantifier.Quantity uses cardinalities directly, which requires FiniteModel. This version captures the same intuition without model infrastructure.

@cite{van-benthem-1984} §2: CONSERV + QUANT together reduce Q's behavior to pairs (a, b) where a = |A \ B| and b = |A ∩ B|.

Equations

• Core.Quantification.QuantityInvariant q = ∀ (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')

def Core.Quantification.outerNeg {α : Type u_1} (q : GQ α) : GQ α

Outer negation: (~Q)(A,B) = ¬Q(A,B) (B&C §4.11). Example: ~every = not-every ("Not every student passed").

Equations

• Core.Quantification.outerNeg q R S = ¬q R S

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

Inner negation: (Q~)(A,B) = Q(A, ¬B) (B&C §4.11). Example: every~ = every...not ("Every student didn't pass").

Equations

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

def Core.Quantification.dualQ {α : Type u_1} (q : GQ α) : GQ α

Dual: Q̌ = ~(Q~) = ¬Q(A, ¬B) (B&C §4.11). Example: every̌ = some, somě = every.

Equations

• Core.Quantification.dualQ q = Core.Quantification.outerNeg (Core.Quantification.innerNeg q)

def Core.Quantification.gqMeet {α : Type u_1} (f g : GQ α) : GQ α

Meet of two GQ denotations: (f ∧ g)(A,B) = f(A,B) ∧ g(A,B). K&S (20): conjunction of dets, e.g., "both John's and Mary's". Also: "between n and m" = (at least n) ∧ (at most m).

Equations

• Core.Quantification.gqMeet f g R S = (f R S ∧ g R S)

def Core.Quantification.gqJoin {α : Type u_1} (f g : GQ α) : GQ α

Join of two GQ denotations: (f ∨ g)(A,B) = f(A,B) ∨ g(A,B). K&S (24): disjunction of dets, e.g., "either John's or Mary's".

Equations

• Core.Quantification.gqJoin f g R S = (f R S ∨ g R S)

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

Restriction of a GQ by a restricting function (adjective/relative clause). K&S (66): h_f(s) = h(f(s)). In our representation, the adjective narrows the restrictor: "tall student" = student ∧ tall.

Equations

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

@[reducible, inline]

abbrev Core.Quantification.NPQ (α : Type u_2) : Type u_2

NP denotation (type ⟨1⟩): a property of properties. This is the model-agnostic version of Ty.ett from TypeShifting.lean. P&W §2.1: an NP like "every student" denotes a set of sets.

Equations

• Core.Quantification.NPQ α = ((α → Prop) → Prop)

def Core.Quantification.restrict {α : Type u_1} (q : GQ α) (A : α → Prop) : NPQ α

Restriction: given a GQ Q and restrictor A, produce the type ⟨1⟩ quantifier Q^[A] (P&W §3.2.2). restrict Q A B = Q A B.

Equations

• Core.Quantification.restrict q A = q A

def Core.Quantification.LivesOn {α : Type u_1} (Q : NPQ α) (A : α → Prop) : Prop

A type ⟨1⟩ quantifier Q "lives on" A iff Q(B) ↔ Q(A ∩ B) for all B. P&W §3.2.2: the restricted quantifier depends only on elements of A.

Equations

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

def Core.Quantification.individual {α : Type u_1} (a : α) : NPQ α

Montagovian individual: the type ⟨1⟩ quantifier I_a = {X : a ∈ X}. P&W §3.2.3: an entity lifts to the principal ultrafilter it generates.

Equations

• Core.Quantification.individual a P = P a

theorem Core.Quantification.scopeUpMono_iff_monotone {α : Type u_1} (q : GQ α) : ScopeUpwardMono q ↔ ∀ (R : α → Prop), Monotone (q R)

ScopeUpwardMono q is ∀ R, Monotone (q R) under the Pi-of-Prop ordering (where S ≤ S' is ∀ x, S x → S' x and Prop-valued ≤ is implication). This bridges GQ-level monotonicity to Mathlib's Monotone, which is what Polarity.lean uses (IsUpwardEntailing = Monotone).

theorem Core.Quantification.scopeDownMono_iff_antitone {α : Type u_1} (q : GQ α) : ScopeDownwardMono q ↔ ∀ (R : α → Prop), Antitone (q R)

ScopeDownwardMono q is ∀ R, Antitone (q R) under the Pi-of-Prop ordering.