von Fintel & Gillies (2021): Still Going Strong

This file formalizes von Fintel and Gillies's return to the strong must of their 2010 paper. Two observations about epistemic can't pose a dilemma for the Mantra: can't patterns with must in its evidential distribution (Observation 4), and can't φ is incompatible with it's possible that φ (Observation 5), so can't can be the negation neither of a strong nor of a weak existential modal. Kernel semantics resolves the dilemma: can't φ is must of the negation, so its evidential signal is that of must, and its assertion, that the modal base excludes φ, contradicts might φ and under a realistic base entails the negation of the prejacent, the thesis S2. On the worked kernel of the earlier paper can't not-blue is defined, true, and excludes might not-blue at once, the joint profile the Mantra cannot assign (cant_dilemma_resolved), and direct information that settles the prejacent gives can't presupposition failure as it does must. The anti-knowledge examples of §4.2, Phil who checked dinner himself against Meryl who followed instructions (24) and (25), are the rows of Data.Examples.VonFintelGillies2021.

References

• [vFG21]
• [vFG10]

The can't dilemma (§4.1, Observations 4 and 5)

The Mantra faces a dilemma: no assignment of force to can't simultaneously explains its evidential distribution (Observation 4: can't patterns like must) and its incompatibility with it's possible that φ (Observation 5). Kernel semantics resolves this: can't φ = must(¬φ) by definition (kernelCant), so Observation 4's evidential parallelism holds by construction, while the strong assertion B_K ⊆ ⟦¬φ⟧ delivers Observation 5.

@[reducible, inline]

abbrev VonFintelGillies2021.notBlue : VonFintelGillies2010.World → Prop

⟦not blue⟧.

Equations

• VonFintelGillies2021.notBlue x✝ = (x✝ ≠ VonFintelGillies2010.World.w1)

theorem VonFintelGillies2021.cant_might_exclusion {W : Type u_1} (k : Modality.Kernel W) (φ : W → Prop) (w : W) (hCant : Modality.kernelCant k φ w = 1) : Modality.kernelMight k φ w = -1

When can't φ is true (B_K ⊆ ⟦¬φ⟧), might φ is false (Observation 5).

theorem VonFintelGillies2021.cant_entails_negation {W : Type u_1} (k : Modality.Kernel W) (φ : W → Prop) (w : W) (hReal : w ∈ k.base) (hTrue : Modality.kernelCant k φ w = 1) : ¬φ w

When B_K is realistic and can't φ is true, ¬φ holds (S2).

theorem VonFintelGillies2021.cant_dilemma_resolved : VonFintelGillies2010.World.w1 ∈ VonFintelGillies2010.mastermindK.base ∧ Modality.kernelCant VonFintelGillies2010.mastermindK notBlue VonFintelGillies2010.World.w1 = 1 ∧ Modality.kernelMight VonFintelGillies2010.mastermindK notBlue VonFintelGillies2010.World.w1 = -1 ∧ ¬notBlue VonFintelGillies2010.World.w1

Over mastermindK a single kernel exhibits evidentiality, strength, and might-exclusion at once, since can't notBlue is defined and true and might notBlue is false — the joint profile the Mantra cannot assign.

theorem VonFintelGillies2021.cant_direct_evidence_infelicity : Modality.kernelCant VonFintelGillies2010.mastermindK VonFintelGillies2010.red VonFintelGillies2010.World.w0 = 0

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