Kernel Semantics for Epistemic Modals

[vFG10]'s kernel semantics: epistemic modals carry an evidential presupposition that the prejacent is not directly settled by the kernel K — the privileged direct-information part of the modal base (Def 4: B_K = ⋂K). The presupposition makes must φ strong (it asserts B_K ⊆ ⟦φ⟧, Def 5) while still signalling indirectness: B_K can entail φ without K directly settling it.

This file provides the reusable kernel apparatus: the Kernel structure, the explicit-representation implementation of directly-settles (Implementation 1, §7.1), the presuppositional operators kernelMust/kernelMight/kernelCant, and bridges to Kratzer necessity. The paper's second, partition-based implementation (Def 7, §7.2), the non-equivalence of the two implementations, and the worked examples live in Studies/VonFintelGillies2010.lean; the can't dilemma of [vFG21] lives in Studies/VonFintelGillies2021.lean; the nandao-Q felicity conditions built on this apparatus live in Studies/Zheng2025.lean.

Main declarations

• Kernel: direct-information propositions with their modal base B_K = ⋂K, entailment (Kernel.followsFrom), and compatibility (Kernel.compatibleWith)
• Kernel.directlySettles: Implementation 1 — some X ∈ K entails or excludes the prejacent
• explicit_implies_entailment: settling implies entailment; the converse fails, which is what makes the presupposition non-trivial
• kernelMust, kernelMight, kernelCant: the presuppositional operators (Defs 5–6), as PartialProps
• kernelMust_iff_simpleNecessity, kernelMust_iff_necessity: the assertion of kernelMust is Kratzer necessity over the induced modal base

Kernel structure ([vFG10] Def 4)

structure Modality.Kernel (W : Type u_2) : Type u_2

A kernel is a set of direct-information propositions, determining the modal base B_K = ⋂K ([vFG10] Def 4).

• props : List (W → Prop)

  The direct-information propositions K.

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

The modal base B_K = ⋂K determined by the kernel.

Equations

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

def Modality.Kernel.toModalBase {W : Type u_1} (k : Kernel W) : Kratzer.ModalBase W

The kernel as a context-independent modal base.

Equations

• k.toModalBase x✝ = k.props

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

K is consistent iff B_K ≠ ∅.

Equations

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

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

φ follows from K iff B_K ⊆ ⟦φ⟧.

Equations

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

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

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

Equations

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

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

The EpistemicFlavor with the kernel's modal base and empty ordering.

Equations

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

theorem Modality.Kernel.followsFrom_iff {W : Type u_1} (k : Kernel W) (φ : W → Prop) : k.followsFrom φ ↔ ∀ w ∈ k.base, φ w

theorem Modality.Kernel.compatibleWith_iff {W : Type u_1} (k : Kernel W) (φ : W → Prop) : k.compatibleWith φ ↔ ∃ w ∈ k.base, φ w

Settling ([vFG10] §7.1, Implementation 1)

def Modality.Kernel.directlySettles {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.

Equations

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

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

If K directly settles φ then B_K ⊆ ⟦φ⟧ or B_K ⊆ ⟦¬φ⟧; the converse fails (see VonFintelGillies2010.entailment_settling_gap).

theorem Modality.Kernel.directlySettles_mono {W : Type u_1} (k : Kernel W) (φ : W → Prop) {k' : Kernel W} (hk : k.props ⊆ k'.props) (h : k.directlySettles φ) : k'.directlySettles φ

@[simp]

theorem Modality.Kernel.base_singleton {W : Type u_1} (p : W → Prop) : { props := [p] }.base = Intensional.Premise.propExtension p

@[simp]

theorem Modality.Kernel.directlySettles_singleton {W : Type u_1} (φ p : W → Prop) : { props := [p] }.directlySettles φ ↔ Intensional.Premise.propExtension p ⊆ Intensional.Premise.propExtension φ ∨ Disjoint (Intensional.Premise.propExtension p) (Intensional.Premise.propExtension φ)

Modal operators ([vFG10] Defs 5–6)

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

⟦must φ⟧ presupposes that K does not directly settle φ and asserts B_K ⊆ ⟦φ⟧.

Equations

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

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

⟦might φ⟧ presupposes that K does not directly settle φ and asserts B_K ∩ ⟦φ⟧ ≠ ∅.

Equations

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

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

⟦can't φ⟧ is ⟦must ¬φ⟧.

Equations

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

Core properties

theorem Modality.must_entails_prejacent {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) (hReal : w ∈ k.base) (hTrue : (kernelMust k φ).assertion w) : φ w

Must φ entails φ when B_K is realistic (the T axiom).

theorem 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

Might φ and ¬must ¬φ have the same assertion content.

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

The empty kernel settles nothing, so must is always defined.

Bridge to Kratzer necessity

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

The assertion of kernel must is Kratzer simple necessity over the induced modal base.

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

The assertion of kernel must is Kratzer necessity with the empty ordering source.