Documentation

Linglib.Theories.Semantics.Tense.TemporalConnectives.Giannakidou

Viewpoint Aspect × Temporal Connective Interaction #

@cite{giannakidou-2002} @cite{karttunen-1974} @cite{klein-1994} @cite{mittwoch-1977}@cite{giannakidou-2002} shows that viewpoint aspect determines negation scope with until:

Architecture #

This file bridges ViewpointAspect operators (IMPF, PRFV) into the temporal connective layer by projecting EventPred through viewpoint aspect to SentDenotation:

EventPred Unit Time ──[impfDenotation]──▷ SentDenotation Time (homogeneous)
EventPred Unit Time ──[prfvDenotation]──▷ SentDenotation Time (quantized)

The world parameter is fixed to Unit: temporal connectives are world-independent (purely temporal structure).

Key Results #

  1. impfDenotation_subinterval_closed: IMPF gives homogeneity
  2. prfvDenotation_not_subinterval_closed: PRFV does not
  3. scope_readings_distinct: wide-scope and narrow-scope ¬until differ
source
def Semantics.Tense.TemporalConnectives.impfDenotation {Time : Type u_1} [LinearOrder Time] (P : Aspect.Core.EventPred Unit Time) :
SentDenotation Time

Project an event predicate to a sentence denotation via imperfective aspect. The result is homogeneous: for each event satisfying P, the denotation includes all subintervals of the event runtime.

This captures @cite{klein-1994}'s IMPF: the reference time (TT) is properly inside the situation time (TSit), so the event extends beyond any particular reference point. Every subinterval of the event runtime is a valid reference window into the ongoing event.

World parameter fixed to Unit: temporal connectives are world-independent.

Equations
Instances For
    source
    def Semantics.Tense.TemporalConnectives.prfvDenotation {Time : Type u_1} [LinearOrder Time] (P : Aspect.Core.EventPred Unit Time) :
    SentDenotation Time

    Project an event predicate to a sentence denotation via perfective aspect. The result is quantized: only the exact event runtime is included.

    This captures @cite{klein-1994}'s PRFV: the situation time (TSit) is contained in the reference time (TT), so the event is viewed as complete. The denotation contains only the event's actual runtime — the bounded interval during which the event occurred.

    Equations
    Instances For
      source
      theorem Semantics.Tense.TemporalConnectives.impfDenotation_subinterval_closed {Time : Type u_1} [LinearOrder Time] (P : Aspect.Core.EventPred Unit Time) (t : Core.Time.Interval Time) (ht : t ∈ impfDenotation P) (t' : Core.Time.Interval Time) (ht' : t'.subinterval t) :
      t' ∈ impfDenotation P

      IMPF denotation satisfies the subinterval property: if interval t is in the denotation (i.e., t ⊆ τ(e) for some event e), then every subinterval of t is also in the denotation.

      This is exactly the homogeneity property that @cite{karttunen-1974} requires of the main clause of durative until. The imperfective viewpoint provides this automatically: since the event extends beyond any reference interval, every sub-window into the event is equally valid.

      source
      theorem Semantics.Tense.TemporalConnectives.impfDenotation_contains_runtime {Time : Type u_1} [LinearOrder Time] (P : Aspect.Core.EventPred Unit Time) (e : Aspect.Core.Eventuality Time) (hP : P () e) :
      e.τ ∈ impfDenotation P

      IMPF denotation contains the event runtime itself (the maximal interval). Every event satisfying P contributes its runtime to the denotation.

      source
      theorem Semantics.Tense.TemporalConnectives.prfvDenotation_not_subinterval_closed :
      ¬∀ (P : Aspect.Core.EventPred Unit ℤ), ∀ t ∈ prfvDenotation P, ∀ (t' : Core.Time.Interval ℤ), t'.subinterval t → t' ∈ prfvDenotation P

      PRFV denotation does NOT have the subinterval property.

      Counterexample: An event with runtime [0, 5]. The interval [0, 5] is in the denotation, but [1, 3] (a strict subinterval) is not — PRFV only includes the exact runtime.

      This is why perfective clauses cannot be main clauses of durative until: they lack the homogeneity that until requires.

      source
      theorem Semantics.Tense.TemporalConnectives.impfDenotation_singleton_eq_stativeDenotation {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) :
      (impfDenotation fun (x : Unit) (e : Aspect.Core.Eventuality Time) => e.τ = i) = stativeDenotation i

      For a single event with runtime i, the IMPF denotation is exactly the stative denotation of i (all subintervals). This connects the ViewpointAspect bridge to the existing temporal connective infrastructure in Basic.lean.

      source
      theorem Semantics.Tense.TemporalConnectives.prfvDenotation_singleton_eq_accomplishmentDenotation {Time : Type u_1} [LinearOrder Time] (i : Core.Time.Interval Time) :
      (prfvDenotation fun (x : Unit) (e : Aspect.Core.Eventuality Time) => e.τ = i) = accomplishmentDenotation i

      For a single event, the PRFV denotation is exactly the accomplishment denotation (singleton containing just the runtime).

      source
      theorem Semantics.Tense.TemporalConnectives.timeTrace_impf_eq_prfv {Time : Type u_1} [LinearOrder Time] (P : Aspect.Core.EventPred Unit Time) :
      timeTrace (impfDenotation P) = timeTrace (prfvDenotation P)

      The time traces of IMPF and PRFV denotations are identical: both equal the set of times contained in some event runtime.

      This is why Karttunen's Level 1 (point-set) definitions cannot distinguish imperfective from perfective clauses — the difference is only visible at Level 2 (interval sets). Giannakidou's scope analysis requires the Level 2 distinction.

      source
      def Semantics.Tense.TemporalConnectives.wideScopeNotUntil {Time : Type u_1} [LinearOrder Time] (A : Aspect.Core.EventPred Unit Time) (B : SentDenotation Time) :
      Prop

      Wide-scope negation over imperfective until:

      ¬∃t [t ∈ timeTrace(IMPF(A)) ∧ t ∈ timeTrace(B)]

      "It's not the case that A was ongoing up to the time of B."

      Available when A is imperfective: the main clause denotes a homogeneous interval set via IMPF, so until can take it as an argument. Negation scopes over the entire until-clause.

      Equations
      Instances For
        source
        def Semantics.Tense.TemporalConnectives.narrowScopeNotUntil {Time : Type u_1} [LinearOrder Time] (A : Aspect.Core.EventPred Unit Time) (B : SentDenotation Time) :
        Prop

        Narrow-scope negation under until (= Karttunen's ¬before):

        ¬(A BEFORE B)

        "A didn't happen before B" — the event occurred, but not prior to B.

        This is the only reading available with perfective main clauses: since PRFV gives a bounded event, until reduces to temporal ordering and negation gives Karttunen's notUntil = ¬before.

        Equations
        Instances For
          source
          theorem Semantics.Tense.TemporalConnectives.narrowScope_eq_not_before {Time : Type u_1} [LinearOrder Time] (A : Aspect.Core.EventPred Unit Time) (B : SentDenotation Time) :
          narrowScopeNotUntil A B ↔ ¬Anscombe.before (prfvDenotation A) B

          Narrow-scope ¬until is exactly ¬before (by definition). This is @cite{karttunen-1974}'s identity, now made explicit in the aspectual decomposition.

          source
          theorem Semantics.Tense.TemporalConnectives.scope_readings_distinct :
          ∃ (A : Aspect.Core.EventPred Unit ℤ) (B : SentDenotation ℤ), wideScopeNotUntil A B ∧ ¬narrowScopeNotUntil A B

          The two scope readings are semantically distinct: there exist A, B where wide-scope holds but narrow-scope fails.

          Counterexample: event A with runtime [0, 5], B at time 7.

          • Wide scope: ¬(any A-time overlaps with time 7). TRUE — 7 ∉ [0, 5].
          • Narrow scope: ¬(A happened before B). FALSE — time 0 < 7, so A precedes B and Anscombe.before holds.

          Intuitively: the sleeping event [0, 5] ended before time 7. The wide-scope reading says "sleeping didn't extend to 7" (true). The narrow-scope reading says "sleeping didn't happen before 7" (false — it did).

          source
          theorem Semantics.Tense.TemporalConnectives.scope_readings_independent :
          ∃ (A : Aspect.Core.EventPred Unit ℤ) (B : SentDenotation ℤ), ¬wideScopeNotUntil A B ∧ narrowScopeNotUntil A B

          The reverse also holds: there exist A, B where narrow-scope holds but wide-scope fails. This confirms the two readings are genuinely independent.

          Counterexample: event A with runtime [5, 10], B over [3, 7].

          • Wide scope: ¬(any A-time overlaps with B). FALSE — time 5 is in both.
          • Narrow scope: ¬(A before B). TRUE — no A-time (≥ 5) precedes ALL B-times (which include 3).
          source
          structure Semantics.Tense.TemporalConnectives.ScopeGeneralization :
          Type

          @cite{giannakidou-2002}'s generalization about viewpoint aspect and scope. This is an empirical generalization, not a logical entailment — it describes which readings are available in natural language, not which are logically possible.

          The formalization above proves that the two scope readings are logically independent (§6), confirming that the restriction to narrow scope under PRFV is a genuine constraint, not a logical consequence.

          • viewpoint : Aspect.Core.ViewpointType

            Viewpoint aspect of the main clause

          • wideScopeAvailable : Bool

            Is wide-scope negation available?

          • narrowScopeAvailable : Bool

            Is narrow-scope negation available?

          Instances For
            source
            instance Semantics.Tense.TemporalConnectives.instReprScopeGeneralization :
            Repr ScopeGeneralization
            Equations
            source
            def Semantics.Tense.TemporalConnectives.instReprScopeGeneralization.repr :
            ScopeGeneralization → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Semantics.Tense.TemporalConnectives.impfScope :
              ScopeGeneralization

              Imperfective main clause: both scope readings available.

              Equations
              Instances For
                source
                def Semantics.Tense.TemporalConnectives.prfvScope :
                ScopeGeneralization

                Perfective main clause: only narrow scope available.

                Equations
                Instances For
                  source
                  theorem Semantics.Tense.TemporalConnectives.giannakidou_scope_pattern :
                  impfScope.wideScopeAvailable = true ∧ impfScope.narrowScopeAvailable = true ∧ prfvScope.wideScopeAvailable = false ∧ prfvScope.narrowScopeAvailable = true

                  Giannakidou's generalization: perfective blocks wide-scope negation; narrow-scope is always available.

                  source
                  theorem Semantics.Tense.TemporalConnectives.wideScopeAvailable_iff_imperfective (sg : ScopeGeneralization) (h : sg = impfScope ∨ sg = prfvScope) :
                  sg.wideScopeAvailable = true ↔ sg.viewpoint = Aspect.Core.ViewpointType.imperfective

                  The availability of wide scope correlates with homogeneity: imperfective → homogeneous → wide scope available; perfective → not homogeneous → wide scope blocked.

                  This is the bridge between the data (§7) and the theory (§§1-2): IMPF gives homogeneity (§2), homogeneity enables durative until, and durative until enables wide-scope negation.