Huijsmans (2025) @cite{huijsmans-2025}

Timing of evidence and epistemic modal claims. Natural Language Semantics 33: 207–254.

The future morphemes səm (ʔayʔaǰuθəm; Central Salish) and will (English) pattern with strong epistemic modals like ćε (ʔayʔaǰuθəm inferential) and must, but their distributions diverge in inferences about non-future eventualities. Huijsmans argues the difference is temporal, not modal strength: səm/will presuppose the modal base is established prior to the earliest moment the prejacent is claimed to hold, while ćε requires at least one modal-base proposition to hold at or following that moment.

Structural claim

The temporal-presupposition partition is structurally identical to the EP-condition partition in Theories/Semantics/Tense/Evidential.lean, but indexed on MBT (modal-base time) rather than EAT (evidence acquisition time). EPCondition is reused under the slot reinterpretation MBT ↦ acquisitionTime, PrejT ↦ eventTime. The bridge is MBTProfile.licenses_iff_EP.

Empirical wedge

Most of Huijsmans's stimuli (cooking, Daniel-home, poison) satisfy MBT < PrejT ∧ EAT < ET — both analyses agree. The Felipe-rain stimulus (ex. 46-49) and clam-digging stimulus (ex. 48-49) have MBT < PrejT but ET < EAT — Huijsmans's MBT analysis correctly licenses will/must; an EAT analysis (with the same partition reinterpreted) does not. MBT_vs_EAT_diverge_on_felipe is the load-bearing theorem.

At-issue content

The at-issue content is Kratzer strong necessity over the modal base, shared across all four lexical entries (modulo modal-base type). It is not formalized in this file; consumers wanting full denotations should combine Modal.flavor with Theories.Semantics.Modality.Kratzer.necessity.

structure Phenomena.Modality.Studies.Huijsmans2025.Stimulus (Time : Type) : Type

A stimulus context, supplying the four temporal anchors needed to state both Huijsmans's MBT predictions and the EAT predictions she is contrasted against. The MBT/EAT split lives in which pair of anchors a profile reads.

• earliestMBT : Time

  ⌜MBT⌝ — the maximum over q ∈ MB of EARLIEST(SHIFT q), i.e. the latest "earliest moment" required by the modal base.

• earliestPrejT : Time

  ⌜PrejT⌝ — EARLIEST(p) for the prejacent p.

• eat : Time

  The (Cumming/Hirayama-Matthewson) evidence-acquisition time.

• et : Time

  The event time of the prejacent.

@[implicit_reducible]

instance Phenomena.Modality.Studies.Huijsmans2025.instReprStimulus {Time✝ : Type} [Repr Time✝] : Repr (Stimulus Time✝)

Equations

• Phenomena.Modality.Studies.Huijsmans2025.instReprStimulus = { reprPrec := Phenomena.Modality.Studies.Huijsmans2025.instReprStimulus.repr }

def Phenomena.Modality.Studies.Huijsmans2025.instReprStimulus.repr {Time✝ : Type} [Repr Time✝] : Stimulus Time✝ → ℕ → Std.Format

Equations

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

inductive Phenomena.Modality.Studies.Huijsmans2025.MBTProfile : Type

The three MBT-presupposition profiles Huijsmans's four lexical items instantiate. A domain-flavored selector over the abstract Core.Time.Relation partition (cf. EPCondition in Tense/Evidential.lean, which selects from the same partition for the EAT/ET slot pair). Only three of the five abstract relations name a Huijsmans modal; the others are unused here.

• strictPrior : MBTProfile

  MBT < PrejT. Modal base established strictly before the prejacent's earliest moment. səm, will. Eq. (35).

• nonProspective : MBTProfile

  PrejT ≤ MBT. At least one MB proposition becomes true at or after the prejacent's earliest moment. ćε. Eq. (36).

• unrestricted : MBTProfile

  No temporal restriction. must.

@[implicit_reducible]

instance Phenomena.Modality.Studies.Huijsmans2025.instDecidableEqMBTProfile : DecidableEq MBTProfile

Equations

• Phenomena.Modality.Studies.Huijsmans2025.instDecidableEqMBTProfile x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Modality.Studies.Huijsmans2025.instReprMBTProfile.repr : MBTProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Modality.Studies.Huijsmans2025.instReprMBTProfile : Repr MBTProfile

Equations

• Phenomena.Modality.Studies.Huijsmans2025.instReprMBTProfile = { reprPrec := Phenomena.Modality.Studies.Huijsmans2025.instReprMBTProfile.repr }

def Phenomena.Modality.Studies.Huijsmans2025.MBTProfile.toRelation : MBTProfile → Core.Time.Relation

Underlying point-relation: the slot pair is (earliestMBT, earliestPrejT), and each profile picks one shape from Relation. Mirrors EPCondition.toRelation in Tense/Evidential.lean.

Equations

• Phenomena.Modality.Studies.Huijsmans2025.MBTProfile.strictPrior.toRelation = Core.Time.Relation.before
• Phenomena.Modality.Studies.Huijsmans2025.MBTProfile.nonProspective.toRelation = Core.Time.Relation.notBefore
• Phenomena.Modality.Studies.Huijsmans2025.MBTProfile.unrestricted.toRelation = Core.Time.Relation.unrestricted

def Phenomena.Modality.Studies.Huijsmans2025.MBTProfile.licenses {Time : Type} [LinearOrder Time] (c : MBTProfile) (s : Stimulus Time) : Prop

The MBT-licensing predicate, derived from the abstract partition.

Equations

• c.licenses s = c.toRelation.eval s.earliestMBT s.earliestPrejT

@[implicit_reducible]

instance Phenomena.Modality.Studies.Huijsmans2025.instDecidableLicensesOfDecidableEq {Time : Type} [LinearOrder Time] [DecidableEq Time] (c : MBTProfile) (s : Stimulus Time) : Decidable (c.licenses s)

Equations

• Phenomena.Modality.Studies.Huijsmans2025.instDecidableLicensesOfDecidableEq c s = id inferInstance

structure Phenomena.Modality.Studies.Huijsmans2025.Modal : Type

A modal in the Huijsmans typology: a label, a (possibly underspecified) modal-flavor, and an MBT-presupposition profile. All four entries in this paper are necessity modals; force is omitted.

• label : String
• flavor : Option Core.Modality.ModalFlavor

  Modal flavor, or none for underspecified (Huijsmans p. 218).

• profile : MBTProfile

def Phenomena.Modality.Studies.Huijsmans2025.instReprModal.repr : Modal → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Modality.Studies.Huijsmans2025.instReprModal : Repr Modal

Equations

• Phenomena.Modality.Studies.Huijsmans2025.instReprModal = { reprPrec := Phenomena.Modality.Studies.Huijsmans2025.instReprModal.repr }

def Phenomena.Modality.Studies.Huijsmans2025.sem : Modal

ʔayʔaǰuθəm future clitic səm. Underspecified for modal base (epistemic and circumstantial uses; Huijsmans §2.3).

Equations

• Phenomena.Modality.Studies.Huijsmans2025.sem = { label := "səm", flavor := none, profile := Phenomena.Modality.Studies.Huijsmans2025.MBTProfile.strictPrior }

def Phenomena.Modality.Studies.Huijsmans2025.will : Modal

English future auxiliary will. Underspecified for modal base (epistemic in non-future-eventuality uses, circumstantial in future-eventuality uses; Huijsmans §2.4).

Equations

• Phenomena.Modality.Studies.Huijsmans2025.will = { label := "will", flavor := none, profile := Phenomena.Modality.Studies.Huijsmans2025.MBTProfile.strictPrior }

def Phenomena.Modality.Studies.Huijsmans2025.che : Modal

ʔayʔaǰuθəm inferential clitic ćε. Epistemic only.

Equations

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

def Phenomena.Modality.Studies.Huijsmans2025.must : Modal

English necessity modal must. Underspecified for modal base; this paper only treats epistemic uses.

Equations

• Phenomena.Modality.Studies.Huijsmans2025.must = { label := "must", flavor := none, profile := Phenomena.Modality.Studies.Huijsmans2025.MBTProfile.unrestricted }

def Phenomena.Modality.Studies.Huijsmans2025.cooking : Stimulus ℤ

(40) Cooking. The fish-cooking stimulus: MB props (fish in oven, typical cook time) hold prior to PrejT (it is cooked). Both MBT and EAT analyses predict səm/will/must ✓, ćε ✗.

Equations

• Phenomena.Modality.Studies.Huijsmans2025.cooking = { earliestMBT := 0, earliestPrejT := 2, eat := 0, et := 2 }

theorem Phenomena.Modality.Studies.Huijsmans2025.cooking_table : will.profile.licenses cooking ∧ sem.profile.licenses cooking ∧ must.profile.licenses cooking ∧ ¬che.profile.licenses cooking

def Phenomena.Modality.Studies.Huijsmans2025.felipeRain : Stimulus ℤ

(46) Felipe-rain. The wedge case. MB props (it is raining, Felipe has no rain jacket) become true earlier than PrejT (Felipe is wet), but the speaker only acquires the evidence later (sees the rain at 6pm, after Felipe has already gotten wet at 5pm). So MBT < PrejT but ET < EAT. Huijsmans correctly licenses will/must; an EAT analysis incorrectly rejects will.

Equations

• Phenomena.Modality.Studies.Huijsmans2025.felipeRain = { earliestMBT := 0, earliestPrejT := 1, eat := 3, et := 1 }

theorem Phenomena.Modality.Studies.Huijsmans2025.felipe_table : will.profile.licenses felipeRain ∧ must.profile.licenses felipeRain ∧ ¬che.profile.licenses felipeRain

def Phenomena.Modality.Studies.Huijsmans2025.smellOfFish : Stimulus ℤ

(50) Smell-of-fish. The smell coincides with PrejT: at least one MB proposition (the fish smells cooked) holds at the moment the prejacent holds. ćε/must ✓, səm/will ✗.

Equations

• Phenomena.Modality.Studies.Huijsmans2025.smellOfFish = { earliestMBT := 1, earliestPrejT := 1, eat := 1, et := 1 }

theorem Phenomena.Modality.Studies.Huijsmans2025.smell_table : che.profile.licenses smellOfFish ∧ must.profile.licenses smellOfFish ∧ ¬will.profile.licenses smellOfFish ∧ ¬sem.profile.licenses smellOfFish

def Phenomena.Modality.Studies.Huijsmans2025.MBTProfile.eatLicenses {Time : Type} [LinearOrder Time] : MBTProfile → Stimulus Time → Prop

The EAT-indexed analogue of MBTProfile.licenses — applies the same partition shape to (eat, et) instead of (earliestMBT, earliestPrejT). Defined inline rather than imported from a (not-yet-existent) Hirayama-Matthewson study file.

Equations

• Phenomena.Modality.Studies.Huijsmans2025.MBTProfile.strictPrior.eatLicenses x✝ = (x✝.eat < x✝.et)
• Phenomena.Modality.Studies.Huijsmans2025.MBTProfile.nonProspective.eatLicenses x✝ = (x✝.et ≤ x✝.eat)
• Phenomena.Modality.Studies.Huijsmans2025.MBTProfile.unrestricted.eatLicenses x✝ = True

@[implicit_reducible]

instance Phenomena.Modality.Studies.Huijsmans2025.instDecidableEatLicensesOfDecidableEq {Time : Type} [LinearOrder Time] [DecidableEq Time] (c : MBTProfile) (s : Stimulus Time) : Decidable (c.eatLicenses s)

Equations

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

theorem Phenomena.Modality.Studies.Huijsmans2025.MBT_vs_EAT_diverge_on_felipe : will.profile.licenses felipeRain ∧ ¬will.profile.eatLicenses felipeRain

The empirical wedge (Huijsmans (46)–(49)).

On the Felipe-rain stimulus the MBT and EAT analyses disagree on will: the MBT-analysis licenses it (matching the judgment), the EAT-analysis rejects it (mispredicting). This is the entire empirical content of Huijsmans's argument compressed to a single decide.