Preconditions and Projection: Explaining Non-Anaphoric Presupposition

[RS24b]

Roberts, C. & Simons, M. (2024). Preconditions and projection: Explaining non-anaphoric presupposition. Linguistics and Philosophy 47(4):703–748.

Key Claims

1. The projective contents of CoS predicates, factives, and selectional restrictions are entailments characterizing ontological preconditions of the associated event type — NOT semantically encoded presuppositions.

2. Projection is a pragmatic default: a speaker who raises an event is taken to assume its preconditions hold (maximizes informativity, per [QGL16] and [War22]).

3. Differential suppression across verb pairs (know/discover, stop/continue) follows from lexical semantic differences (telicity, aspect, CoS status), not from different presupposition "strengths."

4. Filtering in Karttunen environments (conjunction, conditional, disjunction) is explained pragmatically without anaphoric constraints. For disjunction, the account predicts symmetric filtering (contra [Hei83]).

Connection to Existing Theory

This study file imports and bridges:

• Semantics.Events.Phase / Presupposition.Aboutness (EventPhase, entailment classification)
• ChangeOfState.Theory (CoS presuppositions)
• Features.Aktionsart (Vendler classes, telicity)
• ProjectiveContent (Tonhauser taxonomy: all three verb classes are Class C)

Verb classes as event phases

The paper's three verb classes instantiated as EventPhases: CoS predicates, factives, and selectional restrictions, each with complement truth or prior state as ontological precondition.

def RobertsSimons2024.stopAsEventPhase {W : Type u_1} (P : W → Prop) : EventPhase W

"Stop P" as an event phase.

Equations

• RobertsSimons2024.stopAsEventPhase P = { precondition := P, eventOccurs := P, consequence := fun (w : W) => ¬P w }

def RobertsSimons2024.startAsEventPhase {W : Type u_1} (P : W → Prop) : EventPhase W

"Start P" as an event phase.

Equations

• RobertsSimons2024.startAsEventPhase P = { precondition := fun (w : W) => ¬P w, eventOccurs := fun (w : W) => ¬P w, consequence := P }

def RobertsSimons2024.continueAsEventPhase {W : Type u_1} (P : W → Prop) : EventPhase W

"Continue P" as an event phase.

Equations

• RobertsSimons2024.continueAsEventPhase P = { precondition := P, eventOccurs := P, consequence := P }

theorem RobertsSimons2024.stop_precondition_is_presup {W : Type u_1} (P : W → Prop) : (stopAsEventPhase P).precondition = Features.ChangeOfState.priorStatePresup Features.ChangeOfState.CoSType.cessation P

Event-phase precondition = the CoS presupposition of Features.ChangeOfState, per CoS type.

theorem RobertsSimons2024.start_precondition_is_presup {W : Type u_1} (P : W → Prop) : (startAsEventPhase P).precondition = Features.ChangeOfState.priorStatePresup Features.ChangeOfState.CoSType.inception P

theorem RobertsSimons2024.continue_precondition_is_presup {W : Type u_1} (P : W → Prop) : (continueAsEventPhase P).precondition = Features.ChangeOfState.priorStatePresup Features.ChangeOfState.CoSType.continuation P

theorem RobertsSimons2024.stop_consequence_is_assertion {W : Type u_1} (P : W → Prop) : (stopAsEventPhase P).consequence = Features.ChangeOfState.resultStateAssertion Features.ChangeOfState.CoSType.cessation P

Event-phase consequence = the CoS assertion, per CoS type.

theorem RobertsSimons2024.start_consequence_is_assertion {W : Type u_1} (P : W → Prop) : (startAsEventPhase P).consequence = Features.ChangeOfState.resultStateAssertion Features.ChangeOfState.CoSType.inception P

theorem RobertsSimons2024.continue_consequence_is_assertion {W : Type u_1} (P : W → Prop) : (continueAsEventPhase P).consequence = Features.ChangeOfState.resultStateAssertion Features.ChangeOfState.CoSType.continuation P

theorem RobertsSimons2024.stop_is_telic {W : Type u_1} (P : W → Prop) (w : W) (hP : P w) : (stopAsEventPhase P).precondition w ≠ (stopAsEventPhase P).consequence w

"Stop P" is telic: state changes from P to ¬P.

theorem RobertsSimons2024.start_is_telic {W : Type u_1} (P : W → Prop) (w : W) (hNotP : ¬P w) : (startAsEventPhase P).precondition w ≠ (startAsEventPhase P).consequence w

"Start P" is telic: state changes from ¬P to P.

theorem RobertsSimons2024.continue_is_atelic {W : Type u_1} (P : W → Prop) : (continueAsEventPhase P).isAtelic

"Continue P" is atelic: a precondition (prior activity) but no state change ([RS24b] p. 734).

def RobertsSimons2024.knowAsEventPhase {W : Type u_1} (BEL C : W → Prop) : EventPhase W

"Know C" as an event phase: stative, atelic. Precondition: C is true. The knowing state cannot exist without its object.

Equations

• RobertsSimons2024.knowAsEventPhase BEL C = { precondition := C, eventOccurs := fun (w : W) => BEL w ∧ C w, consequence := C }

def RobertsSimons2024.discoverAsEventPhase {W : Type u_1} (IGNORANT C : W → Prop) : EventPhase W

"Discover C" as an event phase: telic, achievement. Two preconditions: C is true AND the agent was previously ignorant.

Equations

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

def RobertsSimons2024.regretAsEventPhase {W : Type u_1} (BEL : W → Prop) : EventPhase W

"Regret p" as an event phase: emotive factive. The ontological precondition is belief, not truth — factivity arises from a pragmatic default to veridicality ([RS24b] p. 731).

Equations

• RobertsSimons2024.regretAsEventPhase BEL = { precondition := BEL, eventOccurs := BEL, consequence := BEL }

theorem RobertsSimons2024.know_is_atelic {W : Type u_1} (BEL C : W → Prop) : (knowAsEventPhase BEL C).isAtelic

Know is atelic: no state change (precondition = consequence).

theorem RobertsSimons2024.regret_is_atelic {W : Type u_1} (BEL : W → Prop) : (regretAsEventPhase BEL).isAtelic

Regret is atelic: the emotive state persists with its grounding belief.

theorem RobertsSimons2024.discover_is_telic {W : Type u_1} (IGNORANT C : W → Prop) (w : W) (hC : C w) (hIgn : IGNORANT w) : (discoverAsEventPhase IGNORANT C).precondition w ≠ (discoverAsEventPhase IGNORANT C).consequence w

Discover is telic: state change from ignorant to knowing.

theorem RobertsSimons2024.factive_precondition_entails_complement {W : Type u_1} (IGNORANT C : W → Prop) (w : W) : (discoverAsEventPhase IGNORANT C).precondition w → C w

Both know and discover have C as (part of) their precondition: complement truth is ontologically required.

theorem RobertsSimons2024.discover_precondition_requires_ignorance {W : Type u_1} (IGNORANT C : W → Prop) (w : W) : (discoverAsEventPhase IGNORANT C).precondition w → IGNORANT w

Discover's extra precondition (prior ignorance) explains its weaker projection in conditional antecedents ([RS24b] §3.2.2).

def RobertsSimons2024.selectionalEventPhase {W : Type u_1} (requirement event : W → Prop) : EventPhase W

A selectional restriction as an event phase: the requirement ("the robot has feet") is an ontological precondition of the event ("the robot kicked the tree"), confirmed by both §2.1 diagnostics.

Equations

• RobertsSimons2024.selectionalEventPhase requirement event = { precondition := requirement, eventOccurs := event, consequence := event }

Aspectual classification

def RobertsSimons2024.cosTypeToAspectualProfile : Features.ChangeOfState.CoSType → Features.AspectualProfile

Aspectual profile per CoS type: "stop"/"start" are achievements (telic, punctual); "continue" is an activity (atelic, durative).

Equations

• RobertsSimons2024.cosTypeToAspectualProfile Features.ChangeOfState.CoSType.cessation = Features.achievementProfile
• RobertsSimons2024.cosTypeToAspectualProfile Features.ChangeOfState.CoSType.inception = Features.achievementProfile
• RobertsSimons2024.cosTypeToAspectualProfile Features.ChangeOfState.CoSType.continuation = Features.activityProfile

def RobertsSimons2024.cosTypeToVendlerClass (t : Features.ChangeOfState.CoSType) : Features.VendlerClass

Vendler class per CoS type, derived from the aspectual profile.

Equations

• RobertsSimons2024.cosTypeToVendlerClass t = (RobertsSimons2024.cosTypeToAspectualProfile t).toVendlerClass

theorem RobertsSimons2024.cos_vendler_telicity_correct (t : Features.ChangeOfState.CoSType) : (cosTypeToVendlerClass t).telicity = match t with | Features.ChangeOfState.CoSType.cessation => Features.Telicity.telic | Features.ChangeOfState.CoSType.inception => Features.Telicity.telic | Features.ChangeOfState.CoSType.continuation => Features.Telicity.atelic

The derived Vendler classes carry the right telicity.

The assertion-only rival

Under an assertion-only view a sentence is just its truth conditions — no event reference, no aboutness — so nothing forces affirmative and negative to share content, and single-index truth conditions cannot even represent a CoS verb.

structure RobertsSimons2024.AssertionOnlyMeaning (W : Type u_2) : Type u_2

The assertion-only meaning: bare truth conditions.

• truthConditions : W → Prop

def RobertsSimons2024.assertionOnly_stop {W : Type u_1} (P : W → Prop) : AssertionOnlyMeaning W

Under assertion-only, "stop P" flattens pre-state and post-state into one evaluation point: P ∧ ¬P.

Equations

• RobertsSimons2024.assertionOnly_stop P = { truthConditions := fun (w : W) => P w ∧ ¬P w }

def RobertsSimons2024.assertionOnly_notStop {W : Type u_1} (P : W → Prop) : AssertionOnlyMeaning W

Under assertion-only, "not stop P" is ¬(P ∧ ¬P) — a tautology.

Equations

• RobertsSimons2024.assertionOnly_notStop P = { truthConditions := fun (w : W) => ¬(P w ∧ ¬P w) }

theorem RobertsSimons2024.assertionOnly_stop_contradictory {W : Type u_1} (P : W → Prop) (w : W) : ¬(assertionOnly_stop P).truthConditions w

Single-index truth conditions cannot represent CoS verbs: the assertion-only "stop" is contradictory at every world.

theorem RobertsSimons2024.assertionOnly_no_presupposition {W : Type u_1} (P : W → Prop) (w : W) (_hNotP : ¬P w) : (assertionOnly_notStop P).truthConditions w

Under assertion-only, the negated sentence is true even where P fails, so "John didn't stop smoking" would not require that he smoked: the view has no presupposition.

Pragmatic suppression conditions

Projection of preconditions is a pragmatic default, not an invariant ([RS24b] §3.2.1).

inductive RobertsSimons2024.SuppressionCondition : Type

Contexts that suppress projection of a precondition: in each, pragmatic reasoning makes it implausible that the speaker presumes the precondition true.

• preconditionKnownFalse : SuppressionCondition

  Interlocutors know or believe the precondition is false or controversial ([RS24b] ex. 23).

• speakerNonCommitment : SuppressionCondition

  Evidence that the speaker does not believe the precondition ([RS24b] ex. 24).

• preconditionAtIssue : SuppressionCondition

  The precondition is at-issue, i.e. currently under discussion ([RS24b] ex. 25).

@[instance_reducible]

instance RobertsSimons2024.instDecidableEqSuppressionCondition : DecidableEq SuppressionCondition

Equations

• RobertsSimons2024.instDecidableEqSuppressionCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance RobertsSimons2024.instReprSuppressionCondition : Repr SuppressionCondition

Equations

• RobertsSimons2024.instReprSuppressionCondition = { reprPrec := RobertsSimons2024.instReprSuppressionCondition.repr }

def RobertsSimons2024.instReprSuppressionCondition.repr : SuppressionCondition → ℕ → Std.Format

Equations

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

def RobertsSimons2024.SuppressionCondition.globalProjection : SuppressionCondition → Bool

Under any suppression condition, precondition content is merely locally entailed, not globally accommodated.

Equations

• x✝.globalProjection = false

theorem RobertsSimons2024.precondition_projects_consequence_doesnt : Semantics.Presupposition.Aboutness.EntailmentRelation.precondition.projects = true ∧ Semantics.Presupposition.Aboutness.EntailmentRelation.consequence.projects = false ∧ Semantics.Presupposition.Aboutness.EntailmentRelation.concomitant.projects = false

The theory predicts the empirical pattern: preconditions project, consequences don't.

theorem RobertsSimons2024.know_atelic {W : Type u_2} (BEL C : W → Prop) : (knowAsEventPhase BEL C).isAtelic

Know is atelic: precondition = consequence (stative, no change).

theorem RobertsSimons2024.discover_telic {W : Type u_2} (IGNORANT C : W → Prop) (w : W) (hC : C w) (hIgn : IGNORANT w) : (discoverAsEventPhase IGNORANT C).isTelic

Discover is telic: precondition ≠ consequence (state change).

theorem RobertsSimons2024.know_discover_both_factive {W : Type u_2} (BEL IGNORANT C : W → Prop) (w : W) : (knowAsEventPhase BEL C).precondition w = C w ∧ ((discoverAsEventPhase IGNORANT C).precondition w → C w)

Both share factivity: complement truth is a precondition.

theorem RobertsSimons2024.discover_has_ignorance_precondition {W : Type u_2} (IGNORANT C : W → Prop) (w : W) : (discoverAsEventPhase IGNORANT C).precondition w → IGNORANT w

Discover has an additional precondition (ignorance) that know lacks. This is the source of differential suppression: the ignorance precondition creates a context in which the speaker signals uncertainty about C.

theorem RobertsSimons2024.stop_telic {W : Type u_2} (P : W → Prop) (w : W) (hP : P w) : (stopAsEventPhase P).isTelic

Stop is telic: involves a state change.

theorem RobertsSimons2024.continue_atelic {W : Type u_2} (P : W → Prop) : (continueAsEventPhase P).isAtelic

Continue is atelic: no state change.

theorem RobertsSimons2024.stop_continue_same_precondition {W : Type u_2} (P : W → Prop) : (stopAsEventPhase P).precondition = (continueAsEventPhase P).precondition

Stop and continue share the same precondition (prior activity P).

theorem RobertsSimons2024.stop_continue_telicity_differs : cosTypeToVendlerClass Features.ChangeOfState.CoSType.cessation ≠ cosTypeToVendlerClass Features.ChangeOfState.CoSType.continuation

But they differ in telicity: stop is telic, continue is atelic.

theorem RobertsSimons2024.selectional_projects_through_negation {W : Type u_2} (req event : W → Prop) (pol : Features.Polarity) : { eventType := selectionalEventPhase req event, polarity := pol }.presupposition = req

Selectional preconditions project through negation. "The robot didn't kick the tree" still implies it has feet.

def RobertsSimons2024.conjunctionFiltering {W : Type u_2} (P : W → Prop) : Prop

In a conjunction "P, and (stop P)", the first conjunct asserts the precondition. R&S: it is pragmatically implausible that the speaker presumes the precondition — they are explicitly asserting it.

Equations

• RobertsSimons2024.conjunctionFiltering P = ∀ (w : W), P w ∧ (RobertsSimons2024.stopAsEventPhase P).eventOccurs w → (RobertsSimons2024.stopAsEventPhase P).precondition w

theorem RobertsSimons2024.conjunction_entails_precondition {W : Type u_2} (P : W → Prop) : conjunctionFiltering P

def RobertsSimons2024.conditionalFiltering {W : Type u_2} (P : W → Prop) : Prop

In a conditional "If P, then stop P", the antecedent supposes P. R&S: the conditional structure itself signals the speaker's lack of commitment to the antecedent, and the function of the conditional is to evaluate the consequent relative to the antecedent. No global presumption of P is pragmatically attributable.

Equations

• RobertsSimons2024.conditionalFiltering P = ∀ (w : W), P w → (RobertsSimons2024.stopAsEventPhase P).precondition w

theorem RobertsSimons2024.conditional_entails_precondition {W : Type u_2} (P : W → Prop) : conditionalFiltering P

def RobertsSimons2024.symmetricDisjunctionFiltering : Prop

R&S's distinctive prediction for disjunction ([RS24b] §4): filtering in disjunction is symmetric for non-anaphoric triggers.

"Either Jane never smoked, or she's stopped." (43)

The first disjunct (¬P) creates a context in which it is reasonable to consider the second disjunct's precondition (P) as locally entailed (if ¬P is false, i.e. P is true). Crucially, R&S argue this filtering works identically in both orders — contra [Hei83]'s asymmetric account.

This is a pragmatic consequence of their view: filtering depends on whether global presumption of the precondition is pragmatically attributable, not on dynamic left-to-right context update.

Equations

• RobertsSimons2024.symmetricDisjunctionFiltering = True

theorem RobertsSimons2024.cos_eventphase_agrees_with_prprop {W : Type u_2} (t : Features.ChangeOfState.CoSType) (P : W → Prop) : (match t with | Features.ChangeOfState.CoSType.cessation => stopAsEventPhase P | Features.ChangeOfState.CoSType.inception => startAsEventPhase P | Features.ChangeOfState.CoSType.continuation => continueAsEventPhase P).precondition = (Features.ChangeOfState.cosSemantics t P).presup

For CoS verbs, EventPhase.precondition agrees with PartialProp.presup. This shows the two representations — the aboutness-based (R&S) and the trivalent (Heim) — agree on what projects, even though they disagree on why it projects.

theorem RobertsSimons2024.presupposition_derivable_from_event_structure (isFactive hasCosType : Bool) : (isFactive || hasCosType) = true ↔ isFactive = true ∨ hasCosType = true

R&S argue that presupposition status follows from event structure, not from a stipulated presupType. A verb presupposes its complement iff it has factivity or CoS event structure. The derivedPresupType accessor on Verb implements this derivation.

theorem RobertsSimons2024.suppression_preserves_entailment (s : SuppressionCondition) : s.globalProjection = false

Suppression does not change what is entailed — only what is presumed.

theorem RobertsSimons2024.stop_end_to_end {W : Type u_2} (P : W → Prop) (w : W) : (stopAsEventPhase P).precondition w = P w ∧ (Semantics.Presupposition.Aboutness.affirmative (stopAsEventPhase P)).presupposition w = P w ∧ (Semantics.Presupposition.Aboutness.affirmative (stopAsEventPhase P)).presupposition w = (Semantics.Presupposition.Aboutness.negative (stopAsEventPhase P)).presupposition w ∧ ((Semantics.Presupposition.Aboutness.negative (stopAsEventPhase P)).assertion w ↔ ¬(Semantics.Presupposition.Aboutness.affirmative (stopAsEventPhase P)).assertion w) ∧ Semantics.Presupposition.Aboutness.EntailmentRelation.precondition.projects = true ∧ Semantics.Presupposition.Aboutness.EntailmentRelation.consequence.projects = false

End-to-end: for "stop P", the full chain from event structure to projection prediction. The precondition (prior state P) is invariant across both polarities, while the consequence (¬P) flips.

theorem RobertsSimons2024.know_end_to_end {W : Type u_2} (BEL C : W → Prop) (w : W) : (knowAsEventPhase BEL C).precondition w = C w ∧ (Semantics.Presupposition.Aboutness.affirmative (knowAsEventPhase BEL C)).presupposition w = C w ∧ (Semantics.Presupposition.Aboutness.affirmative (knowAsEventPhase BEL C)).presupposition w = (Semantics.Presupposition.Aboutness.negative (knowAsEventPhase BEL C)).presupposition w ∧ (knowAsEventPhase BEL C).isAtelic

End-to-end for factives: know's complement truth is an ontological precondition, shares the same structural projection mechanism as CoS verbs, and agrees with the PartialProp representation.

theorem RobertsSimons2024.selectional_end_to_end {W : Type u_2} (req event : W → Prop) (w : W) : (selectionalEventPhase req event).precondition w = req w ∧ (Semantics.Presupposition.Aboutness.affirmative (selectionalEventPhase req event)).presupposition w = req w ∧ (Semantics.Presupposition.Aboutness.affirmative (selectionalEventPhase req event)).presupposition w = (Semantics.Presupposition.Aboutness.negative (selectionalEventPhase req event)).presupposition w

End-to-end for selectional restrictions: same aboutness mechanism, same projection behavior, same structural explanation.