Quantifier Domain Restriction

[RS24a] [CV95] [Pre98] [SGS00] [vF94] [BC81]

[RS24a]: Default Domain Restriction Possibilities. Semantics & Pragmatics 17, Article 13: 1–49.

Core Idea

Quantifier domains are restricted by a contextual predicate C that intersects the restrictor: ⟦every⟧_C(R)(S) = ∀x. C(x) ∧ R(x) → S(x). Ritchie & Schiller argue that existing accounts of domain restriction — rational pragmatic (§2.1), discourse-structural (§2.2), and intentionalist (§2.3) — fail to explain why certain restrictions are defaults. Their proposal (§3): cognitive heuristics (perceptual availability, salience, manipulability) generate a structured set of default domain restriction possibilities (DDRPs) that pragmatic reasoning then selects among.

Nested Spatial Regions

The cognitive heuristic account is grounded in ecological psychology's parsing of space into nested regions. [CV95] distinguish three zones (personal, action, vista); [Pre98] proposes four (peripersonal, focal extrapersonal, action extrapersonal, ambient extrapersonal). We adopt a hybrid terminology with four levels:

peripersonal ⊆ action ⊆ vista ⊆ unrestricted

Each region induces a predicate on entities, yielding a partially ordered set of candidate domain restrictions. Pragmatic reasoning selects among them.

Connection to Conservativity

Domain restriction via C-intersection is well-defined because all natural language determiners are conservative: Q(R, S) = Q(R, R ∩ S). Combined with Extension (spectator irrelevance), restricting the domain to entities satisfying C is equivalent to restricting the restrictor to C ∩ R.

Domain-restricted quantifiers

@[reducible, inline]

abbrev Quantification.DomainRestriction.DomainRestrictor (E : Type u_1) : Type u_1

A domain restrictor is a predicate selecting contextually relevant entities.

Equations

• Quantification.DomainRestriction.DomainRestrictor E = Set E

def Quantification.DomainRestriction.every_restricted {α : Type u_1} (C : DomainRestrictor α) (R S : α → Prop) : Prop

Domain-restricted ⟦every⟧: ∀x. C(x) ∧ R(x) → S(x). Restricts the quantifier domain to entities satisfying C.

Equations

• Quantification.DomainRestriction.every_restricted C R S = Quantification.every_sem (fun (x : α) => C x ∧ R x) S

def Quantification.DomainRestriction.some_restricted {α : Type u_1} (C : DomainRestrictor α) (R S : α → Prop) : Prop

Domain-restricted ⟦some⟧: ∃x. C(x) ∧ R(x) ∧ S(x).

Equations

• Quantification.DomainRestriction.some_restricted C R S = Quantification.some_sem (fun (x : α) => C x ∧ R x) S

def Quantification.DomainRestriction.no_restricted {α : Type u_1} (C : DomainRestrictor α) (R S : α → Prop) : Prop

Domain-restricted ⟦no⟧: ¬∃x. C(x) ∧ R(x) ∧ S(x).

Equations

• Quantification.DomainRestriction.no_restricted C R S = Quantification.no_sem (fun (x : α) => C x ∧ R x) S

Unrestricted recovery

theorem Quantification.DomainRestriction.every_unrestricted {α : Type u_1} (R S : α → Prop) : every_restricted (fun (x : α) => True) R S = every_sem R S

Unrestricted domain recovers the standard quantifier: ⟦every⟧{λ.True}(R)(S) = ⟦every⟧(R)(S).

theorem Quantification.DomainRestriction.some_unrestricted {α : Type u_1} (R S : α → Prop) : some_restricted (fun (x : α) => True) R S = some_sem R S

⟦some⟧{λ.True}(R)(S) = ⟦some⟧(R)(S).

theorem Quantification.DomainRestriction.no_unrestricted {α : Type u_1} (R S : α → Prop) : no_restricted (fun (x : α) => True) R S = no_sem R S

⟦no⟧{λ.True}(R)(S) = ⟦no⟧(R)(S).

Restrictor monotonicity

theorem Quantification.DomainRestriction.every_restricted_anti_mono {α : Type u_1} [Fintype α] [DecidableEq α] {C C' : DomainRestrictor α} {R S : α → Prop} (hCC' : ∀ (x : α), C x → C' x) (h : every_restricted C' R S) : every_restricted C R S

Smaller domain makes ⟦every⟧ easier to satisfy (restrictor ↓MON). If C ⊆ C' and every_C'(R)(S), then every_C(R)(S): fewer entities to check means the universal is weaker.

theorem Quantification.DomainRestriction.some_restricted_mono {α : Type u_1} [Fintype α] [DecidableEq α] {C C' : DomainRestrictor α} {R S : α → Prop} (hCC' : ∀ (x : α), C x → C' x) (h : some_restricted C R S) : some_restricted C' R S

Larger domain makes ⟦some⟧ easier to satisfy (restrictor ↑MON). Dual of every_restricted_anti_mono: more entities to check means more chances to find a witness.

theorem Quantification.DomainRestriction.no_restricted_anti_mono {α : Type u_1} [Fintype α] [DecidableEq α] {C C' : DomainRestrictor α} {R S : α → Prop} (hCC' : ∀ (x : α), C x → C' x) (h : no_restricted C' R S) : no_restricted C R S

Smaller domain makes ⟦no⟧ easier to satisfy (restrictor ↓MON). Like ⟦every⟧, ⟦no⟧ is anti-monotone in the restrictor: fewer entities to check means fewer chances for a counterexample.

Conservativity connection

theorem Quantification.DomainRestriction.every_restricted_conservative {α : Type u_1} (C : DomainRestrictor α) (R S : α → Prop) : every_restricted C R S ↔ every_restricted C R fun (x : α) => R x ∧ S x

Domain-restricted ⟦every⟧ is conservative: ⟦every⟧_C(R, S) ↔ ⟦every⟧_C(R, R ∧ S). Domain restriction preserves the fundamental GQ property. This is the formal justification for the every_restricted definition: conservativity guarantees that restricting the restrictor to C ∩ R preserves the quantifier's meaning.

theorem Quantification.DomainRestriction.every_restricted_spectator {α : Type u_1} {C : DomainRestrictor α} {R S S' : α → Prop} (h : ∀ (x : α), C x → R x → (S x ↔ S' x)) : every_restricted C R S ↔ every_restricted C R S'

Spectator irrelevance for domain restriction: entities outside C ∩ R don't affect ⟦every⟧_C(R, S). If S and S' agree on all entities satisfying both C and R, the restricted quantifier gives the same result. This formalizes the intuition that domain restriction makes irrelevant entities invisible to the quantifier.

theorem Quantification.DomainRestriction.conservative_domain_restricted {E : Type u_1} {Q : GQ E} {C : DomainRestrictor E} (hQ : Conservative Q) : Conservative fun (R S : E → Prop) => Q (fun (x : E) => C x ∧ R x) S

Conservativity is preserved under domain restriction: if Q is conservative, then Q restricted by any domain predicate C is also conservative. Generalizes every_restricted_conservative from every_sem to any conservative GQ. This is the formal justification for the DDRP infrastructure: [BC81]'s conservativity universal guarantees that C-intersection preserves the fundamental GQ property.

Spatial scale and DDRP

inductive Quantification.DomainRestriction.SpatialScale : Type

Spatial scales from ecological psychology.

[CV95] distinguish three zones (personal, action, vista). [Pre98] proposes four (peripersonal, focal extrapersonal, action extrapersonal, ambient extrapersonal). We adopt a hybrid:

• Peripersonal: Within arm's reach (~2m). Direct manipulation.
• Action: Accessible by locomotion (~30m).
• Vista: Visible panorama. Perception without action affordances.
• Unrestricted: The entire universe (degenerate case, no spatial constraint).

• peripersonal : SpatialScale
• action : SpatialScale
• vista : SpatialScale
• unrestricted : SpatialScale

@[implicit_reducible]

instance Quantification.DomainRestriction.instDecidableEqSpatialScale : DecidableEq SpatialScale

Equations

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

@[implicit_reducible]

instance Quantification.DomainRestriction.instReprSpatialScale : Repr SpatialScale

Equations

• Quantification.DomainRestriction.instReprSpatialScale = { reprPrec := Quantification.DomainRestriction.instReprSpatialScale.repr }

def Quantification.DomainRestriction.instReprSpatialScale.repr : SpatialScale → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Quantification.DomainRestriction.instInhabitedSpatialScale : Inhabited SpatialScale

Equations

• Quantification.DomainRestriction.instInhabitedSpatialScale = { default := Quantification.DomainRestriction.instInhabitedSpatialScale.default }

@[implicit_reducible]

instance Quantification.DomainRestriction.instFintypeSpatialScale : Fintype SpatialScale

Equations

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

def Quantification.DomainRestriction.SpatialScale.toFin : SpatialScale → Fin 4

Rank embedding for the linear order on SpatialScale.

Equations

• Quantification.DomainRestriction.SpatialScale.peripersonal.toFin = 0
• Quantification.DomainRestriction.SpatialScale.action.toFin = 1
• Quantification.DomainRestriction.SpatialScale.vista.toFin = 2
• Quantification.DomainRestriction.SpatialScale.unrestricted.toFin = 3

@[implicit_reducible]

instance Quantification.DomainRestriction.instLinearOrderSpatialScale : LinearOrder SpatialScale

peripersonal < action < vista < unrestricted.

Equations

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

@[implicit_reducible]

instance Quantification.DomainRestriction.instOrderTopSpatialScale : OrderTop SpatialScale

Equations

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

@[implicit_reducible]

instance Quantification.DomainRestriction.instOrderBotSpatialScale : OrderBot SpatialScale

Equations

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

structure Quantification.DomainRestriction.DDRP (S : Type u_1) (E : Type u_2) [Preorder S] [OrderTop S] : Type (max u_1 u_2)

Default Domain Restriction Possibilities (DDRPs) — a monotone family of candidate domain restrictors indexed by an ordered scale, with the top of the scale unrestricted.

Given a perceptual scene, cognitive heuristics generate nested spatial regions that induce candidate domain restrictors. The nesting reflects physical containment: what is within reach is also within walking distance, which is also within view.

Parameterized by a scale type S with a preorder and top element, enabling reuse for non-spatial heuristics. SpatialScale is the canonical instantiation; the same nesting structure is instantiated by ASL signing height (HeightDDRP, [DG22]) and comparison class inference ([TG22]).

• region : S → Set E

  Each scale level induces a candidate restrictor on the domain.

• monotone : Monotone self.region

  Nesting: smaller scale ⊆ larger scale.

• top_total : self.region ⊤ = Set.univ

  The top scale is unrestricted.

noncomputable def Quantification.DomainRestriction.DDRP.candidates {S : Type u_1} {E : Type u_2} [Preorder S] [OrderTop S] [Fintype S] (d : DDRP S E) : List (S × DomainRestrictor E)

The candidate domain restrictors: one per scale level. DDRPs constrain the candidate set to a small, structured menu — not the set of all possible predicates (contra pure pragmatic approaches).

Equations

• d.candidates = List.map (fun (s : S) => (s, d.region s)) Fintype.elems.val.toList

DDRP nesting theorems

theorem Quantification.DomainRestriction.DDRP.every_nesting {S : Type u_1} [Preorder S] [OrderTop S] {α : Type u_2} [Fintype α] [DecidableEq α] (d : DDRP S α) (R Sc : α → Prop) {s₁ s₂ : S} (h : s₁ ≤ s₂) : every_restricted (d.region s₂) R Sc → every_restricted (d.region s₁) R Sc

General ⟦every⟧ nesting: truth under a larger scale entails truth under any smaller scale. Subsumes all specific nesting theorems for ⟦every⟧. Follows from restrictor ↓MON of ⟦every⟧ + DDRP monotonicity.

theorem Quantification.DomainRestriction.DDRP.some_nesting {S : Type u_1} [Preorder S] [OrderTop S] {α : Type u_2} [Fintype α] [DecidableEq α] (d : DDRP S α) (R Sc : α → Prop) {s₁ s₂ : S} (h : s₁ ≤ s₂) : some_restricted (d.region s₁) R Sc → some_restricted (d.region s₂) R Sc

General ⟦some⟧ nesting (reversed direction): truth under a smaller scale entails truth under any larger scale. Dual of every_nesting. Follows from restrictor ↑MON of ⟦some⟧ + DDRP monotonicity.

theorem Quantification.DomainRestriction.DDRP.no_nesting {S : Type u_1} [Preorder S] [OrderTop S] {α : Type u_2} [Fintype α] [DecidableEq α] (d : DDRP S α) (R Sc : α → Prop) {s₁ s₂ : S} (h : s₁ ≤ s₂) : no_restricted (d.region s₂) R Sc → no_restricted (d.region s₁) R Sc

General ⟦no⟧ nesting: truth under a larger scale entails truth under any smaller scale. Same direction as ⟦every⟧ (both are restrictor ↓MON). Follows from restrictor ↓MON of ⟦no⟧ + DDRP monotonicity.