Tense–Modal Evidentiality Bridge #
@cite{cumming-2026} @cite{von-fintel-gillies-2010} @cite{zheng-2025}
Connects @cite{cumming-2026}'s tense evidential constraint to @cite{von-fintel-gillies-2010} kernel semantics for epistemic must. Both phenomena reflect the same
underlying requirement: the speaker's evidence is indirect — causally downstream
of the target event but not directly settling it.
The Parallel #
| Cumming (tense) | VF&G (modals) |
|---|---|
| T ≤ A (downstream evidence) | K doesn't settle φ |
| Nonfuture → downstream required | must → indirectness presupposition |
| Future → no constraint | Bare assertion → no presupposition |
| Direct observation → bare past ok | Direct evidence → must infelicitous |
EvidentialPerspective (the three temporal orientations) lives in Core.Evidence;
EPCondition/UPCondition (the five attested constraint shapes) live in
Theories/Semantics.Montague/Sentence/Tense/Evidential.lean.
Concrete Scenario: Dripping Raincoat #
The dripping-raincoat scenario (@cite{zheng-2025}, used in Kernel.lean) provides a concrete bridge: the raincoat evidence is causally downstream of rain (T ≤ A), and the kernel {wearingRaincoat} doesn't settle isRaining.
The kernel defs in Kernel.lean are private. We redefine equivalent
propositions over World4 for the bridge. The world interpretation:
w0 = raining, w1 = sprinkler (wet but not rain), w2 = dry, w3 = unknown.
Wearing a raincoat: true in w0 (rain) and w1 (sprinkler).
Equations
Instances For
It is raining: true only in w0.
Equations
Instances For
The raincoat kernel: K = {wearingRaincoat}.
Equations
Instances For
A concrete evidential frame for the raincoat scenario: S = 0 (speech time now), T = -2 (rain event in the past), R = 0, A = -1 (evidence acquired between event and speech).
Equations
- Phenomena.TenseAspect.CompareTenseModal.raincoatFrame = { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := -2, acquisitionTime := -1 }
Instances For
The raincoat evidence is downstream: T ≤ A (-2 ≤ -1).
The raincoat kernel doesn't settle isRaining: K = {wearingRaincoat}, and wearingRaincoat neither entails nor excludes isRaining.
Downstream implies must-defined: in the raincoat scenario, downstream evidence (T ≤ A) co-occurs with the kernel not settling the prejacent. This is a concrete theorem over World4 — the general claim (that evidence derived from downstream causal effects doesn't individually entail the target event) would require formalizing causation.
Tense–modal evidential parallel: both Cumming's nonfuture constraint
and VF&G's kernelMust presupposition hold simultaneously for the same
scenario. The raincoat evidence is downstream (T ≤ A) AND the kernel
doesn't settle isRaining — so both nonfuture tense ("It rained") and
must ("It must be raining") are felicitous.
Direct evidence blocks both: when evidence is direct (the speaker saw the rain), the kernel settles the prejacent. Then:
kernelMustis undefined (presupposition failure)- The tense evidential constraint is vacuously satisfied (T ≤ A holds trivially when A = T for direct observation)
- The speaker uses a bare assertion ("It's raining"), not "must"
Witness: K = {isRaining} directly settles isRaining.
Strong assertions (ego + direct) correspond to settling kernels. When the speaker has privileged access AND direct evidence, the kernel settles the prejacent — 'must' is infelicitous, bare assertion is used.
Inferential claims (nonparticipant + inference) correspond to non-settling kernels with must-defined presuppositions — the canonical 'must' profile.
Ego↔direct and nonparticipant↔indirect form natural pairs. This is the core glossary insight: epistemic authority and evidential source are orthogonal dimensions that CORRELATE but don't reduce.