Documentation

Linglib.Phenomena.TenseAspect.CompareTenseModal

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 requiredmust → indirectness presupposition
Future → no constraintBare assertion → no presupposition
Direct observation → bare past okDirect evidence → must infelicitous

EvidentialPerspective (the three temporal orientations) lives in Features.Evidentiality; 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.

source
@[reducible, inline]
abbrev Phenomena.TenseAspect.CompareTenseModal.World :
Type
Equations
Instances For
    source
    def Phenomena.TenseAspect.CompareTenseModal.allWorlds :
    List World
    Equations
    Instances For

      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.

      source
      def Phenomena.TenseAspect.CompareTenseModal.wearingRaincoat :
      World → Prop

      Wearing a raincoat: true in w0 (rain) and w1 (sprinkler).

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Phenomena.TenseAspect.CompareTenseModal.instDecidablePredWorldWearingRaincoat :
        DecidablePred wearingRaincoat
        Equations
        source
        def Phenomena.TenseAspect.CompareTenseModal.isRaining :
        World → Prop

        It is raining: true only in w0.

        Equations
        Instances For
          source
          @[implicit_reducible]
          instance Phenomena.TenseAspect.CompareTenseModal.instDecidablePredWorldIsRaining :
          DecidablePred isRaining
          Equations
          source
          def Phenomena.TenseAspect.CompareTenseModal.raincoatK :
          Semantics.Modality.Kernel World

          The raincoat kernel: K = {wearingRaincoat}.

          Equations
          Instances For
            source
            def Phenomena.TenseAspect.CompareTenseModal.raincoatFrame :
            Semantics.Tense.Evidential.EvidentialFrame ℤ

            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
            Instances For
              source
              theorem Phenomena.TenseAspect.CompareTenseModal.raincoat_downstream :
              Semantics.Tense.Evidential.downstreamEvidence raincoatFrame

              The raincoat evidence is downstream: T ≤ A (-2 ≤ -1).

              source
              theorem Phenomena.TenseAspect.CompareTenseModal.raincoat_not_settled :
              ¬Semantics.Modality.directlySettlesExplicit raincoatK isRaining

              The raincoat kernel doesn't settle isRaining: K = {wearingRaincoat}, and wearingRaincoat neither entails nor excludes isRaining.

              source
              theorem Phenomena.TenseAspect.CompareTenseModal.downstream_implies_must_defined :
              Semantics.Tense.Evidential.downstreamEvidence raincoatFrame ∧ (Semantics.Modality.kernelMust raincoatK isRaining).presup 0

              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.

              source
              theorem Phenomena.TenseAspect.CompareTenseModal.tense_modal_evidential_parallel :
              Semantics.Tense.Evidential.downstreamEvidence raincoatFrame ∧ (Semantics.Modality.kernelMust raincoatK isRaining).presup 0 ∧ ¬(Semantics.Modality.kernelMust raincoatK isRaining).assertion 0

              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.

              source
              theorem Phenomena.TenseAspect.CompareTenseModal.direct_evidence_blocks_both :
              have directK := { props := [isRaining] }; Semantics.Modality.directlySettlesExplicit directK isRaining ∧ ¬(Semantics.Modality.kernelMust directK isRaining).presup 0 ∧ have directFrame := { speechTime := 0, perspectiveTime := 0, referenceTime := 0, eventTime := -1, acquisitionTime := -1 }; Semantics.Tense.Evidential.downstreamEvidence directFrame
              source
              theorem Phenomena.TenseAspect.CompareTenseModal.strong_assertion_settles :
              Core.Epistemicity.strongAssertion.source = Features.Evidentiality.EvidentialSource.direct ∧ Core.Epistemicity.strongAssertion.authority = Core.Epistemicity.EpistemicAuthority.ego ∧ have directK := { props := [isRaining] }; Semantics.Modality.directlySettlesExplicit directK 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.

              source
              theorem Phenomena.TenseAspect.CompareTenseModal.inferential_claim_must_profile :
              Core.Epistemicity.inferentialClaim.source = Features.Evidentiality.EvidentialSource.inference ∧ Core.Epistemicity.inferentialClaim.authority = Core.Epistemicity.EpistemicAuthority.nonparticipant ∧ ¬Semantics.Modality.directlySettlesExplicit raincoatK isRaining ∧ (Semantics.Modality.kernelMust raincoatK isRaining).presup 0

              Inferential claims (nonparticipant + inference) correspond to non-settling kernels with must-defined presuppositions — the canonical 'must' profile.

              source
              theorem Phenomena.TenseAspect.CompareTenseModal.authority_source_correlation :
              Core.Epistemicity.strongAssertion.authority = Core.Epistemicity.EpistemicAuthority.ego ∧ Core.Epistemicity.strongAssertion.source = Features.Evidentiality.EvidentialSource.direct ∧ Core.Epistemicity.inferentialClaim.authority = Core.Epistemicity.EpistemicAuthority.nonparticipant ∧ Core.Epistemicity.inferentialClaim.source = Features.Evidentiality.EvidentialSource.inference

              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.