Epistemic Evidentiality — Empirical Data

@cite{kratzer-1991} @cite{von-fintel-gillies-2010} @cite{von-fintel-gillies-2021}

Theory-neutral empirical observations about the interaction between epistemic necessity modals (English must, have to) and evidential source.

Key Generalizations

1. Epistemic must is infelicitous when the speaker has direct evidence for the prejacent (seeing rain → "#It must be raining")
2. Epistemic must is felicitous when the speaker has indirect evidence (seeing wet rain gear → "It must be raining")
3. Despite (1), must φ entails the bare prejacent φ — must is not semantically weak, just evidentially restricted
4. Can't patterns with must, not with weak modals (might, perhaps)

The Strength Ordering (p. 352)

must > almost certainly > presumably > might > bare prejacent (?)

The placement of the bare prejacent is Karttunen's Problem:

• Standard modal logic: must φ ⊨ φ (must is ABOVE bare)
• Naive intuition: φ conveys more confidence than must φ (bare is ABOVE must)

inductive Phenomena.Modality.EpistemicEvidentiality.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).

• reported : EvidenceType

  Reported / hearsay evidence.

instance Phenomena.Modality.EpistemicEvidentiality.instReprEvidenceType : Repr EvidenceType

Equations

• Phenomena.Modality.EpistemicEvidentiality.instReprEvidenceType = { reprPrec := Phenomena.Modality.EpistemicEvidentiality.instReprEvidenceType.repr }

def Phenomena.Modality.EpistemicEvidentiality.instReprEvidenceType.repr : EvidenceType → Nat → Std.Format

Equations

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

instance Phenomena.Modality.EpistemicEvidentiality.instDecidableEqEvidenceType : DecidableEq EvidenceType

Equations

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

instance Phenomena.Modality.EpistemicEvidentiality.instBEqEvidenceType : BEq EvidenceType

Equations

• Phenomena.Modality.EpistemicEvidentiality.instBEqEvidenceType = { beq := Phenomena.Modality.EpistemicEvidentiality.instBEqEvidenceType.beq }

def Phenomena.Modality.EpistemicEvidentiality.instBEqEvidenceType.beq : EvidenceType → EvidenceType → Bool

Equations

• Phenomena.Modality.EpistemicEvidentiality.instBEqEvidenceType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Modality.EpistemicEvidentiality.instInhabitedEvidenceType : Inhabited EvidenceType

Equations

• Phenomena.Modality.EpistemicEvidentiality.instInhabitedEvidenceType = { default := Phenomena.Modality.EpistemicEvidentiality.instInhabitedEvidenceType.default }

def Phenomena.Modality.EpistemicEvidentiality.instInhabitedEvidenceType.default : EvidenceType

Equations

• Phenomena.Modality.EpistemicEvidentiality.instInhabitedEvidenceType.default = Phenomena.Modality.EpistemicEvidentiality.EvidenceType.direct

structure Phenomena.Modality.EpistemicEvidentiality.MustMinimalPair : Type

A minimal pair comparing a bare prejacent with its modalized counterpart.

• bare : String

  The bare prejacent sentence

• must : String

  The must-sentence

• context : String

  Evidential context (what the speaker perceives)

• evidenceType : EvidenceType

  Type of evidence available

• bareFelicitous : Bool

  Is the bare sentence felicitous in this context?

• mustFelicitous : Bool

  Is the must-sentence felicitous in this context?

• mustEntailsPrejacent : Bool

  Does must φ entail φ (speaker judgment on inference validity)?

• exampleNum : String

  Source example number from @cite{von-fintel-gillies-2010}

• notes : String

  Additional notes

instance Phenomena.Modality.EpistemicEvidentiality.instReprMustMinimalPair : Repr MustMinimalPair

Equations

• Phenomena.Modality.EpistemicEvidentiality.instReprMustMinimalPair = { reprPrec := Phenomena.Modality.EpistemicEvidentiality.instReprMustMinimalPair.repr }

def Phenomena.Modality.EpistemicEvidentiality.instReprMustMinimalPair.repr : MustMinimalPair → Nat → Std.Format

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.johnLeft : MustMinimalPair

VF&G ex. 3: "John left" vs. "John must have left." The must-sentence "expresses more conviction" yet is felt to be weaker.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.johnHome : MustMinimalPair

VF&G ex. 4: "John must be at home" vs. "John is at home."

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.mountToby : MustMinimalPair

VF&G ex. 5: "She climbed Mount Toby" vs. "She must have climbed Mount Toby."

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.keysInDrawer : MustMinimalPair

VF&G ex. 2 (Karttunen's Problem stated as question-answer): "They must be in the kitchen drawer" conveys less confidence as an answer to "Where are the keys?" than the bare "They are in the kitchen drawer."

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.billySeesRain : MustMinimalPair

VF&G ex. 6: DIRECT evidence (seeing rain) blocks must.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.billySeesWetGear : MustMinimalPair

VF&G ex. 7: INDIRECT evidence (wet gear, rain is only cause) enables must.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.chrisBall : MustMinimalPair

VF&G ex. 12 (Argument 4.2.1): Elimination reasoning — Chris's ball. Must is perfectly felicitous and feels strong, not weak.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.billyWetGearStrong : MustMinimalPair

VF&G Argument 4.2.2: Billy sees wet gear, knows rain is only cause. The prejacent is entailed ex hypothesi, yet must is felicitous. Pattern: B_K entails the prejacent but the kernel doesn't directly settle it — the gap that licenses must.

Equations

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

structure Phenomena.Modality.EpistemicEvidentiality.InferenceDatum : Type

A datum capturing an inference pattern (modus ponens, contradiction, etc.).

• sentences : List String

  The inference pattern or sentences involved

• judgment : String

  Is the inference valid / the pattern contradictory?

• exampleNum : String

  Source example number from @cite{von-fintel-gillies-2010}

• notes : String

  What this shows about must's strength

def Phenomena.Modality.EpistemicEvidentiality.instReprInferenceDatum.repr : InferenceDatum → Nat → Std.Format

Equations

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

instance Phenomena.Modality.EpistemicEvidentiality.instReprInferenceDatum : Repr InferenceDatum

Equations

• Phenomena.Modality.EpistemicEvidentiality.instReprInferenceDatum = { reprPrec := Phenomena.Modality.EpistemicEvidentiality.instReprInferenceDatum.repr }

def Phenomena.Modality.EpistemicEvidentiality.modusPonens : InferenceDatum

VF&G ex. 14–15 (Argument 4.3.1): Modus ponens with must is valid. If must were weak, the premises would be too weak for the conclusion.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.mustPerhapsContradiction : InferenceDatum

VF&G ex. 16 (Argument 4.3.2): Must-perhaps contradiction. If must φ were compatible with ¬φ, this should be fine. It isn't.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.noRetraction : InferenceDatum

VF&G ex. 17–19 (Argument 4.3.3): Must doesn't allow retraction. Weak modals (might, ought) do.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.mightRetraction : InferenceDatum

VF&G ex. 17 (contrast): Might DOES allow retraction.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.hedgingPreference : InferenceDatum

VF&G ex. 20 (Argument 4.3.4): When hedging is desired, speakers choose probably, not must. If must were weak, it should be the natural hedge.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.cantEvidentialSignal : MustMinimalPair

VF&G ex. 21: "Can't" carries the evidential signal; bare negation doesn't.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.cantDirectEvidence : MustMinimalPair

VF&G ex. 23: Direct evidence blocks can't, paralleling must.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.cantIndirectEvidence : MustMinimalPair

VF&G ex. 24: Indirect evidence enables can't, paralleling must.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.heyWaitAMinute : InferenceDatum

VF&G ex. 22: The "Hey! Wait a minute" test diagnoses a presupposition. Billy challenges Alex's use of must, targeting the evidential component.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.mustBeHungry : MustMinimalPair

VF&G ex. 26: "I must be hungry" — odd because hunger is typically known by direct introspection, not indirect inference.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.cantPossibleContradiction : InferenceDatum

@cite{von-fintel-gillies-2021} ex. 5a/22: Can't φ is incompatible with "it's possible that φ." The flat-footed conjunction is incoherent.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.mustOnlyIncompatibility : InferenceDatum

@cite{von-fintel-gillies-2021} ex. 6/10: Must doesn't combine with only — evidence for top-of-scale status, not weakness.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.philCooksDinner : MustMinimalPair

@cite{von-fintel-gillies-2021} ex. 24: Anti-knowledge — Phil cooking dinner. Direct knowledge makes must infelicitous even without perceptual evidence.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.merylCooksDinner : MustMinimalPair

@cite{von-fintel-gillies-2021} ex. 25: Anti-knowledge — Meryl's indirect knowledge. Meryl hasn't checked everything herself, so must is fine.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.allMinimalPairs : List MustMinimalPair

All minimal pairs.

Equations

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

def Phenomena.Modality.EpistemicEvidentiality.allInferenceData : List InferenceDatum

All inference data.

Equations

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

theorem Phenomena.Modality.EpistemicEvidentiality.direct_evidence_blocks_must : ((List.filter (fun (d : MustMinimalPair) => d.evidenceType == EvidenceType.direct) allMinimalPairs).all fun (d : MustMinimalPair) => !d.mustFelicitous) = true

Key generalization 1: Direct evidence → must infelicitous.

theorem Phenomena.Modality.EpistemicEvidentiality.indirect_evidence_enables_must : ((List.filter (fun (d : MustMinimalPair) => d.evidenceType == EvidenceType.indirect) allMinimalPairs).all fun (d : MustMinimalPair) => d.mustFelicitous) = true

Key generalization 2: Indirect evidence → must felicitous.

theorem Phenomena.Modality.EpistemicEvidentiality.must_always_entails_prejacent : (allMinimalPairs.all fun (d : MustMinimalPair) => d.mustEntailsPrejacent) = true

Key generalization 3: Must always entails the prejacent (in every minimal pair, regardless of evidence type).

theorem Phenomena.Modality.EpistemicEvidentiality.bare_always_felicitous : (allMinimalPairs.all fun (d : MustMinimalPair) => d.bareFelicitous) = true

Key generalization 4: Bare prejacent is always felicitous (the felicity restriction is specific to must, not to the content).

def Phenomena.Modality.EpistemicEvidentiality.EvidenceType.toEvidentialSource : EvidenceType → Core.Evidence.EvidentialSource

Map VF&G's four-way evidence types to Cumming's three-way canonical classification. Direct and elimination map to direct (both involve the speaker's own epistemic access); indirect and reported map to inference and hearsay respectively.

Equations

• Phenomena.Modality.EpistemicEvidentiality.EvidenceType.direct.toEvidentialSource = Core.Evidence.EvidentialSource.direct
• Phenomena.Modality.EpistemicEvidentiality.EvidenceType.indirect.toEvidentialSource = Core.Evidence.EvidentialSource.inference
• Phenomena.Modality.EpistemicEvidentiality.EvidenceType.elimination.toEvidentialSource = Core.Evidence.EvidentialSource.direct
• Phenomena.Modality.EpistemicEvidentiality.EvidenceType.reported.toEvidentialSource = Core.Evidence.EvidentialSource.hearsay

theorem Phenomena.Modality.EpistemicEvidentiality.all_evidence_types_nonfuture (e : EvidenceType) : e.toEvidentialSource.toEvidentialPerspective.isNonfuture = true

All VF&G evidence types map to nonfuture evidential perspectives: every source's perspective has isNonfuture = true.