Documentation

Linglib.Studies.RitchieSchiller2024

[RS24a] — Default Domain Restriction Possibilities #

[RS24a] [CV95] [BJEST17] [Cla96] [Sta02]

Ritchie, K. & Schiller, H. (2024). Default Domain Restriction Possibilities. Semantics & Pragmatics 17, Article 13: 1–49.

The Argument #

When a speaker says "Every bottle is empty" at a dinner party, the hearer restricts the quantifier domain to contextually relevant bottles — not all bottles in the universe (R&S §1, ex. 3). Ritchie & Schiller argue that existing accounts fail to explain why certain restrictions are defaults:

Rational pragmatic (§2.1): RSA/Gricean reasoning doesn't explain default status
Discourse-structural (§2.2): QUD-based accounts are too demanding
Intentionalist (§2.3): speaker-intention accounts are too unconstrained

Their positive proposal (§3): cognitive heuristics — perceptual availability, salience, and manipulability — generate a structured set of default domain restriction possibilities (DDRPs). These are grounded in spatial cognition, where nested spatial regions provide a natural ordering on candidate restrictions.

Scenario #

We construct an illustrative scenario (not from the paper) with 4 entities at increasing spatial distances and 3 world states, then verify key formal consequences of the DDRP framework for both ⟦every⟧ (↓MON) and ⟦some⟧ (↑MON).

Compositional Grounding #

Truth conditions derive from every_restricted / some_restricted (DomainRestriction.lean), which wrap every_sem / some_sem (Quantifier.lean) with a domain restrictor predicate. Nesting theorems derive from DDRP.every_nesting / DDRP.some_nesting, connecting the nested spatial regions to restrictor monotonicity.

RSA Connection #

While R&S argue against RSA as explaining default status (§2.1), DDRPs are compatible with RSA as the selection mechanism: the listener reasons over candidate DDRPs (the latent SpatialScale in the joint posterior) to infer which domain restriction the speaker intended. With a cognitive-default prior biasing toward peripersonal scales, the pragmatic listener's latent marginal infers the proximal restriction (§8). Predictions are checked by exact PMF evaluation on the RSA.Canonical pipeline.

inductive RitchieSchiller2024.Entity :

Entities in the constructed scene: 4 bottles at increasing spatial distances.

b1 : Entity
b2 : Entity
b3 : Entity
b4 : Entity

Instances For

@[implicit_reducible]

instance RitchieSchiller2024.instDecidableEqEntity :

DecidableEq Entity

Equations

RitchieSchiller2024.instDecidableEqEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RitchieSchiller2024.instReprEntity.repr :

Entity → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance RitchieSchiller2024.instReprEntity :

Equations

RitchieSchiller2024.instReprEntity = { reprPrec := RitchieSchiller2024.instReprEntity.repr }

@[implicit_reducible]

instance RitchieSchiller2024.instInhabitedEntity :

Inhabited Entity

Equations

RitchieSchiller2024.instInhabitedEntity = { default := RitchieSchiller2024.instInhabitedEntity.default }

@[implicit_reducible]

instance RitchieSchiller2024.instFintypeEntity :

Fintype Entity

Equations

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

def RitchieSchiller2024.SpatialScene (E : Type u_1) :

Type u_1

A spatial scene: each entity occupies a spatial zone.

Equations

RitchieSchiller2024.SpatialScene E = (E → Quantification.DomainRestriction.SpatialScale)

Instances For

def RitchieSchiller2024.sceneToDDRP {E : Type u_1} (scene : SpatialScene E) :

Quantification.DomainRestriction.DDRP Quantification.DomainRestriction.SpatialScale E

A spatial scene induces a DDRP: region s contains entities in zone ≤ s. Monotonicity and top-totality follow from the ordering on SpatialScale.

Equations

RitchieSchiller2024.sceneToDDRP scene = { region := fun (s : Quantification.DomainRestriction.SpatialScale) (e : E) => scene e ≤ s, monotone := ⋯, top_total := ⋯ }

Instances For

def RitchieSchiller2024.dinnerScene :

SpatialScene Entity

The dinner-party scene: b1,b2 peripersonal, b3 action, b4 vista.

Equations

Instances For

@[reducible, inline]

abbrev RitchieSchiller2024.sceneDDRP :

Quantification.DomainRestriction.DDRP Quantification.DomainRestriction.SpatialScale Entity

DDRP for the bottle scenario, derived from the spatial scene. Peripersonal ⊆ action ⊆ vista (= unrestricted in this indoor scene).

Equations

RitchieSchiller2024.sceneDDRP = RitchieSchiller2024.sceneToDDRP RitchieSchiller2024.dinnerScene

Instances For

inductive RitchieSchiller2024.World :

World states: which bottles are empty.

nearEmpty: only proximal bottles (b1, b2) are empty
midEmpty: proximal + action-space bottles (b1, b2, b3) are empty
allEmpty: all bottles are empty

nearEmpty : World
midEmpty : World
allEmpty : World

Instances For

@[implicit_reducible]

instance RitchieSchiller2024.instDecidableEqWorld :

DecidableEq World

Equations

RitchieSchiller2024.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance RitchieSchiller2024.instReprWorld :

Repr World

Equations

RitchieSchiller2024.instReprWorld = { reprPrec := RitchieSchiller2024.instReprWorld.repr }

def RitchieSchiller2024.instReprWorld.repr :

World → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance RitchieSchiller2024.instInhabitedWorld :

Inhabited World

Equations

RitchieSchiller2024.instInhabitedWorld = { default := RitchieSchiller2024.instInhabitedWorld.default }

@[implicit_reducible]

instance RitchieSchiller2024.instFintypeWorld :

Fintype World

Equations

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

def RitchieSchiller2024.emptyIn :

World → Entity → Bool

Equations

Instances For

def RitchieSchiller2024.isBottle :

Entity → Bool

All entities are bottles in this scenario (trivial restrictor).

Equations

RitchieSchiller2024.isBottle x✝ = true

Instances For

@[reducible, inline]

abbrev RitchieSchiller2024.everyBottleEmpty (scale : Quantification.DomainRestriction.SpatialScale) (w : World) :

Truth of "every bottle is empty" under a given spatial domain restriction. For all entities in the DDRP region that are bottles, they must be empty.

Equations

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

Instances For

theorem RitchieSchiller2024.w_near_peri :

everyBottleEmpty Quantification.DomainRestriction.SpatialScale.peripersonal World.nearEmpty

theorem RitchieSchiller2024.w_near_action :

¬everyBottleEmpty Quantification.DomainRestriction.SpatialScale.action World.nearEmpty

theorem RitchieSchiller2024.w_near_vista :

¬everyBottleEmpty Quantification.DomainRestriction.SpatialScale.vista World.nearEmpty

theorem RitchieSchiller2024.w_mid_peri :

everyBottleEmpty Quantification.DomainRestriction.SpatialScale.peripersonal World.midEmpty

theorem RitchieSchiller2024.w_mid_action :

everyBottleEmpty Quantification.DomainRestriction.SpatialScale.action World.midEmpty

theorem RitchieSchiller2024.w_mid_vista :

¬everyBottleEmpty Quantification.DomainRestriction.SpatialScale.vista World.midEmpty

theorem RitchieSchiller2024.w_all_peri :

everyBottleEmpty Quantification.DomainRestriction.SpatialScale.peripersonal World.allEmpty

theorem RitchieSchiller2024.w_all_action :

everyBottleEmpty Quantification.DomainRestriction.SpatialScale.action World.allEmpty

theorem RitchieSchiller2024.w_all_vista :

everyBottleEmpty Quantification.DomainRestriction.SpatialScale.vista World.allEmpty

@[reducible, inline]

abbrev RitchieSchiller2024.someBottleEmpty (scale : Quantification.DomainRestriction.SpatialScale) (w : World) :

Truth of "some bottle is empty" under a given spatial domain restriction. Some entity in the DDRP region that is a bottle must be empty.

Equations

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

Instances For

theorem RitchieSchiller2024.some_near_peri :

someBottleEmpty Quantification.DomainRestriction.SpatialScale.peripersonal World.nearEmpty

theorem RitchieSchiller2024.some_near_action :

someBottleEmpty Quantification.DomainRestriction.SpatialScale.action World.nearEmpty

theorem RitchieSchiller2024.some_near_vista :

someBottleEmpty Quantification.DomainRestriction.SpatialScale.vista World.nearEmpty

theorem RitchieSchiller2024.some_mid_peri :

someBottleEmpty Quantification.DomainRestriction.SpatialScale.peripersonal World.midEmpty

theorem RitchieSchiller2024.some_mid_action :

someBottleEmpty Quantification.DomainRestriction.SpatialScale.action World.midEmpty

theorem RitchieSchiller2024.some_mid_vista :

someBottleEmpty Quantification.DomainRestriction.SpatialScale.vista World.midEmpty

theorem RitchieSchiller2024.some_all_peri :

someBottleEmpty Quantification.DomainRestriction.SpatialScale.peripersonal World.allEmpty

theorem RitchieSchiller2024.some_all_action :

someBottleEmpty Quantification.DomainRestriction.SpatialScale.action World.allEmpty

theorem RitchieSchiller2024.some_all_vista :

someBottleEmpty Quantification.DomainRestriction.SpatialScale.vista World.allEmpty

theorem RitchieSchiller2024.proximal_default :

everyBottleEmpty Quantification.DomainRestriction.SpatialScale.peripersonal World.nearEmpty ∧ ¬everyBottleEmpty Quantification.DomainRestriction.SpatialScale.action World.nearEmpty ∧ ¬everyBottleEmpty Quantification.DomainRestriction.SpatialScale.vista World.nearEmpty

Proximal default: In the proximal world, only peripersonal restriction makes "every bottle is empty" true. The listener must infer the speaker intended the proximal domain — no other DDRP candidate works.

theorem RitchieSchiller2024.monotonicity_contrast :

everyBottleEmpty Quantification.DomainRestriction.SpatialScale.peripersonal World.nearEmpty ∧ ¬everyBottleEmpty Quantification.DomainRestriction.SpatialScale.action World.nearEmpty ∧ someBottleEmpty Quantification.DomainRestriction.SpatialScale.peripersonal World.nearEmpty ∧ someBottleEmpty Quantification.DomainRestriction.SpatialScale.action World.nearEmpty ∧ someBottleEmpty Quantification.DomainRestriction.SpatialScale.vista World.nearEmpty

↓MON/↑MON contrast: ⟦every⟧ and ⟦some⟧ react oppositely to domain restriction. In the proximal world, ⟦every⟧ is true only under peripersonal restriction (↓MON: smaller domain helps), while ⟦some⟧ is true under all restrictions (↑MON: larger domain never hurts).

theorem RitchieSchiller2024.every_nesting_prop {s₁ s₂ : Quantification.DomainRestriction.SpatialScale} (h : s₁ ≤ s₂) (R S : Entity → Prop) :

Quantification.DomainRestriction.every_restricted (sceneDDRP.region s₂) R S → Quantification.DomainRestriction.every_restricted (sceneDDRP.region s₁) R S

⟦every⟧ nesting (Prop level): truth under a larger scale entails truth under any smaller scale. Derives from DDRP.every_nesting via restrictor ↓MON.

theorem RitchieSchiller2024.some_nesting_prop {s₁ s₂ : Quantification.DomainRestriction.SpatialScale} (h : s₁ ≤ s₂) (R S : Entity → Prop) :

Quantification.DomainRestriction.some_restricted (sceneDDRP.region s₁) R S → Quantification.DomainRestriction.some_restricted (sceneDDRP.region s₂) R S

⟦some⟧ nesting (Prop level): truth under a smaller scale entails truth under any larger scale. Derives from DDRP.some_nesting via restrictor ↑MON.

[KL93] distinguish domain-precise from domain-vague quantificational restrictions. A DomainRestrictor is the degenerate domain-precise case: a single predicate, hence a single precisification — which is why DDRP-restricted every/no tolerate no exceptions via re-precisification.

def RitchieSchiller2024.vagueOfRestrictor {E : Type u_1} (C : Quantification.DomainRestriction.DomainRestrictor E) :

KadmonLandman1993.VagueRestriction (Set E)

Lift a DomainRestrictor into a trivially precise VagueRestriction: the singleton restriction with itself as the only precisification.

Equations

RitchieSchiller2024.vagueOfRestrictor C = { precise := {C}, precisifications := {{C}}, extends_precise := ⋯, precise_mem := ⋯ }

Instances For

theorem RitchieSchiller2024.restrictor_is_domain_precise {E : Type u_1} (C : Quantification.DomainRestriction.DomainRestrictor E) (apply : Set E → Set E) :

KadmonLandman1993.isDomainPrecise (vagueOfRestrictor C) apply

A restrictor-based vague restriction is domain precise in [KL93]'s sense: one precisification, one domain.

inductive RitchieSchiller2024.Utterance :

Utterance type for the RSA model.

everyEmpty : Utterance
someEmpty : Utterance

Instances For

@[implicit_reducible]

instance RitchieSchiller2024.instDecidableEqUtterance :

DecidableEq Utterance

Equations

RitchieSchiller2024.instDecidableEqUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RitchieSchiller2024.instReprUtterance.repr :

Utterance → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance RitchieSchiller2024.instReprUtterance :

Equations

RitchieSchiller2024.instReprUtterance = { reprPrec := RitchieSchiller2024.instReprUtterance.repr }

@[implicit_reducible]

instance RitchieSchiller2024.instInhabitedUtterance :

Inhabited Utterance

Equations

RitchieSchiller2024.instInhabitedUtterance = { default := RitchieSchiller2024.instInhabitedUtterance.default }

@[implicit_reducible]

instance RitchieSchiller2024.instFintypeUtterance :

Fintype Utterance

Equations

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

def RitchieSchiller2024.utteranceMeaning (scale : Quantification.DomainRestriction.SpatialScale) :

Utterance → World → Bool

Literal meaning under a given DDRP scale (Bool for RSA computation).

Equations

RitchieSchiller2024.utteranceMeaning scale RitchieSchiller2024.Utterance.everyEmpty x✝ = decide (RitchieSchiller2024.everyBottleEmpty scale x✝)
RitchieSchiller2024.utteranceMeaning scale RitchieSchiller2024.Utterance.someEmpty x✝ = decide (RitchieSchiller2024.someBottleEmpty scale x✝)

Instances For

inductive RitchieSchiller2024.CognitiveHeuristic :

R&S §3.2: Three cognitive heuristics collectively determine which domain restrictions are defaults. Each heuristic assigns a relevance score to a spatial scale, reflecting how well entities at that scale satisfy the corresponding cognitive criterion.

availability : CognitiveHeuristic
salience : CognitiveHeuristic
manipulability : CognitiveHeuristic

Instances For

@[implicit_reducible]

instance RitchieSchiller2024.instDecidableEqCognitiveHeuristic :

DecidableEq CognitiveHeuristic

Equations

RitchieSchiller2024.instDecidableEqCognitiveHeuristic x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def RitchieSchiller2024.instReprCognitiveHeuristic.repr :

CognitiveHeuristic → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance RitchieSchiller2024.instReprCognitiveHeuristic :

Repr CognitiveHeuristic

Equations

RitchieSchiller2024.instReprCognitiveHeuristic = { reprPrec := RitchieSchiller2024.instReprCognitiveHeuristic.repr }

def RitchieSchiller2024.heuristicScore :

CognitiveHeuristic → Quantification.DomainRestriction.SpatialScale → ℚ

Heuristic score for each (heuristic, scale) pair.

Availability (R&S §3.2 ¶1): Peripersonal objects are maximally available — perceived without bodily distortion. Action/vista objects are available but require effort. Unrestricted objects may not be present at all.
Salience (R&S §3.2 ¶2): Peripersonal and action-space objects are attention-grabbing. Vista/unrestricted objects are less noticeable.
Manipulability (R&S §3.2 ¶3): Only peripersonal objects afford physical interaction (within arm's reach). All others are out of reach.

Equations

Instances For

theorem RitchieSchiller2024.heuristic_anti_mono (h : CognitiveHeuristic) {s₁ s₂ : Quantification.DomainRestriction.SpatialScale} (hle : s₁ ≤ s₂) :

heuristicScore h s₂ ≤ heuristicScore h s₁

Each heuristic is anti-monotone: more proximal scales score at least as high. This captures R&S's claim that proximity enhances all three cognitive dimensions simultaneously.

def RitchieSchiller2024.ddprPrior (s : Quantification.DomainRestriction.SpatialScale) :

ℚ

Latent prior derived from the three cognitive heuristics. The sum reflects R&S §3.2's conjunction: a good default restriction should score high on availability AND salience AND manipulability. The prior is unnormalized — RSA normalizes via the partition function.

Equations

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

Instances For

theorem RitchieSchiller2024.ddprPrior_anti_mono {s₁ s₂ : Quantification.DomainRestriction.SpatialScale} (h : s₁ ≤ s₂) :

ddprPrior s₂ ≤ ddprPrior s₁

The derived prior is anti-monotone: more proximal scales receive higher prior weight. Follows from anti-monotonicity of each heuristic.

PMF face: shared speaker, cognitive-default vs uniform joint priors #

The two listener variants below differ only in the latent prior, so they share one speaker: the literal listener is uniform on utteranceMeaning scale u's world extension, and the speaker normalises literal informativity over the two utterances (α = 1, no cost).

noncomputable def RitchieSchiller2024.L0 :

Quantification.DomainRestriction.SpatialScale → Utterance → PMF World

Per-scale literal listener: uniform on the utterance's world extension.

Equations

RitchieSchiller2024.L0 = RSA.Canonical.L0OfBool RitchieSchiller2024.utteranceMeaning RitchieSchiller2024.ext_nonempty✝

Instances For

instance RitchieSchiller2024.instViableSpeakerProdWorldSpatialScaleUtterancePowUtilityOfNatNatL0 :

RSA.Canonical.ViableSpeaker (RSA.Canonical.powUtility 1 L0)

noncomputable def RitchieSchiller2024.S :

World × Quantification.DomainRestriction.SpatialScale → PMF Utterance

Shared pragmatic speaker S(w, scale) ∝ L0(w | ·, scale) (α = 1, no cost).

Equations

RitchieSchiller2024.S = RSA.Canonical.S1 (RSA.Canonical.powUtility 1 RitchieSchiller2024.L0)

Instances For

Partition sums Z(w, scale) = Σ_u |ext(scale, u)|⁻¹ over the two utterances (extension cards — everyEmpty: peripersonal 3, action 2, vista 1; someEmpty: 3 at every scale): peripersonal 2/3 everywhere; action 1/3 at nearEmpty, else 5/6; vista 1/3 except 4/3 at allEmpty.

Speaker-mass values S(w, scale) u (exact rationals): every — 1/2 at peripersonal, 3/5 at action (mid/all), 3/4 at vista (all), else 0; some — 1/2 at peripersonal, 1, 2/5, 2/5 at action, 1, 1, 1/4 at vista.

Pooled world-sums of speaker mass per scale (the latent-comparison residues): every — peripersonal 3/2, action 6/5, vista 3/4; some — peripersonal 3/2, action 9/5, vista 9/4.

Listeners #

noncomputable def RitchieSchiller2024.ddprJoint :

PMF (World × Quantification.DomainRestriction.SpatialScale)

Cognitive-default joint prior: uniform over worlds (the constant world factor is absorbed by normalisation), ddprPrior over scales.

Equations

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

Instances For

theorem RitchieSchiller2024.ddpr_marg_every :

PMF.marginal S ddprJoint Utterance.everyEmpty ≠ 0

theorem RitchieSchiller2024.ddpr_marg_some :

PMF.marginal S ddprJoint Utterance.someEmpty ≠ 0

noncomputable def RitchieSchiller2024.ddprListener (u : Utterance) (h : PMF.marginal S ddprJoint u ≠ 0) :

PMF (World × Quantification.DomainRestriction.SpatialScale)

Pragmatic listener over the cognitive-default joint prior.

Equations

RitchieSchiller2024.ddprListener u h = RSA.Canonical.L1 RitchieSchiller2024.S RitchieSchiller2024.ddprJoint u h

Instances For

theorem RitchieSchiller2024.L1_latent_peripersonal_gt_action :

(ddprListener Utterance.everyEmpty ddpr_marg_every).snd Quantification.DomainRestriction.SpatialScale.peripersonal > (ddprListener Utterance.everyEmpty ddpr_marg_every).snd Quantification.DomainRestriction.SpatialScale.action

L1_latent peripersonal > action: The listener infers peripersonal as the most likely intended domain restriction, beating the action-space scale. This captures R&S's core claim: cognitive-default priors biasing toward proximal scales cause the listener to default to the nearest restriction.

theorem RitchieSchiller2024.L1_latent_action_gt_vista :

(ddprListener Utterance.everyEmpty ddpr_marg_every).snd Quantification.DomainRestriction.SpatialScale.action > (ddprListener Utterance.everyEmpty ddpr_marg_every).snd Quantification.DomainRestriction.SpatialScale.vista

L1_latent action > vista: The action scale is preferred over vista, showing the full ordering: peripersonal > action > vista.

theorem RitchieSchiller2024.L1_latent_some_peripersonal_gt_action :

(ddprListener Utterance.someEmpty ddpr_marg_some).snd Quantification.DomainRestriction.SpatialScale.peripersonal > (ddprListener Utterance.someEmpty ddpr_marg_some).snd Quantification.DomainRestriction.SpatialScale.action

For "some bottle is empty", the cognitive-default prior overrides the semantic signal: peripersonal is inferred as the most likely scale despite ⟦some⟧ being true under all scales in all worlds. Without the prior, RSA predicts the WRONG ordering (see uniform_some_distal_wins).

R&S §2.1 argue that RSA alone — without cognitive supplementation — cannot explain why certain domain restrictions are defaults. We verify this by constructing an RSA model with uniform latent priors and showing:

1. For ⟦every⟧ (↓MON), RSA with uniform priors *happens* to predict
   peripersonal as most likely — but only because the literal semantics
   provides discriminative signal (it's false under wider scales in some
   worlds). This is not an explanation of default status.

2. For ⟦some⟧ (↑MON), RSA with uniform priors predicts the *wrong*
   ordering: the listener infers vista/unrestricted as most likely, because
   under wider scales, ⟦some⟧ is the only true utterance in more worlds
   (higher L0 probability). Cognitive-default priors are needed to override
   this semantic signal.

This pair of results formalizes R&S's core negative argument: RSA's
predictions depend on the specific quantifier's monotonicity profile,
not on cognitive structure, so RSA alone doesn't explain the cross-quantifier
generalization that proximal restrictions are always preferred.

theorem RitchieSchiller2024.unif_marg_every :

PMF.marginal S (PMF.uniformOfFintype (World × Quantification.DomainRestriction.SpatialScale)) Utterance.everyEmpty ≠ 0

theorem RitchieSchiller2024.unif_marg_some :

PMF.marginal S (PMF.uniformOfFintype (World × Quantification.DomainRestriction.SpatialScale)) Utterance.someEmpty ≠ 0

noncomputable def RitchieSchiller2024.uniformListener (u : Utterance) (h : PMF.marginal S (PMF.uniformOfFintype (World × Quantification.DomainRestriction.SpatialScale)) u ≠ 0) :

PMF (World × Quantification.DomainRestriction.SpatialScale)

Pragmatic listener with a uniform latent prior (no cognitive bias): same speaker as ddprListener, uniform joint.

Equations

RitchieSchiller2024.uniformListener u h = RSA.Canonical.L1 RitchieSchiller2024.S (PMF.uniformOfFintype (RitchieSchiller2024.World × Quantification.DomainRestriction.SpatialScale)) u h

Instances For

theorem RitchieSchiller2024.uniform_every_still_proximal :

(uniformListener Utterance.everyEmpty unif_marg_every).snd Quantification.DomainRestriction.SpatialScale.peripersonal > (uniformListener Utterance.everyEmpty unif_marg_every).snd Quantification.DomainRestriction.SpatialScale.action

R&S §2.1: With uniform priors, RSA still predicts peripersonal for ⟦every⟧ — but only because the literal semantics does the work (⟦every⟧ is false under wider scales in more worlds, so L0 assigns higher probability to narrower scales). This is a semantic accident, not a cognitive explanation.

theorem RitchieSchiller2024.uniform_some_distal_wins :

(uniformListener Utterance.someEmpty unif_marg_some).snd Quantification.DomainRestriction.SpatialScale.vista > (uniformListener Utterance.someEmpty unif_marg_some).snd Quantification.DomainRestriction.SpatialScale.peripersonal

R&S §2.1: With uniform priors, RSA predicts the WRONG ordering for ⟦some⟧ — the listener infers vista as most likely, not peripersonal. This is because under wider scales, ⟦some⟧ is more informative (it's the only true utterance when ⟦every⟧ is false), yielding higher L0. Cognitive-default priors (ddprPrior) are needed to override this.

Connects DDRPs to [BJEST17]'s BToM architecture and [Sta02]'s common ground.

When the scene is common ground ([Cla96] on joint attention), speaker and hearer derive the same DDRP. Different perceptual access yields different DDRPs, motivating R&S's requirement of perceptual co-presence.

noncomputable def RitchieSchiller2024.ddprBToM :

Core.BToMModel ENNReal Utterance World World Quantification.DomainRestriction.SpatialScale Unit Unit World

The DDRP generative model as a BToM instance over ℝ≥0∞: percept and belief are veridical deltas ([BJEST17]'s observer with full perceptual access), the plan model is the shared pragmatic speaker S, and the world-conditioned desire prior is the cognitive-default joint prior.

Equations

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

Instances For

theorem RitchieSchiller2024.ddprBToM_worldMarginal_eq (u : Utterance) (w : World) :

ddprBToM.worldMarginal u w = ∑ l : Quantification.DomainRestriction.SpatialScale, ddprJoint (w, l) * (S (w, l)) u

Delta-collapse: the BToM world marginal is the listener's unnormalized world score, Σ_l prior(w, l) · S(u | w, l).

theorem RitchieSchiller2024.rsa_btom_bridge (u : Utterance) (h : PMF.marginal S ddprJoint u ≠ 0) (w : World) :

(ddprListener u h).fst w = ddprBToM.worldMarginal u w * (PMF.marginal S ddprJoint u)⁻¹

RSA's pragmatic listener IS BToM world-marginal inference, on the mathlib-PMF face: the listener's world marginal is the ddprBToM world marginal, normalized by the utterance's prior predictive mass.

theorem RitchieSchiller2024.shared_scene_shared_ddrp (scene : SpatialScene Entity) (getScene : World → SpatialScene Entity) (hcg : ∀ (w : World), getScene w = scene) (w : World) :

sceneToDDRP (getScene w) = sceneToDDRP scene

When all discourse participants share the same spatial scene, they derive the same DDRP — a prerequisite for successful communication about domain-restricted quantifiers.

def RitchieSchiller2024.partitionScene :

SpatialScene Entity

An alternative scene where b3 is behind a partition (in vista, not action).

Equations

Instances For

theorem RitchieSchiller2024.scenes_differ_on_b3 :

dinnerScene Entity.b3 ≠ partitionScene Entity.b3

theorem RitchieSchiller2024.different_scenes_different_ddrps :

(sceneToDDRP dinnerScene).region ≠ (sceneToDDRP partitionScene).region

Different spatial scenes yield different DDRPs.

theorem RitchieSchiller2024.perception_mismatch_changes_truth :

(¬∀ (e : Entity), dinnerScene e ≤ Quantification.DomainRestriction.SpatialScale.action → isBottle e = true → emptyIn World.nearEmpty e = true) ∧ ∀ (e : Entity), partitionScene e ≤ Quantification.DomainRestriction.SpatialScale.action → isBottle e = true → emptyIn World.nearEmpty e = true

Without perceptual co-presence, domain-restricted quantifiers can receive different truth values: "every bottle is empty" under action-space restriction is false with the dinner scene but true with the partition scene (where b3 is too far to be in the action zone).

R&S §4 argues that non-default domain restrictions arise from explicit discourse moves. When the QUD shifts (e.g., "Where are the blue things?"), the domain restriction can widen beyond the cognitive default. We connect this to the QUD infrastructure from [Rob12].

def RitchieSchiller2024.spatialQUD :

QUD partitioning worlds by spatial emptiness profile: which bottles are empty at each spatial scale? Worlds that agree on the emptiness of peripersonal, action, and vista bottles give the same answer.

Equations

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

Instances For

theorem RitchieSchiller2024.spatialQUD_distinguishes_all :

spatialQUD.sameAnswer World.nearEmpty World.midEmpty = false ∧ spatialQUD.sameAnswer World.midEmpty World.allEmpty = false ∧ spatialQUD.sameAnswer World.nearEmpty World.allEmpty = false

The spatial QUD distinguishes all three worlds: each has a different emptiness profile across scales.

R&S §3.2 argue that default domain restrictions are objective (nonsubjective on [TD02]'s cline): they derive from perceptual/cognitive structure (location, spatial proximity), not from speaker attitude (subjective) or addressee face (intersubjective). This predicts that spatial/temporal restrictions make better defaults than evaluative restrictions (beauty, tastiness).

[scontras-degen-goodman-2017] find that more objective adjectives are
ordered closer to the noun — "the big blue box" over "the blue big box" —
because less subjective content is more useful for communication. R&S
extend this: more objective *domain restrictions* are similarly privileged
as defaults because they are more likely to be shared among participants
and thus better for coordination.

The connection is structural: all three cognitive heuristics (availability,
salience, manipulability) target features that are objective in the sense
that they don't depend on speaker perspective or taste.

def RitchieSchiller2024.ddprSubjectivityLevel :

Features.Subjectivity.SubjectivityLevel

DDRPs are nonsubjective: the three cognitive heuristics (availability, salience, manipulability) all target spatiotemporal properties that don't depend on speaker perspective. This is not stipulated — it follows from the heuristics being defined over SpatialScale, which is a physical (observer-independent) ordering on spatial regions.

Equations

RitchieSchiller2024.ddprSubjectivityLevel = Features.Subjectivity.SubjectivityLevel.nonSubjective

Instances For

theorem RitchieSchiller2024.ddpr_precedes_subjective :

ddprSubjectivityLevel ≤ Features.Subjectivity.SubjectivityLevel.subjective

Objectivity prediction: DDRPs (nonsubjective) precede subjective interpretations on the Traugott-Dasher cline, predicting they are available as defaults before evaluative restrictions require discourse setup. The ordering reflects [SDG17]'s finding: less subjective content is more useful for communication.

theorem RitchieSchiller2024.ddpr_is_minimum (l : Features.Subjectivity.SubjectivityLevel) :

ddprSubjectivityLevel ≤ l

Nonsubjective is the minimum on the Traugott-Dasher cline, so DDRPs precede all subjective and intersubjective interpretations.