Solstad & Bott (2024): Cataphoric Resolution of Projective Content: The Case of Occasion Verbs

An occasion verb such as gratulieren 'congratulate' implies that an eventuality before the agent's action gave the agent reason to act, the occasion. Solstad and Bott show in three rating experiments that the implication projects, that a sentence with an occasion verb is degraded unless another sentence supplies the occasion, and that the supporting sentence may follow the verb's sentence as well as precede it, where pronouns, demonstratives and auch 'too' need it to precede. In the antecedent of a conditional a conjoined clause entailing the occasion filters the implication from either side, where factive and aspectual triggers are filtered from the left only.

Main statements

• SolstadBott2024.strongContextualFelicity_iff: of the three constraints a trigger may place on the discourse around it, only the one demanding a preceding sentence is a strong contextual felicity constraint in the sense of Tonhauser, Beaver, Roberts and Simons.
• SolstadBott2024.contextTests_iff_licenses: a supported context differs reliably from the neutral one in the paper's tests exactly where the trigger's constraint is met.
• SolstadBott2024.Account.filters_iff: incremental local contexts and limited symmetry filter the implication only after the clause entailing it, symmetric local contexts on either side, and local accommodation everywhere.
• SolstadBott2024.fits_iff: of the four accounts only symmetric local contexts fit the occasion verbs of Experiment 3, and only the two asymmetric ones the factive and aspectual triggers.

Implementation notes

• A discourse is the information before and after the trigger's sentence, and a constraint is met in a context type when it holds whenever the supporting sentence entails the content.
• An antecedent is evaluated in the utterance context, without the conditional around it, and an account filters the implication when the antecedent is acceptable in every context.
• A test of Block 1 is reliable when its printed p is below .05, and a contrast of Experiment 3 when its printed t is at least 2 in absolute value, which agrees with the two tests the paper reports for that experiment (reliable_triggerLast_iff).
• The Block 1 means are recomputed from the authors' trial-level data. The Block 2 means of the established triggers are plotted only.

TODO

• The paper's suggestion that an occasion verb raises the question why the agent acted, which must be addressed before or after the verb, is not formalized.

References

• [SB24]
• [TBRS13]
• [TBD18]
• [MZRS20]
• [Sch09a]
• [Kal23]
• [SB22]

Contextual constraints

inductive SolstadBott2024.Felicity : Type

The constraint a trigger places on the discourse around its sentence. It places none, or it demands that what precedes entail the content, the strong contextual felicity of Tonhauser and colleagues, or that what precedes or what follows entail it, as occasion verbs do.

• free : Felicity
• strong : Felicity
• weak : Felicity

@[instance_reducible]

instance SolstadBott2024.instDecidableEqFelicity : DecidableEq Felicity

Equations

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

@[instance_reducible]

instance SolstadBott2024.instReprFelicity : Repr Felicity

Equations

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

def SolstadBott2024.instReprFelicity.repr : Felicity → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SolstadBott2024.instFintypeFelicity : Fintype Felicity

Equations

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

def SolstadBott2024.Felicity.Satisfied {W : Type u_1} (m before after : Set W) : Felicity → Prop

The constraint holds of the content m, given the information before and after the trigger's sentence.

Equations

• SolstadBott2024.Felicity.Satisfied m before after SolstadBott2024.Felicity.free = True
• SolstadBott2024.Felicity.Satisfied m before after SolstadBott2024.Felicity.strong = (before ⊆ m)
• SolstadBott2024.Felicity.Satisfied m before after SolstadBott2024.Felicity.weak = (before ⊆ m ∨ after ⊆ m)

def SolstadBott2024.Context.before {W : Type u_1} (p : Set W) : Context → Set W

The information before the trigger's sentence in a context type, where the supporting sentence has the content p.

Equations

• SolstadBott2024.Context.before p SolstadBott2024.Context.anaphoric = p
• SolstadBott2024.Context.before p x✝ = Set.univ

def SolstadBott2024.Context.after {W : Type u_1} (p : Set W) : Context → Set W

The information after the trigger's sentence in a context type.

Equations

• SolstadBott2024.Context.after p SolstadBott2024.Context.cataphoric = p
• SolstadBott2024.Context.after p x✝ = Set.univ

def SolstadBott2024.Felicity.Licenses (f : Felicity) (k : Context) : Prop

A constraint is met in a context type when it is satisfied whenever the supporting sentence entails the content.

Equations

• f.Licenses k = ∀ (W : Type) (m p : Set W), p ⊆ m → SolstadBott2024.Felicity.Satisfied m (SolstadBott2024.Context.before p k) (SolstadBott2024.Context.after p k) f

theorem SolstadBott2024.Felicity.licenses_iff {f : Felicity} {k : Context} : f.Licenses k ↔ f = free ∨ f = strong ∧ k = Context.anaphoric ∨ f = weak ∧ k ≠ Context.neutral

The strong constraint is met in an anaphoric context only, and the weak one in an anaphoric or a cataphoric context.

@[instance_reducible]

instance SolstadBott2024.instDecidableLicenses (f : Felicity) (k : Context) : Decidable (f.Licenses k)

Equations

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

theorem SolstadBott2024.strongContextualFelicity_iff {W : Type u_1} {f : Felicity} {m : Set W} : (TonhauserEtAl2013.StrongContextualFelicity m fun (b : Set W) => ∃ (a : Set W), Felicity.Satisfied m b a f) ↔ f = Felicity.strong ∨ m = Set.univ

Take a sentence acceptable wherever some continuation meets its constraint. It is acceptable only in contexts that entail the content, the strong contextual felicity of Tonhauser and colleagues, exactly when the constraint is the strong one or the content is trivial. The constraint of occasion verbs is therefore not one.

Anaphoric and cataphoric contexts (Block 1)

def SolstadBott2024.TriggerOne.felicity : TriggerOne → Felicity

The constraint the paper finds for a trigger type of Experiment 1.

Equations

• SolstadBott2024.TriggerOne.occasion.felicity = SolstadBott2024.Felicity.weak
• SolstadBott2024.TriggerOne.pronoun.felicity = SolstadBott2024.Felicity.strong
• SolstadBott2024.TriggerOne.demonstrative.felicity = SolstadBott2024.Felicity.strong
• x✝.felicity = SolstadBott2024.Felicity.free

def SolstadBott2024.TriggerTwo.felicity : TriggerTwo → Felicity

The constraint the paper finds for a trigger type of Experiment 2.

Equations

• SolstadBott2024.TriggerTwo.occasion.felicity = SolstadBott2024.Felicity.weak
• SolstadBott2024.TriggerTwo.too.felicity = SolstadBott2024.Felicity.strong
• x✝.felicity = SolstadBott2024.Felicity.free

theorem SolstadBott2024.contextTests_iff_licenses : (∀ r ∈ contextTestsExp1, r.p.toRat < 1 / 20 ↔ r.trigger.felicity.Licenses r.context) ∧ ∀ r ∈ contextTestsExp2, r.p.toRat < 1 / 20 ↔ r.trigger.felicity.Licenses r.context

In both experiments a supported context differs reliably from the neutral one exactly where the trigger's constraint is met. A following sentence helps occasion verbs and does not help pronouns, demonstratives or auch.

theorem SolstadBott2024.weak_of_occasion_tests (f : Felicity) : (∀ r ∈ contextTestsExp1, r.trigger = TriggerOne.occasion → (r.p.toRat < 1 / 20 ↔ f.Licenses r.context ∧ ¬f.Licenses Context.neutral)) ↔ f = Felicity.weak

The weak constraint is the only one of the three that the tests on occasion verbs fit.

theorem SolstadBott2024.neutral_lt_of_licenses : (∀ (t : TriggerOne) (k : Context), ¬t.felicity.Licenses Context.neutral → t.felicity.Licenses k → (blockOneExp1 t Context.neutral).mean.toRat < (blockOneExp1 t k).mean.toRat) ∧ ∀ (t : TriggerTwo) (k : Context), ¬t.felicity.Licenses Context.neutral → t.felicity.Licenses k → (blockOneExp2 t Context.neutral).mean.toRat < (blockOneExp2 t k).mean.toRat

Where a trigger's constraint is met only with a supporting sentence, the supported sentence is rated above the unsupported one.

Filtering in the antecedent of a conditional (Experiment 3)

def SolstadBott2024.Antecedent.formula {Atom : Type u_2} (p p' q : Atom) : Antecedent → Presupposition.Formula Atom

The antecedent of a condition of Experiment 3, for a trigger with presupposition p and assertion p' and a conjoined clause q.

Equations

• One or more equations did not get rendered due to their size.
• SolstadBott2024.Antecedent.formula p p' q SolstadBott2024.Antecedent.triggerOnly = Presupposition.Formula.trigger p p'

inductive SolstadBott2024.Account : Type

The accounts of filtering the paper weighs. On incremental local contexts and on the limited symmetry of Kalomoiros only what precedes a trigger in a conjunction can satisfy its presupposition, on the symmetric local contexts of Schlenker what follows can too, and on local accommodation the presupposition is asserted in place.

• incremental : Account
• limitedSymmetry : Account
• symmetric : Account
• localAccommodation : Account

@[instance_reducible]

instance SolstadBott2024.instDecidableEqAccount : DecidableEq Account

Equations

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

def SolstadBott2024.instReprAccount.repr : Account → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance SolstadBott2024.instReprAccount : Repr Account

Equations

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

@[instance_reducible]

instance SolstadBott2024.instFintypeAccount : Fintype Account

Equations

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

def SolstadBott2024.Account.Accepts {W : Type u_1} {Atom : Type u_2} (I : Atom → Set W) (C : Set W) (F : Presupposition.Formula Atom) : Account → Prop

The formula is acceptable in the context C on the account.

Equations

• SolstadBott2024.Account.Accepts I C F SolstadBott2024.Account.incremental = Schlenker2009.Satisfaction Schlenker2009.Version.incremental C (Presupposition.Formula.occurrences I F)
• SolstadBott2024.Account.Accepts I C F SolstadBott2024.Account.limitedSymmetry = Kalomoiros2023.LimitedSymmetry C (Presupposition.Formula.occurrences I F)
• SolstadBott2024.Account.Accepts I C F SolstadBott2024.Account.symmetric = Schlenker2009.Satisfaction Schlenker2009.Version.symmetric C (Presupposition.Formula.occurrences I F)
• SolstadBott2024.Account.Accepts I C F SolstadBott2024.Account.localAccommodation = (C ⊆ Function.support fun (w : W) => SignType.ofProp (Presupposition.Formula.middleKleene I F w = 1))

def SolstadBott2024.Account.Filters (a : Account) (x : Antecedent) : Prop

An account filters the implication in an antecedent type when the antecedent is acceptable in every context, provided the conjoined clause entails the implication.

Equations

• a.Filters x = ∀ (Atom W : Type) (I : Atom → Set W) (p p' q : Atom), I q ⊆ I p → ∀ (C : Set W), SolstadBott2024.Account.Accepts I C (SolstadBott2024.Antecedent.formula p p' q x) a

theorem SolstadBott2024.Account.filters_iff {a : Account} {x : Antecedent} : a.Filters x ↔ a = localAccommodation ∨ a = symmetric ∧ x ≠ Antecedent.triggerOnly ∨ (a = incremental ∨ a = limitedSymmetry) ∧ x = Antecedent.triggerLast

Incremental local contexts and limited symmetry filter the implication only after the clause entailing it, symmetric local contexts on either side of it, and local accommodation everywhere.

@[instance_reducible]

instance SolstadBott2024.instDecidableFilters (a : Account) (x : Antecedent) : Decidable (a.Filters x)

Equations

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

def SolstadBott2024.Reliable (g : TriggerGroup) (y : Antecedent) : Prop

A contrast with the trigger-first antecedent is reliable for a group of items.

Equations

• SolstadBott2024.Reliable g y = ((SolstadBott2024.followUp g y).t.toRat ≤ -2 ∨ 2 ≤ (SolstadBott2024.followUp g y).t.toRat)

@[instance_reducible]

instance SolstadBott2024.instDecidableReliable (g : TriggerGroup) (y : Antecedent) : Decidable (Reliable g y)

Equations

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

theorem SolstadBott2024.reliable_triggerLast_iff (g : TriggerGroup) : Reliable g Antecedent.triggerLast ↔ (orderTests g).p.toRat < 1 / 20

The criterion agrees with the tests the paper reports for the trigger-first against the trigger-last antecedent.

def SolstadBott2024.Account.Fits (a : Account) (g : TriggerGroup) : Prop

An account fits a group of items when each other antecedent type differs reliably from the trigger-first one exactly when the account filters the implication in one of the two and not in the other, and the antecedent where it is filtered is then the less projective.

Equations

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

@[instance_reducible]

instance SolstadBott2024.instDecidableFits (a : Account) (g : TriggerGroup) : Decidable (a.Fits g)

Equations

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

theorem SolstadBott2024.fits_iff (a : Account) (g : TriggerGroup) : a.Fits g ↔ g = TriggerGroup.occasion ∧ a = Account.symmetric ∨ g = TriggerGroup.factiveAspectual ∧ (a = Account.incremental ∨ a = Account.limitedSymmetry)

Only symmetric local contexts fit the occasion verbs, and only the two asymmetric accounts the factive and aspectual triggers. Local accommodation fits neither, since it makes the trigger alone as little projective as the trigger after the clause entailing its content.

Projectivity and at-issueness (Block 2)

theorem SolstadBott2024.occasion_set_apart_from_psych (o : Rating) : o ∈ blockTwo → ∀ r ∈ blockTwo, o.experiment = Experiment.exp2 → r.experiment = Experiment.exp2 → o.trigger = Trigger.occasion → r.trigger ≠ Trigger.occasion → r.projectivity.toRat < o.projectivity.toRat ∧ o.atIssueness.toRat < r.atIssueness.toRat

The occasion implication is more projective and less at issue than the implications of the two classes of psychological verbs.

theorem SolstadBott2024.negative_correlation_replicates (r : Correlation) : r ∈ correlations → r.level = Level.triggerTypes → r.r.toRat < 0

Across trigger types projectivity falls as at-issueness rises in both experiments, the correlation of Tonhauser, Beaver and Degen.

theorem SolstadBott2024.shared_bias_distinct_projectivity : SolstadBott2022.VerbClass.agentEvocator.icausBias = SolstadBott2022.VerbClass.expStim.icausBias ∧ ∀ o ∈ blockTwo, ∀ e ∈ blockTwo, o.experiment = Experiment.exp2 → e.experiment = Experiment.exp2 → o.trigger = Trigger.occasion → e.trigger = Trigger.experiencerStimulus → e.projectivity.toRat < o.projectivity.toRat

Occasion verbs and experiencer-stimulus verbs share the object bias of implicit causality, yet the implication of the latter is the less projective, so the bias does not come from projective content alone.

The occasion verbs

theorem SolstadBott2024.occasion_isTrigger (v : German.Verb) : v ∈ German.Verbs.allVerbs → v.senseTag = SenseTag.occasion → v.IsTrigger ∧ ¬v.IsFactive ∧ v.phasal = none ∧ v.implicative = ⊥

The sixteen occasion verbs of the experiments are triggers in the German lexicon by their occasion sense alone, being neither factive nor phasal nor implicative.