von Fintel & Gillies (2010): Must … Stay … Strong!

This file formalizes von Fintel and Gillies's defense of a strong epistemic must against the Mantra that must φ is weaker than its prejacent, Karttunen's problem (2). On the paper's analysis must stays at the top of the scale of epistemic strength (1) and entails its prejacent, and the felt weakness is an evidential presupposition: the kernel of direct information must not directly settle the prejacent, though its modal base may entail it. The kernel apparatus, the explicit-representation implementation of settling (§7.1) and the presuppositional operators (Definitions 4 to 6), is Semantics/Modality/Kernel.lean; this file carries the worked kernel of Figure 3(a), Billy's weather reports in the colors of the Mastermind scenario of §2 (mastermindK), on which must blue is defined and true while might red is undefined, so that indirectness and weakness come apart (§4.1), the validity of if φ, must ψ; φ; so ψ (Argument 4.3.1) and the contradictoriness of must φ but perhaps not φ (Argument 4.3.2), and the second implementation of settling by the partition a kernel induces, a subject matter in which the prejacent is an issue (Definition 7, §7.2), with the two implementations shown non-equivalent in both directions (settlesByPartition).

Implementation notes

The four worlds are red, blue, green and unknown, with red or blue and not red the kernel propositions P ∪ Q and W \ P of the paper's figure. A subject matter is a Setoid, and a proposition is an issue in it when the setoid decides the proposition. The paper's examples are the rows of Data.Examples.VonFintelGillies2010.

References

• [vFG10]
• [Kra91]
• [Kar72]

The kernel model (§7.1)

A four-world instantiation of §7.1's worked kernel K = {P ∪ Q, W \ P} (Billy's weather report, Figure 3(a)), skinned with the colors of the §2 Mastermind scenario (Pascal asking Mordecai Must there be two reds?): P = red-only, Q = blue, so redOrBlue = P ∪ Q and notRed = W \ P. B_K = {w1} entails blue without either kernel proposition settling it.

inductive VonFintelGillies2010.World : Type

Four worlds, with w0 red, w1 blue, w2 green, and w3 unknown.

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

@[instance_reducible]

instance VonFintelGillies2010.instDecidableEqWorld : DecidableEq World

Equations

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

@[instance_reducible]

instance VonFintelGillies2010.instReprWorld : Repr World

Equations

• VonFintelGillies2010.instReprWorld = { reprPrec := VonFintelGillies2010.instReprWorld.repr }

def VonFintelGillies2010.instReprWorld.repr : World → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance VonFintelGillies2010.instInhabitedWorld : Inhabited World

Equations

• VonFintelGillies2010.instInhabitedWorld = { default := VonFintelGillies2010.instInhabitedWorld.default }

@[reducible, inline]

abbrev VonFintelGillies2010.redOrBlue : World → Prop

⟦red or blue⟧ = {w0, w1}, the paper's P ∪ Q.

Equations

• VonFintelGillies2010.redOrBlue w = (w = VonFintelGillies2010.World.w0 ∨ w = VonFintelGillies2010.World.w1)

@[reducible, inline]

abbrev VonFintelGillies2010.notRed : World → Prop

⟦not red⟧ = {w1, w2, w3}, the paper's W \ P.

Equations

• VonFintelGillies2010.notRed x✝ = (x✝ ≠ VonFintelGillies2010.World.w0)

@[reducible, inline]

abbrev VonFintelGillies2010.blue : World → Prop

⟦blue⟧ = {w1}, the paper's Q.

Equations

• VonFintelGillies2010.blue x✝ = (x✝ = VonFintelGillies2010.World.w1)

@[reducible, inline]

abbrev VonFintelGillies2010.red : World → Prop

⟦red⟧ = {w0}, the paper's P.

Equations

• VonFintelGillies2010.red x✝ = (x✝ = VonFintelGillies2010.World.w0)

def VonFintelGillies2010.mastermindK : Modality.Kernel World

The §7.1 kernel {P ∪ Q, W \ P} in Mastermind colors.

Equations

• VonFintelGillies2010.mastermindK = { props := {VonFintelGillies2010.redOrBlue, VonFintelGillies2010.notRed} }

def VonFintelGillies2010.indirectK : Modality.Kernel World

A one-proposition kernel whose base properly contains ⟦blue⟧.

Equations

• VonFintelGillies2010.indirectK = { props := {VonFintelGillies2010.redOrBlue} }

theorem VonFintelGillies2010.mastermind_base : mastermindK.base = {World.w1}

theorem VonFintelGillies2010.mastermind_blue_unsettled : ¬mastermindK.directlySettles blue

theorem VonFintelGillies2010.mastermind_blue_follows : mastermindK.FollowsFrom blue

theorem VonFintelGillies2010.mastermind_must_blue_eq_one : Modality.kernelMust mastermindK blue World.w0 = 1

theorem VonFintelGillies2010.mastermind_red_settled : mastermindK.directlySettles red

theorem VonFintelGillies2010.mastermind_might_red_eq_zero : Modality.kernelMight mastermindK red World.w0 = 0

theorem VonFintelGillies2010.mastermind_redOrBlue_settled : mastermindK.directlySettles redOrBlue

Deep theorems

theorem VonFintelGillies2010.entailment_settling_gap : ∃ (k : Modality.Kernel World) (φ : World → Prop), k.FollowsFrom φ ∧ ¬k.directlySettles φ

B_K can entail φ without K directly settling it, so must φ can be simultaneously defined and true.

theorem VonFintelGillies2010.indirectness_neq_weakness : Modality.kernelMust mastermindK blue World.w0 = 1 ∧ Modality.kernelMust mastermindK red World.w0 = 0 ∧ Modality.kernelMust indirectK blue World.w0 = -1

Indirectness and assertion strength are orthogonal dimensions, since must can be defined and true, undefined, or defined and false (§4.1).

theorem VonFintelGillies2010.modus_ponens_with_must {W : Type u_1} (k : Modality.Kernel W) (φ ψ : W → Prop) (w : W) (hReal : w ∈ k.base) (hCond : φ w → Modality.kernelMust k ψ w = 1) (hPhi : φ w) : ψ w

The argument form "if φ, must ψ; φ; therefore ψ" is valid under realistic B_K (Argument 4.3.1).

theorem VonFintelGillies2010.must_perhaps_contradiction {W : Type u_1} (k : Modality.Kernel W) (φ : W → Prop) (w : W) (hMust : Modality.kernelMust k φ w = 1) : Modality.kernelMight k (fun (w' : W) => ¬φ w') w = -1

Must φ and might ¬φ are jointly contradictory (Argument 4.3.2), since where must φ is true might ¬φ is false.

Implementation 2: settling by partitions (Definition 7, §7.2)

Def 7 presents subject matters as equivalence relations on W: S[P] keeps the pairs of S that agree on P, and P is an issue in S iff S[P] = S. The subject matter S_K determined by a kernel is the refinement S_o[P₁]…[Pₙ] of the universal relation along each kernel proposition — equivalently, the relation "agrees on every X ∈ K". Implementation 2: K directly settles P iff P is an issue in S_K.

def VonFintelGillies2010.subjectMatter {W : Type u_1} (k : Modality.Kernel W) : Setoid W

The subject matter S_K of a kernel, relating worlds that agree on every proposition in K.

Equations

• VonFintelGillies2010.subjectMatter k = { r := fun (w v : W) => ∀ p ∈ k.props, p w ↔ p v, iseqv := ⋯ }

def VonFintelGillies2010.IsIssue {W : Type u_1} (s : Setoid W) (φ : W → Prop) : Prop

P is an issue in a subject matter S when S-equivalent worlds never disagree on P.

Equations

• VonFintelGillies2010.IsIssue s φ = s.Decides {w : W | φ w}

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

K settles P by partition iff P is an issue in S_K.

Equations

• VonFintelGillies2010.settlesByPartition k φ = VonFintelGillies2010.IsIssue (VonFintelGillies2010.subjectMatter k) φ

theorem VonFintelGillies2010.subjectMatter_rel_base {W : Type u_1} (k : Modality.Kernel W) {v w : W} (hv : v ∈ k.base) (hw : w ∈ k.base) : (subjectMatter k) v w

B_K lies in a single cell of the subject matter.

theorem VonFintelGillies2010.partition_implies_entailment {W : Type u_1} (k : Modality.Kernel W) (φ : W → Prop) (h : settlesByPartition k φ) : k.FollowsFrom φ ∨ k.FollowsFrom fun (w : W) => ¬φ w

If K settles φ by partition then B_K ⊆ ⟦φ⟧ or B_K ⊆ ⟦¬φ⟧; as with explicit_implies_entailment, the converse fails.

Non-equivalence of the two implementations (§7.2)

Implementation 1 settles supersets of K-propositions that Implementation 2 misses (K = {P} settles P ∪ Q explicitly, but there are worlds agreeing on P that disagree on P ∪ Q); Implementation 2 settles propositions determined jointly by K-propositions that no single proposition settles (blue is determined by redOrBlue together with notRed).

theorem VonFintelGillies2010.explicit_not_implies_partition : ∃ (k : Modality.Kernel World) (φ : World → Prop), k.directlySettles φ ∧ ¬settlesByPartition k φ

Explicit settling does not imply partition settling, since K = {red} settles redOrBlue explicitly (red ⊆ redOrBlue) but not by partition.

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

Partition settling does not imply explicit settling. mastermindK settles blue by partition, since its cells decide redOrBlue and notRed, which jointly determine blue, but no single kernel proposition entails or excludes it.

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

Entailment does not imply partition settling, since K = {red} entails redOrBlue (B_K = {w0} ⊆ ⟦redOrBlue⟧) but does not settle it by partition.