Iatridou and Zeijlstra (2021): The Complex Beauty of Boundary Adverbials

Iatridou and Zeijlstra analyze in years and until as boundary adverbials that are domain wideners. In years introduces the subintervals of the perfect time span as domain alternatives, which exhaustification turns into a contradiction for the positive perfective claim and leaves vacuous under negation, so it is a negative polarity item. As a domain widener it stretches its left boundary as far as is logically possible, to the greatest event-free span, which forces an event just beyond that boundary, the noncancelable actuality inference, and makes the span contain every event-free alternative, the beyond expectation inference. Until is the mirror image with the left boundary fixed: with an imperfective predicate exhaustification is vacuous, and with a perfective one only the construal exhaustifying the negated claim survives, so the punctual and durative untils of Karttunen and Giannakidou are one word. Against their ambiguity account, negation yields the subinterval property, so its durative until would accept a negated perfective with no event at all, and Greek para mono is an exceptive whose meaning already gives the punctual one.

Main statements

• in_years_contradictory: exhaustified, the positive perfective claim is contradictory when the events are shorter than the span.
• negated_perfective_exh_vacuous, throughout_exh_vacuous: exhaustification is vacuous for a negated perfective and for a predicate holding throughout the span.
• not_throughout_exh_contradictory: exhaustifying the claim that an imperfective predicate does not hold throughout the span is contradictory.
• actuality_inference, event_near_lb, event_near_rb: a widened span forces a relevant event just beyond its widened boundary.
• beyond_expectation_inference: the widened span contains every event-free alternative.
• widened_iff_maximal: the widened span is the event-free span stretched until the sentence would become false.
• not_widened_rb_of_finite: in dense time no span is widened past finitely many events.
• two_until_overgenerates: the durative until of the ambiguity account accepts a negated perfective with no event at all.
• eventiveUntil_of_exceptive: para mono with a temporal argument under negation, read as an exceptive, entails the punctual until meaning, the event included.
• isLeast_rightBoundaries_prfv, isLeast_rightBoundaries_unbounded: a perfective argument of until sets the right boundary at the completion of its event, an imperfective one at the onset.

Implementation notes

• Exhaustification is the shared Exhaustification.exh over the domain alternatives, the claim at every subinterval. Entailment between the alternatives is logical, inclusion between sets of interpretations of the event predicate: a claim is stated for P : V → E → Prop reaching every extension (Function.Surjective P), the extensions themselves (P = id, V = E → Prop) or their negations (surjective_not). A predicate at a world is its extension, τ ∈ PRFV P w being PRFV id (P w) τ by definition. Refuting an entailment assumes the event domain rich, every interval the run time of some event (Function.Surjective Event.τ).
• The paper calls the exhaustified positive claim a logical contradiction. It needs the events to be shorter than the span, as Chierchia's culminated event inside a period of weeks is; an event filling the span exactly survives exhaustification (mem_exh_prfv_iff). The contradiction for the not-throughout claim, (142), needs overlapping events to sum and an interior point of the span.
• The widened span is IsGreatest among the event-free spans with the fixed boundary, its other boundary the right one set by tense for in years and the contextual left one for until. With closed spans and inclusion the forced event lies strictly beyond the widened boundary, and in dense time such a span exists only past infinitely many events; the paper puts "issues of density aside".
• The paper's meaning for para mono, after von Fintel and Iatridou, is an existential that does not itself entail the exception; for the entailment it appeals to "one's favorite semantics" of exceptives. Von Fintel's least-exception semantics, Quantifier.Exceptive, supplies it.
• The paper's summary of the three scopal construals in Section 7.2 has the labels of the first two interchanged relative to (146) and (148), and Section 8 once attaches throughout-not and not-throughout to (148c2) and (148c1), the reverse of (148); the theorems follow (146) and (148).

TODO

• Section 8's fact that in-adverbials lack the universal perfect, (153), on which the exclusion of (154c1–2) rests, is taken as given by the paper and not derived.
• The satisfaction of the actuality inference on a future branch, (155)–(162), and the hypothesis that a presupposed span makes a domain widener a strong polarity item, after Gajewski's account of strong items by enriched meanings, are not formalized.

References

• [IZ21]
• [IAI01]
• [Chi13]
• [KL93]
• [Kar74b]
• [Gia02]
• [VF93]
• [vFFI14]
• [Gaj11]

Domain alternatives and exhaustification

def IatridouZeijlstra2021.domainAlternatives {T : Type u_2} [LinearOrder T] {V : Type u_4} (p : V → Set (NonemptyInterval T)) (τ : NonemptyInterval T) : Set (Set V)

The domain alternatives of the claim p at the span τ are the claim at each of its subintervals, (45b), (49b) and (127).

Equations

• IatridouZeijlstra2021.domainAlternatives p τ = (fun (τ' : NonemptyInterval T) => {v : V | τ' ∈ p v}) '' Set.Iic τ

theorem IatridouZeijlstra2021.exh_domainAlternatives_eq_self {T : Type u_2} [LinearOrder T] {V : Type u_4} {p : V → Set (NonemptyInterval T)} {τ : NonemptyInterval T} (hp : ∀ (v : V), IsLowerSet (p v)) : Exhaustification.exh (domainAlternatives p τ) {v : V | τ ∈ p v} = {v : V | τ ∈ p v}

A claim with the subinterval property entails its domain alternatives, so exhaustifying them is vacuous.

theorem IatridouZeijlstra2021.mem_exh_domainAlternatives_iff {T : Type u_2} [LinearOrder T] {V : Type u_4} {p : V → Set (NonemptyInterval T)} {τ : NonemptyInterval T} (hp : ∀ (τ₁ τ₂ : NonemptyInterval T), {v : V | τ₁ ∈ p v} ⊆ {v : V | τ₂ ∈ p v} ↔ τ₁ ≤ τ₂) {v : V} : v ∈ Exhaustification.exh (domainAlternatives p τ) {v : V | τ ∈ p v} ↔ τ ∈ p v ∧ ∀ τ' < τ, τ' ∉ p v

When the claim at one span entails it at another exactly when the second contains the first, exhaustification negates the claim at every proper subinterval.

In years: the perfective claim and its negation

The assertion of a perfect of the perfective, (14e) and (49a), is Aspect.PRFV: some event's run time lies inside the span. Its domain alternatives are stronger and not entailed, so exhaustification negates them all and the event would have to fill the span, which a culminated event shorter than weeks cannot, (44) and (49). The negated perfective has the subinterval property (Aspect.isLowerSet_compl_prfv), so under negation every alternative is entailed and exhaustification is vacuous, (50). With until the same holds of the until time span: the positive perfective (128)–(132) is contradictory, and so is (146a), exhaustifying the perfective of the negated predicate, while the construal exhaustifying the negated claim, (148b), is vacuous.

theorem IatridouZeijlstra2021.prfv_subset_prfv_iff {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {V : Type u_4} {P : V → E → Prop} (hP : Function.Surjective P) (hrich : Function.Surjective Event.τ) {τ₁ τ₂ : NonemptyInterval T} : {v : V | τ₁ ∈ Aspect.PRFV P v} ⊆ {v : V | τ₂ ∈ Aspect.PRFV P v} ↔ τ₁ ≤ τ₂

Where every extension is available and the event domain is rich, the perfective claim at one span entails it at another exactly when the second contains the first.

theorem IatridouZeijlstra2021.mem_exh_prfv_iff {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {V : Type u_4} {P : V → E → Prop} {τ : NonemptyInterval T} (hP : Function.Surjective P) (hrich : Function.Surjective Event.τ) {v : V} : v ∈ Exhaustification.exh (domainAlternatives (Aspect.PRFV P) τ) {v : V | τ ∈ Aspect.PRFV P v} ↔ (∃ (e : E), Event.τ e = τ ∧ P v e) ∧ ∀ τ' < τ, τ' ∉ Aspect.PRFV P v

Exhaustified, the positive perfective claim requires an event filling the span and none inside a proper subinterval.

theorem IatridouZeijlstra2021.in_years_contradictory {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {V : Type u_4} {P : V → E → Prop} {τ : NonemptyInterval T} (hP : Function.Surjective P) (hrich : Function.Surjective Event.τ) {v : V} (hshort : ∀ (e : E), P v e → Event.τ e ≠ τ) : v ∉ Exhaustification.exh (domainAlternatives (Aspect.PRFV P) τ) {v : V | τ ∈ Aspect.PRFV P v}

Where every relevant event is shorter than the span, the exhaustified positive claim is contradictory, so in years is a negative polarity item, (44) and (49). The positive until sentence (128), the perfect of (152b), the perfective of the negated predicate in (146a) and the presupposition of (180) are instances.

theorem IatridouZeijlstra2021.negated_perfective_exh_vacuous {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {V : Type u_4} {P : V → E → Prop} {τ : NonemptyInterval T} : Exhaustification.exh (domainAlternatives (fun (v : V) => (Aspect.PRFV P v)ᶜ) τ) {v : V | τ ∉ Aspect.PRFV P v} = {v : V | τ ∉ Aspect.PRFV P v}

Under negation exhaustification is vacuous, (50) and (126)–(127), and so is the construal of until that exhaustifies the negated perfective, (148b).

theorem IatridouZeijlstra2021.surjective_not {E : Type u_3} : Function.Surjective fun (v : E → Prop) (e : E) => ¬v e

Negating the extension of the event predicate reaches every extension.

Domain widening: the actuality and beyond expectation inferences

A boundary adverbial sets one boundary of its span, while tense or the argument of until fixes the other (F, the spans ending at t for in years and those starting at t for until). A domain widener stretches its boundary as far as is logically possible: its span is the greatest event-free span with the fixed boundary, Section 4. The event that stops the widening is the actuality inference, Constant's observation, and the span's containing every event-free alternative is the beyond expectation inference. A boundary adverbial that names its own boundary, in (the last) 5 years or since 2015, leaves the actuality inference cancelable and has no beyond expectation inference.

def IatridouZeijlstra2021.Widened {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (F : Set (NonemptyInterval T)) (P : W → E → Prop) (w : W) (τ : NonemptyInterval T) : Prop

The span of a domain widener whose other boundary is fixed by F is the greatest event-free span that F admits.

Equations

• IatridouZeijlstra2021.Widened F P w τ = IsGreatest (F \ Aspect.PRFV P w) τ

theorem IatridouZeijlstra2021.isChain_rb {T : Type u_2} [LinearOrder T] (t : T) : IsChain (fun (x1 x2 : NonemptyInterval T) => x1 ≤ x2) {τ : NonemptyInterval T | τ.toProd.2 = t}

Spans ending at the same time are nested.

theorem IatridouZeijlstra2021.isChain_lb {T : Type u_2} [LinearOrder T] (t : T) : IsChain (fun (x1 x2 : NonemptyInterval T) => x1 ≤ x2) {τ : NonemptyInterval T | τ.toProd.1 = t}

Spans starting at the same time are nested.

theorem IatridouZeijlstra2021.widened_iff_maximal {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {F : Set (NonemptyInterval T)} {P : W → E → Prop} {w : W} {τ : NonemptyInterval T} (hF : IsChain (fun (x1 x2 : NonemptyInterval T) => x1 ≤ x2) F) : Widened F P w τ ↔ Maximal (fun (x : NonemptyInterval T) => x ∈ F \ Aspect.PRFV P w) τ

On a chain of spans sharing the fixed boundary, the widened span is the maximal event-free one, the boundary stretched until the sentence would become false.

theorem IatridouZeijlstra2021.Widened.prfv {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {F : Set (NonemptyInterval T)} {P : W → E → Prop} {w : W} {τ τ' : NonemptyInterval T} (h : Widened F P w τ) (hτ' : τ' ∈ F) (hlt : τ < τ') : τ' ∈ Aspect.PRFV P w

Every wider span with the fixed boundary contains an event.

theorem IatridouZeijlstra2021.actuality_inference {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {F : Set (NonemptyInterval T)} {P : W → E → Prop} {w : W} {τ : NonemptyInterval T} (h : Widened F P w τ) (hw : ∃ τ' ∈ F, τ < τ') : ∃ (e : E), P w e

The actuality inference is not cancelable, Constant's observation (22) and (26), since a relevant event exists whenever the span could be widened at all.

theorem IatridouZeijlstra2021.beyond_expectation_inference {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {F : Set (NonemptyInterval T)} {P : W → E → Prop} {w : W} {τ τ' : NonemptyInterval T} (h : Widened F P w τ) (hτ' : τ' ∈ F) (hfree : τ' ∉ Aspect.PRFV P w) : τ' ≤ τ

The beyond expectation inference, (31)–(33) and (119)–(122), is that the widened span contains every event-free span with the same fixed boundary.

theorem IatridouZeijlstra2021.event_near_lb {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {τ : NonemptyInterval T} {t : T} (h : Widened {τ : NonemptyInterval T | τ.toProd.2 = t} P w τ) {s : T} (hs : s < τ.toProd.1) : ∃ (e : E), P w e ∧ s ≤ (Event.τ e).toProd.1 ∧ (Event.τ e).toProd.1 < τ.toProd.1

With in years the last event starts just before the left boundary of the widened perfect time span, (51), since however close to the boundary one looks an event starts there, (23)–(24).

theorem IatridouZeijlstra2021.event_near_rb {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {τ : NonemptyInterval T} {t : T} (h : Widened {τ : NonemptyInterval T | τ.toProd.1 = t} P w τ) {s : T} (hs : τ.toProd.2 < s) : ∃ (e : E), P w e ∧ (Event.τ e).toProd.2 ≤ s ∧ τ.toProd.2 < (Event.τ e).toProd.2

With until the event ends just after the right boundary of the widened until time span, (123).

theorem IatridouZeijlstra2021.not_widened_rb_of_finite {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {τ : NonemptyInterval T} [DenselyOrdered T] [NoMinOrder T] {t : T} (hfin : {e : E | P w e}.Finite) : ¬Widened {τ : NonemptyInterval T | τ.toProd.2 = t} P w τ

In dense time a perfect time span is widened only past infinitely many events, since with finitely many an event-free span can always be stretched a little further.

theorem IatridouZeijlstra2021.cancelable_of_lb {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {w : W} {t : T} (s : T) (hs : s ≤ t) : (∃ (P : W → E → Prop) (τ : NonemptyInterval T), τ.toProd.1 = s ∧ τ.toProd.2 = t ∧ τ ∉ Aspect.PRFV P w ∧ ∀ (e : E), ¬P w e) ∧ ∀ (e₀ : E), (Event.τ e₀).toProd.2 < s → ∃ (P : W → E → Prop) (τ : NonemptyInterval T), τ.toProd.1 = s ∧ τ.toProd.2 = t ∧ τ ∉ Aspect.PRFV P w ∧ P w e₀

A boundary adverbial that names its left boundary s, in (the last) 5 years or since 2015, leaves the actuality inference cancelable, since the negated perfect holds with no relevant event at all, (11)–(12), and with the last event before the left boundary, (23).

Until with an imperfective predicate

The predicate holds throughout the until time span, (137): Aspect.UNBOUNDED, the span inside the event's run time. Every domain alternative is then entailed and exhaustification is vacuous, for the affirmative (148a) as for the throughout-not reading with the negated event predicate, (139) and (148c1), and the not-throughout reading with negation above the exhaustifier, (148c2). The remaining construal, exhaustifying the not-throughout claim (148b), makes the predicate hold throughout every proper subinterval, (142), which is contradictory once overlapping events sum.

theorem IatridouZeijlstra2021.throughout_exh_vacuous {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {V : Type u_4} {P : V → E → Prop} {τ : NonemptyInterval T} : Exhaustification.exh (domainAlternatives (Aspect.UNBOUNDED P) τ) {v : V | τ ∈ Aspect.UNBOUNDED P v} = {v : V | τ ∈ Aspect.UNBOUNDED P v}

Exhaustifying the throughout claim is vacuous, (137) with (144), and (139) with (141) for the negated event predicate.

theorem IatridouZeijlstra2021.not_unbounded_subset_iff {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {V : Type u_4} {P : V → E → Prop} (hP : Function.Surjective P) (hrich : Function.Surjective Event.τ) {τ₁ τ₂ : NonemptyInterval T} : {v : V | τ₁ ∉ Aspect.UNBOUNDED P v} ⊆ {v : V | τ₂ ∉ Aspect.UNBOUNDED P v} ↔ τ₁ ≤ τ₂

Where every extension is available and the event domain is rich, the not-throughout claim at one span entails it at another exactly when the second contains the first, (142).

theorem IatridouZeijlstra2021.mem_exh_not_unbounded_iff {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {V : Type u_4} {P : V → E → Prop} {τ : NonemptyInterval T} (hP : Function.Surjective P) (hrich : Function.Surjective Event.τ) {v : V} : v ∈ Exhaustification.exh (domainAlternatives (fun (v : V) => (Aspect.UNBOUNDED P v)ᶜ) τ) {v : V | τ ∉ Aspect.UNBOUNDED P v} ↔ τ ∉ Aspect.UNBOUNDED P v ∧ ∀ τ' < τ, τ' ∈ Aspect.UNBOUNDED P v

Exhaustifying the not-throughout claim makes the predicate hold throughout every proper subinterval.

theorem IatridouZeijlstra2021.unbounded_of_forall_lt {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {V : Type u_4} {P : V → E → Prop} {τ : NonemptyInterval T} {v : V} (hsum : ∀ (e₁ e₂ : E), P v e₁ → P v e₂ → (Event.τ e₁).Overlaps (Event.τ e₂) → ∃ (e : E), P v e ∧ Event.τ e₁ ≤ Event.τ e ∧ Event.τ e₂ ≤ Event.τ e) {m : T} (hm₁ : τ.toProd.1 < m) (hm₂ : m < τ.toProd.2) (h : ∀ τ' < τ, τ' ∈ Aspect.UNBOUNDED P v) : τ ∈ Aspect.UNBOUNDED P v

Where overlapping events sum to an event and the span has an interior point, a predicate holding throughout every proper subinterval holds throughout the span.

theorem IatridouZeijlstra2021.not_throughout_exh_contradictory {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {V : Type u_4} {P : V → E → Prop} {τ : NonemptyInterval T} (hP : Function.Surjective P) (hrich : Function.Surjective Event.τ) {v : V} (hsum : ∀ (e₁ e₂ : E), P v e₁ → P v e₂ → (Event.τ e₁).Overlaps (Event.τ e₂) → ∃ (e : E), P v e ∧ Event.τ e₁ ≤ Event.τ e ∧ Event.τ e₂ ≤ Event.τ e) {m : T} (hm₁ : τ.toProd.1 < m) (hm₂ : m < τ.toProd.2) : v ∉ Exhaustification.exh (domainAlternatives (fun (v : V) => (Aspect.UNBOUNDED P v)ᶜ) τ) {v : V | τ ∉ Aspect.UNBOUNDED P v}

With an imperfective predicate the construal exhaustifying the not-throughout claim, (148b), is contradictory, (142).

Against the lexical ambiguity of until

The ambiguity account must deny that negation yields the subinterval property, Section 5.2.2: otherwise its durative until takes a negated perfective on the throughout-not reading, which has no actuality inference, and She did not leave until 5 p.m. and maybe she didn't leave at all, (83), would not be a contradiction. Greek, Section 5.2.1.1, offers no separate punctual until: para mono is the exceptive 'but only', and Dhen thimose para mono htes 'he didn't get angry except yesterday', (69), means what the punctual until is said to mean.

theorem IatridouZeijlstra2021.two_until_overgenerates {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} (hP : ∀ (e : E), ¬P w e) {s t : T} (h : s < t) : Giannakidou2002.durativeUntil (fun (w : W) => (Aspect.PRFV P w)ᶜ) w t

The durative until of [Gia02] accepts a negated perfective, which has the subinterval property, in a model with no relevant event at all.

theorem IatridouZeijlstra2021.eventiveUntil_of_exceptive {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {t₀ : T} (h : Quantifier.Exceptive.IsExceptionSet Quantifier.GQ.no ⊤ (fun (x : T) => x = t₀) fun (t : T) => ∃ (e : E), P w e ∧ t ∈ Event.τ e) : Giannakidou2002.eventiveUntil P w t₀

No time but t₀ is a time of a P-event, the exceptive of dhen … para mono with a temporal argument on the least-exception semantics, says that t₀ is the only such time, which entails the punctual until of [Gia02], the event at t₀ included.

Setting the right boundary

The argument of until contains a definite description over intervals, which picks the maximally informative interval as von Fintel, Fox and Iatridou have definites do, so the right boundary is the first moment at which the argument clause holds of a span ending there. A perfective argument, until she read Anna Karenina, (170)–(171), sets it at the completion of the reading, an imperfective one, until she was working at the grocery store, (172)–(175), at the onset.

theorem IatridouZeijlstra2021.isLeast_rightBoundaries_prfv {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {Q : W → E → Prop} {w : W} {e : E} (he : Q w e) (hfirst : ∀ (e' : E), Q w e' → (Event.τ e).toProd.2 ≤ (Event.τ e').toProd.2) : IsLeast ((fun (x : NonemptyInterval T) => x.toProd.2) '' Aspect.PRFV Q w) (Event.τ e).toProd.2

A perfective argument clause sets the right boundary at the completion of its first event.

theorem IatridouZeijlstra2021.isLeast_rightBoundaries_unbounded {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {Q : W → E → Prop} {w : W} {e : E} (he : Q w e) (hfirst : ∀ (e' : E), Q w e' → (Event.τ e).toProd.1 ≤ (Event.τ e').toProd.1) : IsLeast ((fun (x : NonemptyInterval T) => x.toProd.2) '' Aspect.UNBOUNDED Q w) (Event.τ e).toProd.1

An imperfective argument clause sets the right boundary at the onset of its first event.