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 (W : Type u_2) : Type u_2

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

• props : List (W → Prop)

def Semantics.Modality.Kernel.base {W : Type u_1} (k : Kernel W) : Set W

B_K = ⋂K.

Equations

• k.base = Core.Logic.Intensional.Premise.propIntersection k.props

def Semantics.Modality.Kernel.toModalBase {W : Type u_1} (k : Kernel W) : Core.Logic.Intensional.ModalBase W

Convert to a context-independent modal base.

Equations

• k.toModalBase x✝ = k.props

def Semantics.Modality.Kernel.isConsistent {W : Type u_1} (k : Kernel W) : Prop

Consistency: B_K ≠ ∅.

Equations

• k.isConsistent = Core.Logic.Intensional.Premise.isConsistent k.props

def Semantics.Modality.Kernel.followsFrom {W : Type u_1} (k : Kernel W) (φ : W → Prop) : Prop

φ follows from K iff B_K ⊆ ⟦φ⟧.

Equations

• k.followsFrom φ = Core.Logic.Intensional.Premise.followsFrom φ k.props

def Semantics.Modality.Kernel.compatibleWith {W : Type u_1} (k : Kernel W) (φ : W → Prop) : Prop

φ is compatible with K iff B_K ∩ ⟦φ⟧ ≠ ∅.

Equations

• k.compatibleWith φ = Core.Logic.Intensional.Premise.isCompatibleWith φ k.props

def Semantics.Modality.Kernel.toEpistemicFlavor {W : Type u_1} (k : Kernel W) : Kratzer.EpistemicFlavor W

Induce an EpistemicFlavor for Kratzer modal evaluation.

Equations

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

@[reducible, inline]

abbrev Semantics.Modality.KernelBackground (W : Type u_2) : Type u_2

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

Equations

• Semantics.Modality.KernelBackground W = (W → Semantics.Modality.Kernel W)

def Semantics.Modality.KernelBackground.toModalBase {W : Type u_1} (kb : KernelBackground W) : Core.Logic.Intensional.ModalBase W

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 {W : Type u_1} (k : Kernel W) (φ : W → Prop) : Prop

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

Equations

• Semantics.Modality.directlySettlesExplicit k φ = ∃ x ∈ k.props, (∀ w ∈ Core.Logic.Intensional.Premise.propExtension x, φ w) ∨ ¬∃ w ∈ Core.Logic.Intensional.Premise.propExtension x, φ w

noncomputable def Semantics.Modality.refine {W : Type u_1} (partition : List (List W)) (φ : W → Prop) : List (List W)

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

Uses Classical.propDecidable internally so the signature can be W → Prop without a [DecidablePred] constraint that would interfere with List.foldl.

Equations

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

noncomputable def Semantics.Modality.kernelPartition {W : Type u_1} [Fintype W] (k : Kernel W) : List (List W)

The partition S_K generated by K (@cite{von-fintel-gillies-2010} Def 7). Requires [Fintype W] to enumerate the starting universe.

Equations

• Semantics.Modality.kernelPartition k = List.foldl Semantics.Modality.refine [Finset.univ.toList] k.props

def Semantics.Modality.settlesByPartition {W : Type u_1} [Fintype W] (k : Kernel W) (φ : W → Prop) : Prop

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

Equations

• Semantics.Modality.settlesByPartition k φ = ∀ cell ∈ Semantics.Modality.kernelPartition k, (∀ w ∈ cell, φ w) ∨ ∀ w ∈ cell, ¬φ w

theorem Semantics.Modality.explicit_implies_entailment {W : Type u_1} (k : Kernel W) (φ : W → Prop) (h : directlySettlesExplicit k φ) : k.followsFrom φ ∨ k.followsFrom fun (w : W) => ¬φ w

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 {W : Type u_1} [Fintype W] (k : Kernel W) (φ : W → Prop) (h : settlesByPartition k φ) : k.followsFrom φ ∨ k.followsFrom fun (w : W) => ¬φ w

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 {W : Type u_1} (k : Kernel W) (φ : W → Prop) : Core.Presupposition.PrProp W

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

Equations

• Semantics.Modality.kernelMust k φ = { presup := fun (x : W) => ¬Semantics.Modality.directlySettlesExplicit k φ, assertion := fun (x : W) => k.followsFrom φ }

def Semantics.Modality.kernelMight {W : Type u_1} (k : Kernel W) (φ : W → Prop) : Core.Presupposition.PrProp W

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

Equations

• Semantics.Modality.kernelMight k φ = { presup := fun (x : W) => ¬Semantics.Modality.directlySettlesExplicit k φ, assertion := fun (x : W) => k.compatibleWith φ }

def Semantics.Modality.kernelCant {W : Type u_1} (k : Kernel W) (φ : W → Prop) : Core.Presupposition.PrProp W

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

Equations

• Semantics.Modality.kernelCant k φ = Semantics.Modality.kernelMust k fun (w : W) => ¬φ w

def Semantics.Modality.kernelMustW {W : Type u_1} (kb : KernelBackground W) (φ : W → Prop) : Core.Presupposition.PrProp W

W-dependent ⟦must φ⟧.

Equations

• Semantics.Modality.kernelMustW kb φ = { presup := fun (w : W) => ¬Semantics.Modality.directlySettlesExplicit (kb w) φ, assertion := fun (w : W) => (kb w).followsFrom φ }

def Semantics.Modality.kernelMightW {W : Type u_1} (kb : KernelBackground W) (φ : W → Prop) : Core.Presupposition.PrProp W

W-dependent ⟦might φ⟧.

Equations

• Semantics.Modality.kernelMightW kb φ = { presup := fun (w : W) => ¬Semantics.Modality.directlySettlesExplicit (kb w) φ, assertion := fun (w : W) => (kb w).compatibleWith φ }

Core properties

theorem Semantics.Modality.must_is_strong {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) (_hDef : (kernelMust k φ).presup w) : (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 {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) (hReal : w ∈ k.base) (_hDef : (kernelMust k φ).presup w) (hTrue : (kernelMust k φ).assertion w) : φ w

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

theorem Semantics.Modality.kernel_duality {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) : (kernelMight k φ).assertion w ↔ ¬(kernelMust k fun (w' : W) => ¬φ w').assertion w

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

theorem Semantics.Modality.empty_kernel_always_defined {W : Type u_1} (φ : W → Prop) (w : W) : (kernelMust { props := [] } φ).presup w

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

Bridge to Kratzer.lean

theorem Semantics.Modality.kernelMust_eq_simpleNecessity {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) : (kernelMust k φ).assertion w ↔ Kratzer.simpleNecessity k.toModalBase φ w

Kernel must assertion ↔ Kratzer simple necessity.

theorem Semantics.Modality.kernelMust_eq_necessity {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) : (kernelMust k φ).assertion w ↔ Kratzer.necessity k.toModalBase Core.Logic.Intensional.emptyBackground φ w

Kernel must assertion ↔ full Kratzer necessity with empty ordering.

theorem Semantics.Modality.kernelMust_eq_epistemicNecessity {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) : (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 {W : Type u_1} (kb : KernelBackground W) (φ : W → Prop) (w : W) : (kernelMustW kb φ).assertion w ↔ Kratzer.necessity kb.toModalBase Core.Logic.Intensional.emptyBackground φ w

W-dependent kernel must ↔ world-dependent Kratzer necessity.

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

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

The example uses a local 4-element World to keep the propositional layout readable; the abstract theory above is generic over any W : Type*.

inductive Semantics.Modality.World : Type

4-world type used by the Mastermind and Raincoat examples. Public so consumers can refer to the same toy type when reusing these examples (e.g., the Zheng 2025 study file consumes raincoatK).

• w0 : World
• w1 : World
• w2 : World
• w3 : World

@[implicit_reducible]

instance Semantics.Modality.instDecidableEqWorld : DecidableEq World

Equations

• Semantics.Modality.instDecidableEqWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Modality.instReprWorld : Repr World

Equations

• Semantics.Modality.instReprWorld = { reprPrec := Semantics.Modality.instReprWorld.repr }

def Semantics.Modality.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

def Semantics.Modality.instInhabitedWorld.default : World

Equations

• Semantics.Modality.instInhabitedWorld.default = Semantics.Modality.World.w0

@[implicit_reducible]

instance Semantics.Modality.instInhabitedWorld : Inhabited World

Equations

• Semantics.Modality.instInhabitedWorld = { default := Semantics.Modality.instInhabitedWorld.default }

@[implicit_reducible]

instance Semantics.Modality.instFintypeWorld : Fintype World

Equations

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

theorem Semantics.Modality.mastermind_base : Semantics.Modality.mastermindK✝.base = {World.w1}

theorem Semantics.Modality.mastermind_blue_unsettled : ¬directlySettlesExplicit Semantics.Modality.mastermindK✝ Semantics.Modality.blue✝

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

theorem Semantics.Modality.mastermind_must_blue_defined : (kernelMust Semantics.Modality.mastermindK✝ Semantics.Modality.blue✝).presup World.w0

theorem Semantics.Modality.mastermind_must_blue_true : (kernelMust Semantics.Modality.mastermindK✝ Semantics.Modality.blue✝).assertion World.w0

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

theorem Semantics.Modality.mastermind_might_red_undefined : ¬(kernelMight Semantics.Modality.mastermindK✝ Semantics.Modality.red✝).presup World.w0

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

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 World) (φ : World → Prop), directlySettlesExplicit k φ ∧ ¬settlesByPartition k φ

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. We refute settlesByPartition by showing .w1 and .w2 are co-located in S_K (they agree on red — both are not-red — so co-location is preserved by foldl_refine_preserves_colocated) yet disagree on redOrBlue.

theorem Semantics.Modality.partition_not_implies_explicit : ∃ (k : Kernel World) (φ : World → Prop), settlesByPartition k φ ∧ ¬directlySettlesExplicit k φ

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. Each cell is {redOrBlue, notRed}- uniform (by kernelPartition_cells_uniform); since blue w ↔ redOrBlue w ∧ notRed w for every world, cells are blue-uniform.

theorem Semantics.Modality.entailment_not_implies_partition : ∃ (k : Kernel World) (φ : World → Prop), k.followsFrom φ ∧ ¬settlesByPartition k φ

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.

TODO: partition-side proof deferred.

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

theorem Semantics.Modality.entailment_settling_gap : ∃ (k : Kernel World) (φ : World → Prop), k.followsFrom φ ∧ ¬directlySettlesExplicit k φ

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 World.w0 ∧ (kernelMust Semantics.Modality.mastermindK✝ Semantics.Modality.blue✝).assertion World.w0) ∧ ¬(kernelMust Semantics.Modality.mastermindK✝ Semantics.Modality.red✝).presup World.w0 ∧ (kernelMust Semantics.Modality.indirectK✝ Semantics.Modality.blue✝).presup World.w0 ∧ ¬(kernelMust Semantics.Modality.indirectK✝ Semantics.Modality.blue✝).assertion World.w0

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

theorem Semantics.Modality.modus_ponens_with_must {W : Type u_1} (k : Kernel W) (φ ψ : W → Prop) (w : W) (hReal : w ∈ k.base) (_hDef : (kernelMust k ψ).presup w) (hCond : φ w → (kernelMust k ψ).assertion w) (hPhi : φ w) : ψ w

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 {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) (_hDef : (kernelMust k φ).presup w) (hMust : (kernelMust k φ).assertion w) : ¬(kernelMight k fun (w' : W) => ¬φ w').assertion w

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 {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) (hSettled : directlySettlesExplicit k φ) : ¬(kernelMust k φ).presup w

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

theorem Semantics.Modality.settling_monotone {W : Type u_1} (k : Kernel W) (p φ : W → Prop) (hSettled : directlySettlesExplicit k φ) : directlySettlesExplicit { props := p :: k.props } φ

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 {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) (hCant : (kernelCant k φ).assertion w) : ¬(kernelMight k φ).assertion w

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 {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) (hReal : w ∈ k.base) (_hDef : (kernelCant k φ).presup w) (hTrue : (kernelCant k φ).assertion w) : ¬φ w

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

theorem Semantics.Modality.cant_evidential_parallel {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) : (kernelCant k φ).presup w = (kernelMust k fun (w' : W) => ¬φ 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 : World.w1 ∈ Semantics.Modality.mastermindK✝.base ∧ (kernelCant Semantics.Modality.mastermindK✝ Semantics.Modality.notBlue✝).presup World.w1 ∧ (kernelCant Semantics.Modality.mastermindK✝ Semantics.Modality.notBlue✝).assertion World.w1 ∧ ¬(kernelMight Semantics.Modality.mastermindK✝ Semantics.Modality.notBlue✝).assertion World.w1 ∧ ¬Semantics.Modality.notBlue✝ World.w1

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 World.w0

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

theorem Semantics.Modality.cant_eq_must_neg {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) : (kernelCant k φ).presup w = (kernelMust k fun (w' : W) => ¬φ w').presup w ∧ (kernelCant k φ).assertion w = (kernelMust k fun (w' : W) => ¬φ 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 (W : Type u_2) : Type u_2

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

Equations

• Semantics.Modality.Background W = List (W → Prop)

def Semantics.Modality.backgroundBase {W : Type u_1} (u : Background W) : Set W

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

Equations

• Semantics.Modality.backgroundBase u = Core.Logic.Intensional.Premise.propIntersection u

def Semantics.Modality.Kernel.incompatibleWith {W : Type u_1} (k : Kernel W) (u : Background W) : Prop

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

Equations

• k.incompatibleWith u = ¬Core.Logic.Intensional.Premise.isConsistent (k.props ++ u)

def Semantics.Modality.evidenceRaises {W : Type u_1} [Fintype W] (p φ : W → Prop) [DecidablePred p] [DecidablePred φ] : Prop

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

The cardinalities are taken over Finset.univ filtered by the respective predicates, which requires [DecidablePred p] and [DecidablePred φ].

Equations

• Semantics.Modality.evidenceRaises p φ = ({w : W | p w ∧ φ w}.card * Finset.univ.card > (Finset.filter φ Finset.univ).card * (Finset.filter p Finset.univ).card)

def Semantics.Modality.Kernel.evidenceSupports {W : Type u_1} [Fintype W] (k : Kernel W) (φ : W → Prop) [DecidablePred φ] : Prop

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

Requires global decidability for kernel propositions; we use Classical.propDecidable since k.props is a list of arbitrary W → Prop.

Equations

• k.evidenceSupports φ = ∃ x ∈ k.props, Semantics.Modality.evidenceRaises x φ

def Semantics.Modality.nandaoFelicitous {W : Type u_1} [Fintype W] (k : Kernel W) (u : Background W) (φ : W → Prop) [DecidablePred φ] : Prop

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 {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) : ¬directlySettlesExplicit k φ ↔ (kernelMust k φ).presup w

Nandao condition (iii) = presupposition of kernelMust.

theorem Semantics.Modality.nandao_pure_inquiry {W : Type u_1} [Fintype W] (k : Kernel W) (u : Background W) (φ : W → Prop) [DecidablePred φ] (hEv : k.evidenceSupports φ) (hInc : k.incompatibleWith u) (hUns : ¬directlySettlesExplicit k φ) : nandaoFelicitous k u φ

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).

def Semantics.Modality.wearingRaincoat : World → Prop

Equations

• Semantics.Modality.wearingRaincoat Semantics.Modality.World.w0 = True
• Semantics.Modality.wearingRaincoat Semantics.Modality.World.w1 = True
• Semantics.Modality.wearingRaincoat w = False

def Semantics.Modality.expectDry : World → Prop

Equations

• Semantics.Modality.expectDry Semantics.Modality.World.w2 = True
• Semantics.Modality.expectDry Semantics.Modality.World.w3 = True
• Semantics.Modality.expectDry w = False

def Semantics.Modality.isRaining : World → Prop

Equations

• Semantics.Modality.isRaining Semantics.Modality.World.w0 = True
• Semantics.Modality.isRaining w = False

@[implicit_reducible]

instance Semantics.Modality.instDecidablePredWorldWearingRaincoat : DecidablePred wearingRaincoat

Equations

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

@[implicit_reducible]

instance Semantics.Modality.instDecidablePredWorldExpectDry : DecidablePred expectDry

Equations

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

@[implicit_reducible]

instance Semantics.Modality.instDecidablePredWorldIsRaining : DecidablePred isRaining

Equations

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

def Semantics.Modality.raincoatK : Kernel World

Equations

• Semantics.Modality.raincoatK = { props := [Semantics.Modality.wearingRaincoat] }

def Semantics.Modality.dryU : Background World

Equations

• Semantics.Modality.dryU = [Semantics.Modality.expectDry]

theorem Semantics.Modality.raincoat_nandao_felicitous : nandaoFelicitous raincoatK dryU isRaining

"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.

TODO: full proof requires unfolding `evidenceSupports` (which uses
`Classical.propDecidable`) into a concrete computation. The proposition
holds — wearingRaincoat raises the probability of isRaining (1/2 vs 1/4) —
but threading the decidability instance through `decide` is delicate.
Statement preserved. 

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

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

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

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

TODO: full proof requires showing the joint kernel + background is
consistent for the wearingRaincoat-only K. Statement preserved. 

theorem Semantics.Modality.nandao_mastermind_bridge : (kernelMust Semantics.Modality.mastermindK✝ Semantics.Modality.blue✝).presup World.w0 ∧ ¬directlySettlesExplicit Semantics.Modality.mastermindK✝ Semantics.Modality.blue✝

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