Williams (2025): the presuppositions of forget

Williams accounts for when the complement of forget carries a covert modal. Forget is factive whatever its complement, after the Kiparskys, and with a plain infinitive the presupposed proposition is modal: John forgot to stop by the flower shop presupposes that John was supposed to. White puts the modal in every nonfinite complement, but a PRO-ing gerund and a Spanish perfect infinitive, both nonfinite, presuppose the event and not an obligation, so the modal heads plain infinitives only. The modal is a last resort for Bondarenko's pre-existence presupposition, that the embedded event started before the forgetting: an anterior complement meets it as soon as the complement holds, while a plain infinitive contradicts it and needs the modal.

Main results

• needsMod_aspP: a plain infinitive needs the modal.
• not_needsMod_anterior_aspP: the anterior complements do not.
• preEx_mod_iff: the presupposition under the modal.
• mca_overgenerates: White's Modalized Complement Analysis overgenerates.

Implementation notes

• The paper's complements are Champollion's continuations, from a predicate of events to a proposition at a time (28). Each one the paper builds closes a predicate of events against the continuation, and the only continuations applied are the trivial one of Krifka's closure (27) and equality with the embedded event in (28b), so a complement here is the predicate of events itself (Complement), and closure binds its event (Complement.closure).
• mathlib orders intervals by inclusion: the paper's τ(e) ⊆ t is (τ e) ≤ t, its t' < t in (30a) and (30b) is t'.Precedes t, the t ≤ t' of (37) is t.IsBefore t', and LB is .fst.
• Pre-existence is Event.PreExists of Semantics/Events/PreExistence.lean, shared with Studies/Bondarenko2020. (28b) as printed binds the complement's time existentially, and so bound it cannot tell the plain infinitive from the anterior complements (exists_anterior_iff). The derivations (32), (34) and (36) evaluate the complement at the attitude holder's subjective now, which PreEx takes to be the run time of the forgetting.
• (30a) and (30b) are printed as one formula, so (32) and (34) are one theorem. The paper implements the perfect after Kratzer, and (30b) prints it as strict precedence, not the ViewpointType.perfect relation, whose intervals may touch.
• (40)(i) and (40)(ii) are assumptions about the plan state, not consequences of (37), and the proper inclusion of the subjective now in the plan's run time in (40)(ii) does not by itself start the plan earlier; the prose does ("the runtime of Mod begins before this"). The plan state's starting earlier is a hypothesis of not_needsMod_mod. A state with no plan worlds satisfies (37) vacuously.
• Plain infinitives are simultaneous with the matrix reference time, after Wurmbrand, which places AspP at the subjective now in (36).
• The assertion of (28a), that the attitude holder does not believe the complement, plays no part in the argument and is not formalized; neither is the necessity and sufficiency presupposition (5b), which the paper leaves to future work, nor the implicative entailment of forgot to, after Karttunen, which it sets aside (fn. 1).
• The English fragment has an implicative forget taking an infinitive and a factive one taking a finite clause or a gerund, English.Verbs.forget and English.Verbs.forget_rog; Williams' uniformity hypothesis takes them to be one verb. mca_overgenerates reads their frames.

References

• [Wil25]
• [Whi14]
• [KK70]
• [Bon20]
• [Cha15]
• [Kri89]
• [Kra98a]
• [Wur14]
• [Kar71a]

Complements

@[reducible, inline]

abbrev Williams2025.Complement (W : Type u_4) (E : Type u_5) (T : Type u_6) [LinearOrder T] : Type (max (max u_4 u_5) u_6)

A complement gives the events it describes at a reference time in a world.

Equations

• Williams2025.Complement W E T = (W → NonemptyInterval T → E → Prop)

def Williams2025.Complement.closure {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] (C : Complement W E T) : W → Set (NonemptyInterval T)

The closure (27) of a complement binds its event.

Equations

• C.closure w = {t : NonemptyInterval T | ∃ (e : E), C w t e}

def Williams2025.aspP {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) : Complement W E T

In AspP, (30c), the plain infinitive, perfective aspect locates the event within the reference time.

Equations

• Williams2025.aspP P w t e = (Event.τ e ≤ t ∧ P w e)

theorem Williams2025.closure_aspP {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) : (aspP P).closure = Aspect.PRFV P

Closing AspP gives the perfective.

def Williams2025.anterior {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] (C : Complement W E T) : Complement W E T

Under the past tense of the gerund, (30a), and the perfect, (30b), the complement holds at a reference time preceding t.

Equations

• Williams2025.anterior C w t e = ∃ (t' : NonemptyInterval T), t'.Precedes t ∧ C w t' e

def Williams2025.mod {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] (plan : E → NonemptyInterval T → W → Set W) (C : Complement W E T) : Complement W E T

Under the plan modal, (37), the plan state s is the complement's event, and in every world of its plan the complement holds at a time from t on.

Equations

• Williams2025.mod plan C w t s = ∀ w' ∈ plan s t w, ∃ (t' : NonemptyInterval T), t.IsBefore t' ∧ C.closure w' t'

Pre-existence

def Williams2025.PreEx {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (C : Complement W E T) (e : E) (w : W) : Prop

Pre-existence, (28b), holds at the forgetting e when the complement describes an event at the subjective now, the run time of e, that starts before e does.

Equations

• Williams2025.PreEx C e w = Event.PreExists Event.τ (C w (Event.τ e)) (Event.τ e).toProd.1

def Williams2025.NeedsMod {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (C : Complement W E T) : Prop

A complement needs the modal when it contradicts pre-existence at every forgetting, so that without the modal the sentence is a presupposition failure (§5).

Equations

• Williams2025.NeedsMod C = ∀ (e : E) (w : W), ¬Williams2025.PreEx C e w

theorem Williams2025.PreEx.closure {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {C : Complement W E T} {w : W} {e : E} (h : PreEx C e w) : C.closure w (Event.τ e)

Pre-existence gives factivity, the complement holding at the forgetting.

theorem Williams2025.exists_anterior_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] {C : Complement W E T} {w : W} [NoMaxOrder T] {p : E → Prop} : (∃ (e : E) (t : NonemptyInterval T), anterior C w t e ∧ p e) ↔ ∃ (e : E) (t : NonemptyInterval T), C w t e ∧ p e

(28b) as printed, ∃ e'' t, C w t e'' ∧ (τ e'').fst < (τ e).fst, binds the complement's time, and an existentially bound time absorbs the anterior shift.

The complements under pre-existence, §6

theorem Williams2025.precedes_of_anterior_aspP {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 : NonemptyInterval T} {e : E} (h : anterior (aspP P) w t e) : (Event.τ e).Precedes t

Under the anterior shift the embedded event precedes the reference time, (32)(iii), (34)(iii).

theorem Williams2025.preEx_anterior_aspP_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {e : E} : PreEx (anterior (aspP P)) e w ↔ (anterior (aspP P)).closure w (Event.τ e)

For the gerund and the perfect infinitive, pre-existence is the complement's holding at the forgetting, (32), (34).

theorem Williams2025.not_preEx_aspP {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {e : E} : ¬PreEx (aspP P) e w

A plain infinitive contradicts pre-existence, (36).

theorem Williams2025.preEx_mod_iff {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {C : Complement W E T} {plan : E → NonemptyInterval T → W → Set W} {w : W} {e : E} : PreEx (mod plan C) e w ↔ ∃ (s : E), mod plan C w (Event.τ e) s ∧ (Event.τ s).toProd.1 < (Event.τ e).toProd.1

Under the modal the presupposition is that the plan holds and began before the forgetting, (39).

The modal as a last resort, (15)

theorem Williams2025.needsMod_aspP {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] (P : W → E → Prop) : NeedsMod (aspP P)

A plain infinitive needs the modal, (15a).

theorem Williams2025.not_needsMod_anterior_aspP {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {P : W → E → Prop} {w : W} {e f : E} (h : P w e) (hf : (Event.τ e).Precedes (Event.τ f)) : ¬NeedsMod (anterior (aspP P))

The gerund and the perfect infinitive do not need the modal once the predicate has an event that precedes a forgetting f, (15b).

theorem Williams2025.not_needsMod_mod {W : Type u_1} {T : Type u_2} {E : Type u_3} [LinearOrder T] [Event.TemporalTrace E T] {C : Complement W E T} {plan : E → NonemptyInterval T → W → Set W} {w : W} {f s : E} (hs : mod plan C w (Event.τ f) s) (hlt : (Event.τ s).toProd.1 < (Event.τ f).toProd.1) : ¬NeedsMod (mod plan C)

The modal meets pre-existence at a forgetting f, given a plan holding at the subjective now that began before it, (40).

Against the Modalized Complement Analysis, §3.1

theorem Williams2025.mca_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} {e f : E} (h : P w e) (hf : (Event.τ e).Precedes (Event.τ f)) : (∀ fr ∈ English.Verbs.forget.valency.frames, White2014.Modalized fr) ∧ (∃ fr ∈ English.Verbs.forget_rog.valency.frames, White2014.Modalized fr) ∧ NeedsMod (aspP P) ∧ ¬NeedsMod (anterior (aspP P))

[Whi14] modalizes the infinitive of the implicative forget and the gerund of the factive one alike, but the infinitive frame hosts the plain infinitive, which needs the modal, and the perfect infinitive, which like the gerund does not, so whether the modal heads a complement is not a matter of its frame.

The began tests, (19) and (21)

Days are integers, Monday 1, Tuesday 2, Wednesday 3, and Mary forgets on Tuesday.