Documentation

Linglib.Phenomena.TenseAspect.Studies.Abusch1997

Tense: ContextTower #

@cite{abusch-1997} @cite{schlenker-2003} @cite{von-stechow-2009}

End-to-end derivation chain connecting the ContextTower infrastructure to concrete tense phenomena. The core insight: embedded tense is modeled as a temporalShift on the tower, and the embedded clause's perspective time is read from the shifted (innermost) context.

Derivation Chain #

Core.Context.Tower (ContextTower, push, innermost, origin)
    ↓
Core.Context.Shifts (temporalShift: changes time, preserves agent/world)
    ↓
This file: tower operations produce the Reichenbach frames in Data.lean
    ↓
Phenomena.TenseAspect.Data (matrixSaid, embeddedSickSimultaneous, etc.)

Key Results #

  1. Root clause = root tower: contextAt 0 = origin, so P = S (speech time)
  2. SOT embedding = temporal shift: temporalShift(matrixEventTime) produces the embedded perspective time P' = E_matrix
  3. Double access = origin reading: present-under-past reads time from .origin (speech time), not .local (matrix event time)
  4. Tower depth = embedding depth: one attitude verb = depth 1; nested attitudes = depth 2+
source
@[reducible, inline]
abbrev Phenomena.TenseAspect.Studies.Abusch1997.TenseCtx :
Type

A minimal tense context: world, agent, position, and time (as ℤ).

Equations
Instances For
    source
    def Phenomena.TenseAspect.Studies.Abusch1997.speechCtx :
    TenseCtx

    The speech-act context: time = 0 (speech time).

    Equations
    Instances For
      source
      def Phenomena.TenseAspect.Studies.Abusch1997.rootTower :
      Core.Context.ContextTower TenseCtx

      A root clause is a tower with no shifts: depth 0.

      Equations
      Instances For
        source
        theorem Phenomena.TenseAspect.Studies.Abusch1997.root_perspective_eq_speech :
        rootTower.innermost.time = rootTower.origin.time

        In a root tower, the innermost context IS the origin. Therefore P = S (perspective time = speech time), which is the defining property of root clauses in the Reichenbach framework.

        source
        theorem Phenomena.TenseAspect.Studies.Abusch1997.root_depth_zero :
        rootTower.depth = 0

        Root tower has depth 0.

        source
        def Phenomena.TenseAspect.Studies.Abusch1997.sotTower :
        Core.Context.ContextTower TenseCtx

        "John said..." pushes a temporal shift: the matrix event time (-2) becomes the embedded clause's perspective time.

        This models @cite{von-stechow-2009}: the attitude verb transmits its event time to the embedded clause.

        Equations
        Instances For
          source
          theorem Phenomena.TenseAspect.Studies.Abusch1997.sot_perspective_shifted :
          sotTower.innermost.time = -2

          After the temporal shift, the embedded perspective time is the matrix event time (-2), not the speech time (0). This is the SOT mechanism: embedded tense is evaluated relative to the matrix event time.

          source
          theorem Phenomena.TenseAspect.Studies.Abusch1997.sot_origin_preserved :
          sotTower.origin.time = 0

          The temporal shift doesn't change the origin — speech time is still 0. This is Kaplan's thesis: the speech-act context is invariant under embedding.

          source
          theorem Phenomena.TenseAspect.Studies.Abusch1997.sot_depth_one :
          sotTower.depth = 1

          SOT tower has depth 1 (one embedding).

          source
          theorem Phenomena.TenseAspect.Studies.Abusch1997.sot_perspective_matches_matrix_event :
          sotTower.innermost.time = matrixSaid.eventTime

          The embedded perspective time (-2) equals the matrix event time in matrixSaid. This is the end-to-end bridge: tower operation → Reichenbach frame.

          source
          theorem Phenomena.TenseAspect.Studies.Abusch1997.simultaneous_perspective_match :
          sotTower.innermost.time = embeddedSickSimultaneous.perspectiveTime

          The simultaneous reading: embedded R' = embedded P = matrix E = -2. This matches embeddedSickSimultaneous.perspectiveTime.

          source
          def Phenomena.TenseAspect.Studies.Abusch1997.presentAccess :
          Core.Context.AccessPattern TenseCtx ℤ

          "John said Mary IS sick" (present-under-past): the present tense in the embedded clause reads from the ORIGIN (speech time), not from the shifted context. This is the double-access reading: the embedded present anchors to speech time despite being under a past matrix verb.

          Tower model: the embedded present uses DepthSpec.origin for its temporal coordinate, reading time = 0 from the origin.

          Equations
          Instances For
            source
            theorem Phenomena.TenseAspect.Studies.Abusch1997.double_access_reads_speech_time :
            presentAccess.resolve sotTower = 0

            Present-under-past reads speech time (0), not matrix event time (-2).

            source
            theorem Phenomena.TenseAspect.Studies.Abusch1997.double_access_matches_data :
            presentAccess.resolve sotTower = embeddedSickPresent.speechTime

            The embedded present's time (0) matches the speech time in embeddedSickPresent. End-to-end: tower origin access → Reichenbach frame perspective time.

            source
            def Phenomena.TenseAspect.Studies.Abusch1997.shiftedAccess :
            Core.Context.AccessPattern TenseCtx ℤ

            The shifted reading ("Mary WAS sick before John said so") reads from the LOCAL (innermost) context. The embedded past tense evaluates its reference time relative to the shifted perspective time.

            Equations
            Instances For
              source
              theorem Phenomena.TenseAspect.Studies.Abusch1997.shifted_reads_matrix_time :
              shiftedAccess.resolve sotTower = -2

              Shifted reading reads matrix event time (-2) from the innermost context.

              source
              theorem Phenomena.TenseAspect.Studies.Abusch1997.shifted_matches_data :
              shiftedAccess.resolve sotTower = embeddedSickShifted.perspectiveTime

              The shifted reading's perspective time matches the embedded frame.

              source
              theorem Phenomena.TenseAspect.Studies.Abusch1997.kaplan_thesis_for_tense :
              presentAccess.resolve sotTower = presentAccess.resolve rootTower

              Kaplan's thesis formalized: an origin-accessing expression yields the same value regardless of how many shifts are pushed. The speech time is invariant under SOT embedding.

              source
              def Phenomena.TenseAspect.Studies.Abusch1997.nestedTower :
              Core.Context.ContextTower TenseCtx

              "John said that Mary believed that Bill was sick" — double embedding. Two temporal shifts: first to John's saying time (-2), then to Mary's believing time (-4).

              Equations
              Instances For
                source
                theorem Phenomena.TenseAspect.Studies.Abusch1997.nested_depth_two :
                nestedTower.depth = 2

                Double embedding has depth 2.

                source
                theorem Phenomena.TenseAspect.Studies.Abusch1997.nested_innermost :
                nestedTower.innermost.time = -4

                The innermost context in a doubly-embedded clause reads the most deeply shifted time (-4).

                source
                theorem Phenomena.TenseAspect.Studies.Abusch1997.nested_origin_preserved :
                nestedTower.origin.time = 0

                Even under double embedding, the origin (speech time) is preserved.

                source
                theorem Phenomena.TenseAspect.Studies.Abusch1997.nested_double_access :
                presentAccess.resolve nestedTower = 0

                Double access still works at depth 2: present-under-past-under-past reads from the origin.