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 source IsIndirect
• 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
• must_evidence_matches_izvorski_ev: must imposes the same indirect-evidence restriction as [Izv97]'s Bulgarian EV
• entailment_settling_gap: B_K can entail φ without K directly settling it — the gap that makes the evidential presupposition non-trivial
• subjectMatter, settlesByPartition: the paper's second implementation of directly-settles (Def 7, §7.2) — the subject matter S_K as an equivalence relation on worlds
• explicit_not_implies_partition, partition_not_implies_explicit: the §7.2 boundary cases showing the two implementations are non-equivalent

Evidence types

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 → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance VonFintelGillies2010.instReprEvidenceType : Repr EvidenceType

Equations

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

@[instance_reducible]

instance VonFintelGillies2010.instDecidableEqEvidenceType : DecidableEq EvidenceType

Equations

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

@[instance_reducible]

instance VonFintelGillies2010.instInhabitedEvidenceType : Inhabited EvidenceType

Equations

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

def VonFintelGillies2010.EvidenceType.toCoarseSource : EvidenceType → Semantics.Evidential.CoarseSource

The collapse onto the Aikhenvald taxonomy. Elimination reasoning is inference, not direct access — which is why elimination licenses must (VF&G ex. 12).

Equations

• VonFintelGillies2010.EvidenceType.direct.toCoarseSource = Semantics.Evidential.CoarseSource.direct
• VonFintelGillies2010.EvidenceType.indirect.toCoarseSource = Semantics.Evidential.CoarseSource.inference
• VonFintelGillies2010.EvidenceType.elimination.toCoarseSource = Semantics.Evidential.CoarseSource.inference

@[instance_reducible]

instance VonFintelGillies2010.instHasCoarseSourceEvidenceType : Semantics.Evidential.HasCoarseSource EvidenceType

VF&G evidence types declare their coarse source; the evidential perspective derives via the canonical source mapping.

Equations

• VonFintelGillies2010.instHasCoarseSourceEvidenceType = { toCoarseSource := fun (e : VonFintelGillies2010.EvidenceType) => some e.toCoarseSource }

theorem VonFintelGillies2010.all_evidence_types_nonfuture (e : EvidenceType) : Semantics.Evidential.IsNonfuture e

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

Adapters over the example rows

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

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

The evidential restriction

theorem VonFintelGillies2010.must_felicitous_iff_indirect (row : Data.Examples.LinguisticExample) : row ∈ mustPairs → (row.judgment = Features.Judgment.acceptable ↔ ∀ e ∈ evidenceOf row, e.toCoarseSource.IsIndirect)

A must or can't sentence is felicitous iff the speaker's evidence source IsIndirect: 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 ↔ ∀ e ∈ evidenceOf row, e.toCoarseSource.IsIndirect)

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_evidence_matches_izvorski_ev : (∀ row ∈ mustPairs, row.judgment = Features.Judgment.acceptable ↔ ∀ e ∈ evidenceOf row, e.toCoarseSource.IsIndirect) ∧ ∀ d ∈ Izvorski1997.evMustData, Izvorski1997.EvRequiresIndirect d

Felicity of the modalized member tracks CoarseSource.IsIndirect in VF&G's must rows exactly as in [Izv97]'s Bulgarian EV paradigm: the two epistemic operators presuppose the same coarse indirect-evidence basis.

Must is strong

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

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.

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

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

The kernel model ([vFG10] §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 ⋯

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

Equations

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

@[instance_reducible]

instance VonFintelGillies2010.instReprWorld : Repr World

Equations

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

@[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)

@[reducible, inline]

abbrev VonFintelGillies2010.notBlue : World → Prop

⟦not blue⟧, used by the [vFG21] can't dilemma.

Equations

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

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_defined : (Modality.kernelMust mastermindK blue).presup World.w0

theorem VonFintelGillies2010.mastermind_must_blue_true : (Modality.kernelMust mastermindK blue).assertion World.w0

theorem VonFintelGillies2010.mastermind_red_settled : mastermindK.directlySettles red

theorem VonFintelGillies2010.mastermind_might_red_undefined : ¬(Modality.kernelMight mastermindK red).presup World.w0

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).presup World.w0 ∧ (Modality.kernelMust mastermindK blue).assertion World.w0) ∧ ¬(Modality.kernelMust mastermindK red).presup World.w0 ∧ (Modality.kernelMust indirectK blue).presup World.w0 ∧ ¬(Modality.kernelMust indirectK blue).assertion World.w0

Indirectness and assertion strength are orthogonal dimensions: 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 ψ).assertion w) (hPhi : φ w) : ψ w

The argument form "if φ, must ψ; φ; therefore ψ" is valid under realistic B_K ([vFG10] 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 φ).assertion w) : ¬(Modality.kernelMight k fun (w' : W) => ¬φ w').assertion w

Must φ and might ¬φ are jointly contradictory ([vFG10] Argument 4.3.2).

Implementation 2: settling by partitions ([vFG10] Def 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: S-equivalent worlds never disagree on P.

Equations

• VonFintelGillies2010.IsIssue s φ = ∀ (w v : W), s w v → (φ w ↔ φ v)

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: 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 — 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: K = {red} entails redOrBlue (B_K = {w0} ⊆ ⟦redOrBlue⟧) but does not settle it by partition.