[IZ21]: The complex beauty of boundary adverbials: in years and until

[IZ21] [IAI01] [Kip02]

Iatridou & Zeijlstra (Linguistic Inquiry 52(1), 2021) unify two classes of boundary adverbials:

• LB adverbials (in years, since, in (the last) 5 years): set the left boundary of the Perfect Time Span (PTS), with RB set by Tense.
• RB adverbials (until): set the right boundary of the Until Time Span (UTS), with LB 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

The PTS framework (LB / RB / PTS terminology) is from [IAI01]; UTS, AI/BEI, and the NPI-status analysis of in years / until are this paper's contribution. The substrate below extends IAI 2001's PTS with the IZ 2021 machinery.

Status

Substrate inherited from Semantics/Tense/PTS.lean (deleted; relocated here per CLAUDE.md graduation rule). Verified against the IZ 2021 PDF: the abbreviation table (PTS, UTS, LB, RB, AI, BEI, NPI) confirms the terminology; the "in years / until unification" is the paper's central claim; domain widener appears 15+ times in the text. The Lean encoding of the NPI strength classification and the exhaustification machinery is faithful to the paper's analytical framework but has not been line-by-line cross-checked against IZ 2021's specific theorems.

inductive IatridouZeijlstra2021.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

@[implicit_reducible]

instance IatridouZeijlstra2021.instDecidableEqTimeSpanKind : DecidableEq TimeSpanKind

Equations

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

def IatridouZeijlstra2021.instReprTimeSpanKind.repr : TimeSpanKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance IatridouZeijlstra2021.instReprTimeSpanKind : Repr TimeSpanKind

Equations

• IatridouZeijlstra2021.instReprTimeSpanKind = { reprPrec := IatridouZeijlstra2021.instReprTimeSpanKind.repr }

def IatridouZeijlstra2021.TimeSpanKind.tenseSetsBoundary : TimeSpanKind → IatridouEtAl2001.BoundaryKind

The boundary set by Tense (not by the adverbial). PTS: Tense sets the RB. UTS: context/Tense sets the LB. Mirror-image relationship ([IZ21] §8).

Equations

• IatridouZeijlstra2021.TimeSpanKind.pts.tenseSetsBoundary = IatridouEtAl2001.BoundaryKind.right
• IatridouZeijlstra2021.TimeSpanKind.uts.tenseSetsBoundary = IatridouEtAl2001.BoundaryKind.left

def IatridouZeijlstra2021.TimeSpanKind.adverbialSetsBoundary : TimeSpanKind → IatridouEtAl2001.BoundaryKind

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

Equations

• IatridouZeijlstra2021.TimeSpanKind.pts.adverbialSetsBoundary = IatridouEtAl2001.BoundaryKind.left
• IatridouZeijlstra2021.TimeSpanKind.uts.adverbialSetsBoundary = IatridouEtAl2001.BoundaryKind.right

theorem IatridouZeijlstra2021.pts_uts_mirror : TimeSpanKind.pts.adverbialSetsBoundary ≠ TimeSpanKind.uts.adverbialSetsBoundary

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

inductive IatridouZeijlstra2021.NPIStrength : Type

NPI strength classification. Strong NPIs require antiadditive environments; weak NPIs require only DE environments. [Zwa98] [Gaj11]

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

@[implicit_reducible]

instance IatridouZeijlstra2021.instDecidableEqNPIStrength : DecidableEq NPIStrength

Equations

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

def IatridouZeijlstra2021.instReprNPIStrength.repr : NPIStrength → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance IatridouZeijlstra2021.instReprNPIStrength : Repr NPIStrength

Equations

• IatridouZeijlstra2021.instReprNPIStrength = { reprPrec := IatridouZeijlstra2021.instReprNPIStrength.repr }

structure IatridouZeijlstra2021.BoundaryAdverbial : Type

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

[IZ21] §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 : IatridouEtAl2001.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? [Chi13]: domain widening requires contrastive focus under negation. In years is always contrastively focused; until is contrastively focused only when under negation.

• compatiblePerfect : List Kiparsky2002.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.

@[implicit_reducible]

instance IatridouZeijlstra2021.instReprBoundaryAdverbial : Repr BoundaryAdverbial

Equations

• IatridouZeijlstra2021.instReprBoundaryAdverbial = { reprPrec := IatridouZeijlstra2021.instReprBoundaryAdverbial.repr }

def IatridouZeijlstra2021.instReprBoundaryAdverbial.repr : BoundaryAdverbial → ℕ → Std.Format

Equations

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

def IatridouZeijlstra2021.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). [IZ21] §3–4

Equations

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

def IatridouZeijlstra2021.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 IatridouZeijlstra2021.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 IatridouZeijlstra2021.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). [IZ21] §7: one until, not two.

Equations

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

theorem IatridouZeijlstra2021.inYears_sets_lb : inYears.boundary = TimeSpanKind.pts.adverbialSetsBoundary

In years sets the LB (matching PTS).

theorem IatridouZeijlstra2021.until_sets_rb : until_.boundary = TimeSpanKind.uts.adverbialSetsBoundary

Until sets the RB (matching UTS).

theorem IatridouZeijlstra2021.both_domain_wideners : inYears.introducesDomainAlts = true ∧ until_.introducesDomainAlts = true

In years and until are both domain wideners.

theorem IatridouZeijlstra2021.both_strong_npis : inYears.npiStrength = NPIStrength.strong ∧ until_.npiStrength = NPIStrength.strong

In years and until are both strong NPIs.

theorem IatridouZeijlstra2021.contrastive_asymmetry : inYears.alwaysContrastive = true ∧ until_.alwaysContrastive = false

In years is always contrastive; until is not.

theorem IatridouZeijlstra2021.inYears_eperfect_only : Kiparsky2002.PerfectReading.universal ∉ inYears.compatiblePerfect ∧ Kiparsky2002.PerfectReading.universal ∈ inTheLast5Years.compatiblePerfect

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

theorem IatridouZeijlstra2021.nonNPI_no_domainAlts : since2015.introducesDomainAlts = false ∧ inTheLast5Years.introducesDomainAlts = false

Non-NPI boundary adverbials do not introduce domain alternatives.

def IatridouZeijlstra2021.SubdomainAlternatives {Time : Type u_2} [LinearOrder Time] (τ : NonemptyInterval Time) : Set (NonemptyInterval Time)

The subdomain alternatives of a time span τ are all subintervals of τ. [Chi13] Ch. 1; [IZ21] §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

• IatridouZeijlstra2021.SubdomainAlternatives τ = Set.Iic τ

theorem IatridouZeijlstra2021.self_in_subdomain {Time : Type u_2} [LinearOrder Time] (τ : NonemptyInterval Time) : τ ∈ SubdomainAlternatives τ

Subdomain alternatives of τ include τ itself.

theorem IatridouZeijlstra2021.subdomain_monotone {Time : Type u_2} [LinearOrder Time] (τ₁ τ₂ : NonemptyInterval Time) (h : τ₁ ≤ τ₂) : SubdomainAlternatives τ₁ ⊆ SubdomainAlternatives τ₂

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

def IatridouZeijlstra2021.eventInSpan {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (τ : NonemptyInterval 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

• IatridouZeijlstra2021.eventInSpan P w τ = ∃ (e : Event Time), e.τ ≤ τ ∧ P w e

def IatridouZeijlstra2021.noEventInSpan {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (τ : NonemptyInterval Time) : Prop

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

Equations

• IatridouZeijlstra2021.noEventInSpan P w τ = ¬IatridouZeijlstra2021.eventInSpan P w τ

theorem IatridouZeijlstra2021.eventInSpan_monotone {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (τ₁ τ₂ : NonemptyInterval Time) (h : τ₁ ≤ τ₂) : 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 IatridouZeijlstra2021.subdomain_alts_nonweaker {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (τ τ' : NonemptyInterval 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 IatridouZeijlstra2021.positive_exhaustification_contradicts {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (τ : NonemptyInterval Time) (_hassert : eventInSpan P w τ) (hexh : ∀ τ' ∈ SubdomainAlternatives τ, τ' ≠ τ → noEventInSpan P w τ') (τ_sub : NonemptyInterval Time) : τ_sub ≤ τ → τ_sub ≠ τ → eventInSpan P w τ_sub → False

Positive environment contradiction ([IZ21] §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 IatridouZeijlstra2021.negated_subdomain_weaker {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (τ τ' : NonemptyInterval Time) (h : τ' ≤ τ) : 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 IatridouZeijlstra2021.actualityInference {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (τ : NonemptyInterval Time) : Prop

Actuality Inference ([IZ21] §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

• IatridouZeijlstra2021.actualityInference P w τ = IatridouZeijlstra2021.eventInSpan P w τ

def IatridouZeijlstra2021.aiAtBoundary {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (w : W) (τ : NonemptyInterval Time) : Prop

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

Equations

• IatridouZeijlstra2021.aiAtBoundary P w τ = ∃ (e : Event Time), e.τ.toProd.2 = τ.toProd.1 ∧ P w e

structure IatridouZeijlstra2021.BeyondExpectationInference {Time : Type u_2} [LinearOrder Time] : Type u_2

Beyond Expectation Inference ([IZ21] §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 : NonemptyInterval Time

  The actual time span

• expectedBound : NonemptyInterval Time

  The contextually expected upper bound on the time span

• beyondExpectation : self.expectedBound ≤ 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 IatridouZeijlstra2021.perfectiveContainment {Time : Type u_2} [LinearOrder Time] (e : Event Time) (τ : NonemptyInterval Time) : Prop

Perfective contributes ST ⊆ TT: the event is contained in the time span. [IZ21] §1 (eq. 17a), following [Kle94]. Equivalently, the E-perfect: the event is contained in the PTS.

Equations

• IatridouZeijlstra2021.perfectiveContainment e τ = (e.τ ≤ τ)

def IatridouZeijlstra2021.imperfectiveContainment {Time : Type u_2} [LinearOrder Time] (e : Event Time) (τ : NonemptyInterval Time) : Prop

Imperfective contributes TT ⊆ ST: the time span is contained in the event. [IZ21] §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

• IatridouZeijlstra2021.imperfectiveContainment e τ = (τ ≤ e.τ)

theorem IatridouZeijlstra2021.impf_subdomain_entailed {W : Type u_1} {Time : Type u_2} [LinearOrder Time] (P : W → Event Time → Prop) (hSub : Semantics.Aspect.SubintervalProperty.HasSubintervalProp P) (w : W) (e : Event Time) (τ : NonemptyInterval Time) (hP : P w e) (hImpf : τ ≤ e.τ) (τ' : NonemptyInterval Time) (hτ' : τ' ≤ τ) : 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. [IZ21] §7.2

theorem IatridouZeijlstra2021.constants_observation : inYears.introducesDomainAlts = true ∧ inTheLast5Years.introducesDomainAlts = false

Constant's Observation ([IZ21] §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 IatridouZeijlstra2021.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. [IZ21] §11

Equations

• IatridouZeijlstra2021.isDomainWidener adv = adv.introducesDomainAlts

theorem IatridouZeijlstra2021.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 IatridouZeijlstra2021.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.