Documentation

Linglib.Theories.Semantics.Modality.TemporalConstraint

Modal Base Temporal Constraints #

@cite{klecha-2016}

Klecha-namespace dispatch on ModalBaseKind for the temporal constraints that fall out of @cite{klecha-2016}'s modal-base-pronoun architecture, plus bridges from Attitude / ModalFlavor to ModalBaseKind.

The framework-neutral interval predicates (isActualHistory, isFutureHistory, etc.) and the situation-base derivation theorems live in Core.Modality.HistoricalAlternatives. This file's role is the Klecha-specific projection: dispatch on ModalBaseKind to select between the actual-history (RT ≤ EvalT) and future-history (RT > EvalT) constraints.

Klecha's key insight: the temporal orientation of a modal is determined by the temporal structure of its accessible histories, which is encoded in the modal base pronoun:

The ULC is derived by .2 projection from actualHistoryBase membership (see actualHistoryBase_derives_ulc in Core.Modality.HistoricalAlternatives); the dispatch theorem attitudeTemporalConstraint_derived_doxastic below makes the Klecha-namespace face of that derivation kernel-checked.

Temporal Constraints on Embedded RT #

source
def Semantics.Modality.TemporalConstraint.doxConstrainsRT {Time : Type u_1} [LE Time] (evalTime refTime : Time) :
Prop

Doxastic temporal constraint: embedded reference time must be an actual time relative to the modal's evaluation time (RT ≤ EvalT).

This is the compositional source of the Upper Limit Constraint. @cite{klecha-2016} derives it from DOX's temporal character: since DOX returns actual histories (ending at t), the embedded event must be located within that interval.

Equations
Instances For
    source
    def Semantics.Modality.TemporalConstraint.cirConstrainsRT {Time : Type u_1} [LT Time] (evalTime refTime : Time) :
    Prop

    Circumstantial temporal constraint: embedded reference time must be a future time relative to the modal's evaluation time (RT > EvalT).

    This is what permits future-oriented readings under hope, pray, and circumstantial/teleological/deontic modals. @cite{klecha-2016} derives it from CIR's temporal character: since CIR returns future histories (departing from t), the embedded event must be located after that time.

    Equations
    Instances For
      source
      theorem Semantics.Modality.TemporalConstraint.dox_is_upper_limit {Time : Type u_1} [LE Time] (evalTime refTime : Time) :
      doxConstrainsRT evalTime refTime ↔ refTime ≤ evalTime

      The doxastic constraint IS the upper limit: RT ≤ EvalT.

      source
      theorem Semantics.Modality.TemporalConstraint.cir_permits_future_ref {Time : Type u_1} [LinearOrder Time] (evalTime refTime : Time) (h : cirConstrainsRT evalTime refTime) :
      ¬refTime ≤ evalTime

      The circumstantial constraint permits future reference: RT > EvalT.

      source
      def Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint {Time : Type u_1} [LinearOrder Time] (kind : Core.Modality.ModalBaseKind) (evalTime refTime : Time) :
      Prop

      Attitude verbs compatible with DOX impose an upper limit; those compatible with CIR do not. This is Klecha's central result: the temporal constraint varies with the modal base, not the attitude verb per se.

      think → DOX only → upper limit hope → CIR (or DOX) → no upper limit with CIR

      Equations
      Instances For
        source
        theorem Semantics.Modality.TemporalConstraint.dox_compatible_with_past {Time : Type u_1} [LinearOrder Time] (evalTime refTime : Time) (hPast : refTime < evalTime) :
        attitudeTemporalConstraint Core.Modality.ModalBaseKind.doxastic evalTime refTime

        Under DOX, past tense is compatible (RT < EvalT → RT ≤ EvalT).

        source
        theorem Semantics.Modality.TemporalConstraint.dox_incompatible_with_future {Time : Type u_1} [LinearOrder Time] (evalTime refTime : Time) (hFut : refTime > evalTime) :
        ¬attitudeTemporalConstraint Core.Modality.ModalBaseKind.doxastic evalTime refTime

        Under DOX, future tense is incompatible (RT > EvalT → ¬ RT ≤ EvalT).

        source
        theorem Semantics.Modality.TemporalConstraint.cir_compatible_with_future {Time : Type u_1} [LinearOrder Time] (evalTime refTime : Time) (hFut : refTime > evalTime) :
        attitudeTemporalConstraint Core.Modality.ModalBaseKind.circumstantial evalTime refTime

        Under CIR, future tense is compatible (RT > EvalT).

        Klecha 2016: constraint as derivation, not stipulation #

        The two theorems below make @cite{klecha-2016}'s central architectural claim kernel-checked: attitudeTemporalConstraint is derived from membership in the corresponding situation-base (actualHistoryBase for DOX, futureHistoryBase for CIR), not stipulated.

        This is the formal contrast with @cite{abusch-1997}'s ULC, which is stipulated as a presupposition on T-nodes; here, ULC follows by .2 projection through the situation-base definition. The substrate derivation lives in Core.Modality.HistoricalAlternatives as actualHistoryBase_time_actual / futureHistoryBase_time_future; these theorems re-express it in the Klecha-namespace attitudeTemporalConstraint form.

        source
        theorem Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint_derived_doxastic {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (s s' : Core.WorldTimeIndex W Time) (h : s' ∈ Core.Modality.HistoricalAlternatives.actualHistoryBase history s) :
        attitudeTemporalConstraint Core.Modality.ModalBaseKind.doxastic s.time s'.time

        @cite{klecha-2016} eq (35a): DOX returns the actual history base. Membership in actualHistoryBase derives the doxastic temporal constraint (Upper Limit Constraint) by .2 projection.

        source
        theorem Semantics.Modality.TemporalConstraint.attitudeTemporalConstraint_derived_circumstantial {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (history : Core.Modality.HistoricalAlternatives.WorldHistory W Time) (s s' : Core.WorldTimeIndex W Time) (h : s' ∈ Core.Modality.HistoricalAlternatives.futureHistoryBase history s) :
        attitudeTemporalConstraint Core.Modality.ModalBaseKind.circumstantial s.time s'.time

        @cite{klecha-2016} eq (35b): CIR returns the future history base. Membership in futureHistoryBase derives the circumstantial temporal constraint (future orientation) by .2 projection.

        Attitude → ModalBaseKind bridge #

        source
        def Semantics.Modality.TemporalConstraint.Attitude.toModalBaseKind :
        Features.Attitude → Core.Modality.ModalBaseKind

        Derive ModalBaseKind from Attitude classification. @cite{klecha-2016}: doxastic attitudes select DOX, preferential attitudes select CIR. The derived kind determines temporal orientation.

        Note: preferential attitudes CAN also take DOX (e.g., "I hope she already left" = DOX → past reading). This function returns the kind that distinguishes them: the kind that PERMITS future orientation.

        Equations
        Instances For
          source
          theorem Semantics.Modality.TemporalConstraint.doxastic_selects_dox (v : Features.Veridicality) :
          Attitude.toModalBaseKind (Features.Attitude.doxastic v) = Core.Modality.ModalBaseKind.doxastic

          Doxastic attitudes select DOX.

          source
          theorem Semantics.Modality.TemporalConstraint.preferential_selects_cir (k : Features.Preferential) :
          Attitude.toModalBaseKind (Features.Attitude.preferential k) = Core.Modality.ModalBaseKind.circumstantial

          Preferential attitudes select CIR (= can access future histories).

          source
          theorem Semantics.Modality.TemporalConstraint.permitsCirc_iff_cir (a : Features.Attitude) :
          a.PermitsCircumstantial ↔ Attitude.toModalBaseKind a = Core.Modality.ModalBaseKind.circumstantial

          PermitsCircumstantial ↔ toModalBaseKind = .circumstantial.

          ModalFlavor → ModalBaseKind bridge #

          @cite{klecha-2016} Table 1: the temporal orientation of a modal correlates with its flavor. Epistemic modals are past/present-oriented (DOX-like); circumstantial, deontic, bouletic, and teleological modals are future-oriented (CIR-like). This function bridges the four-way ModalFlavor classification (from Core.Modality) to Klecha's binary ModalBaseKind.

          source
          def Semantics.Modality.TemporalConstraint.ModalFlavor.toModalBaseKind :
          Core.Modality.ModalFlavor → Core.Modality.ModalBaseKind

          Map modal flavor to modal base kind. Epistemic → DOX (past/present orientation). Circumstantial, deontic, bouletic → CIR (future orientation).

          Equations
          Instances For
            source
            theorem Semantics.Modality.TemporalConstraint.epistemic_is_dox :
            ModalFlavor.toModalBaseKind Core.Modality.ModalFlavor.epistemic = Core.Modality.ModalBaseKind.doxastic

            Epistemic modals are DOX-like.

            source
            theorem Semantics.Modality.TemporalConstraint.circumstantial_is_cir :
            ModalFlavor.toModalBaseKind Core.Modality.ModalFlavor.circumstantial = Core.Modality.ModalBaseKind.circumstantial

            Circumstantial modals are CIR-like.

            source
            theorem Semantics.Modality.TemporalConstraint.deontic_is_cir :
            ModalFlavor.toModalBaseKind Core.Modality.ModalFlavor.deontic = Core.Modality.ModalBaseKind.circumstantial

            Deontic modals are CIR-like.

            source
            theorem Semantics.Modality.TemporalConstraint.bouletic_is_cir :
            ModalFlavor.toModalBaseKind Core.Modality.ModalFlavor.bouletic = Core.Modality.ModalBaseKind.circumstantial

            Bouletic modals are CIR-like.

            source
            theorem Semantics.Modality.TemporalConstraint.epistemic_blocks_future :
            (ModalFlavor.toModalBaseKind Core.Modality.ModalFlavor.epistemic).permitsOrientation Core.Time.Tense.GramTense.future = false

            Table 1 consequence: epistemic modals block future orientation.

            source
            theorem Semantics.Modality.TemporalConstraint.circumstantial_permits_future :
            (ModalFlavor.toModalBaseKind Core.Modality.ModalFlavor.circumstantial).permitsOrientation Core.Time.Tense.GramTense.future = true

            Table 1 consequence: circumstantial modals permit future orientation.

            source
            theorem Semantics.Modality.TemporalConstraint.deontic_permits_future :
            (ModalFlavor.toModalBaseKind Core.Modality.ModalFlavor.deontic).permitsOrientation Core.Time.Tense.GramTense.future = true

            Table 1 consequence: deontic modals permit future orientation.

            source
            theorem Semantics.Modality.TemporalConstraint.non_epistemic_is_cir (f : Core.Modality.ModalFlavor) (h : f ≠ Core.Modality.ModalFlavor.epistemic) :
            ModalFlavor.toModalBaseKind f = Core.Modality.ModalBaseKind.circumstantial

            All non-epistemic flavors map to CIR.