Tonhauser, Beaver, Roberts & Simons (2013): a taxonomy of projective content

[TBRS13] sort projective contents by two diagnosable properties. A trigger imposes a strong contextual felicity constraint with respect to its content m if it is acceptable only in m-positive contexts (11), where a context is m-positive if it entails m and m-neutral if it entails neither m nor ¬m (10), so acceptability in an m-neutral context refutes the constraint (12i). Under a belief predicate, m has local effect when it is part of the attitude holder's belief state, and obligatory local effect when it always does (§5), so acceptability with the holder ignorant of m refutes it (41i). The two properties cross-classify the English and Guaraní triggers of Table 2 into classes A–D (Semantics/Presupposition/ProjectiveContent.lean), cutting across the traditional presuppositions: pronouns (A) and stop (C) are both classical presuppositions (stop_pronoun_classes_differ).

§8 argues that a theory on which a presupposition is acceptable iff its local context entails it ([Kar74a], [Hei83], [Sch09a]) predicts every trigger to impose the constraint and to have obligatory local effect — to be class A. Against the substrate's own rendering of that theory, Context.presupSatisfied at the matrix and BeliefEmbedding.presupAttributedToHolder under belief, this is scf_of_satisfaction and ole_of_satisfaction; Table 2's classes B–D are the counterexamples (exists_trigger_not_classA).

def TonhauserEtAl2013.MPositive {W : Type u_1} (m : Set W) (c : CommonGround.ContextSet W) : Prop

(10): the context entails m.

Equations

• TonhauserEtAl2013.MPositive m c = c.entails m

def TonhauserEtAl2013.MNeutral {W : Type u_1} (m : Set W) (c : CommonGround.ContextSet W) : Prop

(10): the context entails neither m nor ¬m.

Equations

• TonhauserEtAl2013.MNeutral m c = (¬c.entails m ∧ ¬c.entails mᶜ)

def TonhauserEtAl2013.StrongContextualFelicity {W : Type u_1} (m : Set W) (Acc : CommonGround.ContextSet W → Prop) : Prop

(11): uttering the trigger's sentence, acceptable in the contexts Acc, is acceptable only in m-positive contexts.

Equations

• TonhauserEtAl2013.StrongContextualFelicity m Acc = ∀ (c : CommonGround.ContextSet W), Acc c → TonhauserEtAl2013.MPositive m c

theorem TonhauserEtAl2013.not_scf_of_acceptable_neutral {W : Type u_1} (m : Set W) (c : CommonGround.ContextSet W) {Acc : CommonGround.ContextSet W → Prop} (h : Acc c) (hn : MNeutral m c) : ¬StrongContextualFelicity m Acc

(12i): acceptability in an m-neutral context refutes the constraint.

def TonhauserEtAl2013.LocalEffect {W : Type u_1} {E : Type u_2} (m : Set W) (Dox : E → W → W → Prop) (a : E) (w : W) : Prop

§5: under a believes S at w, m has local effect when it is part of a's belief state.

Equations

• TonhauserEtAl2013.LocalEffect m Dox a w = CommonGround.ContextSet.entails (Dox a w) m

def TonhauserEtAl2013.ObligatoryLocalEffect {W : Type u_1} {E : Type u_2} (m : Set W) (Dox : E → W → W → Prop) (a : E) (Acc : CommonGround.ContextSet W → Prop) : Prop

Obligatory local effect: wherever the belief report is acceptable, m has local effect.

Equations

• TonhauserEtAl2013.ObligatoryLocalEffect m Dox a Acc = ∀ (c : CommonGround.ContextSet W), Acc c → ∀ w ∈ c, TonhauserEtAl2013.LocalEffect m Dox a w

theorem TonhauserEtAl2013.not_ole_of_acceptable_ignorant {W : Type u_1} {E : Type u_2} (m : Set W) (c : CommonGround.ContextSet W) {Dox : E → W → W → Prop} {a : E} {Acc : CommonGround.ContextSet W → Prop} (h : Acc c) {w : W} (hw : w ∈ c) (hig : MNeutral m (Dox a w)) : ¬ObligatoryLocalEffect m Dox a Acc

(41i): acceptability of the report with the holder ignorant of m refutes obligatory local effect.

Against local satisfaction (§8)

theorem TonhauserEtAl2013.scf_of_satisfaction {W : Type u_1} (p : Semantics.Presupposition.PartialProp W) : StrongContextualFelicity p.presup fun (x : CommonGround.ContextSet W) => Semantics.Presupposition.Context.presupSatisfied x p

A trigger acceptable exactly where its local context entails its presupposition imposes the strong contextual felicity constraint.

theorem TonhauserEtAl2013.ole_of_satisfaction {W : Type u_1} {E : Type u_2} (p : Semantics.Presupposition.PartialProp W) (Dox : E → W → W → Prop) (a : E) : ObligatoryLocalEffect p.presup Dox a fun (x : CommonGround.ContextSet W) => Semantics.Presupposition.BeliefEmbedding.presupAttributedToHolder { globalCtx := x, dox := Dox, agent := a } p

Under belief, local satisfaction is satisfaction in the holder's belief state, so the presupposition has obligatory local effect.

theorem TonhauserEtAl2013.exists_trigger_not_classA : Semantics.Presupposition.ProjectiveContent.classFromProperties Semantics.Presupposition.ProjectiveContent.StrongContextualFelicity.requires Semantics.Presupposition.ProjectiveContent.ObligatoryLocalEffect.obligatory = Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classA ∧ ∃ (t : Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger), t.toClass ≠ Semantics.Presupposition.ProjectiveContent.ProjectiveClass.classA

Local satisfaction thus predicts class A for every trigger; Table 2 has triggers of every other class.

theorem TonhauserEtAl2013.stop_pronoun_classes_differ : Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.stop_prestate.toClass ≠ Semantics.Presupposition.ProjectiveContent.ProjectiveTrigger.pronoun_existence.toClass

The classes cut across the traditional presuppositions: pronouns and stop are both classical presuppositions, in classes A and C.