The aboutness account of projection

[RS24b]'s mechanism for non-anaphoric presupposition: sentences refer to event types (EventPhase); event types have inherent ontological preconditions; and "John stopped" and "John didn't stop" refer to the same event type — negation affects the claim about the event, not which event is referenced. Preconditions therefore project, because they are tied to event reference rather than to the polarity-dependent claim.

Main declarations

• EventSentence — a sentence as event reference (aboutness) plus a polarity-dependent claim (assertion); its presupposition is the precondition of the referenced event type, so projection through negation (presupposition_projects) holds by construction while assertions flip (assertion_differs).
• EntailmentRelation — precondition vs consequence vs concomitant; only preconditions project by pragmatic default (projects).

The paper's verb-class instances (CoS predicates, factives, selectional restrictions), aspectual classification, and suppression conditions live in Studies/RobertsSimons2024.lean.

structure Semantics.Presupposition.Aboutness.EventSentence (W : Type u_2) : Type u_2

A sentence that refers to an event type and makes a polarity-dependent claim about it.

• eventType : EventPhase W

  The event type this sentence is about

• polarity : Features.Polarity

  The polarity of the claim

def Semantics.Presupposition.Aboutness.EventSentence.aboutness {W : Type u_1} (s : EventSentence W) : EventPhase W

The aboutness of a sentence: the event type it refers to, independent of polarity.

Equations

• s.aboutness = s.eventType

def Semantics.Presupposition.Aboutness.EventSentence.assertion {W : Type u_1} (s : EventSentence W) : W → Prop

The claim made: affirmed sentences assert the consequence obtains, negated ones that it doesn't.

Equations

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

def Semantics.Presupposition.Aboutness.EventSentence.presupposition {W : Type u_1} (s : EventSentence W) : W → Prop

The presupposition comes from aboutness, not from the assertion: it is the precondition of the referenced event type.

Equations

• s.presupposition = s.aboutness.precondition

def Semantics.Presupposition.Aboutness.affirmative {W : Type u_1} (e : EventPhase W) : EventSentence W

An affirmative sentence about an event type.

Equations

• Semantics.Presupposition.Aboutness.affirmative e = { eventType := e, polarity := Features.Polarity.positive }

def Semantics.Presupposition.Aboutness.negative {W : Type u_1} (e : EventPhase W) : EventSentence W

A negative sentence about an event type.

Equations

• Semantics.Presupposition.Aboutness.negative e = { eventType := e, polarity := Features.Polarity.negative }

theorem Semantics.Presupposition.Aboutness.presupposition_projects {W : Type u_1} (e : EventPhase W) : (affirmative e).presupposition = (negative e).presupposition

Presuppositions project through negation: derived from aboutness, which affirmation and negation share.

theorem Semantics.Presupposition.Aboutness.assertion_differs {W : Type u_1} (e : EventPhase W) (w : W) : (negative e).assertion w ↔ ¬(affirmative e).assertion w

Assertions flip with polarity while presuppositions stay constant.

Entailment classification

inductive Semantics.Presupposition.Aboutness.EntailmentRelation : Type

Classification of entailment relations between a sentence and its implied content: only preconditions project ([RS24b] §2.1 diagnostics: "ψ, which is part of what allowed for φ" and the counterfactual "if not-ψ, φ would not have been possible").

• precondition : EntailmentRelation

  Temporally prior, enables the event. Projects by pragmatic default.

• consequence : EntailmentRelation

  Temporally posterior, results from the event. At-issue.

• concomitant : EntailmentRelation

  Mereological part or co-occurring state. At-issue. Example: "Jane shouted" entails "Jane made sound" — the sound-making is part of the shouting, not a precondition for it.

@[instance_reducible]

instance Semantics.Presupposition.Aboutness.instDecidableEqEntailmentRelation : DecidableEq EntailmentRelation

Equations

• Semantics.Presupposition.Aboutness.instDecidableEqEntailmentRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Semantics.Presupposition.Aboutness.instReprEntailmentRelation : Repr EntailmentRelation

Equations

• Semantics.Presupposition.Aboutness.instReprEntailmentRelation = { reprPrec := Semantics.Presupposition.Aboutness.instReprEntailmentRelation.repr }

def Semantics.Presupposition.Aboutness.instReprEntailmentRelation.repr : EntailmentRelation → Nat → Std.Format

Equations

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

def Semantics.Presupposition.Aboutness.EntailmentRelation.projects : EntailmentRelation → Bool

Only precondition entailments project by pragmatic default.

Equations

• Semantics.Presupposition.Aboutness.EntailmentRelation.precondition.projects = true
• Semantics.Presupposition.Aboutness.EntailmentRelation.consequence.projects = false
• Semantics.Presupposition.Aboutness.EntailmentRelation.concomitant.projects = false