Kernel Semantics for Epistemic Modals

@cite{von-fintel-gillies-2010} @cite{von-fintel-gillies-2021}

@cite{von-fintel-gillies-2010} kernel semantics. Epistemic modals carry an evidential presupposition that the prejacent is not directly settled by the kernel K ⊆ B_K. The central result (entailment_settling_gap) is that B_K can entail φ without K directly settling it, making the presupposition non-trivial.

The 2021 paper extends the analysis to can't, exposing a dilemma for the weakness Mantra: no assignment of force to can't simultaneously explains its evidential distribution (Observation 4) and its incompatibility with it's possible (Observation 5). Kernel semantics resolves this because can't φ = must(¬φ) is simultaneously strong and evidentially constrained.

Helpers

Kernel structure (@cite{von-fintel-gillies-2010} Def 4)

structure Semantics.Modality.Kernel : Type

A kernel: a set of direct-information propositions with B_K = ⋂K.

• props : List (BProp Attitudes.Intensional.World)

def Semantics.Modality.Kernel.base (k : Kernel) : List Attitudes.Intensional.World

B_K = ⋂K.

Equations

• k.base = Semantics.Modality.Kratzer.propIntersection k.props

def Semantics.Modality.Kernel.toModalBase (k : Kernel) : Kratzer.ModalBase

Convert to a context-independent modal base.

Equations

• k.toModalBase x✝ = k.props

def Semantics.Modality.Kernel.isConsistent (k : Kernel) : Bool

Consistency: B_K ≠ ∅.

Equations

• k.isConsistent = Semantics.Modality.Kratzer.isConsistent k.props

def Semantics.Modality.Kernel.followsFrom (k : Kernel) (φ : BProp Attitudes.Intensional.World) : Bool

φ follows from K iff B_K ⊆ ⟦φ⟧.

Equations

• k.followsFrom φ = Semantics.Modality.Kratzer.followsFrom φ k.props

def Semantics.Modality.Kernel.toEpistemicFlavor (k : Kernel) : Kratzer.EpistemicFlavor

Induce an EpistemicFlavor for Kratzer modal evaluation.

Equations

• k.toEpistemicFlavor = { evidence := k.toModalBase }

@[reducible, inline]

abbrev Semantics.Modality.KernelBackground : Type

World-dependent kernel assignment K^c(w).

Equations

• Semantics.Modality.KernelBackground = (Semantics.Attitudes.Intensional.World → Semantics.Modality.Kernel)

def Semantics.Modality.KernelBackground.toModalBase (kb : KernelBackground) : Kratzer.ModalBase

Convert to a Kratzer modal base.

Equations

• kb.toModalBase w = (kb w).props

Settling (@cite{von-fintel-gillies-2010} Def 5)

def Semantics.Modality.directlySettlesExplicit (k : Kernel) (φ : BProp Attitudes.Intensional.World) : Bool

K directly settles P iff some X ∈ K entails P or is incompatible with P (Implementation 1).

Equations

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

def Semantics.Modality.refine (partition : List (List Attitudes.Intensional.World)) (φ : BProp Attitudes.Intensional.World) : List (List Attitudes.Intensional.World)

Refine a partition along φ-boundaries (@cite{von-fintel-gillies-2010} subject matter).

Equations

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

def Semantics.Modality.kernelPartition (k : Kernel) : List (List Attitudes.Intensional.World)

The partition S_K generated by K (@cite{von-fintel-gillies-2010} Def 7).

Equations

• Semantics.Modality.kernelPartition k = List.foldl Semantics.Modality.refine [Semantics.Attitudes.Intensional.allWorlds] k.props

def Semantics.Modality.settlesByPartition (k : Kernel) (φ : BProp Attitudes.Intensional.World) : Bool

K settles P via partition iff P is a union of cells in S_K (Implementation 2).

Equations

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

theorem Semantics.Modality.explicit_implies_entailment (k : Kernel) (φ : BProp Attitudes.Intensional.World) (h : directlySettlesExplicit k φ = true) : k.followsFrom φ = true ∨ (k.followsFrom fun (w : Attitudes.Intensional.World) => !φ w) = true

What both implementations share: settling implies entailment. If K directly settles φ (Implementation 1), then B_K ⊆ ⟦φ⟧ or B_K ⊆ ⟦¬φ⟧. If X ∈ K entails φ then B_K ⊆ X ⊆ ⟦φ⟧; if X excludes φ then B_K ⊆ X ⊆ ⟦¬φ⟧.

theorem Semantics.Modality.partition_implies_entailment (k : Kernel) (φ : BProp Attitudes.Intensional.World) (h : settlesByPartition k φ = true) : k.followsFrom φ = true ∨ (k.followsFrom fun (w : Attitudes.Intensional.World) => !φ w) = true

Partition settling implies entailment: if S_K settles φ then B_K ⊆ ⟦φ⟧ or B_K ⊆ ⟦¬φ⟧. All worlds in B_K agree on every X ∈ K (they all satisfy every X), so they occupy a single cell of S_K. If that cell is φ-uniform, B_K inherits the uniformity.

Modal operators (@cite{von-fintel-gillies-2010} Defs 5–6)

def Semantics.Modality.kernelMust (k : Kernel) (φ : BProp Attitudes.Intensional.World) : Core.Presupposition.PrProp Attitudes.Intensional.World

⟦must φ⟧: presupposes K doesn't settle φ; asserts B_K ⊆ ⟦φ⟧.

Equations

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

def Semantics.Modality.kernelMight (k : Kernel) (φ : BProp Attitudes.Intensional.World) : Core.Presupposition.PrProp Attitudes.Intensional.World

⟦might φ⟧: presupposes K doesn't settle φ; asserts B_K ∩ ⟦φ⟧ ≠ ∅.

Equations

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

def Semantics.Modality.kernelCant (k : Kernel) (φ : BProp Attitudes.Intensional.World) : Core.Presupposition.PrProp Attitudes.Intensional.World

⟦can't φ⟧ = must(¬φ).

Equations

• Semantics.Modality.kernelCant k φ = Semantics.Modality.kernelMust k fun (w : Semantics.Attitudes.Intensional.World) => !φ w

def Semantics.Modality.kernelMustW (kb : KernelBackground) (φ : BProp Attitudes.Intensional.World) : Core.Presupposition.PrProp Attitudes.Intensional.World

World-dependent ⟦must φ⟧.

Equations

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

def Semantics.Modality.kernelMightW (kb : KernelBackground) (φ : BProp Attitudes.Intensional.World) : Core.Presupposition.PrProp Attitudes.Intensional.World

World-dependent ⟦might φ⟧.

Equations

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

Core properties

theorem Semantics.Modality.must_is_strong (k : Kernel) (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (_hDef : (kernelMust k φ).presup w = true) : (kernelMust k φ).assertion w = Kratzer.simpleNecessity k.toModalBase φ w

Must is strong: when defined, must φ = universal necessity over B_K.

theorem Semantics.Modality.must_entails_prejacent (k : Kernel) (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hReal : w ∈ k.base) (_hDef : (kernelMust k φ).presup w = true) (hTrue : (kernelMust k φ).assertion w = true) : φ w = true

T axiom: must φ entails φ when B_K is realistic (w ∈ B_K).

theorem Semantics.Modality.kernel_duality (k : Kernel) (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : (kernelMight k φ).assertion w = !(kernelMust k fun (w' : Attitudes.Intensional.World) => !φ w').assertion w

Duality: might φ ↔ ¬(must ¬φ) in assertion content.

theorem Semantics.Modality.empty_kernel_always_defined (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : (kernelMust { props := [] } φ).presup w = true

Empty kernel: nothing is settled, so must is always defined.

Bridge to Kratzer.lean

theorem Semantics.Modality.kernelMust_eq_simpleNecessity (k : Kernel) (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : (kernelMust k φ).assertion w = Kratzer.simpleNecessity k.toModalBase φ w

Kernel must assertion = Kratzer simple necessity.

theorem Semantics.Modality.kernelMust_eq_necessity (k : Kernel) (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : (kernelMust k φ).assertion w = Kratzer.necessity k.toModalBase Kratzer.emptyBackground φ w

Kernel must assertion = full Kratzer necessity with empty ordering.

This extends kernelMust_eq_simpleNecessity by connecting through kernelMust_eq_simpleNecessity: kernel must = simple necessity.

theorem Semantics.Modality.kernelMust_eq_epistemicNecessity (k : Kernel) (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : (kernelMust k φ).assertion w = Kratzer.necessity k.toEpistemicFlavor.evidence k.toEpistemicFlavor.ordering φ w

Kernel must assertion = Kratzer necessity evaluated via EpistemicFlavor.

This bridges the kernel (@cite{von-fintel-gillies-2010}) to Kratzer's parametric semantics: kernel must is exactly Kratzer necessity with the kernel's epistemic flavor.

theorem Semantics.Modality.kernelMustW_eq_necessity (kb : KernelBackground) (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : (kernelMustW kb φ).assertion w = Kratzer.necessity kb.toModalBase Kratzer.emptyBackground φ w

World-dependent kernel must = world-dependent Kratzer necessity.

kernelMustW kb φ asserts necessity (kb.toModalBase) emptyBackground φ at each world.

Mastermind example (@cite{von-fintel-gillies-2010} pp. 365–366)

w0 = red, w1 = blue, w2 = green, w3 = unknown. K = {redOrBlue, notRed}, B_K = {w1}.

theorem Semantics.Modality.mastermind_base : Semantics.Modality.mastermindK✝.base = [Core.Proposition.World4.w1]

theorem Semantics.Modality.mastermind_blue_unsettled : directlySettlesExplicit Semantics.Modality.mastermindK✝ Semantics.Modality.blue✝ = false

theorem Semantics.Modality.mastermind_blue_follows : Semantics.Modality.mastermindK✝.followsFrom Semantics.Modality.blue✝ = true

theorem Semantics.Modality.mastermind_must_blue_defined : (kernelMust Semantics.Modality.mastermindK✝ Semantics.Modality.blue✝).presup Core.Proposition.World4.w0 = true

theorem Semantics.Modality.mastermind_must_blue_true : (kernelMust Semantics.Modality.mastermindK✝ Semantics.Modality.blue✝).assertion Core.Proposition.World4.w0 = true

theorem Semantics.Modality.mastermind_red_settled : directlySettlesExplicit Semantics.Modality.mastermindK✝ Semantics.Modality.red✝ = true

theorem Semantics.Modality.mastermind_might_red_undefined : (kernelMight Semantics.Modality.mastermindK✝ Semantics.Modality.red✝).presup Core.Proposition.World4.w0 = false

theorem Semantics.Modality.mastermind_redOrBlue_settled : directlySettlesExplicit Semantics.Modality.mastermindK✝ Semantics.Modality.redOrBlue✝ = true

Non-equivalence of the two implementations (@cite{von-fintel-gillies-2010} §7, p. 379)

The explicit and partition-based implementations of "directly settles" are non-equivalent. Implementation 1 settles supersets of K-propositions that Implementation 2 misses; Implementation 2 settles propositions determined jointly by K-propositions that no single proposition settles. Both, however, imply entailment (see explicit_implies_entailment and partition_implies_entailment above).

theorem Semantics.Modality.explicit_not_implies_partition : ∃ (k : Kernel) (φ : BProp Attitudes.Intensional.World), directlySettlesExplicit k φ = true ∧ settlesByPartition k φ = false

Counterexample (Impl 1 ↛ Impl 2): K = {red}, φ = redOrBlue. red ⊆ redOrBlue so Impl 1 settles, but S_K = {{w0},{w1,w2,w3}} and the cell {w1,w2,w3} straddles redOrBlue.

theorem Semantics.Modality.partition_not_implies_explicit : ∃ (k : Kernel) (φ : BProp Attitudes.Intensional.World), settlesByPartition k φ = true ∧ directlySettlesExplicit k φ = false

Counterexample (Impl 2 ↛ Impl 1): K = mastermindK, φ = blue. No single X ∈ K entails or excludes blue, but S_K = {{w0},{w1},{w2,w3}} resolves blue into a union of cells.

theorem Semantics.Modality.entailment_not_implies_partition : ∃ (k : Kernel) (φ : BProp Attitudes.Intensional.World), k.followsFrom φ = true ∧ settlesByPartition k φ = false

Entailment does not imply partition settling: B_K ⊆ ⟦φ⟧ does not guarantee S_K settles φ. Same witness as explicit_not_implies_partition: K = {red} entails redOrBlue (B_K = {w0} ⊆ ⟦redOrBlue⟧) but the partition cell {w1,w2,w3} straddles redOrBlue.

Deep theorems (@cite{von-fintel-gillies-2010})

theorem Semantics.Modality.entailment_settling_gap : ∃ (k : Kernel) (φ : BProp Attitudes.Intensional.World), k.followsFrom φ = true ∧ directlySettlesExplicit k φ = false

Entailment-settling gap: B_K can entail φ without K settling it. This gap makes the evidential presupposition non-trivial: must φ can be simultaneously defined and true.

theorem Semantics.Modality.indirectness_neq_weakness : ((kernelMust Semantics.Modality.mastermindK✝ Semantics.Modality.blue✝).presup Core.Proposition.World4.w0 = true ∧ (kernelMust Semantics.Modality.mastermindK✝¹ Semantics.Modality.blue✝¹).assertion Core.Proposition.World4.w0 = true) ∧ (kernelMust Semantics.Modality.mastermindK✝² Semantics.Modality.red✝).presup Core.Proposition.World4.w0 = false ∧ (kernelMust Semantics.Modality.indirectK✝ Semantics.Modality.blue✝²).presup Core.Proposition.World4.w0 = true ∧ (kernelMust Semantics.Modality.indirectK✝¹ Semantics.Modality.blue✝³).assertion Core.Proposition.World4.w0 = false

Indirectness ≠ weakness: three independent cases show indirectness and assertion strength are orthogonal dimensions.

theorem Semantics.Modality.modus_ponens_with_must (k : Kernel) (φ ψ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hReal : w ∈ k.base) (_hDef : (kernelMust k ψ).presup w = true) (hCond : φ w = true → (kernelMust k ψ).assertion w = true) (hPhi : φ w = true) : ψ w = true

Modus ponens with must (@cite{von-fintel-gillies-2010} Arg 4.3.1): the argument form "if φ, must ψ; φ; ∴ ψ" is valid under realistic B_K.

theorem Semantics.Modality.must_perhaps_contradiction (k : Kernel) (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (_hDef : (kernelMust k φ).presup w = true) (hMust : (kernelMust k φ).assertion w = true) : (kernelMight k fun (w' : Attitudes.Intensional.World) => !φ w').assertion w = false

Must-perhaps contradiction (@cite{von-fintel-gillies-2010} Arg 4.3.2): must φ ∧ might ¬φ is contradictory. When B_K ⊆ ⟦φ⟧, we have B_K ∩ ⟦¬φ⟧ = ∅.

theorem Semantics.Modality.direct_evidence_infelicity (k : Kernel) (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hSettled : directlySettlesExplicit k φ = true) : (kernelMust k φ).presup w = false

Direct evidence infelicity: when K settles φ, must φ is undefined.

theorem Semantics.Modality.settling_monotone (k : Kernel) (p φ : BProp Attitudes.Intensional.World) (hSettled : directlySettlesExplicit k φ = true) : directlySettlesExplicit { props := p :: k.props } φ = true

Settling is monotone: more propositions in K means more is settled.

Can't dilemma (@cite{von-fintel-gillies-2021} §4, Observations 4–5)

The Mantra faces a dilemma: no assignment of force to can't simultaneously explains its evidential distribution (paralleling must) and its incompatibility with it's possible that φ. Kernel semantics resolves this because can't φ = must(¬φ) is strong AND evidentially constrained.

theorem Semantics.Modality.cant_might_exclusion (k : Kernel) (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hCant : (kernelCant k φ).assertion w = true) : (kernelMight k φ).assertion w = false

Can't–might exclusion (@cite{von-fintel-gillies-2021} Obs 5): when can't φ holds (B_K ⊆ ⟦¬φ⟧), might φ is false (B_K ∩ ⟦φ⟧ = ∅).

theorem Semantics.Modality.cant_entails_negation (k : Kernel) (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) (hReal : w ∈ k.base) (_hDef : (kernelCant k φ).presup w = true) (hTrue : (kernelCant k φ).assertion w = true) : φ w = false

Can't entails negation (@cite{von-fintel-gillies-2021} via S2): when B_K is realistic and can't φ is defined and true, φ(w) = false.

theorem Semantics.Modality.cant_evidential_parallel (k : Kernel) (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : (kernelCant k φ).presup w = (kernelMust k fun (w' : Attitudes.Intensional.World) => !φ w').presup w

Can't evidential parallelism (@cite{von-fintel-gillies-2021} Obs 4): can't φ has the same presupposition structure as must(¬φ).

theorem Semantics.Modality.cant_dilemma_resolved : List.elem Core.Proposition.World4.w1 Semantics.Modality.mastermindK✝.base = true ∧ (kernelCant Semantics.Modality.mastermindK✝¹ Semantics.Modality.notBlue✝).presup Core.Proposition.World4.w1 = true ∧ (kernelCant Semantics.Modality.mastermindK✝² Semantics.Modality.notBlue✝¹).assertion Core.Proposition.World4.w1 = true ∧ (kernelMight Semantics.Modality.mastermindK✝³ Semantics.Modality.notBlue✝²).assertion Core.Proposition.World4.w1 = false ∧ Semantics.Modality.notBlue✝³ Core.Proposition.World4.w1 = false

Can't dilemma resolved: a single kernel simultaneously exhibits evidentiality, strength, and might-exclusion. Witness: K = {redOrBlue, notRed}, φ = notBlue. Then can't(notBlue) = must(blue), which is defined (blue unsettled), true (B_K ⊆ ⟦blue⟧), and excludes might(notBlue).

theorem Semantics.Modality.cant_direct_evidence_infelicity : (kernelCant Semantics.Modality.mastermindK✝ Semantics.Modality.red✝).presup Core.Proposition.World4.w0 = false

Direct evidence blocks can't, paralleling must: when K settles ¬φ, can't φ has presupposition failure.

theorem Semantics.Modality.cant_eq_must_neg (k : Kernel) (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : (kernelCant k φ).presup w = (kernelMust k fun (w' : Attitudes.Intensional.World) => !φ w').presup w ∧ (kernelCant k φ).assertion w = (kernelMust k fun (w' : Attitudes.Intensional.World) => !φ w').assertion w

can't φ and must(¬φ) are intensionally identical.

Prior information state and nandao-Q felicity

@cite{zheng-2025} shows Mandarin nandao-Qs are evidence-driven, not bias-driven. The felicity condition has three parts: (i) evidence in K supports the prejacent, (ii) K conflicts with prior expectations U, (iii) the prejacent is not directly settled in K. Condition (iii) is the same presupposition as kernelMust.

@[reducible, inline]

abbrev Semantics.Modality.Background : Type

Prior information state (beliefs, norms, desires) before encountering evidence. Distinct from the kernel (direct evidence) and the CG (shared).

Equations

• Semantics.Modality.Background = List (BProp Semantics.Attitudes.Intensional.World)

def Semantics.Modality.backgroundBase (u : Background) : List Attitudes.Intensional.World

B_U = ⋂U: worlds compatible with the prior information state.

Equations

• Semantics.Modality.backgroundBase u = Semantics.Modality.Kratzer.propIntersection u

def Semantics.Modality.Kernel.incompatibleWith (k : Kernel) (u : Background) : Bool

K and U are incompatible: B_K ∩ B_U = ∅ (the evidence is unexpected).

Equations

• k.incompatibleWith u = !Semantics.Modality.Kratzer.isConsistent (k.props ++ u)

def Semantics.Modality.evidenceRaises (p φ : BProp Attitudes.Intensional.World) : Bool

Evidence p raises the probability of φ: P(φ|p) > P(φ). Computed via cross-multiplication to avoid rationals.

Equations

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

def Semantics.Modality.Kernel.evidenceSupports (k : Kernel) (φ : BProp Attitudes.Intensional.World) : Bool

Some proposition in K raises the probability of φ (condition i).

Equations

• k.evidenceSupports φ = k.props.any fun (x : BProp Semantics.Attitudes.Intensional.World) => Semantics.Modality.evidenceRaises x φ

def Semantics.Modality.nandaoFelicitous (k : Kernel) (u : Background) (φ : BProp Attitudes.Intensional.World) : Bool

Nandao-Q felicity (@cite{zheng-2025}, condition 11 for polar questions): (i) some evidence in K raises P(φ), (ii) K and U are incompatible (evidence is unexpected), (iii) φ is not directly settled in K.

Equations

• Semantics.Modality.nandaoFelicitous k u φ = (k.evidenceSupports φ && k.incompatibleWith u && !Semantics.Modality.directlySettlesExplicit k φ)

theorem Semantics.Modality.nandao_must_presupposition (k : Kernel) (φ : BProp Attitudes.Intensional.World) (w : Attitudes.Intensional.World) : (!directlySettlesExplicit k φ) = (kernelMust k φ).presup w

Nandao condition (iii) = presupposition of kernelMust.

theorem Semantics.Modality.nandao_pure_inquiry (k : Kernel) (u : Background) (φ : BProp Attitudes.Intensional.World) (hEv : k.evidenceSupports φ = true) (hInc : k.incompatibleWith u = true) (hUns : directlySettlesExplicit k φ = false) : nandaoFelicitous k u φ = true

Pure inquiry: nandao is felicitous without epistemic bias (@cite{zheng-2025} ex. 3). The three conditions suffice; no prior belief about φ is required.

Dripping raincoat scenario (@cite{zheng-2025} exx. 2–3, 5)

w0 = raining, w1 = sprinkler (wet but not rain), w2 = dry, w3 = unknown. K = {wearingRaincoat}: direct evidence that someone entered with a wet coat. U = {expectDry}: prior expectation of no rain (normative or doxastic).

theorem Semantics.Modality.raincoat_nandao_felicitous : nandaoFelicitous Semantics.Modality.raincoatK✝ Semantics.Modality.dryU✝ Semantics.Modality.isRaining✝ = true

"Nandao waimian xiayu-le ma?" is felicitous with a dripping raincoat. P(rain|coat) = 1/2 > P(rain) = 1/4; K ∩ U = ∅; rain unsettled by K.

theorem Semantics.Modality.no_evidence_nandao_infelicitous : nandaoFelicitous { props := [] } Semantics.Modality.dryU✝ Semantics.Modality.isRaining✝ = false

Without evidence, nandao is infelicitous (@cite{zheng-2025} ex. 5 ctx 2).

theorem Semantics.Modality.expected_evidence_infelicitous : have expectWet := [Semantics.Modality.wearingRaincoat✝]; nandaoFelicitous Semantics.Modality.raincoatK✝ expectWet Semantics.Modality.isRaining✝ = false

When evidence is expected (K compatible with U), nandao is infelicitous (@cite{zheng-2025} ex. 6 ctx 2).

theorem Semantics.Modality.nandao_mastermind_bridge : (kernelMust Semantics.Modality.mastermindK✝ Semantics.Modality.blue✝).presup Core.Proposition.World4.w0 = true ∧ (!decide (directlySettlesExplicit Semantics.Modality.mastermindK✝¹ Semantics.Modality.blue✝¹ = true)) = true

Nandao reuses the mastermind kernel: "must blue" and "nandao blue?" share condition (iii). When must is defined, nandao's indirectness condition holds.