Documentation

Linglib.Phenomena.Modality.Studies.Kratzer2012Scenario

Conditional Modality Data — Rain and Wet Streets (@cite{kratzer-2012} §2.9) #

Four worlds with two properties (rain, wet street) and a causal regularity:

WorldRainWet StreetNotes
w0yesyesNormal causation
w1yesnoBroken drainage (anomalous)
w2noyesSprinkler
w3nonoNormal non-rain

Two time points: yesterday (t = −1) and now (t = 0). Rain occurs yesterday; wetness holds now. The function atTime projects World → ℤ → Bool to BProp World at a specific time, bridging the temporal and modal type systems.

Reference: Kratzer, A. (2012). Modals and Conditionals. Oxford University Press. Ch. 2 §2.9.

Atemporal propositions #

source
def Phenomena.Modality.ConditionalModality.rained :
BProp Semantics.Attitudes.Intensional.World

It rained: true at w0 (normal rain) and w1 (rain + broken drainage).

Equations
Instances For
    source
    def Phenomena.Modality.ConditionalModality.streetWet :
    BProp Semantics.Attitudes.Intensional.World

    The street is wet: true at w0 (rain → wet) and w2 (sprinkler).

    Equations
    Instances For

      Temporal propositions and the type bridge #

      source
      def Phenomena.Modality.ConditionalModality.rainedAt :
      Semantics.Attitudes.Intensional.World → ℤ → Bool

      Rain as a temporal proposition: it rained yesterday (t = −1).

      Equations
      Instances For
        source
        def Phenomena.Modality.ConditionalModality.wetStreetAt :
        Semantics.Attitudes.Intensional.World → ℤ → Bool

        Wet street as a temporal proposition: the street is wet now (t = 0).

        Equations
        Instances For
          source
          def Phenomena.Modality.ConditionalModality.atTime (p : Semantics.Attitudes.Intensional.World → ℤ → Bool) (t : ℤ) :
          BProp Semantics.Attitudes.Intensional.World

          The type bridge: project a temporal proposition at a specific time to a world proposition BProp World. This is what allows a past-tense antecedent to enter a Kratzer modal base.

          Equations
          Instances For

            Conversational backgrounds #

            source
            def Phenomena.Modality.ConditionalModality.totallyRealisticBg :
            Semantics.Modality.Kratzer.ModalBase

            Totally realistic modal base: ∩f(w) = {w} for each world. Each world's fact set contains the proposition "being exactly that world."

            Equations
            Instances For
              source
              def Phenomena.Modality.ConditionalModality.normalcySource :
              Semantics.Modality.Kratzer.OrderingSource

              Normalcy ordering source: ranks worlds where rain-without-wet-street is abnormal. The ordering proposition penalizes w1 (rained ∧ ¬streetWet).

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

                Theory-neutral facts #

                source
                theorem Phenomena.Modality.ConditionalModality.w0_rained_wet :
                rained Core.Proposition.World4.w0 = true ∧ streetWet Core.Proposition.World4.w0 = true
                source
                theorem Phenomena.Modality.ConditionalModality.w1_rained_dry :
                rained Core.Proposition.World4.w1 = true ∧ streetWet Core.Proposition.World4.w1 = false
                source
                theorem Phenomena.Modality.ConditionalModality.w2_dry_wet :
                rained Core.Proposition.World4.w2 = false ∧ streetWet Core.Proposition.World4.w2 = true
                source
                theorem Phenomena.Modality.ConditionalModality.w3_dry_dry :
                rained Core.Proposition.World4.w3 = false ∧ streetWet Core.Proposition.World4.w3 = false
                source
                theorem Phenomena.Modality.ConditionalModality.atTime_rainedAt_yesterday :
                atTime rainedAt (-1) = rained

                Temporal projection at yesterday recovers the atemporal rained.

                source
                theorem Phenomena.Modality.ConditionalModality.atTime_wetStreetAt_now :
                atTime wetStreetAt 0 = streetWet

                Temporal projection at now recovers the atemporal streetWet.