Ritchie and Schiller (2024): Default domain restriction possibilities

This file formalizes the paper's account of why some implicit restrictions on quantifier domains, to the present location and time, are available without conversational setup while others, by colour, history, aesthetics or subkind, are not. The domain of quantification is what is relevant to the interlocutors' joint purpose, and when only the minimal shared aims of predicting, explaining and manipulating the environment are in place the domain is delivered by cognitive heuristics: perceptual availability, and the two salience heuristics of perceptual salience and manipulability, which filter the available objects. A Situation fixes what is present, perceivable, attention-grabbing and controllable from a viewpoint, the heuristics are its filters, Situation.restrictors, and every restriction they deliver lies within the here and now, default_subset_present, which is why locational and temporal restrictions are the defaults. Non-default restrictions become available when a discourse move or a prior plan installs a more specific purpose, Situation.domain, and displacement is the same heuristics applied from another viewpoint. The paper's examples are rows, and default_of_acceptable records that every restriction acceptable without setup is a heuristic one.

Implementation notes

The nesting of the heuristics is derived from their definition as intersections with the available objects, so the filters form an order homomorphism from the heuristic scale to domains and the quantifier entailments between them come from the substrate. The paper's arguments against rational-pragmatic, discourse-structural and intentionalist explanations, its objectivity and spatial-cognition supplements, and its proposed experiments are not formalized.

References

• K. Ritchie, H. Schiller, Default domain restriction possibilities (2024)
• C. Roberts, Information structure in discourse: towards an integrated formal theory of pragmatics (2012)
• H. P. Grice, Logic and conversation (1975)
• G. Scontras, J. Degen, N. D. Goodman, Subjectivity predicts adjective ordering preferences (2017)

Cognitive heuristics

structure RitchieSchiller2024.Situation (V : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A perceptual situation relative to viewpoints records which entities are present at the viewpoint's location and time, which it could perceive with minimal bodily distortion, which grab its attention, and which it could control, move or interact with.

• present : V → Set E
• perceivable : V → Set E
• attentionGrabbing : V → Set E
• controllable : V → Set E

def RitchieSchiller2024.Situation.available {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) : Set E

The perceptually available entities are the perceivable ones, which only present objects are.

Equations

• s.available v = s.present v ∩ s.perceivable v

def RitchieSchiller2024.Situation.manipulable {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) : Set E

The manipulable entities are the available and controllable ones, the second salience heuristic.

Equations

• s.manipulable v = s.available v ∩ s.controllable v

def RitchieSchiller2024.Situation.salient {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) : Set E

The salient entities are the available ones that are attention-grabbing or manipulable, manipulability being a way of being salient.

Equations

• s.salient v = s.available v ∩ (s.attentionGrabbing v ∪ s.controllable v)

theorem RitchieSchiller2024.Situation.available_subset_present {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) : s.available v ⊆ s.present v

theorem RitchieSchiller2024.Situation.salient_subset_available {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) : s.salient v ⊆ s.available v

theorem RitchieSchiller2024.Situation.manipulable_subset_salient {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) : s.manipulable v ⊆ s.salient v

inductive RitchieSchiller2024.Heuristic : Type

The heuristics as filters on the domain, from the most restrictive to none.

• manipulability : Heuristic
• salience : Heuristic
• availability : Heuristic
• none : Heuristic

@[instance_reducible]

instance RitchieSchiller2024.instDecidableEqHeuristic : DecidableEq Heuristic

Equations

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

@[instance_reducible]

instance RitchieSchiller2024.instFintypeHeuristic : Fintype Heuristic

Equations

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

def RitchieSchiller2024.Heuristic.toFin : Heuristic → Fin 4

Equations

• RitchieSchiller2024.Heuristic.manipulability.toFin = 0
• RitchieSchiller2024.Heuristic.salience.toFin = 1
• RitchieSchiller2024.Heuristic.availability.toFin = 2
• RitchieSchiller2024.Heuristic.none.toFin = 3

theorem RitchieSchiller2024.Heuristic.toFin_injective : Function.Injective toFin

@[instance_reducible]

noncomputable instance RitchieSchiller2024.Heuristic.instLinearOrder : LinearOrder Heuristic

Equations

• RitchieSchiller2024.Heuristic.instLinearOrder = LinearOrder.lift' RitchieSchiller2024.Heuristic.toFin RitchieSchiller2024.Heuristic.toFin_injective

@[instance_reducible]

instance RitchieSchiller2024.Heuristic.instOrderTop : OrderTop Heuristic

Equations

• RitchieSchiller2024.Heuristic.instOrderTop = { top := RitchieSchiller2024.Heuristic.none, le_top := ⋯ }

def RitchieSchiller2024.Situation.restrictors {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) : Heuristic →o Set E

The default domain restriction possibilities of a situation are the domains the heuristics deliver, nested because each filters the last, so an order homomorphism from the heuristic scale to domains.

Equations

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

theorem RitchieSchiller2024.Situation.restrictors_top {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) : (s.restrictors v) ⊤ = Set.univ

The top of the scale leaves the domain unrestricted.

def RitchieSchiller2024.Situation.IsDefault {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) (C : Set E) : Prop

A restriction is a default in a situation when a heuristic delivers it.

Equations

• s.IsDefault v C = ∃ (h : RitchieSchiller2024.Heuristic), (s.restrictors v) h = C

theorem RitchieSchiller2024.default_subset_present {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) {h : Heuristic} (hh : h ≠ ⊤) : (s.restrictors v) h ⊆ s.present v

Every default restriction, short of no restriction, keeps to what is present at the viewpoint's location and time: this is why the here and now are the default restriction possibilities.

theorem RitchieSchiller2024.not_isDefault_of_not_subset {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) {C : Set E} (hC : ¬C ⊆ s.present v) (hu : C ≠ Set.univ) : ¬s.IsDefault v C

A restriction reaching beyond the here and now is no default, so the displaced readings of the paper's section 4.1 come from applying the heuristics at another viewpoint.

theorem RitchieSchiller2024.every_salient_of_every_available {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) (R S : E → Prop) : Quantifier.GQ.every.adjRestrict (s.available v) R S → Quantifier.GQ.every.adjRestrict (s.salient v) R S

A universal claim true of the available objects is true of the salient ones, so an utterance judged on what is in reach, as in the meadow, is weaker than one judged on all that is in view, as in the room; the converse fails.

theorem RitchieSchiller2024.some_available_of_some_salient {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) (R S : E → Prop) : Quantifier.GQ.some.adjRestrict (s.salient v) R S → Quantifier.GQ.some.adjRestrict (s.available v) R S

Joint purposes

inductive RitchieSchiller2024.Purpose (E : Type u_3) : Type u_3

The joint purpose in force is either the minimal shared aims, under which a heuristic fixes the domain, or a specific purpose, installed by a discourse move or a prior plan, which makes its own objects relevant.

• minimal {E : Type u_3} (h : Heuristic) : Purpose E
• specific {E : Type u_3} (relevant : Set E) : Purpose E

def RitchieSchiller2024.Situation.domain {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) : Purpose E → Set E

The domain of quantification tracks the objects relevant to the joint purpose.

Equations

• s.domain v (RitchieSchiller2024.Purpose.minimal h) = (s.restrictors v) h
• s.domain v (RitchieSchiller2024.Purpose.specific relevant) = relevant

theorem RitchieSchiller2024.isDefault_domain_minimal {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) (h : Heuristic) : s.IsDefault v (s.domain v (Purpose.minimal h))

Under the minimal aims the domain is a default.

theorem RitchieSchiller2024.exists_specific_of_not_isDefault {V : Type u_1} {E : Type u_2} (s : Situation V E) (v : V) {p : Purpose E} (hp : ¬s.IsDefault v (s.domain v p)) : ∃ (relevant : Set E), p = Purpose.specific relevant

A non-default domain requires a specific purpose.

The paper's examples

inductive RitchieSchiller2024.Restriction : Type

What an implicit restriction restricts by.

• location : Restriction
• time : Restriction
• availability : Restriction
• salience : Restriction
• manipulability : Restriction
• color : Restriction
• aesthetic : Restriction
• history : Restriction
• subkind : Restriction
• shape : Restriction
• plan : Restriction

@[instance_reducible]

instance RitchieSchiller2024.instDecidableEqRestriction : DecidableEq Restriction

Equations

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

@[instance_reducible]

instance RitchieSchiller2024.instFintypeRestriction : Fintype Restriction

Equations

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

def RitchieSchiller2024.Restriction.IsHeuristic : Restriction → Prop

The restrictions the cognitive heuristics deliver.

Equations

• RitchieSchiller2024.Restriction.location.IsHeuristic = True
• RitchieSchiller2024.Restriction.time.IsHeuristic = True
• RitchieSchiller2024.Restriction.availability.IsHeuristic = True
• RitchieSchiller2024.Restriction.salience.IsHeuristic = True
• RitchieSchiller2024.Restriction.manipulability.IsHeuristic = True
• x✝.IsHeuristic = False

@[instance_reducible]

instance RitchieSchiller2024.instDecidablePredRestrictionIsHeuristic : DecidablePred Restriction.IsHeuristic

Equations

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

inductive RitchieSchiller2024.Anchor : Type

Whether a locational or temporal restriction is to the speaker's here and now.

• hereNow : Anchor
• elsewhere : Anchor

@[instance_reducible]

instance RitchieSchiller2024.instDecidableEqAnchor : DecidableEq Anchor

Equations

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

@[instance_reducible]

instance RitchieSchiller2024.instFintypeAnchor : Fintype Anchor

Equations

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

inductive RitchieSchiller2024.Setup : Type

The conversational setup, if any, that introduces a specific purpose.

• none : Setup
• question : Setup
• assertion : Setup
• directive : Setup
• priorGoal : Setup
• displacement : Setup

@[instance_reducible]

instance RitchieSchiller2024.instDecidableEqSetup : DecidableEq Setup

Equations

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

@[instance_reducible]

instance RitchieSchiller2024.instFintypeSetup : Fintype Setup

Equations

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

structure RitchieSchiller2024.Row : Type

An example records the intended restriction, its anchor, the setup, and the judgment.

• restriction : Restriction
• anchor : Anchor
• setup : Setup
• judgment : Judgment

def RitchieSchiller2024.Row.IsDefault (d : Row) : Prop

A default restriction possibility is a heuristic restriction anchored to the here and now.

Equations

• d.IsDefault = (d.restriction.IsHeuristic ∧ d.anchor = RitchieSchiller2024.Anchor.hereNow)

@[instance_reducible]

instance RitchieSchiller2024.instDecidablePredRowIsDefault : DecidablePred Row.IsDefault

Equations

• RitchieSchiller2024.instDecidablePredRowIsDefault x✝ = { decide := decide x✝.restriction.IsHeuristic && decide (x✝.anchor = RitchieSchiller2024.Anchor.hereNow), reflects_decide := ⋯ }

def RitchieSchiller2024.Row.ofDatum (e : Datum) : Option Row

A datum read into its row; the anchor is the here and now unless the row says otherwise.

Equations

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

theorem RitchieSchiller2024.isSome_ofDatum (e : Datum) : e ∈ Examples.all → (Row.ofDatum e).isSome = true

Every example is read.

def RitchieSchiller2024.data : List Row

The paper's examples.

Equations

• RitchieSchiller2024.data = List.filterMap RitchieSchiller2024.Row.ofDatum RitchieSchiller2024.Examples.all

theorem RitchieSchiller2024.default_of_acceptable (d : Row) : d ∈ data → d.setup = Setup.none → d.judgment = Judgment.acceptable → d.IsDefault

Every restriction acceptable without conversational setup is a default one, so a non-default restriction is available only through a discourse move, a prior plan or displacement.

theorem RitchieSchiller2024.nondefault_attested : (∃ d ∈ data, ¬d.IsDefault ∧ d.judgment = Judgment.acceptable) ∧ ∃ d ∈ data, d.IsDefault ∧ d.setup = Setup.none ∧ d.judgment = Judgment.acceptable

Non-default restrictions do become available, and defaults are attested without setup.