Perfect Time Span / Until Time Span — Unified Framework

@cite{iatridou-anagnostopoulou-izvorski-2001} @cite{iatridou-zeijlstra-2021} @cite{von-fintel-iatridou-2019}

Boundary adverbials (in years, since, until, in (the last) 5 years) set a boundary of a time span. @cite{iatridou-zeijlstra-2021} unify two classes:

• LB adverbials (in years, since, in (the last) 5 years): set the left boundary of the Perfect Time Span (PTS). The RB is set by Tense.
• RB adverbials (until): set the right boundary of the Until Time Span (UTS). The LB is contextually set.

Both classes can be boundary domain wideners — they introduce subdomain alternatives to their time span, triggering exhaustification. When they are, they produce two noncancelable inferences:

1. Actuality Inference (AI): the relevant event took place
2. Beyond Expectation Inference (BEI): the time span is larger than expected

This module consolidates the PTS/UTS framework that was previously scattered across Aspect/Core.lean (RB, LB, PERF), TemporalAdverbials.lean (PTSConstraint), PerfectPolysemy.lean (PerfectReading), and MaximalInformativity.lean (pts, MeasureFun). It re-exports the core operators and adds the unified boundary-adverbial abstraction.

Architecture

Aspect/Core.lean     RB, LB, PERF, PERF_XN, IMPF, PRFV
        ↑
TemporalAdverbials   PTSConstraint, AdverbialType, PERF_ADV
        ↑
PerfectPolysemy      PerfectReading, existential/universalReading
        ↑
   THIS FILE          BoundaryKind, TimeSpanKind, BoundaryAdverbial
                      SubdomainAlternatives, DomainWideningResult

inductive Semantics.Tense.PTS.BoundaryKind : Type

Which boundary of a time span an adverbial sets.

• left: LB adverbials (in years, since, in (the last) 5 years)
• right: RB adverbials (until)

• left : BoundaryKind
• right : BoundaryKind

instance Semantics.Tense.PTS.instDecidableEqBoundaryKind : DecidableEq BoundaryKind

Equations

• Semantics.Tense.PTS.instDecidableEqBoundaryKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Tense.PTS.instReprBoundaryKind.repr : BoundaryKind → ℕ → Std.Format

Equations

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

instance Semantics.Tense.PTS.instReprBoundaryKind : Repr BoundaryKind

Equations

• Semantics.Tense.PTS.instReprBoundaryKind = { reprPrec := Semantics.Tense.PTS.instReprBoundaryKind.repr }

def Semantics.Tense.PTS.instBEqBoundaryKind.beq : BoundaryKind → BoundaryKind → Bool

Equations

• Semantics.Tense.PTS.instBEqBoundaryKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Tense.PTS.instBEqBoundaryKind : BEq BoundaryKind

Equations

• Semantics.Tense.PTS.instBEqBoundaryKind = { beq := Semantics.Tense.PTS.instBEqBoundaryKind.beq }

inductive Semantics.Tense.PTS.TimeSpanKind : Type

Which time span the adverbial operates on.

• pts: the Perfect Time Span (LB set by adverbial or context, RB by Tense)
• uts: the Until Time Span (LB contextually set, RB by until's argument)

• pts : TimeSpanKind
• uts : TimeSpanKind

instance Semantics.Tense.PTS.instDecidableEqTimeSpanKind : DecidableEq TimeSpanKind

Equations

• Semantics.Tense.PTS.instDecidableEqTimeSpanKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Tense.PTS.instReprTimeSpanKind.repr : TimeSpanKind → ℕ → Std.Format

Equations

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

instance Semantics.Tense.PTS.instReprTimeSpanKind : Repr TimeSpanKind

Equations

• Semantics.Tense.PTS.instReprTimeSpanKind = { reprPrec := Semantics.Tense.PTS.instReprTimeSpanKind.repr }

def Semantics.Tense.PTS.instBEqTimeSpanKind.beq : TimeSpanKind → TimeSpanKind → Bool

Equations

• Semantics.Tense.PTS.instBEqTimeSpanKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Tense.PTS.instBEqTimeSpanKind : BEq TimeSpanKind

Equations

• Semantics.Tense.PTS.instBEqTimeSpanKind = { beq := Semantics.Tense.PTS.instBEqTimeSpanKind.beq }

def Semantics.Tense.PTS.TimeSpanKind.tenseSetsBoundary : TimeSpanKind → BoundaryKind

The boundary set by Tense (not by the adverbial). PTS: Tense sets the RB. UTS: context/Tense sets the LB. Mirror-image relationship (@cite{iatridou-zeijlstra-2021} §8).

Equations

• Semantics.Tense.PTS.TimeSpanKind.pts.tenseSetsBoundary = Semantics.Tense.PTS.BoundaryKind.right
• Semantics.Tense.PTS.TimeSpanKind.uts.tenseSetsBoundary = Semantics.Tense.PTS.BoundaryKind.left

def Semantics.Tense.PTS.TimeSpanKind.adverbialSetsBoundary : TimeSpanKind → BoundaryKind

The boundary set by the adverbial itself. PTS adverbials set LB; UTS adverbials set RB.

Equations

• Semantics.Tense.PTS.TimeSpanKind.pts.adverbialSetsBoundary = Semantics.Tense.PTS.BoundaryKind.left
• Semantics.Tense.PTS.TimeSpanKind.uts.adverbialSetsBoundary = Semantics.Tense.PTS.BoundaryKind.right

theorem Semantics.Tense.PTS.pts_uts_mirror : TimeSpanKind.pts.adverbialSetsBoundary ≠ TimeSpanKind.uts.adverbialSetsBoundary

PTS and UTS are mirror images: they set opposite boundaries.

inductive Semantics.Tense.PTS.NPIStrength : Type

NPI strength classification. Strong NPIs require antiadditive environments; weak NPIs require only DE environments. @cite{zwarts-1998} @cite{gajewski-2011}

• strong : NPIStrength
• weak : NPIStrength
• none_ : NPIStrength

instance Semantics.Tense.PTS.instDecidableEqNPIStrength : DecidableEq NPIStrength

Equations

• Semantics.Tense.PTS.instDecidableEqNPIStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Tense.PTS.instReprNPIStrength : Repr NPIStrength

Equations

• Semantics.Tense.PTS.instReprNPIStrength = { reprPrec := Semantics.Tense.PTS.instReprNPIStrength.repr }

def Semantics.Tense.PTS.instReprNPIStrength.repr : NPIStrength → ℕ → Std.Format

Equations

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

def Semantics.Tense.PTS.instBEqNPIStrength.beq : NPIStrength → NPIStrength → Bool

Equations

• Semantics.Tense.PTS.instBEqNPIStrength.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Tense.PTS.instBEqNPIStrength : BEq NPIStrength

Equations

• Semantics.Tense.PTS.instBEqNPIStrength = { beq := Semantics.Tense.PTS.instBEqNPIStrength.beq }

structure Semantics.Tense.PTS.BoundaryAdverbial : Type

A boundary adverbial: a temporal expression that sets one boundary of a time span (PTS or UTS).

@cite{iatridou-zeijlstra-2021} §3, §5: in years and until are both boundary adverbials that share the property of being domain wideners (introducing subdomain alternatives).

• form : String

  Surface form

• timeSpan : TimeSpanKind

  Which time span this adverbial operates on

• boundary : BoundaryKind

  Which boundary it sets

• introducesDomainAlts : Bool

  Does this adverbial introduce subdomain alternatives?

• npiStrength : NPIStrength

  Is this adverbial a (strong) NPI?

• alwaysContrastive : Bool

  Is the adverbial always contrastively focused? @cite{chierchia-2013}: domain widening requires contrastive focus under negation. In years is always contrastively focused; until is contrastively focused only when under negation.

• compatiblePerfect : List PerfectPolysemy.PerfectReading

  Compatible perfect types (for PTS adverbials). In years is compatible only with E-perfect; in (the last) 5 years is compatible with both E-perfect and U-perfect.

instance Semantics.Tense.PTS.instReprBoundaryAdverbial : Repr BoundaryAdverbial

Equations

• Semantics.Tense.PTS.instReprBoundaryAdverbial = { reprPrec := Semantics.Tense.PTS.instReprBoundaryAdverbial.repr }

def Semantics.Tense.PTS.instReprBoundaryAdverbial.repr : BoundaryAdverbial → ℕ → Std.Format

Equations

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

def Semantics.Tense.PTS.inYears : BoundaryAdverbial

In years (in days, in months, etc.): strong NPI LB adverbial. Sets the LB of the PTS by stretching backward from the RB. Introduces subdomain alternatives. Always contrastively focused. Compatible only with E-perfect (not U-perfect). @cite{iatridou-zeijlstra-2021} §3–4

Equations

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

def Semantics.Tense.PTS.inTheLast5Years : BoundaryAdverbial

In (the last) 5 years: non-NPI LB adverbial. Sets the LB of the PTS by specifying a duration from the RB. Does NOT introduce domain alternatives (not a domain widener). Compatible with both E-perfect and U-perfect.

Equations

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

def Semantics.Tense.PTS.since2015 : BoundaryAdverbial

Since 2015: non-NPI LB adverbial. Sets the LB of the PTS by naming it. Does NOT introduce domain alternatives.

Equations

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

def Semantics.Tense.PTS.until_ : BoundaryAdverbial

Until (5pm / I left): unified RB adverbial. Sets the RB of the UTS. Always introduces subdomain alternatives (the domain-widening effect surfaces only under contrastive focus). @cite{iatridou-zeijlstra-2021} §7: one until, not two.

Equations

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

theorem Semantics.Tense.PTS.inYears_sets_lb : inYears.boundary = TimeSpanKind.pts.adverbialSetsBoundary

In years sets the LB (matching PTS).

theorem Semantics.Tense.PTS.until_sets_rb : until_.boundary = TimeSpanKind.uts.adverbialSetsBoundary

Until sets the RB (matching UTS).

theorem Semantics.Tense.PTS.both_domain_wideners : inYears.introducesDomainAlts = true ∧ until_.introducesDomainAlts = true

In years and until are both domain wideners.

theorem Semantics.Tense.PTS.both_strong_npis : inYears.npiStrength = NPIStrength.strong ∧ until_.npiStrength = NPIStrength.strong

In years and until are both strong NPIs.

theorem Semantics.Tense.PTS.contrastive_asymmetry : inYears.alwaysContrastive = true ∧ until_.alwaysContrastive = false

In years is always contrastive; until is not.

theorem Semantics.Tense.PTS.inYears_eperfect_only : PerfectPolysemy.PerfectReading.universal ∉ inYears.compatiblePerfect ∧ PerfectPolysemy.PerfectReading.universal ∈ inTheLast5Years.compatiblePerfect

In years is E-perfect only; in (the last) 5 years allows both.

theorem Semantics.Tense.PTS.nonNPI_no_domainAlts : since2015.introducesDomainAlts = false ∧ inTheLast5Years.introducesDomainAlts = false

Non-NPI boundary adverbials do not introduce domain alternatives.

def Semantics.Tense.PTS.SubdomainAlternatives {Time : Type u_2} [LinearOrder Time] (τ : Core.Time.Interval Time) : Set (Core.Time.Interval Time)

The subdomain alternatives of a time span τ are all subintervals of τ. @cite{chierchia-2013} Ch. 1; @cite{iatridou-zeijlstra-2021} §4:

When in years is present, the assertion (49a) is: ∃e.[meet(e, Joe, Mary) ∧ Run(e) ⊆ τ] and its domain alternatives (49b) are: {∃e.[meet(e, Joe, Mary) ∧ Run(e) ⊆ τ'] | τ' ⊆ τ}

These subdomain alternatives are logically stronger than the assertion (entailed by it), because if a culminated event took place in a subinterval of τ, it also took place in τ.

Equations

• Semantics.Tense.PTS.SubdomainAlternatives τ = {τ' : Core.Time.Interval Time | τ'.subinterval τ}

theorem Semantics.Tense.PTS.self_in_subdomain {Time : Type u_2} [LinearOrder Time] (τ : Core.Time.Interval Time) : τ ∈ SubdomainAlternatives τ

Subdomain alternatives of τ include τ itself.

theorem Semantics.Tense.PTS.subdomain_monotone {Time : Type u_2} [LinearOrder Time] (τ₁ τ₂ : Core.Time.Interval Time) (h : τ₁.subinterval τ₂) : SubdomainAlternatives τ₁ ⊆ SubdomainAlternatives τ₂

Subdomain alternatives of a subinterval are a subset of subdomain alternatives of the superinterval.

def Semantics.Tense.PTS.eventInSpan {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Aspect.Core.EventPred W Time) (w : W) (τ : Core.Time.Interval Time) : Prop

An event of type P has its runtime inside time span τ. This is the assertion form for both PTS and UTS: ∃e.[P(e) ∧ Run(e) ⊆ τ]

Equations

• Semantics.Tense.PTS.eventInSpan P w τ = ∃ (e : Semantics.Tense.Aspect.Core.Eventuality Time), e.τ.subinterval τ ∧ P w e

def Semantics.Tense.PTS.noEventInSpan {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Aspect.Core.EventPred W Time) (w : W) (τ : Core.Time.Interval Time) : Prop

Negated form: no P-event has runtime inside τ. ¬∃e.[P(e) ∧ Run(e) ⊆ τ]

Equations

• Semantics.Tense.PTS.noEventInSpan P w τ = ¬Semantics.Tense.PTS.eventInSpan P w τ

theorem Semantics.Tense.PTS.eventInSpan_monotone {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Aspect.Core.EventPred W Time) (w : W) (τ₁ τ₂ : Core.Time.Interval Time) (h : τ₁.subinterval τ₂) : eventInSpan P w τ₁ → eventInSpan P w τ₂

If a culminated event occurs in a subinterval, it occurs in the superinterval. Entailment from subinterval to superinterval.

theorem Semantics.Tense.PTS.subdomain_alts_nonweaker {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Aspect.Core.EventPred W Time) (w : W) (τ τ' : Core.Time.Interval Time) (h : τ' ∈ SubdomainAlternatives τ) : eventInSpan P w τ' → eventInSpan P w τ

Subdomain alternatives for culminated events are all nonweaker: every subdomain alternative entails the assertion. This is because eventInSpan is monotone in the time span.

theorem Semantics.Tense.PTS.positive_exhaustification_contradicts {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Aspect.Core.EventPred W Time) (w : W) (τ : Core.Time.Interval Time) (_hassert : eventInSpan P w τ) (hexh : ∀ τ' ∈ SubdomainAlternatives τ, τ' ≠ τ → noEventInSpan P w τ') (τ_sub : Core.Time.Interval Time) : τ_sub.subinterval τ → τ_sub ≠ τ → eventInSpan P w τ_sub → False

Positive environment contradiction (@cite{iatridou-zeijlstra-2021} §4): In a positive (non-DE) context, exhaustification of subdomain alternatives requires negating all nonweaker alternatives. But ALL subdomain alternatives are entailed by the assertion (by subdomain_alts_nonweaker). Negating them contradicts the assertion → logical contradiction → ungrammaticality.

This explains why in years is an NPI: "*Joe has met Mary in weeks" is ungrammatical because exhaustification of the domain alternatives in a positive context yields contradiction.

theorem Semantics.Tense.PTS.negated_subdomain_weaker {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Aspect.Core.EventPred W Time) (w : W) (τ τ' : Core.Time.Interval Time) (h : τ'.subinterval τ) : noEventInSpan P w τ → noEventInSpan P w τ'

Negative environment: exhaustification is vacuous. Under negation, subdomain alternatives ¬∃e.[P(e) ∧ Run(e) ⊆ τ'] are WEAKER than the assertion ¬∃e.[P(e) ∧ Run(e) ⊆ τ] (for τ' ⊆ τ). Since no subdomain alternative is stronger, there is nothing to exclude, and exhaustification applies vacuously. No contradiction arises.

def Semantics.Tense.PTS.actualityInference {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Aspect.Core.EventPred W Time) (w : W) (τ : Core.Time.Interval Time) : Prop

Actuality Inference (@cite{iatridou-zeijlstra-2021} §4): With in years, the LB of the PTS can only be set at the point where an event of the relevant sort took place (since in years stretches backward from the RB until it finds such an event). Therefore, the existence of the event is presupposed — it is the only thing that can define the LB.

Formally: if the LB is set by a domain-widening boundary adverbial that stretches as far as possible, the LB must be at the most recent occurrence of the event. This makes the event's occurrence a presupposition, not just an implicature — hence noncancelable.

Equations

• Semantics.Tense.PTS.actualityInference P w τ = Semantics.Tense.PTS.eventInSpan P w τ

def Semantics.Tense.PTS.aiAtBoundary {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Aspect.Core.EventPred W Time) (w : W) (τ : Core.Time.Interval Time) : Prop

The AI with in years is at the LB: the event occurs at the LB point.

Equations

• Semantics.Tense.PTS.aiAtBoundary P w τ = ∃ (e : Semantics.Tense.Aspect.Core.Eventuality Time), e.τ.finish = τ.start ∧ P w e

structure Semantics.Tense.PTS.BeyondExpectationInference {Time : Type u_2} [LinearOrder Time] : Type u_2

Beyond Expectation Inference (@cite{iatridou-zeijlstra-2021} §2): In years conveys that the PTS is larger than a contextually salient alternative. "He hasn't had a seizure in months" conveys the PTS is larger than a contextually salient number of months.

This follows from domain widening: the time span is stretched beyond any contextual alternative, so the event occurred earlier than expected.

• actualSpan : Core.Time.Interval Time

  The actual time span

• expectedBound : Core.Time.Interval Time

  The contextually expected upper bound on the time span

• beyondExpectation : self.expectedBound.subinterval self.actualSpan

  The actual span is larger (the event is earlier than expected)

• strict : self.expectedBound ≠ self.actualSpan

  The spans are not equal (the actual is strictly larger)

def Semantics.Tense.PTS.perfectiveContainment {Time : Type u_2} [LinearOrder Time] (e : Aspect.Core.Eventuality Time) (τ : Core.Time.Interval Time) : Prop

Perfective contributes ST ⊆ TT: the event is contained in the time span. @cite{iatridou-zeijlstra-2021} §1 (eq. 17a), following @cite{klein-1994}. Equivalently, the E-perfect: the event is contained in the PTS.

Equations

• Semantics.Tense.PTS.perfectiveContainment e τ = e.τ.subinterval τ

def Semantics.Tense.PTS.imperfectiveContainment {Time : Type u_2} [LinearOrder Time] (e : Aspect.Core.Eventuality Time) (τ : Core.Time.Interval Time) : Prop

Imperfective contributes TT ⊆ ST: the time span is contained in the event. @cite{iatridou-zeijlstra-2021} §1 (eq. 17b). With the subinterval property, every subinterval of a P-event is also a P-event. This is the key to until-d (affirmative imperfective).

Equations

• Semantics.Tense.PTS.imperfectiveContainment e τ = τ.subinterval e.τ

theorem Semantics.Tense.PTS.impf_subdomain_entailed {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : Aspect.Core.EventPred W Time) (hSub : Aspect.SubintervalProperty.HasSubintervalProp P) (w : W) (e : Aspect.Core.Eventuality Time) (τ : Core.Time.Interval Time) (hP : P w e) (hImpf : τ.subinterval e.τ) (τ' : Core.Time.Interval Time) (hτ' : τ'.subinterval τ) : eventInSpan P w τ'

Under IMPF + subinterval property, all subdomain alternatives of the assertion are ENTAILED (not merely nonweaker). This means exhaustification is vacuous for affirmative imperfectives — explaining why until-d (affirmative imperfective + until) is fine without negation. @cite{iatridou-zeijlstra-2021} §7.2

theorem Semantics.Tense.PTS.constants_observation : inYears.introducesDomainAlts = true ∧ inTheLast5Years.introducesDomainAlts = false

Constant's Observation (@cite{iatridou-zeijlstra-2021} §1): The AI of in years is noncancelable, unlike the AI of in (the last) 5 years.

(22a) "He hasn't had a seizure in years." ... #In fact, he has never had one. [noncancelable]

vs.

(11b) "She hasn't had one in the last 5 years." ... I don't know about earlier. [cancelable]

This follows from domain widening: in years stretches the PTS maximally, so the LB can only be set by a prior event occurrence. In (the last) 5 years fixes the LB independently (by counting backward), so the event occurrence is merely implicated, not presupposed.

def Semantics.Tense.PTS.isDomainWidener (adv : BoundaryAdverbial) : Bool

A BoundaryAdverbial that is a domain widener is predicted to be a strong NPI (not weak). This is because domain widening operates on presupposed content (the PTS/UTS existence), and strong NPIs are those whose exhaustifier accesses non-truth-conditional content. @cite{iatridou-zeijlstra-2021} §11

Equations

• Semantics.Tense.PTS.isDomainWidener adv = adv.introducesDomainAlts

theorem Semantics.Tense.PTS.domain_widener_is_strong_npi : (isDomainWidener inYears = true ∧ inYears.npiStrength = NPIStrength.strong) ∧ isDomainWidener until_ = true ∧ until_.npiStrength = NPIStrength.strong

Domain wideners among boundary adverbials are strong NPIs.

theorem Semantics.Tense.PTS.non_widener_not_npi : (isDomainWidener since2015 = false ∧ since2015.npiStrength = NPIStrength.none_) ∧ isDomainWidener inTheLast5Years = false ∧ inTheLast5Years.npiStrength = NPIStrength.none_

Non-widener boundary adverbials are not NPIs.