Huijsmans (2025): Timing of evidence and epistemic modal claims

This file formalizes Huijsmans's account of the ʔayʔaǰuθəm future clitic səm and inferential č̓ɛ and of English will and must as strong epistemic necessity modals that differ in a presupposition on the timing of the evidence. The modal base is a set of propositions each with an earliest moment at which it holds (IsEarliest); səm and will presuppose that every modal-base proposition holds before the earliest moment of the prejacent (FuturePresup), č̓ɛ that at least one holds at or after it (InferentialPresup), and must presupposes nothing. Where the earliest moments exist, the two presuppositions are complementary (futurePresup_iff_not_inferentialPresup), which is the distribution of Section 4: contexts with all the evidence in place before the prejacent take səm and will, and contexts with evidence arising at or after it take č̓ɛ, with must felicitous in both. An empty modal base falsifies the inferential's presupposition (not_inferentialPresup_empty), the prediction the paper checks against the cat that has gone missing.

The rival analysis in terms of an evidence acquisition time relates that time to the event time on the library's Tense.EvidentialFrame. Evidence that has become true can be acquired only afterwards, so the inferential's presupposition entails downstream evidence (downstream_of_inferentialPresup); the converse fails, and the contexts where the speaker learns of rain or of a night's clam-digging after the wetting or the cold are the wedge: the modal-base timing licenses will, and the acquisition timing does not (felipe_future, felipe_not_eatFuture).

Implementation notes

• The earliest moment of a proposition is taken in the evaluation world rather than in a maximally similar one, and the modal-base propositions are already shifted to untensed ones, so the reference-time index and the abstraction rule are not represented.
• The contexts of Section 4 are stated by the onset times of the eventualities, following the remark that a proposition describing an eventuality holds forever after it; the at-issue content is Kratzer necessity over the best worlds with the non-past orientation of the future morphemes.

References

• [Hui25]
• [Kra81b]
• [Con02]
• [BC03]

Earliest moments and the presuppositions

def Huijsmans2025.IsEarliest {T : Type u_1} {W : Type u_2} [LinearOrder T] (p : T → W → Prop) (w : W) (m : T) : Prop

The earliest moment at which an untensed proposition holds in a world, the function of (63), is a time at which it holds that precedes every other.

Equations

• Huijsmans2025.IsEarliest p w m = (p m w ∧ ∀ (t : T), p t w → m ≤ t)

theorem Huijsmans2025.IsEarliest.unique {T : Type u_1} {W : Type u_2} [LinearOrder T] {p : T → W → Prop} {w : W} {m m' : T} (h : IsEarliest p w m) (h' : IsEarliest p w m') : m = m'

def Huijsmans2025.FuturePresup {T : Type u_1} {W : Type u_2} [LinearOrder T] (mb : Set (T → W → Prop)) (p : T → W → Prop) (w : W) : Prop

The presupposition of səm and will, (65), is that every modal-base proposition has its earliest moment before the earliest moment of the prejacent.

Equations

• Huijsmans2025.FuturePresup mb p w = ∀ q ∈ mb, ∃ (mq : T) (mp : T), Huijsmans2025.IsEarliest q w mq ∧ Huijsmans2025.IsEarliest p w mp ∧ mq < mp

def Huijsmans2025.InferentialPresup {T : Type u_1} {W : Type u_2} [LinearOrder T] (mb : Set (T → W → Prop)) (p : T → W → Prop) (w : W) : Prop

The presupposition of č̓ɛ, (87), is that some modal-base proposition has its earliest moment at or after the earliest moment of the prejacent.

Equations

• Huijsmans2025.InferentialPresup mb p w = ∃ q ∈ mb, ∃ (mq : T) (mp : T), Huijsmans2025.IsEarliest q w mq ∧ Huijsmans2025.IsEarliest p w mp ∧ mp ≤ mq

theorem Huijsmans2025.futurePresup_iff_not_inferentialPresup {T : Type u_1} {W : Type u_2} [LinearOrder T] {mb : Set (T → W → Prop)} {p : T → W → Prop} {w : W} (hmb : ∀ q ∈ mb, ∃ (m : T), IsEarliest q w m) (hp : ∃ (m : T), IsEarliest p w m) : FuturePresup mb p w ↔ ¬InferentialPresup mb p w

Where the earliest moments exist, the two presuppositions are complementary, so the contexts of Section 4 split between səm and č̓ɛ.

theorem Huijsmans2025.not_inferentialPresup_empty {T : Type u_1} {W : Type u_2} [LinearOrder T] (p : T → W → Prop) (w : W) : ¬InferentialPresup ∅ p w

An inference from no evidence cannot be an inferential, as in (56).

The at-issue content

def Huijsmans2025.modalBaseAt {T : Type u_1} {W : Type u_2} (mb : Set (T → W → Prop)) (t : T) : Modality.Background W

The modal base at a reference time, as the world-propositions of the untensed ones.

Equations

• Huijsmans2025.modalBaseAt mb t x✝ = (fun (q : T → W → Prop) (w : W) => q t w) '' mb

def Huijsmans2025.futureClaim {T : Type u_1} {W : Type u_2} [LinearOrder T] (mb : Set (T → W → Prop)) (h : Modality.Background W) (p : T → W → Prop) (t : T) (w : W) : Prop

The at-issue content of səm and will, (62), is that the prejacent holds at or after the reference time in every best world.

Equations

• Huijsmans2025.futureClaim mb h p t w = Modality.necessity (Huijsmans2025.modalBaseAt mb t) h (fun (w' : W) => ∃ (t' : T), t ≤ t' ∧ p t' w') w

def Huijsmans2025.necessityClaim {T : Type u_1} {W : Type u_2} (mb : Set (T → W → Prop)) (h : Modality.Background W) (p : T → W → Prop) (t : T) (w : W) : Prop

The at-issue content of č̓ɛ and must, (87) and (96), is that the prejacent holds at the reference time in every best world.

Equations

• Huijsmans2025.necessityClaim mb h p t w = Modality.necessity (Huijsmans2025.modalBaseAt mb t) h (fun (w' : W) => p t w') w

theorem Huijsmans2025.futureClaim_of_necessityClaim {T : Type u_1} {W : Type u_2} [LinearOrder T] {mb : Set (T → W → Prop)} {h : Modality.Background W} {p : T → W → Prop} {t : T} {w : W} (hc : necessityClaim mb h p t w) : futureClaim mb h p t w

Present orientation is a case of the future morphemes' non-past orientation.

The evidence acquisition time

def Huijsmans2025.EatFuture {T : Type u_1} [LinearOrder T] (f : Tense.EvidentialFrame T) : Prop

On the rival analysis (39), the future morphemes require the evidence to be acquired before the event, and the inferential at or after it, the frame's Downstream.

Equations

• Huijsmans2025.EatFuture f = (f.acquisitionTime < f.eventTime)

@[instance_reducible]

instance Huijsmans2025.instDecidableEatFuture {T : Type u_1} [LinearOrder T] (f : Tense.EvidentialFrame T) : Decidable (EatFuture f)

Equations

• Huijsmans2025.instDecidableEatFuture f = Huijsmans2025.instDecidableEatFuture._aux_1 f

def Huijsmans2025.AcquiredAfterOnset {T : Type u_1} {W : Type u_2} [LinearOrder T] (mb : Set (T → W → Prop)) (w : W) (f : Tense.EvidentialFrame T) : Prop

A modal-base proposition can be acquired only once it holds.

Equations

• Huijsmans2025.AcquiredAfterOnset mb w f = ∀ q ∈ mb, ∀ (m : T), Huijsmans2025.IsEarliest q w m → m ≤ f.acquisitionTime

theorem Huijsmans2025.downstream_of_inferentialPresup {T : Type u_1} {W : Type u_2} [LinearOrder T] {mb : Set (T → W → Prop)} {p : T → W → Prop} {w : W} {f : Tense.EvidentialFrame T} (hacq : AcquiredAfterOnset mb w f) (hev : IsEarliest p w f.eventTime) (h : InferentialPresup mb p w) : f.Downstream

The inferential's presupposition entails downstream evidence when the prejacent's earliest moment is the event time, the remark of Section 4.2 that the two analyses agree on č̓ɛ in one direction.

The contexts of Section 4

def Huijsmans2025.from' (o : ℤ) : ℤ → Unit → Prop

A proposition describing an eventuality holds from its onset on.

Equations

• Huijsmans2025.from' o t x✝ = (o ≤ t)

theorem Huijsmans2025.isEarliest_from' (o : ℤ) : IsEarliest (from' o) () o

theorem Huijsmans2025.isEarliest_from'_iff {o m : ℤ} : IsEarliest (from' o) () m ↔ m = o

structure Huijsmans2025.Context : Type

A context gives the onsets of the modal-base eventualities, the onset of the prejacent eventuality, and the times of the evidence's acquisition and of the utterance.

• onsets : List ℤ
• prejacent : ℤ
• acquisition : ℤ
• speech : ℤ

def Huijsmans2025.Context.mb (c : Context) : Set (ℤ → Unit → Prop)

Equations

• c.mb = {q : ℤ → Unit → Prop | ∃ o ∈ c.onsets, q = Huijsmans2025.from' o}

def Huijsmans2025.Context.frame (c : Context) : Tense.EvidentialFrame ℤ

Equations

• c.frame = { speechTime := c.speech, eventTime := c.prejacent, acquisitionTime := c.acquisition }

theorem Huijsmans2025.Context.futurePresup_iff (c : Context) : FuturePresup c.mb (from' c.prejacent) () ↔ ∀ o ∈ c.onsets, o < c.prejacent

In the form of the diagrams, (35) says that every onset precedes the prejacent's.

theorem Huijsmans2025.Context.inferentialPresup_iff (c : Context) : InferentialPresup c.mb (from' c.prejacent) () ↔ ∃ o ∈ c.onsets, c.prejacent ≤ o

In the form of the diagrams, (36) says that some onset is at or after the prejacent's.

@[instance_reducible]

instance Huijsmans2025.Context.instDecidableFuturePresupIntUnitMbFrom'PrejacentUnit (c : Context) : Decidable (FuturePresup c.mb (from' c.prejacent) ())

Equations

• c.instDecidableFuturePresupIntUnitMbFrom'PrejacentUnit = decidable_of_iff (∀ o ∈ c.onsets, o < c.prejacent) ⋯

@[instance_reducible]

instance Huijsmans2025.Context.instDecidableInferentialPresupIntUnitMbFrom'PrejacentUnit (c : Context) : Decidable (InferentialPresup c.mb (from' c.prejacent) ())

Equations

• c.instDecidableInferentialPresupIntUnitMbFrom'PrejacentUnit = decidable_of_iff (∃ o ∈ c.onsets, c.prejacent ≤ o) ⋯

def Huijsmans2025.cooking : Context

In (40)–(41) the fish went into the oven and past occasions are known before it is cooked, and the watch is checked before the cooking is complete.

Equations

• Huijsmans2025.cooking = { onsets := [0, 0], prejacent := 2, acquisition := 1, speech := 2 }

def Huijsmans2025.daniel : Context

In (42)–(43) Daniel's leaving and the length of the trip precede his getting home.

Equations

• Huijsmans2025.daniel = { onsets := [0, 0], prejacent := 2, acquisition := 1, speech := 3 }

def Huijsmans2025.poison : Context

In (44)–(45) the poisoning precedes the death.

Equations

• Huijsmans2025.poison = { onsets := [0, 0], prejacent := 2, acquisition := 0, speech := 3 }

def Huijsmans2025.felipe : Context

In (46)–(47) the rain and the coat left behind precede Felipe's wetting at five, but the speaker sees the rain only at six.

Equations

• Huijsmans2025.felipe = { onsets := [4, 0], prejacent := 5, acquisition := 6, speech := 6 }

def Huijsmans2025.clamDigging : Context

In (48)–(49) the cold night and the clam-digging precede the friend's getting cold, and the speaker learns of the clam-digging the next day.

Equations

• Huijsmans2025.clamDigging = { onsets := [0, 0], prejacent := 1, acquisition := 2, speech := 2 }

def Huijsmans2025.smell : Context

In (50)–(51) the smell of the fish arises as it is cooked.

Equations

• Huijsmans2025.smell = { onsets := [1], prejacent := 1, acquisition := 1, speech := 1 }

def Huijsmans2025.driveway : Context

In (52)–(53) and (83) the car is in the driveway from the arrival home on.

Equations

• Huijsmans2025.driveway = { onsets := [1], prejacent := 1, acquisition := 2, speech := 2 }

def Huijsmans2025.bear : Context

In (54)–(55) the bear stops moving as it dies.

Equations

• Huijsmans2025.bear = { onsets := [1], prejacent := 1, acquisition := 2, speech := 2 }

def Huijsmans2025.homeFromWork : Context

In (57)–(58) evidence both before and at the prejacent, the time of day and the car and lights, is taken together.

Equations

• Huijsmans2025.homeFromWork = { onsets := [0, 1, 1], prejacent := 1, acquisition := 2, speech := 2 }

def Huijsmans2025.ovenAndSmell : Context

In (59)–(60) there are twenty minutes in the oven and the smell, and the smell may be set aside.

Equations

• Huijsmans2025.ovenAndSmell = { onsets := [0, 1], prejacent := 1, acquisition := 1, speech := 1 }

def Huijsmans2025.ovenOnly : Context

Equations

• Huijsmans2025.ovenOnly = { onsets := [0], prejacent := 1, acquisition := 1, speech := 1 }

def Huijsmans2025.missingCat : Context

In (56) there is no evidence at all.

Equations

• Huijsmans2025.missingCat = { onsets := [], prejacent := 1, acquisition := 0, speech := 0 }

theorem Huijsmans2025.cooking_future : FuturePresup cooking.mb (from' cooking.prejacent) ()

theorem Huijsmans2025.cooking_not_inferential : ¬InferentialPresup cooking.mb (from' cooking.prejacent) ()

theorem Huijsmans2025.felipe_future : FuturePresup felipe.mb (from' felipe.prejacent) ()

theorem Huijsmans2025.felipe_not_inferential : ¬InferentialPresup felipe.mb (from' felipe.prejacent) ()

theorem Huijsmans2025.felipe_not_eatFuture : ¬EatFuture felipe.frame

The evidence is acquired after the event, so the acquisition analysis rejects will and səm here, against the judgments.

theorem Huijsmans2025.felipe_downstream : felipe.frame.Downstream

theorem Huijsmans2025.clamDigging_future : FuturePresup clamDigging.mb (from' clamDigging.prejacent) ()

theorem Huijsmans2025.clamDigging_not_eatFuture : ¬EatFuture clamDigging.frame

theorem Huijsmans2025.smell_inferential : InferentialPresup smell.mb (from' smell.prejacent) ()

theorem Huijsmans2025.smell_not_future : ¬FuturePresup smell.mb (from' smell.prejacent) ()

theorem Huijsmans2025.driveway_inferential : InferentialPresup driveway.mb (from' driveway.prejacent) ()

theorem Huijsmans2025.bear_not_future : ¬FuturePresup bear.mb (from' bear.prejacent) ()

theorem Huijsmans2025.homeFromWork_inferential : InferentialPresup homeFromWork.mb (from' homeFromWork.prejacent) ()

In (57) evidence on both sides of the prejacent forces the inferential.

theorem Huijsmans2025.homeFromWork_not_future : ¬FuturePresup homeFromWork.mb (from' homeFromWork.prejacent) ()

theorem Huijsmans2025.ovenAndSmell_inferential : InferentialPresup ovenAndSmell.mb (from' ovenAndSmell.prejacent) ()

In (59)–(60), with the smell in the modal base the inferential is licensed, and with it set aside the future is.

theorem Huijsmans2025.ovenOnly_future : FuturePresup ovenOnly.mb (from' ovenOnly.prejacent) ()

theorem Huijsmans2025.missingCat_not_inferential : ¬InferentialPresup missingCat.mb (from' missingCat.prejacent) ()