Documentation

Linglib.Theories.Semantics.Attitudes.PreExistence

Pre-Existence and Modal Insertion in Factive Complements #

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

@cite{ippolito-kiss-williams-2026} argues that the distribution of the covert modal in non-finite complements of forget is governed by the pre-existence presupposition.

Pre-Existence #

Pre-existence says: the lower event must have started before the attitude event. For forget: the event of forgetting must be preceded by the start of whatever event the complement describes.

PreEx(Q)(e)(w) ≡ ∃(e'', t). Q(λe'. e'=e'')(t)(w) ∧ LB(τ(e'')) < LB(τ(e))

Temporal Satisfaction #

Whether a complement type inherently satisfies pre-existence depends on its temporal profile:

ComplementTemporal ProfileSatisfies PreEx?
Finite CPPast/present tense → event before/at matrixyes
PRO-ing gerundGerund aspect → event before/at matrixyes
Perfect infinitivePerfect → event before matrixyes
Plain infinitiveNo tense → forward-orientedno

When pre-existence is NOT inherently satisfied (plain infinitives), a covert modal (Mod) is inserted to shift the presupposition from "the event started" to "the obligation/plan started" — which DOES precede the forgetting.

SMINC Generalization #

Selectivity of Modal Insertion in Non-finite Contexts (@cite{ippolito-kiss-williams-2026}, p. 8, (15)): the covert modal Mod heads the complement of forget just in case the complement is a plain infinitive.

source
def Semantics.Attitudes.PreExistence.satisfiesPreExistence :
Core.Verbs.ComplementType → Bool

Does this complement type's temporal profile inherently satisfy the pre-existence presupposition?

Finite CPs and questions have tense morphology that locates the embedded event before or at the matrix event time. Gerunds have aspectual content that does the same. Plain infinitives lack both, so their embedded event is forward-oriented — violating pre-existence.

Note: this is a simplification. The paper's full analysis uses event semantics with temporal traces (LB(τ(e)) comparisons). This predicate captures the key prediction without the event-semantic machinery.

The current ComplementType does not distinguish perfect from plain infinitives. For English, .infinitival corresponds to the plain to-infinitive; the Spanish/Italian perfect infinitive would need a new constructor.

Equations
Instances For
    source
    def Semantics.Attitudes.PreExistence.needsModalInsertion (ct : Core.Verbs.ComplementType) :
    Bool

    Whether a factive verb's complement requires covert modal insertion to satisfy the pre-existence presupposition.

    Un@cite{ippolito-kiss-williams-2026}: Mod is inserted iff the complement type does not inherently satisfy pre-existence. This is the SMINC generalization (Selectivity of Modal Insertion in Non-finite Contexts).

    Equations
    Instances For
      source
      theorem Semantics.Attitudes.PreExistence.finiteClause_satisfies_preExistence :
      satisfiesPreExistence Core.Verbs.ComplementType.finiteClause = true

      Finite clauses satisfy pre-existence (tense locates event in past).

      source
      theorem Semantics.Attitudes.PreExistence.gerund_satisfies_preExistence :
      satisfiesPreExistence Core.Verbs.ComplementType.gerund = true

      Not all non-finite types violate pre-existence: gerunds satisfy it. This is the key prediction that distinguishes @cite{ippolito-kiss-williams-2026} from the Modalized Complement Analysis.

      source
      theorem Semantics.Attitudes.PreExistence.infinitival_violates_preExistence :
      satisfiesPreExistence Core.Verbs.ComplementType.infinitival = false

      Plain infinitives violate pre-existence.

      source
      theorem Semantics.Attitudes.PreExistence.sminc_infinitival_needs_modal :
      needsModalInsertion Core.Verbs.ComplementType.infinitival = true

      SMINC: modal insertion occurs with infinitivals but not gerunds.

      source
      theorem Semantics.Attitudes.PreExistence.sminc_gerund_no_modal :
      needsModalInsertion Core.Verbs.ComplementType.gerund = false
      source
      theorem Semantics.Attitudes.PreExistence.sminc_finite_no_modal :
      needsModalInsertion Core.Verbs.ComplementType.finiteClause = false
      source
      def Semantics.Attitudes.PreExistence.mcaPrediction (ct : Core.Verbs.ComplementType) :
      Bool

      The MCA predicts modal insertion for ALL non-finite complements. @cite{ippolito-kiss-williams-2026} shows this overgenerates: gerunds don't get modalized.

      Equations
      Instances For
        source
        theorem Semantics.Attitudes.PreExistence.mca_williams_agree_finite :
        mcaPrediction Core.Verbs.ComplementType.finiteClause = needsModalInsertion Core.Verbs.ComplementType.finiteClause

        MCA and Williams agree on finite complements: no modal.

        source
        theorem Semantics.Attitudes.PreExistence.mca_williams_agree_infinitival :
        mcaPrediction Core.Verbs.ComplementType.infinitival = needsModalInsertion Core.Verbs.ComplementType.infinitival

        MCA and Williams agree on plain infinitives: modal.

        source
        theorem Semantics.Attitudes.PreExistence.mca_williams_diverge_gerund :
        mcaPrediction Core.Verbs.ComplementType.gerund ≠ needsModalInsertion Core.Verbs.ComplementType.gerund

        MCA and Williams DIVERGE on gerunds: MCA predicts modal, Williams does not. The gerund case is the paper's central empirical argument against the MCA.

        source
        theorem Semantics.Attitudes.PreExistence.mca_overpredicts_gerund :
        mcaPrediction Core.Verbs.ComplementType.gerund = true ∧ needsModalInsertion Core.Verbs.ComplementType.gerund = false

        The divergence decomposed: MCA predicts modal for gerunds but pre-existence analysis correctly does not.