Question Support — cross-tradition s ⊨ Q interface

A theory-neutral typeclass for the relation "state s supports / resolves question Q". The literature calls this support in inquisitive semantics (s ⊨ Q); the @cite{ginzburg-2012} KOS framework calls it answerhood (a fact resolves a question); decision-theoretic and TTR variants give yet other names. This file fixes the shared mathlib-shaped interface.

Why two classes

Different consumers of the support relation have different decidability profiles. Mathlib's pattern (compare LE vs LinearOrder) is to expose the bare relation as one typeclass and refine it for decidable-evaluation use cases:

• Support State Question — bare Prop-valued relation. Inquisitive (Set W) ⊨ (Question W) lives here: set membership in a LowerSet is generally undecidable, so the substrate provides only the relation.
• DecidableSupport State Question — extends Support with per-pair decidability. KOS's String/String, partition, and TTR instances all live here: their underlying = / BEq / pattern-match resolution is genuinely decidable. KOS QUD-downdate (DGB.downdateQud) and the list-based allResolvedList aggregator demand this refinement.

Consumers requiring only the relation take [Support …]; consumers that evaluate the relation (filter, decide, list aggregation) take [DecidableSupport …].

Notation

Scoped s ⊨ q for Support.supports s q lives in Core.Question so it can coexist with the inquisitive s ⊨ p from Core.Question.Basic (once the namespace consolidates, this notation simply becomes the canonical one).

Specialisations

• Core.Question.Relevance — partiallyAnswers and moveRelevant (Roberts QUD-relevance) over Question W. Specific notions, not a typeclass.
• Semantics.Questions.Resolution — Resolves, MentionSome, MentionAll over Set W → Question W. Each is a candidate Support instance for the inquisitive substrate.
• Phenomena/Focus/Studies/IppolitoKissWilliams2022.lean — IKW evidential SUPPORT (introduced in @cite{ippolito-kiss-williams-2022}, reused by @cite{ippolito-kiss-williams-2025}): doxastic + probabilistic. Prior-parameterised, so it does not fit this typeclass; see that file's Supports directly.

class Core.Question.Support (State : Type u_1) (Question : Type u_2) : Type (max u_1 u_2)

The state s supports / resolves the question q.

In inquisitive semantics this is s ⊨ Q (@cite{ciardelli-groenendijk-roelofsen-2018}); in @cite{ginzburg-2012} this is "FACTS contextually entail an answer to q". The interface is intentionally minimal: just the binary relation. The specialisations — exhaustive, mention-some, partial, probabilistic — each refine this base.

• supports : State → Question → Prop

  The support / resolution relation.

def Core.Question.«term_⊨_» : Lean.TrailingParserDescr

The support / resolution relation.

Equations

• Core.Question.«term_⊨_» = Lean.ParserDescr.trailingNode `Core.Question.«term_⊨_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊨ ") (Lean.ParserDescr.cat `term 0))

class Core.Question.DecidableSupport (State : Type u_1) (Question : Type u_2) extends Core.Question.Support State Question : Type (max u_1 u_2)

Support relation with decidable evaluation. Refines Support with the per-pair decidability needed by KOS QUD-downdate and similar consumers. Mirrors mathlib's LinearOrder extends PartialOrder pattern, where the refinement adds decidableLE etc. fields.

• supports : State → Question → Prop
• decSupports (s : State) (q : Question) : Decidable (Support.supports s q)

  Per-pair decidability of Support.supports.

def Core.Question.Support.AllResolved {State : Type u_1} {Question : Type u_2} [Support State Question] (states : Set State) (questions : Set Question) : Prop

Every question in questions is supported by some state in states. The carrier-agnostic mathlib shape: Set quantification over the support relation.

Equations

• Core.Question.Support.AllResolved states questions = ∀ (q : Question), q ∈ questions → ∃ (s : State), s ∈ states ∧ Core.Question.Support.supports s q

def Core.Question.DecidableSupport.allResolvedList {State : Type u_1} {Question : Type u_2} [DecidableSupport State Question] (states : List State) (questions : List Question) : Prop

Every question in the list is supported by some state in the list. Specialisation of Support.AllResolved for ordered carriers (KOS QUD stacks).

Equations

• Core.Question.DecidableSupport.allResolvedList states questions = ∀ (q : Question), q ∈ questions → ∃ (s : State), s ∈ states ∧ Core.Question.Support.supports s q

@[implicit_reducible]

instance Core.Question.DecidableSupport.allResolvedList.instDecidable {State : Type u_1} {Question : Type u_2} [DecidableSupport State Question] (states : List State) (questions : List Question) : Decidable (allResolvedList states questions)

Equations

• Core.Question.DecidableSupport.allResolvedList.instDecidable states questions = id inferInstance