Quantifier Domain Restriction

@cite{ritchie-schiller-2024} @cite{cutting-vishton-1995} @cite{previc-1998} @cite{stanley-szab-2000} @cite{von-fintel-1994} @cite{barwise-cooper-1981}

@cite{ritchie-schiller-2024}: 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. @cite{cutting-vishton-1995} distinguish three zones (personal, action, vista); @cite{previc-1998} 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.

@[reducible, inline]

abbrev Semantics.Lexical.Determiner.DomainRestriction.DomainRestrictor (E : Type u_1) : Type u_1

A domain restrictor is a predicate selecting contextually relevant entities.

Equations

• Semantics.Lexical.Determiner.DomainRestriction.DomainRestrictor E = (E → Bool)

def Semantics.Lexical.Determiner.DomainRestriction.every_restricted (m : Montague.Model) [Fintype m.Entity] (C : DomainRestrictor m.Entity) (R S : m.Entity → Bool) : Bool

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

Equations

• Semantics.Lexical.Determiner.DomainRestriction.every_restricted m C R S = Semantics.Lexical.Determiner.Quantifier.every_sem m (fun (x : m.interpTy Semantics.Montague.Ty.e) => C x && R x) S

def Semantics.Lexical.Determiner.DomainRestriction.some_restricted (m : Montague.Model) [Fintype m.Entity] (C : DomainRestrictor m.Entity) (R S : m.Entity → Bool) : Bool

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

Equations

• Semantics.Lexical.Determiner.DomainRestriction.some_restricted m C R S = Semantics.Lexical.Determiner.Quantifier.some_sem m (fun (x : m.interpTy Semantics.Montague.Ty.e) => C x && R x) S

def Semantics.Lexical.Determiner.DomainRestriction.no_restricted (m : Montague.Model) [Fintype m.Entity] (C : DomainRestrictor m.Entity) (R S : m.Entity → Bool) : Bool

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

Equations

• Semantics.Lexical.Determiner.DomainRestriction.no_restricted m C R S = Semantics.Lexical.Determiner.Quantifier.no_sem m (fun (x : m.interpTy Semantics.Montague.Ty.e) => C x && R x) S

theorem Semantics.Lexical.Determiner.DomainRestriction.every_unrestricted {m : Montague.Model} [Fintype m.Entity] (R S : m.Entity → Bool) : every_restricted m (fun (x : m.Entity) => true) R S = Quantifier.every_sem m R S

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

theorem Semantics.Lexical.Determiner.DomainRestriction.some_unrestricted {m : Montague.Model} [Fintype m.Entity] (R S : m.Entity → Bool) : some_restricted m (fun (x : m.Entity) => true) R S = Quantifier.some_sem m R S

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

theorem Semantics.Lexical.Determiner.DomainRestriction.no_unrestricted {m : Montague.Model} [Fintype m.Entity] (R S : m.Entity → Bool) : no_restricted m (fun (x : m.Entity) => true) R S = Quantifier.no_sem m R S

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

theorem Semantics.Lexical.Determiner.DomainRestriction.every_restricted_anti_mono {m : Montague.Model} [Fintype m.Entity] {C C' : DomainRestrictor m.Entity} {R S : m.Entity → Bool} (hCC' : ∀ (x : m.Entity), C x = true → C' x = true) (h : every_restricted m C' R S = true) : every_restricted m C R S = true

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 Semantics.Lexical.Determiner.DomainRestriction.some_restricted_mono {m : Montague.Model} [Fintype m.Entity] {C C' : DomainRestrictor m.Entity} {R S : m.Entity → Bool} (hCC' : ∀ (x : m.Entity), C x = true → C' x = true) (h : some_restricted m C R S = true) : some_restricted m C' R S = true

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 Semantics.Lexical.Determiner.DomainRestriction.no_restricted_anti_mono {m : Montague.Model} [Fintype m.Entity] {C C' : DomainRestrictor m.Entity} {R S : m.Entity → Bool} (hCC' : ∀ (x : m.Entity), C x = true → C' x = true) (h : no_restricted m C' R S = true) : no_restricted m C R S = true

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.

theorem Semantics.Lexical.Determiner.DomainRestriction.every_restricted_conservative {m : Montague.Model} [Fintype m.Entity] (C : DomainRestrictor m.Entity) (R S : m.Entity → Bool) : every_restricted m C R S = every_restricted m C R fun (x : m.Entity) => 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 Semantics.Lexical.Determiner.DomainRestriction.every_restricted_spectator {m : Montague.Model} [Fintype m.Entity] {C : DomainRestrictor m.Entity} {R S S' : m.Entity → Bool} (h : ∀ (x : m.Entity), C x = true → R x = true → S x = S' x) : every_restricted m C R S = every_restricted m 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 Semantics.Lexical.Determiner.DomainRestriction.conservative_domain_restricted {E : Type u_1} {Q : Core.Quantification.GQ E} {C : DomainRestrictor E} (hQ : Core.Quantification.Conservative Q) : Core.Quantification.Conservative fun (R S : E → Bool) => 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: @cite{barwise-cooper-1981}'s conservativity universal guarantees that C-intersection preserves the fundamental GQ property.

inductive Semantics.Lexical.Determiner.DomainRestriction.SpatialScale : Type

Spatial scales from ecological psychology.

@cite{cutting-vishton-1995} distinguish three zones (personal, action, vista). @cite{previc-1998} 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

instance Semantics.Lexical.Determiner.DomainRestriction.instDecidableEqSpatialScale : DecidableEq SpatialScale

Equations

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

instance Semantics.Lexical.Determiner.DomainRestriction.instBEqSpatialScale : BEq SpatialScale

Equations

• Semantics.Lexical.Determiner.DomainRestriction.instBEqSpatialScale = { beq := Semantics.Lexical.Determiner.DomainRestriction.instBEqSpatialScale.beq }

def Semantics.Lexical.Determiner.DomainRestriction.instBEqSpatialScale.beq : SpatialScale → SpatialScale → Bool

Equations

• Semantics.Lexical.Determiner.DomainRestriction.instBEqSpatialScale.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Determiner.DomainRestriction.instReprSpatialScale : Repr SpatialScale

Equations

• Semantics.Lexical.Determiner.DomainRestriction.instReprSpatialScale = { reprPrec := Semantics.Lexical.Determiner.DomainRestriction.instReprSpatialScale.repr }

def Semantics.Lexical.Determiner.DomainRestriction.instReprSpatialScale.repr : SpatialScale → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Determiner.DomainRestriction.instInhabitedSpatialScale : Inhabited SpatialScale

Equations

• Semantics.Lexical.Determiner.DomainRestriction.instInhabitedSpatialScale = { default := Semantics.Lexical.Determiner.DomainRestriction.instInhabitedSpatialScale.default }

def Semantics.Lexical.Determiner.DomainRestriction.instInhabitedSpatialScale.default : SpatialScale

Equations

• Semantics.Lexical.Determiner.DomainRestriction.instInhabitedSpatialScale.default = Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal

instance Semantics.Lexical.Determiner.DomainRestriction.instFintypeSpatialScale : Fintype SpatialScale

Equations

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

def Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.toFin : SpatialScale → Fin 4

Rank embedding for the linear order on SpatialScale.

Equations

• Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal.toFin = 0
• Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action.toFin = 1
• Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.vista.toFin = 2
• Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.unrestricted.toFin = 3

instance Semantics.Lexical.Determiner.DomainRestriction.instLinearOrderSpatialScale : LinearOrder SpatialScale

peripersonal < action < vista < unrestricted.

Equations

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

instance Semantics.Lexical.Determiner.DomainRestriction.instOrderTopSpatialScale : OrderTop SpatialScale

Equations

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

instance Semantics.Lexical.Determiner.DomainRestriction.instOrderBotSpatialScale : OrderBot SpatialScale

Equations

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

@[reducible, inline]

abbrev Semantics.Lexical.Determiner.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).

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.

Now an alias for Core.NestedRestriction.NestedRestriction, which extracts the shared nesting structure used by both domain restriction and comparison class inference.

Equations

• Semantics.Lexical.Determiner.DomainRestriction.DDRP S E = Core.NestedRestriction S E

noncomputable def Semantics.Lexical.Determiner.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

theorem Semantics.Lexical.Determiner.DomainRestriction.DDRP.every_nesting {S : Type u_1} [Preorder S] [OrderTop S] {m : Montague.Model} [Fintype m.Entity] (d : DDRP S m.Entity) (R Sc : m.Entity → Bool) {s₁ s₂ : S} (h : s₁ ≤ s₂) : every_restricted m (d.region s₂) R Sc = true → every_restricted m (d.region s₁) R Sc = true

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 Semantics.Lexical.Determiner.DomainRestriction.DDRP.some_nesting {S : Type u_1} [Preorder S] [OrderTop S] {m : Montague.Model} [Fintype m.Entity] (d : DDRP S m.Entity) (R Sc : m.Entity → Bool) {s₁ s₂ : S} (h : s₁ ≤ s₂) : some_restricted m (d.region s₁) R Sc = true → some_restricted m (d.region s₂) R Sc = true

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 Semantics.Lexical.Determiner.DomainRestriction.DDRP.no_nesting {S : Type u_1} [Preorder S] [OrderTop S] {m : Montague.Model} [Fintype m.Entity] (d : DDRP S m.Entity) (R Sc : m.Entity → Bool) {s₁ s₂ : S} (h : s₁ ≤ s₂) : no_restricted m (d.region s₂) R Sc = true → no_restricted m (d.region s₁) R Sc = true

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.