@cite{ritchie-schiller-2024} — Default Domain Restriction Possibilities

@cite{ritchie-schiller-2024} @cite{cutting-vishton-1995} @cite{baker-jara-ettinger-saxe-tenenbaum-2017} @cite{clark-1996} @cite{stalnaker-2002}

Ritchie, H. & Schiller, K. (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 (= Latent in RSAConfig) to infer which domain restriction the speaker intended. We demonstrate this connection in §7.

inductive Phenomena.Quantification.Studies.RitchieSchiller2024.Entity : Type

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

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

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instDecidableEqEntity : DecidableEq Entity

Equations

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

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqEntity : BEq Entity

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqEntity = { beq := Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqEntity.beq }

def Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqEntity.beq : Entity → Entity → Bool

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqEntity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instReprEntity : Repr Entity

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instReprEntity = { reprPrec := Phenomena.Quantification.Studies.RitchieSchiller2024.instReprEntity.repr }

def Phenomena.Quantification.Studies.RitchieSchiller2024.instReprEntity.repr : Entity → ℕ → Std.Format

Equations

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

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedEntity : Inhabited Entity

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedEntity = { default := Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedEntity.default }

def Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedEntity.default : Entity

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedEntity.default = Phenomena.Quantification.Studies.RitchieSchiller2024.Entity.b1

def Phenomena.Quantification.Studies.RitchieSchiller2024.bottleModel : Semantics.Montague.Model

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.bottleModel = { Entity := Phenomena.Quantification.Studies.RitchieSchiller2024.Entity, decEq := inferInstance }

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instFintypeEntityBottleModel : Fintype bottleModel.Entity

Equations

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

def Phenomena.Quantification.Studies.RitchieSchiller2024.near : Entity → Bool

Peripersonal space: entities within arm's reach (b1, b2 on the table).

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.near Phenomena.Quantification.Studies.RitchieSchiller2024.Entity.b1 = true
• Phenomena.Quantification.Studies.RitchieSchiller2024.near Phenomena.Quantification.Studies.RitchieSchiller2024.Entity.b2 = true
• Phenomena.Quantification.Studies.RitchieSchiller2024.near x✝ = false

def Phenomena.Quantification.Studies.RitchieSchiller2024.mid : Entity → Bool

Action space: entities accessible by locomotion (b1, b2, b3).

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.mid Phenomena.Quantification.Studies.RitchieSchiller2024.Entity.b4 = false
• Phenomena.Quantification.Studies.RitchieSchiller2024.mid x✝ = true

def Phenomena.Quantification.Studies.RitchieSchiller2024.sceneDDRP : Semantics.Lexical.Determiner.DomainRestriction.DDRP Semantics.Lexical.Determiner.DomainRestriction.SpatialScale Entity

DDRP for the bottle scenario. Near ⊆ mid ⊆ vista (= unrestricted in this indoor scene).

Equations

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

inductive Phenomena.Quantification.Studies.RitchieSchiller2024.World : Type

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

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instDecidableEqWorld : DecidableEq World

Equations

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

def Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqWorld.beq : World → World → Bool

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqWorld : BEq World

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqWorld = { beq := Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqWorld.beq }

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instReprWorld : Repr World

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instReprWorld = { reprPrec := Phenomena.Quantification.Studies.RitchieSchiller2024.instReprWorld.repr }

def Phenomena.Quantification.Studies.RitchieSchiller2024.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedWorld : Inhabited World

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedWorld = { default := Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedWorld.default }

def Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedWorld.default : World

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedWorld.default = Phenomena.Quantification.Studies.RitchieSchiller2024.World.nearEmpty

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instFintypeWorld : Fintype World

Equations

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

def Phenomena.Quantification.Studies.RitchieSchiller2024.emptyIn : World → Entity → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Quantification.Studies.RitchieSchiller2024.emptyIn Phenomena.Quantification.Studies.RitchieSchiller2024.World.allEmpty x✝ = true
• Phenomena.Quantification.Studies.RitchieSchiller2024.emptyIn Phenomena.Quantification.Studies.RitchieSchiller2024.World.midEmpty x✝ = true
• Phenomena.Quantification.Studies.RitchieSchiller2024.emptyIn Phenomena.Quantification.Studies.RitchieSchiller2024.World.nearEmpty x✝ = false

def Phenomena.Quantification.Studies.RitchieSchiller2024.isBottle : bottleModel.Entity → Bool

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

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.isBottle x✝ = true

def Phenomena.Quantification.Studies.RitchieSchiller2024.everyBottleEmpty (scale : Semantics.Lexical.Determiner.DomainRestriction.SpatialScale) (w : World) : Bool

Truth of "every bottle is empty" under a given spatial domain restriction.

Equations

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

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.w_near_peri : everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal World.nearEmpty = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.w_near_action : everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action World.nearEmpty = false

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.w_near_vista : everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.vista World.nearEmpty = false

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.w_mid_peri : everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal World.midEmpty = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.w_mid_action : everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action World.midEmpty = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.w_mid_vista : everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.vista World.midEmpty = false

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.w_all_peri : everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal World.allEmpty = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.w_all_action : everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action World.allEmpty = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.w_all_vista : everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.vista World.allEmpty = true

def Phenomena.Quantification.Studies.RitchieSchiller2024.someBottleEmpty (scale : Semantics.Lexical.Determiner.DomainRestriction.SpatialScale) (w : World) : Bool

Truth of "some bottle is empty" under a given spatial domain restriction.

Equations

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

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.some_near_peri : someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal World.nearEmpty = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.some_near_action : someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action World.nearEmpty = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.some_near_vista : someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.vista World.nearEmpty = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.some_mid_peri : someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal World.midEmpty = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.some_mid_action : someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action World.midEmpty = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.some_mid_vista : someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.vista World.midEmpty = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.some_all_peri : someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal World.allEmpty = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.some_all_action : someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action World.allEmpty = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.some_all_vista : someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.vista World.allEmpty = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.proximal_default : everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal World.nearEmpty = true ∧ everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action World.nearEmpty = false ∧ everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.vista World.nearEmpty = false

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. This illustrates R&S's claim (§3.1) that perceptual availability biases hearers toward proximal domains: when only one candidate restriction works, pragmatic selection is forced.

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.monotonicity_contrast : everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal World.nearEmpty = true ∧ everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action World.nearEmpty = false ∧ someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal World.nearEmpty = true ∧ someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action World.nearEmpty = true ∧ someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.vista World.nearEmpty = true

↓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 Phenomena.Quantification.Studies.RitchieSchiller2024.nesting_action_to_peri (w : World) : everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action w = true → everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal w = true

⟦every⟧ nesting: truth under any scale entails truth under any smaller scale. Uses the general DDRP.every_nesting theorem parameterized by the ordering.

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.nesting_vista_to_action (w : World) : everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.vista w = true → everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action w = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.nesting_vista_to_peri (w : World) : everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.vista w = true → everyBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal w = true

Transitive nesting: vista → peripersonal (2-step composition).

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.some_nesting_peri_to_action (w : World) : someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal w = true → someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action w = true

⟦some⟧ nesting (reversed): truth under any scale entails truth under any larger scale. The ↑MON dual of ⟦every⟧ nesting.

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.some_nesting_action_to_vista (w : World) : someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action w = true → someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.vista w = true

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.some_nesting_peri_to_vista (w : World) : someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.peripersonal w = true → someBottleEmpty Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.vista w = true

Transitive ⟦some⟧ nesting: peripersonal → vista (2-step composition).

inductive Phenomena.Quantification.Studies.RitchieSchiller2024.Utterance : Type

Utterance type for the RSA model.

• everyEmpty : Utterance
• someEmpty : Utterance

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instDecidableEqUtterance : DecidableEq Utterance

Equations

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

def Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqUtterance.beq : Utterance → Utterance → Bool

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqUtterance : BEq Utterance

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqUtterance = { beq := Phenomena.Quantification.Studies.RitchieSchiller2024.instBEqUtterance.beq }

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instReprUtterance : Repr Utterance

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instReprUtterance = { reprPrec := Phenomena.Quantification.Studies.RitchieSchiller2024.instReprUtterance.repr }

def Phenomena.Quantification.Studies.RitchieSchiller2024.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

def Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedUtterance.default : Utterance

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedUtterance.default = Phenomena.Quantification.Studies.RitchieSchiller2024.Utterance.everyEmpty

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedUtterance : Inhabited Utterance

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedUtterance = { default := Phenomena.Quantification.Studies.RitchieSchiller2024.instInhabitedUtterance.default }

instance Phenomena.Quantification.Studies.RitchieSchiller2024.instFintypeUtterance : Fintype Utterance

Equations

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

def Phenomena.Quantification.Studies.RitchieSchiller2024.utteranceMeaning (scale : Semantics.Lexical.Determiner.DomainRestriction.SpatialScale) : Utterance → World → Bool

Literal meaning under a given DDRP scale.

Equations

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

noncomputable def Phenomena.Quantification.Studies.RitchieSchiller2024.domainRestrictionRSA : RSA.RSAConfig Utterance World

RSAConfig instantiation with DDRPs as the latent variable.

The listener reasons over which spatial scale the speaker intended when uttering a quantified sentence. Latent = SpatialScale: L1 marginalizes over candidate domain restrictions to infer the speaker's intended domain.

While R&S argue against RSA as explaining default status (§2.1), their DDRPs are fully compatible with RSA as the selection mechanism once the candidate set is fixed by cognitive heuristics. This models the pragmatic step: given the DDRP candidates, which one did the speaker intend?

Equations

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

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.l0_reflects_every (s : Semantics.Lexical.Determiner.DomainRestriction.SpatialScale) (w : World) (h : everyBottleEmpty s w = true) : domainRestrictionRSA.meaning () s Utterance.everyEmpty w = 1

L0 correctly reflects literal semantics: when ⟦every⟧ is true under a given scale, L0's score is positive.

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.l0_reflects_every_false (s : Semantics.Lexical.Determiner.DomainRestriction.SpatialScale) (w : World) (h : everyBottleEmpty s w = false) : domainRestrictionRSA.meaning () s Utterance.everyEmpty w = 0

L0 correctly reflects literal semantics: when ⟦every⟧ is false under a given scale, L0's score is zero.

Connects DDRPs to @cite{baker-jara-ettinger-saxe-tenenbaum-2017}'s BToM architecture and @cite{stalnaker-2002}'s common ground.

1. Perception-generated DDRPs: A spatial scene induces a DDRP via sceneToDDRP. Monotonicity follows from transitivity of ≤ on SpatialScale.

2. BToM instantiation: RSAConfig.toBToM gives a BToM model; the bridge theorem L1_eq_btom_worldMarginal proves L1 IS BToM world-marginal.

3. Common-ground constraint: When the scene is common ground, speaker and hearer derive the same DDRP (@cite{clark-1996} on joint attention).

4. Perfect-perception collapse: Under perfect perception, the perception-generated DDRP equals the hand-written one.

5. Imperfect perception: Different perceptual access → different DDRPs, motivating R&S's requirement of perceptual co-presence.

def Phenomena.Quantification.Studies.RitchieSchiller2024.SpatialScene (E : Type u_1) : Type u_1

A spatial scene: each entity occupies a spatial zone.

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.SpatialScene E = (E → Semantics.Lexical.Determiner.DomainRestriction.SpatialScale)

def Phenomena.Quantification.Studies.RitchieSchiller2024.perceivable {E : Type u_1} (scene : SpatialScene E) (threshold : Semantics.Lexical.Determiner.DomainRestriction.SpatialScale) (e : E) : Bool

Entities perceivable at a given scale threshold: those whose zone ≤ threshold.

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.perceivable scene threshold e = decide (scene e ≤ threshold)

def Phenomena.Quantification.Studies.RitchieSchiller2024.sceneToDDRP {E : Type u_1} (scene : SpatialScene E) : Semantics.Lexical.Determiner.DomainRestriction.DDRP Semantics.Lexical.Determiner.DomainRestriction.SpatialScale E

A spatial scene induces a DDRP. Region s contains entities in zone ≤ s.

Equations

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

def Phenomena.Quantification.Studies.RitchieSchiller2024.dinnerScene : SpatialScene Entity

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

Equations

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

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.sceneToDDRP_eq_sceneDDRP : (sceneToDDRP dinnerScene).region = sceneDDRP.region

sceneToDDRP dinnerScene agrees with sceneDDRP.

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.rsa_btom_bridge (u : Utterance) (w : World) : domainRestrictionRSA.L1agent.score u w = domainRestrictionRSA.toBToM.worldMarginal u w

The RSA-BToM bridge applies to the domain restriction RSA config.

def Phenomena.Quantification.Studies.RitchieSchiller2024.actualScene (_w : World) : SpatialScene Entity

The actual scene at each world.

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.actualScene _w = Phenomena.Quantification.Studies.RitchieSchiller2024.dinnerScene

def Phenomena.Quantification.Studies.RitchieSchiller2024.ddprGroundedInCG (scene : SpatialScene Entity) (cg : Core.CommonGround.BContextSet World) : Prop

A DDRP is grounded in common ground when the spatial scene is common knowledge among discourse participants.

Equations

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

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.dinnerScene_is_cg : ddprGroundedInCG dinnerScene fun (x : World) => true

The dinner scene is common ground.

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.shared_scene_shared_ddrp (scene : SpatialScene Entity) (cg : Core.CommonGround.BContextSet World) (hcg : ddprGroundedInCG scene cg) (w : World) : cg w = true → sceneToDDRP (actualScene w) = sceneToDDRP scene

When the scene is common ground, speaker and hearer derive the same DDRP.

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.perception_generates_rsa_ddrp (s : Semantics.Lexical.Determiner.DomainRestriction.SpatialScale) (w : World) : everyBottleEmpty s w = Semantics.Lexical.Determiner.DomainRestriction.every_restricted bottleModel ((sceneToDDRP dinnerScene).region s) isBottle (emptyIn w)

Under perfect perception, the perception-generated DDRP yields the same truth conditions as the hand-written one.

def Phenomena.Quantification.Studies.RitchieSchiller2024.scaleCategory : Core.BToM.LatentCategory

SpatialScale is a mental state (speaker's private choice).

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.scaleCategory = Core.BToM.LatentCategory.mental

def Phenomena.Quantification.Studies.RitchieSchiller2024.sceneCategory : Core.BToM.LatentCategory

The spatial scene is shared (perceptual co-presence).

Equations

• Phenomena.Quantification.Studies.RitchieSchiller2024.sceneCategory = Core.BToM.LatentCategory.shared

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.scale_is_mental : scaleCategory = Core.BToM.LatentCategory.mental

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.scene_is_shared : sceneCategory = Core.BToM.LatentCategory.shared

def Phenomena.Quantification.Studies.RitchieSchiller2024.ddprClassification : RSA.BToMGrounding.LatentClassification Semantics.Lexical.Determiner.DomainRestriction.SpatialScale

Full latent classification for the domain restriction model.

Equations

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

def Phenomena.Quantification.Studies.RitchieSchiller2024.partitionScene : SpatialScene Entity

An alternative scene where b3 is behind a partition.

Equations

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

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.scenes_differ_on_b3 : dinnerScene Entity.b3 ≠ partitionScene Entity.b3

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.different_scenes_different_ddrps : (sceneToDDRP dinnerScene).region ≠ (sceneToDDRP partitionScene).region

Different spatial scenes yield different DDRPs.

theorem Phenomena.Quantification.Studies.RitchieSchiller2024.perception_mismatch_changes_truth : Semantics.Lexical.Determiner.DomainRestriction.every_restricted bottleModel ((sceneToDDRP dinnerScene).region Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action) isBottle (emptyIn World.nearEmpty) = false ∧ Semantics.Lexical.Determiner.DomainRestriction.every_restricted bottleModel ((sceneToDDRP partitionScene).region Semantics.Lexical.Determiner.DomainRestriction.SpatialScale.action) isBottle (emptyIn World.nearEmpty) = true

Without perceptual co-presence, domain-restricted quantifiers can receive different truth values.