Presuppositions of forget Across Complement Frames

@cite{kiparsky-kiparsky-1970} @cite{williams-2026} @cite{white-2014} @misc{white-2014}

Theory-neutral empirical data from @cite{ippolito-kiss-williams-2026}, who shows that forget is uniformly factive across all complement types, but the content of the presupposition varies:

• With finite CPs and PRO-ing gerunds: the presupposition is non-modal (directly presupposes complement truth)
• With plain to-infinitives: the presupposition is modal (presupposes an obligation or plan)

This file records the empirical judgments that motivate the SMINC generalization (Selectivity of Modal Insertion in Non-finite Contexts): the covert modal only appears with plain infinitives.

Key Data (Table 1, p. 8)

Complement	Example	Presup content
finite CP	"forgot that she stopped"	non-modal (she stopped)
PRO-ing gerund	"forgot stopping by"	non-modal (stopped)
plain infinitive	"forgot to stop by"	modal (was supposed to stop)

Uniform Factivity

The paper follows @cite{white-2014} in arguing that forget is canonically factive in ALL uses — both the cognition reading ("forgot that p") and the psych-action reading ("forgot to VP"). There is no lexical ambiguity. What varies is the content of the presupposition, not its presence.

inductive Phenomena.Presupposition.ForgetPresuppositions.PresupContent : Type

Whether a factive presupposition has modal content.

@cite{ippolito-kiss-williams-2026} shows that forget always presupposes, but the content varies by complement type:

• .nonModal: directly presupposes complement truth
• .modal: presupposes a modalized version (obligation/plan)

• nonModal : PresupContent

  Directly presupposes complement truth: "forgot that p" → presupposes p

• modal : PresupContent

  Presupposes a modalized version: "forgot to VP" → presupposes should VP

instance Phenomena.Presupposition.ForgetPresuppositions.instDecidableEqPresupContent : DecidableEq PresupContent

Equations

• Phenomena.Presupposition.ForgetPresuppositions.instDecidableEqPresupContent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.ForgetPresuppositions.instReprPresupContent.repr : PresupContent → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.ForgetPresuppositions.instReprPresupContent : Repr PresupContent

Equations

• Phenomena.Presupposition.ForgetPresuppositions.instReprPresupContent = { reprPrec := Phenomena.Presupposition.ForgetPresuppositions.instReprPresupContent.repr }

instance Phenomena.Presupposition.ForgetPresuppositions.instBEqPresupContent : BEq PresupContent

Equations

• Phenomena.Presupposition.ForgetPresuppositions.instBEqPresupContent = { beq := Phenomena.Presupposition.ForgetPresuppositions.instBEqPresupContent.beq }

def Phenomena.Presupposition.ForgetPresuppositions.instBEqPresupContent.beq : PresupContent → PresupContent → Bool

Equations

• Phenomena.Presupposition.ForgetPresuppositions.instBEqPresupContent.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.Presupposition.ForgetPresuppositions.ForgetJudgment : Type

An empirical judgment about forget's presupposition in a particular complement frame.

Every entry has a presupposition (uniform factivity); what varies is the content (modal vs. non-modal).

• frame : Core.Verbs.ComplementType

  Complement frame being tested

• sentence : String

  Example sentence

• presupParaphrase : String

  What is presupposed (paraphrase)

• content : PresupContent

  Is the presupposition modal or non-modal?

def Phenomena.Presupposition.ForgetPresuppositions.instReprForgetJudgment.repr : ForgetJudgment → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.ForgetPresuppositions.instReprForgetJudgment : Repr ForgetJudgment

Equations

• Phenomena.Presupposition.ForgetPresuppositions.instReprForgetJudgment = { reprPrec := Phenomena.Presupposition.ForgetPresuppositions.instReprForgetJudgment.repr }

def Phenomena.Presupposition.ForgetPresuppositions.instBEqForgetJudgment.beq : ForgetJudgment → ForgetJudgment → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Presupposition.ForgetPresuppositions.instBEqForgetJudgment.beq x✝¹ x✝ = false

instance Phenomena.Presupposition.ForgetPresuppositions.instBEqForgetJudgment : BEq ForgetJudgment

Equations

• Phenomena.Presupposition.ForgetPresuppositions.instBEqForgetJudgment = { beq := Phenomena.Presupposition.ForgetPresuppositions.instBEqForgetJudgment.beq }

Cognition reading (finite CP)

"Forgot that p" presupposes p (non-modal). This is the canonical factive reading recognized since @cite{kiparsky-kiparsky-1970}.

@cite{ippolito-kiss-williams-2026}, ex. (1): "Ana forgot that she stopped by the flower shop." Presupposes: Ana stopped by the flower shop.

def Phenomena.Presupposition.ForgetPresuppositions.forget_finiteCP : ForgetJudgment

Equations

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

Cognition reading (PRO-ing gerund)

"Forgot V-ing" presupposes V-ing occurred (non-modal). This is the critical evidence against the Modalized Complement Analysis's overprediction: the gerund is non-finite but NOT modalized.

@cite{ippolito-kiss-williams-2026}, ex. (12): "Ana forgot stopping by the flower shop." Presupposes: Ana stopped by the flower shop.

def Phenomena.Presupposition.ForgetPresuppositions.forget_gerund : ForgetJudgment

Equations

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

Psych-action reading (plain infinitive)

"Forgot to VP" presupposes a plan or obligation to VP (modal). Un@cite{ippolito-kiss-williams-2026}, this arises because the plain infinitive's forward-oriented temporal profile violates the pre-existence presupposition, triggering covert modal insertion.

@cite{ippolito-kiss-williams-2026}, ex. (3): "Ana forgot to stop by the flower shop." Presupposes: Ana was supposed to / had a plan to stop.

def Phenomena.Presupposition.ForgetPresuppositions.forget_infinitival : ForgetJudgment

Equations

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

def Phenomena.Presupposition.ForgetPresuppositions.allForgetJudgments : List ForgetJudgment

All forget judgments across complement frames.

Equations

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

theorem Phenomena.Presupposition.ForgetPresuppositions.forget_uniformly_factive : allForgetJudgments.length = 3

Uniform factivity: forget has a presupposition in every frame. (All entries exist — there is no "absent presupposition" case.)

theorem Phenomena.Presupposition.ForgetPresuppositions.not_all_modal : (allForgetJudgments.all fun (x : ForgetJudgment) => x.content == PresupContent.modal) = false

Not all presuppositions are modal: finite and gerund cases are non-modal.

theorem Phenomena.Presupposition.ForgetPresuppositions.not_all_nonModal : (allForgetJudgments.all fun (x : ForgetJudgment) => x.content == PresupContent.nonModal) = false

Not all presuppositions are non-modal: the infinitival case is modal.

theorem Phenomena.Presupposition.ForgetPresuppositions.modal_count : (List.filter (fun (x : ForgetJudgment) => x.content == PresupContent.modal) allForgetJudgments).length = 1

The modal presupposition arises with exactly one frame (the infinitival).

theorem Phenomena.Presupposition.ForgetPresuppositions.nonModal_count : (List.filter (fun (x : ForgetJudgment) => x.content == PresupContent.nonModal) allForgetJudgments).length = 2

The non-modal presupposition arises with exactly two frames.