Kernel semantics for epistemic modals

Von Fintel and Gillies give epistemic modals an evidential presupposition: the prejacent is not directly settled by the kernel K, the direct-information part of the modal base, whose intersection is the base B_K. The presupposition makes must φ strong, asserting that B_K entails φ, while still signalling indirectness, since B_K can entail φ without K directly settling it. The partition-based implementation and the worked examples are in Studies/VonFintelGillies2010.lean, the can't dilemma in Studies/VonFintelGillies2021.lean.

Main definitions

• Kernel: a set of direct-information propositions, with its base Kernel.base.
• Kernel.directlySettles: some member of the kernel entails or excludes the prejacent.
• kernelMust, kernelMight, kernelCant: the presuppositional operators, trivalent propositions undefined where the kernel directly settles the prejacent.

Main statements

• explicit_implies_entailment: direct settling implies entailment, but not conversely.
• kernelMight_eq_neg_kernelCant: might is the negation of can't, presupposition and all.
• Kernel.followsFrom_iff_simpleNecessity: the assertion of kernelMust is Kratzer's simple necessity over the kernel.

References

• [vFG10]
• [vFG21]

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 : Set (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 = {w : W | sInf k.props w}

@[simp]

theorem Modality.Kernel.mem_base {W : Type u_1} {k : Kernel W} {w : W} : w ∈ k.base ↔ ∀ p ∈ k.props, p w

def Modality.Kernel.toBackground {W : Type u_1} (k : Kernel W) : Background W

The kernel as a context-independent modal base.

Equations

• k.toBackground x✝ = k.props

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

K is consistent iff B_K ≠ ∅.

Equations

• k.IsConsistent = k.base.Nonempty

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

φ follows from K iff B_K ⊆ ⟦φ⟧.

Equations

• k.FollowsFrom φ = (sInf 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 φ = ∃ w ∈ k.base, φ w

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

• k.directlySettles φ = ∃ x ∈ k.props, {w : W | x w} ⊆ {w : W | φ w} ∨ Disjoint {w : W | x w} {w : W | φ w}

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 = {w : W | p w}

@[simp]

theorem Modality.Kernel.directlySettles_singleton {W : Type u_1} (φ p : W → Prop) : { props := {p} }.directlySettles φ ↔ {w : W | p w} ⊆ {w : W | φ w} ∨ Disjoint {w : W | p w} {w : W | φ w}

@[simp]

theorem Modality.Kernel.directlySettles_not {W : Type u_1} (k : Kernel W) (φ : W → Prop) : (k.directlySettles fun (w' : W) => ¬φ w') ↔ k.directlySettles φ

Settling is symmetric under negation, since a proposition entails φ iff it is incompatible with ¬φ.

Modal operators ([vFG10] Defs 5–6)

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

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

Equations

• Modality.kernelMust k φ = {_w : W | ¬k.directlySettles φ}.indicator fun (x : W) => SignType.ofProp (k.FollowsFrom φ)

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

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

Equations

• Modality.kernelMight k φ = {_w : W | ¬k.directlySettles φ}.indicator fun (x : W) => SignType.ofProp (k.compatibleWith φ)

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

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

Equations

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

@[simp]

theorem Modality.kernelMust_eq_zero_iff {W : Type u_1} {k : Kernel W} {φ : W → Prop} {w : W} : kernelMust k φ w = 0 ↔ k.directlySettles φ

@[simp]

theorem Modality.kernelMust_eq_one_iff {W : Type u_1} {k : Kernel W} {φ : W → Prop} {w : W} : kernelMust k φ w = 1 ↔ ¬k.directlySettles φ ∧ k.FollowsFrom φ

@[simp]

theorem Modality.kernelMust_eq_neg_one_iff {W : Type u_1} {k : Kernel W} {φ : W → Prop} {w : W} : kernelMust k φ w = -1 ↔ ¬k.directlySettles φ ∧ ¬k.FollowsFrom φ

@[simp]

theorem Modality.kernelMight_eq_zero_iff {W : Type u_1} {k : Kernel W} {φ : W → Prop} {w : W} : kernelMight k φ w = 0 ↔ k.directlySettles φ

@[simp]

theorem Modality.kernelMight_eq_one_iff {W : Type u_1} {k : Kernel W} {φ : W → Prop} {w : W} : kernelMight k φ w = 1 ↔ ¬k.directlySettles φ ∧ k.compatibleWith φ

@[simp]

theorem Modality.kernelMight_eq_neg_one_iff {W : Type u_1} {k : Kernel W} {φ : W → Prop} {w : W} : kernelMight k φ w = -1 ↔ ¬k.directlySettles φ ∧ ¬k.compatibleWith φ

Core properties

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

The assertion of must φ, B_K ⊆ ⟦φ⟧, entails φ when B_K is realistic (the T axiom).

theorem Modality.Kernel.compatibleWith_iff_not_followsFrom_not {W : Type u_1} (k : Kernel W) (φ : W → Prop) : k.compatibleWith φ ↔ ¬k.FollowsFrom fun (w' : W) => ¬φ w'

The assertion of might φ is the negation of the assertion of must ¬φ.

theorem Modality.kernelMight_eq_neg_kernelCant {W : Type u_1} (k : Kernel W) (φ : W → Prop) : kernelMight k φ = -kernelCant k φ

Might φ is the negation of can't φ, with the same presupposition and the negated assertion.

theorem Modality.kernelMust_empty_ne_zero {W : Type u_1} (φ : W → Prop) (w : W) : kernelMust { props := ∅ } φ w ≠ 0

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

Bridge to Kratzer necessity

theorem Modality.Kernel.followsFrom_iff_simpleNecessity {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) : k.FollowsFrom φ ↔ simpleNecessity k.toBackground φ w

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

theorem Modality.Kernel.followsFrom_iff_necessity {W : Type u_1} (k : Kernel W) (φ : W → Prop) (w : W) : k.FollowsFrom φ ↔ necessity k.toBackground ⊥ φ w

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