von Fintel & Gillies (2021): Still Going Strong

[vFG21]

Follow-up to [vFG10]: the indirectness signal of must is anti-knowledge, not anti-perception — direct-enough knowledge blocks must even without perceptual evidence (Phil/Meryl dinner pair) — and can't φ is incompatible with it's possible that φ (Observation 5).

Main declarations

• evidential_restriction_extends: the 2010 felicity ↔ indirectness biconditional holds on the anti-knowledge rows
• cant_might_exclusion: when can't φ holds, might φ is false (Observation 5)
• cant_dilemma_resolved: a single kernel simultaneously exhibits evidentiality, strength, and might-exclusion — the assignment of force to can't the Mantra cannot deliver

def VonFintelGillies2021.mustPairs : List Data.Examples.LinguisticExample

Rows whose primary text is the modalized member of a bare/modal minimal pair.

Equations

• VonFintelGillies2021.mustPairs = List.filter (fun (x : Data.Examples.LinguisticExample) => x.feature? "kind" == some "must_pair") VonFintelGillies2021.Examples.all

theorem VonFintelGillies2021.evidential_restriction_extends (row : Data.Examples.LinguisticExample) : row ∈ mustPairs → (row.judgment = Features.Judgment.acceptable ↔ Option.map VonFintelGillies2010.EvidenceType.toCoarseSource (VonFintelGillies2010.evidenceOf row) ≠ some Semantics.Evidential.CoarseSource.direct)

The evidential restriction extends to rows where "direct" is direct-enough knowledge rather than perception: Phil, who checked everything himself, cannot say Dinner must be ready (ex. 24); Meryl, whose information is indirect, can (ex. 25).

The can't dilemma ([vFG21] §4, Observations 4–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.

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

When can't φ holds (B_K ⊆ ⟦¬φ⟧), might φ is false ([vFG21] 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 φ).assertion w) : ¬φ w

When B_K is realistic and can't φ holds, ¬φ holds ([vFG21] via S2).

theorem VonFintelGillies2021.cant_dilemma_resolved : VonFintelGillies2010.World.w1 ∈ VonFintelGillies2010.mastermindK.base ∧ (Modality.kernelCant VonFintelGillies2010.mastermindK VonFintelGillies2010.notBlue).presup VonFintelGillies2010.World.w1 ∧ (Modality.kernelCant VonFintelGillies2010.mastermindK VonFintelGillies2010.notBlue).assertion VonFintelGillies2010.World.w1 ∧ ¬(Modality.kernelMight VonFintelGillies2010.mastermindK VonFintelGillies2010.notBlue).assertion VonFintelGillies2010.World.w1 ∧ ¬VonFintelGillies2010.notBlue VonFintelGillies2010.World.w1

A single kernel simultaneously exhibits evidentiality, strength, and might-exclusion: over mastermindK, can't notBlue is defined, true, and excludes might notBlue — the joint profile the Mantra cannot assign.

theorem VonFintelGillies2021.cant_direct_evidence_infelicity : ¬(Modality.kernelCant VonFintelGillies2010.mastermindK VonFintelGillies2010.red).presup VonFintelGillies2010.World.w0

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