[SB24]: Cataphoric resolution of projective content — occasion verbs

[SB24] [TBRS13] [TBD18] [Hei83] [Sch08d] [Sch09a]

Three rating experiments (S&P 17:11) establish occasion verbs (German bestrafen "punish", kritisieren "criticise", danken "thank", …) as a new class of projective-content trigger. Occasion verbs are interpersonal action verbs whose agent acts in response to a presupposed prior eventuality — the occasion. "The judge punished Peter" asserts a punishing action and presupposes that Peter did something wrong.

This file formalizes the paper's structural claims, not its statistics:

• Projectivity (Exps 1–2, Block 2): occasion verbs pattern with established triggers — high projectivity, low at-issueness — and separate from psych verbs. The per-expression means feed Generalizations.Projectivity (see below).
• Cataphoric resolution (Exps 1–2, Block 1): occasion verbs are felicitous in both m-anaphoric and m-cataphoric contexts (the resolving material may precede or follow the trigger). This is unique to occasion verbs among the triggers tested. Effect sizes (e.g. neutral→anaphoric β ≈ 22, neutral→cataphoric β ≈ 18 on the 0–100 scale, both p < .001) are reported in prose, per project convention; the qualitative claim is encoded by ContextPolarity.
• Symmetric filtering (Exp 3): in conjoined conditional antecedents, occasion verbs filter regardless of conjunct order (trigger-first ≈ trigger-last, |t| ≈ 1), whereas factive/aspectual ([MZRS20]) triggers filter only left-to-right (trigger-last ≪ trigger-first, |t| ≈ 16). Encoded by FilteringDirection.

Tonhauser et al. (2013) classification

Occasion verbs are Class C (SCF=no, OLE=yes), with factives (know) and change-of-state verbs (stop), but are distinguished by bidirectional context resolution and symmetric filtering — "a cage of their own".

Main declarations

• FilteringDirection, ContextPolarity — the typed axes that encode the cataphoric-resolution and symmetric-filtering findings.
• occasionVerbProfile vs factiveProfile — cage_of_their_own proves they differ despite sharing Class C.
• occasionEventPhase, symmetricLocalCtxAntecedent — the presupposition as an EventPhase and the Heim/Schlenker filtering models.
• gpp_underpredicts_above_diagonal — occasion verbs project above the GPP diagonal (the mirror of [TBD18]'s establish).

Filtering direction and context resolution

inductive SolstadBott2024.FilteringDirection : Type

Filtering direction for presupposition triggers. [SB24] Exp 3 shows occasion verbs allow symmetric filtering, while factives and change-of-state verbs only allow left-to-right filtering.

• leftToRight : FilteringDirection
• symmetric : FilteringDirection

@[instance_reducible]

instance SolstadBott2024.instDecidableEqFilteringDirection : DecidableEq FilteringDirection

Equations

• SolstadBott2024.instDecidableEqFilteringDirection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def SolstadBott2024.instReprFilteringDirection.repr : FilteringDirection → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SolstadBott2024.instReprFilteringDirection : Repr FilteringDirection

Equations

• SolstadBott2024.instReprFilteringDirection = { reprPrec := SolstadBott2024.instReprFilteringDirection.repr }

inductive SolstadBott2024.ContextPolarity : Type

Context-resolution direction, refining [TBRS13]'s "m-positive" by where the resolving material can appear.

• mNeutral : ContextPolarity
• mAnaphoric : ContextPolarity
• mCataphoric : ContextPolarity

@[instance_reducible]

instance SolstadBott2024.instDecidableEqContextPolarity : DecidableEq ContextPolarity

Equations

• SolstadBott2024.instDecidableEqContextPolarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance SolstadBott2024.instReprContextPolarity : Repr ContextPolarity

Equations

• SolstadBott2024.instReprContextPolarity = { reprPrec := SolstadBott2024.instReprContextPolarity.repr }

def SolstadBott2024.instReprContextPolarity.repr : ContextPolarity → ℕ → Std.Format

Equations

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

Occasion verbs are Class C triggers

theorem SolstadBott2024.occasion_verb_is_classC : Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.occasion_verb.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC

Occasion verbs are Class C in the [TBRS13] taxonomy: SCF=no (can be informative), OLE=yes (attributed to attitude holder).

theorem SolstadBott2024.classC_no_scf : Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC.scf = Semantics.Presupposition.ProjectiveContent.StrongContextualFelicity.noRequires

Class C triggers do not require prior establishment in context.

theorem SolstadBott2024.classC_has_ole : Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classC.ole = Semantics.Presupposition.ProjectiveContent.ObligatoryLocalEffect.obligatory

Class C triggers have obligatory local effect under belief embedding.

theorem SolstadBott2024.occasion_verb_patterns_with_stop_know : Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.occasion_verb.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.stop_prestate.toClass ∧ Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.occasion_verb.toClass = Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.know_complement.toClass

Occasion verbs pattern with stop and know — all Class C.

German occasion-verb inventory

def SolstadBott2024.occasionVerbEntries : List German.Predicates.GermanVerbEntry

The 16 German occasion verbs tested in [SB24], derived from Fragment entries with the .occasion sense tag.

Equations

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

theorem SolstadBott2024.occasion_verb_count : occasionVerbEntries.length = 16

16 occasion verbs were tested.

theorem SolstadBott2024.all_occasion_entries_tagged : (occasionVerbEntries.all fun (x : German.Predicates.GermanVerbEntry) => x.senseTag == SenseTag.occasion) = true

All entries in the occasion-verb list use the .occasion sense tag.

theorem SolstadBott2024.all_occasion_entries_soft_trigger : (occasionVerbEntries.all fun (x : German.Predicates.GermanVerbEntry) => x.presupType == some PresupTriggerType.softTrigger) = true

All entries in the occasion-verb list are soft presupposition triggers.

"A cage of their own"

The cataphoric-resolution and symmetric-filtering findings are encoded as typed profile fields, so the paper's qualitative result — occasion verbs differ from factives despite sharing Class C — is a theorem about the profiles rather than a threshold on regression estimates.

structure SolstadBott2024.TriggerProfile : Type

Profile of a trigger across the dimensions tested by [SB24].

• projectiveClass : Semantics.Presupposition.ProjectiveContent.ProjectiveClass
• contextPolarities : List ContextPolarity
• filteringDirection : FilteringDirection

def SolstadBott2024.instDecidableEqTriggerProfile.decEq (x✝ x✝¹ : TriggerProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance SolstadBott2024.instDecidableEqTriggerProfile : DecidableEq TriggerProfile

Equations

• SolstadBott2024.instDecidableEqTriggerProfile = SolstadBott2024.instDecidableEqTriggerProfile.decEq

@[instance_reducible]

instance SolstadBott2024.instReprTriggerProfile : Repr TriggerProfile

Equations

• SolstadBott2024.instReprTriggerProfile = { reprPrec := SolstadBott2024.instReprTriggerProfile.repr }

def SolstadBott2024.instReprTriggerProfile.repr : TriggerProfile → ℕ → Std.Format

Equations

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

def SolstadBott2024.occasionVerbProfile : TriggerProfile

Occasion verbs: Class C, bidirectional (anaphoric + cataphoric) resolution, symmetric filtering.

Equations

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

def SolstadBott2024.factiveProfile : TriggerProfile

Factives/aspectuals: Class C, no SCF constraint (neutral ≈ anaphoric in Exp 1), left-to-right filtering only ([MZRS20]).

Equations

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

theorem SolstadBott2024.same_projective_class : occasionVerbProfile.projectiveClass = factiveProfile.projectiveClass

Occasion verbs share Class C with factives.

theorem SolstadBott2024.cage_of_their_own : occasionVerbProfile ≠ factiveProfile

Despite sharing Class C, occasion verbs differ from factives — the "cage of their own" result.

theorem SolstadBott2024.distinguished_by_filtering_not_class : occasionVerbProfile.filteringDirection ≠ factiveProfile.filteringDirection ∧ occasionVerbProfile.contextPolarities ≠ factiveProfile.contextPolarities

The distinguishing features are filtering direction and bidirectional resolution, not the projective class.

Occasion-verb presupposition as EventPhase

def SolstadBott2024.occasionEventPhase {W : Type u_1} (occasion engagement outcome : W → Prop) : EventPhase W

Model an occasion verb's presupposition as an EventPhase. "The judge punished Peter": precondition = Peter did something wrong (the occasion); eventOccurs = the punishing action; consequence = Peter is punished. The precondition projects.

Equations

• SolstadBott2024.occasionEventPhase occasion engagement outcome = { precondition := occasion, eventOccurs := engagement, consequence := outcome }

theorem SolstadBott2024.occasion_presup_projects {W : Type u_1} (occasion engagement outcome : W → Prop) : (Semantics.Presupposition.Aboutness.affirmative (occasionEventPhase occasion engagement outcome)).presupposition = (Semantics.Presupposition.Aboutness.negative (occasionEventPhase occasion engagement outcome)).presupposition

The occasion presupposition projects through negation: "The judge didn't punish Peter" still presupposes Peter did something wrong.

Asymmetric filtering ([Hei83])

theorem SolstadBott2024.heim_antecedent_projects {W : Type u_1} (c : CommonGround.ContextSet W) (trigger _consequence : Semantics.Presupposition.PartialProp W) (h : ∃ (w : W), c w ∧ ¬trigger.presup w) : Semantics.Presupposition.Context.presupProjects c trigger

Under Heim's asymmetric filtering, the local context at a conditional antecedent is the global context, so an occasion verb there projects. "If the judge punishes Peter, he was convicted": at "punishes" the presupposition is not entailed → projects.

Symmetric filtering ([Sch08d], [Sch09a])

def SolstadBott2024.symmetricLocalCtxAntecedent {W : Type u_1} (c : CommonGround.ContextSet W) (consequent : Semantics.Presupposition.PartialProp W) : CommonGround.ContextSet W

Symmetric filtering makes the consequent's assertion available to the local context at the antecedent.

Equations

• SolstadBott2024.symmetricLocalCtxAntecedent c consequent = c.update consequent.assertion

theorem SolstadBott2024.symmetric_filters_when_consequent_entails {W : Type u_1} (c : CommonGround.ContextSet W) (trigger consequent : Semantics.Presupposition.PartialProp W) (h : ∀ (w : W), c w → consequent.assertion w → trigger.presup w) : Semantics.Presupposition.Context.presupSatisfied (symmetricLocalCtxAntecedent c consequent) trigger

When the consequent entails the occasion presupposition, symmetric filtering predicts it is filtered.

Bridge to [SB22]

Occasion verbs are the agent-evocator class of [SB22]: the same underspecified eventuality that drives the NP2 implicit-causality bias is the projecting occasion. The IC bias and the presupposition are distinct — occasion verbs and experiencer-stimulus psych verbs share the NP2 bias, yet occasion verbs are far more projective (Exp 2: .69 vs .52; see the prediction section).

theorem SolstadBott2024.occasion_is_agent_evocator_bias : SolstadBott2022.VerbClass.agentEvocator.predictedBias = SolstadBott2022.ICBias.np2

Occasion verbs are the agent-evocator class; their predicted IC bias is NP2.

theorem SolstadBott2024.ic_bias_shared_with_expStim : SolstadBott2022.VerbClass.agentEvocator.predictedBias = SolstadBott2022.VerbClass.expStim.predictedBias

IC bias and projectivity dissociate: occasion verbs share the NP2 bias with experiencer-stimulus psych verbs, yet (by the Exp 2 data pooled in Generalizations.Projectivity) project more strongly. The shared bias is structural; the projectivity gap is empirical.

Predicting against the data

The Exp 1–2 projectivity/at-issueness means are artifact-sourced rows in Data.Examples.SolstadBott2024, pooled into Generalizations.Projectivity.allData alongside [TBD18]. Occasion verbs (proj .79/.69, at-issueness .32/.35) sit in the high-projectivity / low-at-issueness quadrant — patterning with established triggers and above the GPP diagonal (they project more than their at-issueness predicts, the mirror of establish). Psychological verbs (SE .54/.52, ES .52/.46) are midrange, off the GPP pattern. These per-row facts are computed over allData; the provable content is the account's systematic error.

theorem SolstadBott2024.gpp_underpredicts_above_diagonal (d : Generalizations.Projectivity.ProjectionDatum) (h : ↑d.notAtIssueness < ↑d.projectivity) : ↑(TonhauserBeaverDegen2018.gppProjection d.atIssueness) < ↑d.projectivity

Content that projects above its not-at-issueness — occasion verbs — is under-predicted by the GPP's tight reading (gppProjection). The mirror of [TBD18]'s below-diagonal establish.