Pre-Existence Theory vs. Empirical Data

@cite{white-2014}

Connects the pre-existence theory (from PreExistence.lean) to empirical data about forget's presuppositions (from ForgetPresuppositions.lean) and to the English verb Fragment.

What This File Tests

1. Pre-existence predictions match data — needsModalInsertion correctly predicts which frames get modal vs. non-modal presuppositions

2. MCA overprediction — the Modalized Complement Analysis wrongly predicts a modal presupposition for the gerund case

3. Fragment consistency — the two Fragment entries for forget (implicative and factive/rogative) align with the theory

The pre-existence theory predicts: modal presupposition iff the complement type does NOT satisfy pre-existence. We verify this against each judgment from @cite{ippolito-kiss-williams-2025}.

theorem Phenomena.Presupposition.Studies.White2014.preEx_correct_finiteCP : Semantics.Attitudes.PreExistence.needsModalInsertion ForgetPresuppositions.forget_finiteCP.frame = false ∧ ForgetPresuppositions.forget_finiteCP.content = ForgetPresuppositions.PresupContent.nonModal

Finite CP: pre-existence satisfied → non-modal presupposition. Matches: "forgot that she stopped" presupposes she stopped.

theorem Phenomena.Presupposition.Studies.White2014.preEx_correct_gerund : Semantics.Attitudes.PreExistence.needsModalInsertion ForgetPresuppositions.forget_gerund.frame = false ∧ ForgetPresuppositions.forget_gerund.content = ForgetPresuppositions.PresupContent.nonModal

Gerund: pre-existence satisfied → non-modal presupposition. Matches: "forgot stopping by" presupposes stopped. This is the case that refutes the MCA's overprediction.

theorem Phenomena.Presupposition.Studies.White2014.preEx_correct_infinitival : Semantics.Attitudes.PreExistence.needsModalInsertion ForgetPresuppositions.forget_infinitival.frame = true ∧ ForgetPresuppositions.forget_infinitival.content = ForgetPresuppositions.PresupContent.modal

Plain infinitive: pre-existence NOT satisfied → modal presupposition. Matches: "forgot to stop by" presupposes was supposed to stop.

theorem Phenomena.Presupposition.Studies.White2014.preEx_matches_all_data : (ForgetPresuppositions.allForgetJudgments.all fun (j : ForgetPresuppositions.ForgetJudgment) => (j.content == ForgetPresuppositions.PresupContent.modal) == Semantics.Attitudes.PreExistence.needsModalInsertion j.frame) = true

Aggregate: the pre-existence theory matches all data points. Modal content arises iff modal insertion is needed.

The Modalized Complement Analysis predicts modal presuppositions for ALL non-finite complements. This overgenerates for gerunds: "forgot stopping by" has a non-modal presupposition.

theorem Phenomena.Presupposition.Studies.White2014.mca_wrong_on_gerund : Semantics.Attitudes.PreExistence.mcaPrediction ForgetPresuppositions.forget_gerund.frame = true ∧ ForgetPresuppositions.forget_gerund.content = ForgetPresuppositions.PresupContent.nonModal

MCA wrongly predicts a modal presupposition for the gerund case.

theorem Phenomena.Presupposition.Studies.White2014.mca_correct_finiteCP : Semantics.Attitudes.PreExistence.mcaPrediction ForgetPresuppositions.forget_finiteCP.frame = false

MCA correctly handles the finite case.

theorem Phenomena.Presupposition.Studies.White2014.mca_correct_infinitival : Semantics.Attitudes.PreExistence.mcaPrediction ForgetPresuppositions.forget_infinitival.frame = true

MCA correctly handles the infinitival case.

theorem Phenomena.Presupposition.Studies.White2014.mca_score : (List.filter (fun (j : ForgetPresuppositions.ForgetJudgment) => (j.content == ForgetPresuppositions.PresupContent.modal) == Semantics.Attitudes.PreExistence.mcaPrediction j.frame) ForgetPresuppositions.allForgetJudgments).length = 2

MCA matches only 2 of 3 data points; pre-existence matches all 3.

theorem Phenomena.Presupposition.Studies.White2014.preEx_score : (List.filter (fun (j : ForgetPresuppositions.ForgetJudgment) => (j.content == ForgetPresuppositions.PresupContent.modal) == Semantics.Attitudes.PreExistence.needsModalInsertion j.frame) ForgetPresuppositions.allForgetJudgments).length = 3

The English Fragment has two entries for forget: - forget (implicative, infinitival complement): "forgot to VP" - forget_rog (factive/rogative, finite complement): "forgot that p"

Un@cite{ippolito-kiss-williams-2025}, these are NOT two distinct lexical items but
one verb with uniform factivity. The Fragment's split is a practical
choice: it separates the implicative entailment pattern (forgot to VP
→ didn't VP) from the rogative/factive pattern (forgot that p / forgot
whether p). Williams's pre-existence analysis explains why these two
uses surface differently without positing lexical ambiguity. 

theorem Phenomena.Presupposition.Studies.White2014.forget_rog_is_factive : Fragments.English.Predicates.Verbal.forget_rog.factivePresup = true

The factive entry (forget_rog) has factivePresup = true.

theorem Phenomena.Presupposition.Studies.White2014.forget_takes_infinitival : Fragments.English.Predicates.Verbal.forget.complementType = Core.Verbs.ComplementType.infinitival

The implicative entry takes infinitival complements.

theorem Phenomena.Presupposition.Studies.White2014.forget_rog_takes_finite : Fragments.English.Predicates.Verbal.forget_rog.complementType = Core.Verbs.ComplementType.finiteClause

The factive entry takes finite complements.

theorem Phenomena.Presupposition.Studies.White2014.forget_rog_satisfies_preExistence : Semantics.Attitudes.PreExistence.satisfiesPreExistence Fragments.English.Predicates.Verbal.forget_rog.complementType = true

The factive entry's primary complement satisfies pre-existence.

theorem Phenomena.Presupposition.Studies.White2014.forget_inf_violates_preExistence : Semantics.Attitudes.PreExistence.satisfiesPreExistence Fragments.English.Predicates.Verbal.forget.complementType = false

The implicative entry's complement does NOT satisfy pre-existence. This is why the modal is inserted, yielding the obligation reading.

Basic verification that ComplementType.isFinite classifies correctly. These hold independently of any theory of factivity.

theorem Phenomena.Presupposition.Studies.White2014.finiteClause_isFinite : Core.Verbs.ComplementType.finiteClause.isFinite = true

theorem Phenomena.Presupposition.Studies.White2014.question_isFinite : Core.Verbs.ComplementType.question.isFinite = true

theorem Phenomena.Presupposition.Studies.White2014.infinitival_not_finite : Core.Verbs.ComplementType.infinitival.isFinite = false

theorem Phenomena.Presupposition.Studies.White2014.gerund_not_finite : Core.Verbs.ComplementType.gerund.isFinite = false