Documentation

Studies.Klecha2016

Klecha (2016): Modality and Embedded Temporal Operators #

Klecha accounts for the temporal orientation of finite clauses under attitude verbs through their modal bases. His new data, (2) and (3), are past-under-past sentences with hope and pray whose embedded event follows the attitude, readings Abusch's Upper Limit Constraint forbids and think lacks, (6). The modal base pronouns of (35) carry the constraint: dox returns actual histories, ending at the evaluation time, and cir future histories, beginning after it, so each base is the substrate's base oriented by a tense cell. A past-under-past clause has an underlying past or non-past, and its readings are the orientations its attitude's modal bases and its tense both admit: think takes dox alone, hope either.

Implementation notes #

References #

source
inductive Klecha2016.Background :
Type

The modal base pronouns of (35), dox returning the actual histories π’œ_t, which end at the evaluation time, and cir the future histories β„±_t, which begin after it.

Instances For
    source
    @[instance_reducible]
    instance Klecha2016.instDecidableEqBackground :
    DecidableEq Background
    Equations
    source
    def Klecha2016.instReprBackground.repr :
    Background β†’ β„• β†’ Std.Format
    Equations
    Instances For
      source
      @[instance_reducible]
      instance Klecha2016.instReprBackground :
      Repr Background
      Equations
      source
      def Klecha2016.Background.orientations :
      Background β†’ Finset Ordering

      The orientations a modal base admits for the reference time of its prejacent relative to the evaluation time are past and present under dox and future under cir (Table 1).

      Equations
      Instances For
        source
        def Klecha2016.Background.base {W : Type u_1} {T : Type u_2} [LT T] (m : Background) (history : HistoricalAlternatives W T) (s : Reference.Index W T) :
        Set (Reference.Index W T)

        The situations a modal base makes accessible from s, (35), the alternatives at the times its orientations admit.

        Equations
        Instances For
          source
          theorem Klecha2016.Background.base_dox_cir {W : Type u_1} {T : Type u_2} [LT T] (history : HistoricalAlternatives W T) (s : Reference.Index W T) :
          dox.base history s = history.actualHistoryBase s ∧ cir.base history s = history.futureHistoryBase s

          The doxastic base is the substrate's actual-history base and the circumstantial base its future-history base.

          source
          theorem Klecha2016.Background.compare_mem_orientations {W : Type u_1} {T : Type u_2} [LinearOrder T] (m : Background) (history : HistoricalAlternatives W T) {s s' : Reference.Index W T} (h : s' ∈ m.base history s) :
          compare s'.time s.time ∈ m.orientations

          The time of a situation accessible from s bears an admitted orientation to the evaluation time, since Ο„(k|t) is defined only for t within the history k, (53)–(55).

          source
          theorem Klecha2016.Background.orientations_dox :
          dox.orientations = Tense.upperLimitConstraint

          The doxastic modal base admits exactly the orientations the Upper Limit Constraint of [Abu97] allows, so the constraint is derived from the modal base rather than imposed on tense (Β§4.2).

          source
          theorem Klecha2016.Background.upperLimitConstraint_of_mem_dox {W : Type u_1} {T : Type u_2} [LinearOrder T] (history : HistoricalAlternatives W T) {s s' : Reference.Index W T} (h : s' ∈ dox.base history s) :
          compare s'.time s.time ∈ Tense.upperLimitConstraint

          The time of a doxastically accessible situation obeys the Upper Limit Constraint at the evaluation time.

          source
          theorem Klecha2016.Background.cells :
          dox.orientations ∩ Semantics.Denotes.denote Tense.past = Semantics.Denotes.denote Tense.past ∧ dox.orientations ∩ Tense.nonpast = Semantics.Denotes.denote Tense.present ∧ cir.orientations ∩ Tense.nonpast = Semantics.Denotes.denote Tense.future ∧ cir.orientations ∩ Semantics.Denotes.denote Tense.past = βˆ…

          The derivations of Β§3.3 as the four cells of modal base against tense, (43): dox with a past is past, dox with a non-past is simultaneous, (55), cir with a non-past is future, (53), and cir with a past is empty.

          Attitude verbs, Β§3.1 #

          source
          def Klecha2016.modalBases :
          Attitude β†’ Finset Background

          A doxastic verb combines with dox alone and a preferential verb with either modal base, (34).

          Equations
          Instances For
            source
            def Klecha2016.readings (a : Attitude) (Ο„ : Finset Ordering) :
            Finset Ordering

            The orientations open to a clause of underlying tense Ο„ embedded under an attitude of class a are those admitted both by one of the attitude's modal bases and by the tense.

            Equations
            Instances For
              source
              theorem Klecha2016.readings_union (a : Attitude) (τ₁ Ο„β‚‚ : Finset Ordering) :
              readings a (τ₁ βˆͺ Ο„β‚‚) = readings a τ₁ βˆͺ readings a Ο„β‚‚

              A past-under-past clause, whose past morphology is agreement with the matrix tense, has an underlying past or non-past, so its readings are those of past-under-present and present-under-present together, the takeaway of (4)–(7).

              source
              theorem Klecha2016.past_union_nonpast :
              Semantics.Denotes.denote Tense.past βˆͺ Tense.nonpast = Finset.univ
              source
              theorem Klecha2016.think_readings (a : Attitude) :
              a ∈ English.Verbs.think.attitude.toList β†’ readings a Finset.univ = Semantics.Denotes.denote Tense.past βˆͺ Semantics.Denotes.denote Tense.present ∧ readings a Tense.nonpast = Semantics.Denotes.denote Tense.present

              Under think an embedded clause is past or simultaneous, never future, the upper limit, and a present under a present is simultaneous only, which the eventive of (7a) cannot be, (6) and (7).

              source
              theorem Klecha2016.hope_readings (a : Attitude) :
              a ∈ English.Verbs.hope.attitude.toList β†’ readings a Finset.univ = Finset.univ ∧ readings a Tense.nonpast = Tense.nonpast ∧ readings a (Semantics.Denotes.denote Tense.past) = Semantics.Denotes.denote Tense.past

              Under hope every orientation is open to a past-under-past clause, the future one through cir with an underlying non-past, (48)–(54), and a past under a present is past, (4) and (5).

              source
              theorem Klecha2016.matrix_nonpast_present :
              Background.dox.orientations ∩ Tense.nonpast = Semantics.Denotes.denote Tense.present

              The covert epistemic necessity of a matrix clause is a dox modal, so a matrix non-past has present reference only, which rules out (45a) *It rains tomorrow (Β§3.2).

              The data, (1)–(3) #

              source
              def Klecha2016.verbOf :
              String β†’ Option English.Verbs.Verb

              The attitude verb of a row, from the fragment.

              Equations
              Instances For
                source
                def Klecha2016.cells :
                List (String Γ— Finset Ordering)

                The orientation cells a row reports on.

                Equations
                Instances For
                  source
                  theorem Klecha2016.rows_readings (e : Datum) :
                  e ∈ Examples.all β†’ βˆ€ v ∈ (e.feature? "verb" >>= verbOf).toList, βˆ€ a ∈ v.attitude.toList, βˆ€ c ∈ cells, βˆ€ j ∈ (e.feature? c.1).toList, j = "available" ↔ c.2 βŠ† readings a Finset.univ

                  The rows agree with the analysis. An orientation a row reports available under its verb lies among the readings of a past-under-past clause under that verb and one reported unavailable does not, so (2) and (3) are the attested future readings under hope and pray and (1) the upper limit under think.