Linglib.Phenomena.Focus.Studies.DeoThomas2025

inductive DeoThomas2025.AlternativeSource :

Where the alternatives for just come from. Roothian alternatives are the standard focus-semantic alternatives; the other sources are what distinguish just from only.

roothian : AlternativeSource
granularity : AlternativeSource
causal : AlternativeSource
elaboration : AlternativeSource
normative : AlternativeSource

Instances For

source

@[implicit_reducible]

instance DeoThomas2025.instReprAlternativeSource :

Repr AlternativeSource

Equations

DeoThomas2025.instReprAlternativeSource = { reprPrec := DeoThomas2025.instReprAlternativeSource.repr }

source

def DeoThomas2025.instReprAlternativeSource.repr :

AlternativeSource → ℕ → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance DeoThomas2025.instDecidableEqAlternativeSource :

DecidableEq AlternativeSource

Equations

DeoThomas2025.instDecidableEqAlternativeSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def DeoThomas2025.associatedSource :

Phenomena.Focus.Exclusives.JustFlavor → AlternativeSource

Map each flavor of just to its alternative source.

Equations

Instances For

source

structure DeoThomas2025.DiscourseContext (W : Type u_1) :

Type u_1

A discourse context provides construals of an underspecified question (UQ) together with Quality and Relevance filters.

Construals are Questions (sets of alternative propositions), matching the paper's definition (30)-(31): questions are sets of propositions that cover the common ground. This is more faithful than using partitions (QUD), since the paper explicitly notes that granularity-based construals generally cannot be ordered by question entailment (fn. 20).

W is the world type.

construals : List (Core.Question W)
The available construals of UQ_c
quality : Core.Question W → Bool
Does the speaker have sufficient evidence to answer this question?
relevance : Core.Question W → Bool
Is this question relevant to the current discourse?
nonempty : self.construals ≠ []
There must be at least one construal

Instances For

source

def DeoThomas2025.answerable {W : Type u_1} (ctx : DiscourseContext W) (q : Core.Question W) :

Bool

A question is answerable iff it passes both Quality and Relevance (34).

Equations

DeoThomas2025.answerable ctx q = (ctx.quality q && ctx.relevance q)

Instances For

source

def DeoThomas2025.isWidestAnswerable {W : Type u_1} (ctx : DiscourseContext W) (q : Core.Question W) :

Prop

OPT_c(Q) (@cite{deo-thomas-2025} (35)): the optimal question in a set of construals.

q is the widest answerable construal: it is answerable, it is in the construal set, and no strictly wider answerable construal exists.

Width is measured by Core.Question.widerThan ((32)), the paper's comparison of question inquisitivity — explicitly weaker than G&S question entailment (fn. 20), because granularity-based construals generally cannot be ordered by entailment strength.

Equations

DeoThomas2025.isWidestAnswerable ctx q = (q ∈ ctx.construals ∧ DeoThomas2025.answerable ctx q = true ∧ ∀ q' ∈ ctx.construals, DeoThomas2025.answerable ctx q' = true → ¬q'.widerThan q)

Instances For

source

def DeoThomas2025.classifyContext {W : Type u_1} (ctx : DiscourseContext W) :

Phenomena.Focus.Exclusives.ContextType

Classify a discourse context by WHY the widest answerable construal is optimal. Connects to Phenomena.Focus.Exclusives.ContextType.

(37a) answerable: all construals are answerable → CQ = widest overall
(37b) qualityFail: some construal fails Quality (speaker lacks evidence)
(37c) relevanceFail: some construal fails Relevance (not discourse-relevant)

Equations

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

Instances For

source

theorem DeoThomas2025.only_substitutes_iff_roothian (d : Phenomena.Focus.Exclusives.JustDatum) :

d ∈ Phenomena.Focus.Exclusives.allJustData → (d.onlyOk = true ↔ associatedSource d.flavor = AlternativeSource.roothian)

Only can replace just exactly when the alternatives are Roothian (complement-exclusion and rank-order). Verified against all empirical data.

source

theorem DeoThomas2025.quality_fail_implies_causal (d : Phenomena.Focus.Exclusives.JustDatum) :

d ∈ Phenomena.Focus.Exclusives.allJustData → d.contextType = Phenomena.Focus.Exclusives.ContextType.qualityFail → associatedSource d.flavor = AlternativeSource.causal

Quality-failure contexts yield only causal-alternative flavors (unexplanatory, minimal sufficiency).

source

theorem DeoThomas2025.relevance_fail_implies_elaboration (d : Phenomena.Focus.Exclusives.JustDatum) :

d ∈ Phenomena.Focus.Exclusives.allJustData → d.contextType = Phenomena.Focus.Exclusives.ContextType.relevanceFail → associatedSource d.flavor = AlternativeSource.elaboration

Relevance-failure contexts yield only elaboration-alternative flavors (unelaboratory).

source

theorem DeoThomas2025.only_requires_shared_cq (d : Phenomena.Focus.Exclusives.JustDatum) :

d ∈ Phenomena.Focus.Exclusives.allJustData → d.onlyOk = true → associatedSource d.flavor = AlternativeSource.roothian

only is felicitous only with Roothian alternatives (shared CQ). just is felicitous regardless of alternative source. This is WHY they diverge: only exhaustifies over shared alternatives, just widens the question.

source

theorem DeoThomas2025.all_flavors_attested :

All 9 JustFlavor constructors are attested in the empirical data.

source

def DeoThomas2025.wxdyAlternativeSource :

AlternativeSource

WXDY's incredulity arises from a normative expectation violation: the situation violates what the speaker considers normal/appropriate. This is the same alternative source as counterexpectational just ("He's just texting during the lecture!").

WXDY: "What's this fly doing in my soup?" — violates dining norms
just: "He's just texting during the lecture!" — violates classroom norms

Equations

DeoThomas2025.wxdyAlternativeSource = DeoThomas2025.AlternativeSource.normative

Instances For

source

theorem DeoThomas2025.wxdy_incongruity_is_counterexpectational :

wxdyAlternativeSource = associatedSource Phenomena.Focus.Exclusives.JustFlavor.counterexpectational

WXDY's incongruity and counterexpectational just share the same alternative source: both involve normative expectations being violated.

Partition refinement implies question width #

The paper's central formal insight: finer granularity produces wider questions. At the partition level, "finer" is QUD.refines (every fine cell ⊆ some coarse cell), equivalently q.toSetoid ≤ q'.toSetoid in mathlib's Setoid lattice. At the issue level, "wider" is Core.Question.widerThan (@cite{deo-thomas-2025} (32): same info, no coarse answer ⊊ fine answer, some fine answer ⊊ coarse answer). The bridge: toIssue := Core.Question.fromSetoid ∘ QUD.toSetoid preserves this relationship.

The proof is an order-theoretic one-liner over Setoid: every alternative of Core.Question.fromSetoid r is either ∅ or an equivalence class of r (alt_fromSetoid_subset_classes), and the q-class of w₀ is contained in the q'-class of w₀ by refinement, with v₀ witnessing strict containment. This replaces a 100-line Bool/List proof that managed indices into worlds : List W and case-split on properlyContains.

source

def DeoThomas2025.toIssue {W : Type u_2} (q : QUD W) :

Core.Question W

A QUD partitions a meaning space via an equivalence relation; via QUD.toSetoid and Core.Question.fromSetoid, every QUD induces an inquisitive content whose alternatives are exactly the QUD's equivalence classes. The bridge is one-way: not every Core.Question arises from a QUD (mention-some, intermediate-exhaustive, and conditional-question alternatives are non-disjoint or non-exhaustive and so are not representable as the cells of any equivalence relation — @cite{theiler-etal-2018}).

Equations

DeoThomas2025.toIssue q = Core.Question.fromSetoid q.toSetoid

Instances For

source

theorem DeoThomas2025.refinement_implies_wider {W : Type u_2} (q q' : QUD W) (hRefines : q.refines q') (w₀ v₀ : W) (hCoarse : q'.r w₀ v₀) (hFine : ¬q.r w₀ v₀) :

(toIssue q).widerThan (toIssue q')

Strict partition refinement implies issue width.

If q (strictly) refines q' (q is the finer partition), then toIssue q is wider than toIssue q' as Core.Questions.

The strictness witnesses w₀, v₀ : W share a coarse cell (q'.r w₀ v₀) but not a fine cell (¬ q.r w₀ v₀); they witness condition (c).

The proof establishes the three conditions of Core.Question.widerThan:

(a) Same info: both fromSetoid-derived issues have info = univ.
(b) No q'-alternative is properly contained in any q-alternative: alternatives are classes (or ∅); under refinement, classes only widen as we go from the finer to the coarser setoid, so the reverse containment is impossible.
(c) Some q-alternative properly contained in some q'-alternative: witnessed by the q-class and q'-class of w₀, with v₀ showing the inclusion is strict.

The full chain: finer granularity → wider question #

Composes the two independently proved steps:

finer_granularity_refines (from Theories.Semantics.Degree.Granularity): if ε₁ ∣ ε₂, the ε₁-partition refines the ε₂-partition
refinement_implies_wider (proved above): strict partition refinement → issue width

This is the formal content of the lexical entry (36): just selects the widest answerable construal, which — when alternatives vary by granularity — is the finest one the speaker can answer.

source

theorem DeoThomas2025.finer_granularity_implies_wider (n ε₁ ε₂ : ℕ) (hdvd : ε₁ ∣ ε₂) (w₀ v₀ : Fin n) (hCoarse : (Semantics.Degree.Granularity.granQUD n ε₂).r w₀ v₀) (hFine : ¬(Semantics.Degree.Granularity.granQUD n ε₁).r w₀ v₀) :

(toIssue (Semantics.Degree.Granularity.granQUD n ε₁)).widerThan (toIssue (Semantics.Degree.Granularity.granQUD n ε₂))

The complete granularity–width chain (@cite{deo-thomas-2025} §3.1.2–3.2).

If ε₁ divides ε₂ (finer grain) and there exist worlds that share a coarse cell but not a fine cell, then the fine-grained question is strictly wider than the coarse-grained question.

This is the general version of Figure 1: any uniform-grain-width scale satisfies the width relation when grain widths are divisible.

source

def DeoThomas2025.fig1Worlds :

List (Fin 8)

The 8-point age scale from Figure 1 (@cite{deo-thomas-2025}).

Equations

DeoThomas2025.fig1Worlds = [0, 1, 2, 3, 4, 5, 6, 7]

Instances For

source

def DeoThomas2025.coarseQ :

QUD (Fin 8)

Coarse granularity: 2 cells of 4 (e.g., "younger half" vs "older half"). Worlds 0–3 share one answer, worlds 4–7 share another.

Equations

DeoThomas2025.coarseQ = QUD.ofProject fun (w : Fin 8) => ↑w / 4

Instances For

source

def DeoThomas2025.fineQ :

QUD (Fin 8)

Fine granularity: 4 cells of 2 (e.g., {0,1}, {2,3}, {4,5}, {6,7}). Each pair of adjacent worlds shares an answer.

Equations

DeoThomas2025.fineQ = QUD.ofProject fun (w : Fin 8) => ↑w / 2

Instances For

source

theorem DeoThomas2025.coarseQ_is_granQUD :

coarseQ = Semantics.Degree.Granularity.granQUD 8 4

Figure 1's partitions are instances of the general granQUD.

source

theorem DeoThomas2025.fineQ_is_granQUD :

fineQ = Semantics.Degree.Granularity.granQUD 8 2

source

theorem DeoThomas2025.fig1_strict_refinement :

fineQ.refines coarseQ ∧ ¬coarseQ.refines fineQ

Fine strictly refines coarse: knowing the fine answer determines the coarse answer, but not vice versa (0 and 2 share a coarse cell but not a fine cell).

source

theorem DeoThomas2025.fig1_finer_is_wider :

(toIssue fineQ).widerThan (toIssue coarseQ)

Figure 1 via the general granularity–width theorem. The fine 4-cell partition produces a wider issue than the coarse 2-cell partition over the 8-point domain.

Witnessed by worlds 0 and 2: they share a coarse cell (0/4 = 2/4 = 0) but not a fine cell (0/2 = 0 ≠ 2/2 = 1).