Documentation

Linglib.Phenomena.Modality.Studies.Kratzer1981

Epistemic Threshold Bridge #

Connects the English modal fragment (Fragments.English.FunctionWords) to Ying et al.'s (2025) epistemic threshold semantics (Theories.Semantics.Attitudes.EpistemicThreshold).

The Bridge #

Each English epistemic modal auxiliary maps to an EpistemicEntry with a fitted threshold from Table 1(b). The bridge proves:

  1. Form agreement: the Fragment's form field matches the Theory's name
  2. Force–threshold consistency: necessity-force modals have strictly higher thresholds than possibility-force modals on their epistemic reading
  3. Within-force scalar ordering: threshold ordering captures scalar differences (must > should, may > might) that binary force cannot express

Dependency Direction #

Fragments/English/FunctionWords.lean (AuxEntry, modalMeaning)
                ↓
Theories/Semantics/Attitudes/EpistemicThreshold.lean (EpistemicEntry, θ)
                ↓
Phenomena/Modality/EpistemicThresholdBridge.lean (this file)
source
def Phenomena.Modality.EpistemicThresholdBridge.toEpistemicEntry (a : Fragments.English.FunctionWords.AuxEntry) :
Option Semantics.Attitudes.EpistemicThreshold.EpistemicEntry

Map an English modal auxiliary to its epistemic threshold entry. Only epistemic modals have a threshold; non-epistemic uses (deontic, circumstantial) are none.

The mapping derives from the Fragment's form field — no duplication of lexical data.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Phenomena.Modality.EpistemicThresholdBridge.epistemicForce (a : Fragments.English.FunctionWords.AuxEntry) :
    Option Core.Modality.ModalForce

    Extract the epistemic force of a modal auxiliary, if it has an epistemic reading. Returns none for purely deontic/circumstantial modals (e.g., shall).

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

      Per-entry verification: the Fragment's form matches the Theory's name. These are true by construction since toEpistemicEntry pattern-matches on the Fragment's form and returns the corresponding Theory entry.

      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.must_form :
      Option.map (fun (x : Semantics.Attitudes.EpistemicThreshold.EpistemicEntry) => x.name) (toEpistemicEntry Fragments.English.FunctionWords.must) = some "must"
      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.should_form :
      Option.map (fun (x : Semantics.Attitudes.EpistemicThreshold.EpistemicEntry) => x.name) (toEpistemicEntry Fragments.English.FunctionWords.should) = some "should"
      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.may_form :
      Option.map (fun (x : Semantics.Attitudes.EpistemicThreshold.EpistemicEntry) => x.name) (toEpistemicEntry Fragments.English.FunctionWords.may) = some "may"
      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.might_form :
      Option.map (fun (x : Semantics.Attitudes.EpistemicThreshold.EpistemicEntry) => x.name) (toEpistemicEntry Fragments.English.FunctionWords.might) = some "might"
      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.could_form :
      Option.map (fun (x : Semantics.Attitudes.EpistemicThreshold.EpistemicEntry) => x.name) (toEpistemicEntry Fragments.English.FunctionWords.could) = some "could"
      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.shall_no_threshold :
      toEpistemicEntry Fragments.English.FunctionWords.shall = none

      Non-epistemic modals have no threshold entry.

      The key empirical prediction: necessity-force epistemic modals have strictly higher thresholds than possibility-force epistemic modals.

      □ modals: must (0.95) > should (0.80)
◇ modals: may (0.30) > might/could (0.20)
□ > ◇: should (0.80) > may (0.30)

      This connects two independent characterizations of the same items:

      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.necessity_gt_possibility_must_might :
      Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.must_.θ > Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.might_.θ

      Every necessity-force epistemic modal has a higher threshold than every possibility-force epistemic modal.

      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.necessity_gt_possibility_must_may :
      Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.must_.θ > Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.may_.θ
      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.necessity_gt_possibility_should_might :
      Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.should_.θ > Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.might_.θ
      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.necessity_gt_possibility_should_may :
      Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.should_.θ > Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.may_.θ
      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.necessity_gt_possibility_should_could :
      Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.should_.θ > Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.could_.θ
      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.must_is_necessity :
      epistemicForce Fragments.English.FunctionWords.must = some Core.Modality.ModalForce.necessity

      The epistemic force of must is necessity (derived from Fragment).

      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.might_is_possibility :
      epistemicForce Fragments.English.FunctionWords.might = some Core.Modality.ModalForce.possibility

      The epistemic force of might is possibility (derived from Fragment).

      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.should_is_weakNecessity :
      epistemicForce Fragments.English.FunctionWords.should = some Core.Modality.ModalForce.weakNecessity

      The epistemic force of should is weak necessity (derived from Fragment).

      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.may_is_possibility :
      epistemicForce Fragments.English.FunctionWords.may = some Core.Modality.ModalForce.possibility

      The epistemic force of may is possibility (derived from Fragment).

      Thresholds decrease monotonically with force: must (□) > should (□w) > may (◇) > might = could (◇). The □ > □w gap is captured by the 3-way ModalForce distinction; the within-◇ gap remains a scalar difference.

      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.must_gt_should :
      Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.must_.θ > Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.should_.θ

      □ > □w: must (strong necessity) > should (weak necessity).

      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.may_gt_might :
      Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.may_.θ > Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.might_.θ

      Among possibility modals: may > might. Both are ◇ but may is stronger.

      source
      theorem Phenomena.Modality.EpistemicThresholdBridge.might_eq_could :
      Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.might_.θ = Semantics.Attitudes.EpistemicThreshold.EpistemicEntry.could_.θ

      might = could in threshold (both 0.20).