Deo and Thomas (2025): Addressing the widest answerable question

Deo and Thomas analyse English just as a domain-widening strategy. Besides the uses it shares with only, just has emphatic, precisifying, minimal-sufficiency, unexplanatory, unelaboratory and counterexpectational uses, in some of which its prejacent answers no standard construal of the current question. The account replaces the current question by an underspecified question, the set of a question's construals at a context, and compares construals by width, which is weaker than question entailment. Just presupposes that the current question is the widest construal that the speaker can answer truthfully and relevantly, and asserts its prejacent.

Main definitions

• DeoThomas2025.WiderThan: the width order on construals, (32).
• DeoThomas2025.Context.IsOptimal: the widest answerable construal, (35).
• DeoThomas2025.just: the lexical entry, (36).

Main results

• DeoThomas2025.Context.IsOptimal.widest_or_quality_or_relevance: the three kinds of context in which a construal is optimal, (37).
• DeoThomas2025.Context.isOptimal_ofSet_iff: the unexplanatory and unelaboratory uses, §4.4 and §4.5.
• DeoThomas2025.widerThan_fromSetoid: a finer partition is a wider construal, §4.2 and §4.7.
• DeoThomas2025.widerThan_grain, DeoThomas2025.figure1: a finer grain is wider without refining the coarser one, so width is not entailment, Figure 1 and fn. 20.
• DeoThomas2025.widerThan_zone: extreme adjectives, Figure 2 of §4.8.
• DeoThomas2025.widerThan_mentionAll: mention-all is wider than mention-some, §4.1.

Implementation notes

A construal is a Question, whose alternatives Question.alt are the maximal resolving states, so (30a) holds by construction and (30b) is Question.info. The context of (31) carries the common ground, the construals, and the speaker's Quality and Relevance verdicts as primitives, with the paper's requirements that every construal cover the common ground and that any two construals be comparable by width, which is what makes the optimal construal unique. Partition construals are Question.fromSetoid, so refinement is the order on Setoid. Grains are Degree.grain, whose cells are centred on the multiples of the width, so that a measure phrase denotes the cell it lies at the centre of, (24); Figure 1's year and half-year grains are grain 1 and grain (1 / 2) on ℝ. Worlds for the constituent question of §4.1 are the extensions of its predicate. The exhaustive interpretation of the prejacent is a mandatory implicature that the paper leaves to Gricean reasoning, §4.1 and §4.9, and is not formalized; neither are the interpretation of the prejacent relative to the granularity of the current question in (36), the minimal-sufficiency construal of §4.3, whose alternatives are fixed by a causal structure, nor the Focus Principle, (21).

References

• [DT25]
• [TD20]
• [BC08]
• [CB14]
• [CGR18]
• [GS84]
• [Mor12]
• [Wie18]
• [War20]

Width, (32)

def DeoThomas2025.WiderThan {W : Type u_1} (P Q : Question W) : Prop

P is wider than Q, (32), when the two cover the same common ground, no alternative of Q is properly contained in an alternative of P, and some alternative of P is properly contained in an alternative of Q.

Equations

• DeoThomas2025.WiderThan P Q = (P.info = Q.info ∧ (∀ q ∈ Q.alt, ∀ p ∈ P.alt, ¬q ⊂ p) ∧ ∃ p ∈ P.alt, ∃ q ∈ Q.alt, p ⊂ q)

theorem DeoThomas2025.WiderThan.irrefl {W : Type u_1} (P : Question W) : ¬WiderThan P P

theorem DeoThomas2025.WiderThan.asymm {W : Type u_1} {P Q : Question W} (h : WiderThan P Q) : ¬WiderThan Q P

theorem DeoThomas2025.widerThan_ofSet {W : Type u_1} {P : Question W} {s p : Set W} (hs : P.info = s) (hp : p ∈ P.alt) (hne : p ≠ s) : WiderThan P (Question.ofSet s)

The trivial construal, whose one alternative is the common ground, is narrower than any other construal of the same common ground; it is the disjunction of all possible causes of §4.4.

The context, (31), and the optimal construal, (33) to (35)

structure DeoThomas2025.Context (W : Type u_2) : Type u_2

A context, (31), carries the common ground, the construals of the underspecified question, each a cover of the common ground and any two comparable by width, and the speaker's verdicts on which questions satisfy Quality and Relevance, (34).

• info : Set W

  The common ground.

• uq : Set (Question W)

  The construals of the underspecified question.

• quality : Question W → Prop

  The speaker has sufficient evidence that a true answer is accessible, (34a).

• relevance : Question W → Prop

  The speaker considers answering the question relevant to the discourse goals, (34b).

• nonempty : self.uq.Nonempty
• info_eq (q : Question W) : q ∈ self.uq → q.info = self.info
• comparable (q : Question W) : q ∈ self.uq → ∀ q' ∈ self.uq, q ≠ q' → WiderThan q q' ∨ WiderThan q' q

def DeoThomas2025.Context.Answerable {W : Type u_1} (c : Context W) (q : Question W) : Prop

A question is answerable when it satisfies Quality and Relevance, (34).

Equations

• c.Answerable q = (c.quality q ∧ c.relevance q)

def DeoThomas2025.Context.IsWidest {W : Type u_1} (c : Context W) (q : Question W) : Prop

A construal is the widest, (33), when none is wider.

Equations

• c.IsWidest q = (q ∈ c.uq ∧ ∀ q' ∈ c.uq, ¬DeoThomas2025.WiderThan q' q)

def DeoThomas2025.Context.IsOptimal {W : Type u_1} (c : Context W) (q : Question W) : Prop

A construal is optimal, (35), when it is answerable and no wider construal is.

Equations

• c.IsOptimal q = (q ∈ c.uq ∧ c.Answerable q ∧ ∀ q' ∈ c.uq, c.Answerable q' → ¬DeoThomas2025.WiderThan q' q)

theorem DeoThomas2025.Context.IsWidest.unique {W : Type u_1} {c : Context W} {q q' : Question W} (h : c.IsWidest q) (h' : c.IsWidest q') : q = q'

The widest construal is unique, since any two construals are comparable.

theorem DeoThomas2025.Context.IsOptimal.unique {W : Type u_1} {c : Context W} {q q' : Question W} (h : c.IsOptimal q) (h' : c.IsOptimal q') : q = q'

The optimal construal is unique, as the definite description of (35) requires.

theorem DeoThomas2025.Context.IsWidest.isOptimal {W : Type u_1} {c : Context W} {q : Question W} (h : c.IsWidest q) (ha : c.Answerable q) : c.IsOptimal q

The widest construal, when answerable, is the optimal one, (37a).

theorem DeoThomas2025.Context.IsOptimal.not_answerable {W : Type u_1} {c : Context W} {q q' : Question W} (h : c.IsOptimal q) (hq' : q' ∈ c.uq) (hw : WiderThan q' q) : ¬c.Answerable q'

No construal wider than the optimal one is answerable.

theorem DeoThomas2025.Context.IsOptimal.widest_or_quality_or_relevance {W : Type u_1} {c : Context W} {q : Question W} (h : c.IsOptimal q) : c.IsWidest q ∨ (∃ q' ∈ c.uq, WiderThan q' q ∧ ¬c.quality q') ∨ ∃ q' ∈ c.uq, WiderThan q' q ∧ c.quality q' ∧ ¬c.relevance q'

An optimal construal is the widest, or some wider construal fails Quality, or some wider construal satisfies Quality and fails Relevance, the three kinds of context of (37).

theorem DeoThomas2025.Context.isOptimal_ofSet_iff {W : Type u_1} {c : Context W} (hmem : Question.ofSet c.info ∈ c.uq) (hnt : ∀ q ∈ c.uq, q ≠ Question.ofSet c.info → ∃ p ∈ q.alt, p ≠ c.info) : c.IsOptimal (Question.ofSet c.info) ↔ c.Answerable (Question.ofSet c.info) ∧ ∀ q ∈ c.uq, q ≠ Question.ofSet c.info → ¬c.Answerable q

The trivial construal is optimal exactly when it is answerable and no other construal is, as in the unexplanatory use, where the others fail Quality, and the unelaboratory use, where they fail Relevance, §4.4 and §4.5.

The lexical entry, (36)

noncomputable def DeoThomas2025.just {W : Type u_1} (c : Context W) (cq : Question W) (p : Set W) : W → SignType

Just with the current question cq and prejacent p presupposes that cq is the optimal construal of the underspecified question and asserts p, (36).

Equations

• DeoThomas2025.just c cq p = {_w : W | c.IsOptimal cq}.indicator fun (w : W) => SignType.ofProp (w ∈ p)

@[simp]

theorem DeoThomas2025.just_eq_zero_iff {W : Type u_1} {c : Context W} {cq : Question W} {p : Set W} {w : W} : just c cq p w = 0 ↔ ¬c.IsOptimal cq

@[simp]

theorem DeoThomas2025.just_eq_one_iff {W : Type u_1} {c : Context W} {cq : Question W} {p : Set W} {w : W} : just c cq p w = 1 ↔ c.IsOptimal cq ∧ w ∈ p

theorem DeoThomas2025.eq_of_just_ne_zero {W : Type u_1} {c : Context W} {cq cq' : Question W} {p p' : Set W} {w w' : W} (h : just c cq p w ≠ 0) (h' : just c cq' p' w' ≠ 0) : cq = cq'

Two defined uses of just in one context address the same current question, since the presupposition fixes the construal.

Partitions: refinement is width, §4.2 and §4.7

theorem DeoThomas2025.widerThan_fromSetoid {W : Type u_1} {r s : Setoid W} (h : r < s) : WiderThan (Question.fromSetoid r) (Question.fromSetoid s)

A finer partition of the common ground is a wider construal, (40b) against (40a).

Grains, (22) to (24), and Figure 1

theorem DeoThomas2025.widerThan_grain {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] {ε₁ ε₂ : α} (h₁ : 0 < ε₁) (h : ε₁ < ε₂) : WiderThan (Question.fromSetoid (Degree.grain ε₁)) (Question.fromSetoid (Degree.grain ε₂))

The finer grain is the wider construal, (23) and §4.7.1, since no cell of the coarser grain is properly contained in a cell of the finer one and the finer cell around 0 is properly contained in the coarser cell around 0.

theorem DeoThomas2025.figure1 : WiderThan (Question.fromSetoid (Degree.grain (1 / 2))) (Question.fromSetoid (Degree.grain 1)) ∧ ¬Degree.grain (1 / 2) ≤ Degree.grain 1 ∧ ¬Question.fromSetoid (Degree.grain (1 / 2)) ≤ Question.fromSetoid (Degree.grain 1)

In Figure 1, in years, the half-year grain is wider than the year grain but does not refine it, since halving the width never refines a grain; so the construals are ordered by width and not by [GS84]'s entailment, fn. 20.

Extreme adjectives, §4.8

def DeoThomas2025.zone (m : ℕ) : Setoid ℕ

The construal of a degree question whose zone of indifference, [Mor12], begins at m distinguishes the degrees below m and identifies those from m on.

Equations

• DeoThomas2025.zone m = Setoid.ker fun (x : ℕ) => min x m

theorem DeoThomas2025.widerThan_zone {m m' : ℕ} (h : m < m') : WiderThan (Question.fromSetoid (zone m')) (Question.fromSetoid (zone m))

A construal whose zone of indifference begins later is finer and so wider, Figure 2; the emphatic use takes the zone to begin as late as the speaker can conceive.

Constituent questions, §4.1

def DeoThomas2025.mentionAll {A : Type u_2} : Question (Set A)

The mention-all construal of which x is P?, over worlds that are extensions of P, has one alternative per nonempty extension.

Equations

• DeoThomas2025.mentionAll = Question.which {E : Set A | E.Nonempty} fun (E : Set A) => {E}

def DeoThomas2025.mentionSome {A : Type u_2} : Question (Set A)

The mention-some construal has one alternative per individual, the worlds in which it is P.

Equations

• DeoThomas2025.mentionSome = Question.which Set.univ fun (a : A) => {E : Set A | a ∈ E}

theorem DeoThomas2025.widerThan_mentionAll {A : Type u_2} [Nontrivial A] : WiderThan mentionAll mentionSome

The mention-all construal of a constituent question is wider than the mention-some one, §4.1, since none of its alternatives is entailed by an alternative of the mention-some construal.