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

[vFG10] [Kra91]

Epistemic must carries an indirect-evidence signal yet is semantically strong: must φ entails φ.

Karttunen's Problem: standard modal logic gives must φ ⊨ φ, yet the bare prejacent is felt to convey more confidence than the must-claim ([Kra91] p. 645: "I make a stronger claim in uttering (5a) than in (5b)"). VF&G's resolution keeps must at the top of the strength ordering (p. 352: must > almost certainly > presumably > might) and locates the felt weakness in an evidential presupposition: the speaker's kernel must not directly settle the prejacent.

Main declarations

• EvidenceType, EvidenceType.toCoarseSource: VF&G's evidence-type classification and its collapse onto the Aikhenvald taxonomy
• must_felicitous_iff_indirect: over the example rows, the modalized member of a bare/modal minimal pair is felicitous iff the speaker's evidence is not coarse-direct
• cant_patterns_with_must: the same biconditional restricted to the can't rows, derived from the previous theorem
• must_entails_prejacent: every minimal pair records prejacent entailment — including the infelicitous direct-evidence rows

inductive VonFintelGillies2010.EvidenceType : Type

The type of evidence the speaker has for the prejacent.

• direct : EvidenceType

  Direct sensory observation (seeing, hearing).

• indirect : EvidenceType

  Indirect inference from observable effects.

• elimination : EvidenceType

  Elimination reasoning (ruling out alternatives).

def VonFintelGillies2010.instReprEvidenceType.repr : EvidenceType → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance VonFintelGillies2010.instReprEvidenceType : Repr EvidenceType

Equations

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

@[implicit_reducible]

instance VonFintelGillies2010.instDecidableEqEvidenceType : DecidableEq EvidenceType

Equations

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

@[implicit_reducible]

instance VonFintelGillies2010.instInhabitedEvidenceType : Inhabited EvidenceType

Equations

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

def VonFintelGillies2010.EvidenceType.toCoarseSource : EvidenceType → Features.Evidentiality.CoarseSource

Collapse to the Aikhenvald taxonomy. Elimination reasoning is inference, not direct access: the kernel does not directly settle the prejacent — which is why elimination licenses must (VF&G ex. 12).

Equations

• VonFintelGillies2010.EvidenceType.direct.toCoarseSource = Features.Evidentiality.CoarseSource.direct
• VonFintelGillies2010.EvidenceType.indirect.toCoarseSource = Features.Evidentiality.CoarseSource.inference
• VonFintelGillies2010.EvidenceType.elimination.toCoarseSource = Features.Evidentiality.CoarseSource.inference

@[implicit_reducible]

instance VonFintelGillies2010.instHasEvidentialPerspectiveEvidenceType : Features.Evidentiality.HasEvidentialPerspective EvidenceType

VF&G evidence types inherit an evidential perspective via the canonical Aikhenvald source mapping.

Equations

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

theorem VonFintelGillies2010.all_evidence_types_nonfuture (e : EvidenceType) : Features.Evidentiality.IsNonfuture e

All VF&G evidence types are nonfuture: their perspective is always retrospective or contemporaneous (T ≤ A).

def VonFintelGillies2010.evidenceOf (row : Data.Examples.LinguisticExample) : Option EvidenceType

Evidence-type adapter: the row's evidence feature as an EvidenceType.

Equations

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

def VonFintelGillies2010.mustPairs : List Data.Examples.LinguisticExample

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

Equations

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

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

Evidential restriction: a must/can't sentence is felicitous iff the speaker's evidence is not coarse-direct. Direct perception (exx. 6, 23) blocks the modal; inference — causal (exx. 7, 21, 24, 26) or by elimination (ex. 12) — licenses it.

theorem VonFintelGillies2010.cant_patterns_with_must (row : Data.Examples.LinguisticExample) : row ∈ List.filter (fun (x : Data.Examples.LinguisticExample) => x.feature? "modal" == some "cant") mustPairs → (row.judgment = Features.Judgment.acceptable ↔ Option.map EvidenceType.toCoarseSource (evidenceOf row) ≠ some Features.Evidentiality.CoarseSource.direct)

Can't patterns with must: the evidential restriction holds uniformly on the negative-modal rows (exx. 21, 23, 24) — can't groups with must, not with weak modals.

theorem VonFintelGillies2010.must_entails_prejacent (row : Data.Examples.LinguisticExample) : row ∈ mustPairs → row.feature? "must_entails_prejacent" = some "true"

Must is strong: every minimal pair records that the modalized sentence entails its prejacent — including the direct-evidence rows where the modal is infelicitous. The restriction is evidential, not a weakening of content. The supporting inference rows (modus ponens is valid, must φ ∧ perhaps ¬φ is contradictory, retraction fails) are in the same JSON under kind = inference.

theorem VonFintelGillies2010.bare_always_felicitous (row : Data.Examples.LinguisticExample) : row ∈ mustPairs → ∀ (alt : String × Features.Judgment), alt ∈ row.alternatives → alt.snd = Features.Judgment.acceptable

The bare prejacent is felicitous in every context: the felicity restriction is contributed by the modal, not by the content.