Tonhauser, Beaver, Roberts and Simons (2013): Toward a Taxonomy of Projective Content

A content projects when it survives the embedding of its trigger under negation, in a question, under a possibility modal or in the antecedent of a conditional, the family of sentences. Tonhauser, Beaver, Roberts and Simons sort projective contents by two properties, stated here for a context, a set of worlds, and a content m, a proposition. A trigger imposes a strong contextual felicity constraint when its sentence is acceptable only in contexts that entail m. The content has obligatory local effect when a belief report with the trigger in its complement is acceptable only where the holder's epistemic state, the local context of the complement, entails m. The two properties cross to give four classes, and the diagnostics applied to Paraguayan Guaraní and English find contents in all four.

Main statements

• TonhauserEtAl2013.excludes_matrix_iff, TonhauserEtAl2013.excludes_belief_iff: a class rules out an utterance in a context that does not entail the content exactly when it has the constraint, and a belief report whose holder does not believe the content exactly when it has obligatory local effect.
• TonhauserEtAl2013.judgment_rows: each of the paper's examples is unacceptable exactly when the class of its content rules it out.
• TonhauserEtAl2013.eq_of_excludes_iff: a judgment in a neutral context and a judgment of a belief report separate the four classes.
• TonhauserEtAl2013.acceptable_rows_of_ne_A: local satisfaction gives every content both properties, and each of the other three classes has an acceptable example that this rules out.

Implementation notes

• Acceptability is taken as given, as the contexts in which consultants accept a sentence. The context is the utterance context before any accommodation, so the argument against local satisfaction leaves the reply by accommodation open, as the paper notes.
• A member of the family of sentences is acceptable only where its clause is acceptable in its local context, the image of the context under a reflexive relation, so a constraint on that context projects (StrongContextualFelicity.of_image). Projection of the other contents is diagnosed by implication judgments, which are not modelled; the rows of (1) record such judgments.
• A stance to the negation of a content requires a consistent state, since the diagnostics need a belief predicate that enforces consistency.

References

• [TBRS13]
• [CMCG90]
• [Mat04]
• [Kar74a]
• [Hei83]
• [Sch09a]

Contexts and contents

inductive TonhauserEtAl2013.Stance : Type

The stance of a body of information to a content m, which it entails, or leaves open together with its negation, or contradicts while being consistent, (10).

• positive : Stance
• neutral : Stance
• negative : Stance

@[instance_reducible]

instance TonhauserEtAl2013.instDecidableEqStance : DecidableEq Stance

Equations

• TonhauserEtAl2013.instDecidableEqStance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TonhauserEtAl2013.instReprStance.repr : Stance → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance TonhauserEtAl2013.instReprStance : Repr Stance

Equations

• TonhauserEtAl2013.instReprStance = { reprPrec := TonhauserEtAl2013.instReprStance.repr }

@[instance_reducible]

instance TonhauserEtAl2013.instFintypeStance : Fintype Stance

Equations

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

def TonhauserEtAl2013.Stance.Holds {W : Type u_1} (c m : Set W) : Stance → Prop

The information c has the stance to the content m.

Equations

• TonhauserEtAl2013.Stance.Holds c m TonhauserEtAl2013.Stance.positive = (c ⊆ m)
• TonhauserEtAl2013.Stance.Holds c m TonhauserEtAl2013.Stance.neutral = (¬c ⊆ m ∧ ¬c ⊆ mᶜ)
• TonhauserEtAl2013.Stance.Holds c m TonhauserEtAl2013.Stance.negative = (c.Nonempty ∧ c ⊆ mᶜ)

theorem TonhauserEtAl2013.Stance.Holds.not_subset {W : Type u_1} {s : Stance} {c m : Set W} (h : Holds c m s) (hs : s ≠ positive) : ¬c ⊆ m

The two properties

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

The trigger's sentence, acceptable in the contexts Acc, is acceptable only in contexts that entail m, (11).

Equations

• TonhauserEtAl2013.StrongContextualFelicity m Acc = ∀ (c : Set W), Acc c → c ⊆ m

def TonhauserEtAl2013.ObligatoryLocalEffect {W : Type u_1} (R : SetRel W W) (m : Set W) (Acc : Set W → Prop) : Prop

A belief report with the trigger in its complement, acceptable in the contexts Acc, is acceptable only in contexts that entail that the holder believes m, (40). The belief is the core of m along the holder's doxastic accessibility R.

Equations

• TonhauserEtAl2013.ObligatoryLocalEffect R m Acc = TonhauserEtAl2013.StrongContextualFelicity (R.core m) Acc

theorem TonhauserEtAl2013.obligatoryLocalEffect_iff {W : Type u_1} {R : SetRel W W} {m : Set W} {Acc : Set W → Prop} : ObligatoryLocalEffect R m Acc ↔ ∀ (c : Set W), Acc c → R.image c ⊆ m

A content has obligatory local effect when the local context of the complement, the image of the context under the holder's doxastic accessibility, entails it.

theorem TonhauserEtAl2013.StrongContextualFelicity.of_image {W : Type u_1} {R : SetRel W W} {m : Set W} {Acc Acc' : Set W → Prop} [R.IsRefl] (h : StrongContextualFelicity m Acc) (hloc : ∀ (c : Set W), Acc' c → Acc (R.image c)) : StrongContextualFelicity m Acc'

A constraint on the local context of an embedded sentence is a constraint on the context of the embedding one when the embedding is along a reflexive relation, as in the family of sentences. The constraint then projects, (24).

theorem TonhauserEtAl2013.StrongContextualFelicity.obligatoryLocalEffect {W : Type u_1} {R : SetRel W W} {m : Set W} {Acc Acc' : Set W → Prop} (h : StrongContextualFelicity m Acc) (hloc : ∀ (c : Set W), Acc' c → Acc (R.image c)) : ObligatoryLocalEffect R m Acc'

A constraint that must be met in the local context of a belief report gives the content obligatory local effect, (41).

The four classes

inductive TonhauserEtAl2013.ProjectiveClass : Type

The classes of projective content, Table 1.

• A : ProjectiveClass
• B : ProjectiveClass
• C : ProjectiveClass
• D : ProjectiveClass

@[instance_reducible]

instance TonhauserEtAl2013.instDecidableEqProjectiveClass : DecidableEq ProjectiveClass

Equations

• TonhauserEtAl2013.instDecidableEqProjectiveClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def TonhauserEtAl2013.instReprProjectiveClass.repr : ProjectiveClass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance TonhauserEtAl2013.instReprProjectiveClass : Repr ProjectiveClass

Equations

• TonhauserEtAl2013.instReprProjectiveClass = { reprPrec := TonhauserEtAl2013.instReprProjectiveClass.repr }

@[instance_reducible]

instance TonhauserEtAl2013.instFintypeProjectiveClass : Fintype ProjectiveClass

Equations

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

def TonhauserEtAl2013.ProjectiveClass.StrongContextualFelicity (k : ProjectiveClass) : Prop

The triggers of the class impose the strong contextual felicity constraint.

Equations

• k.StrongContextualFelicity = (k = TonhauserEtAl2013.ProjectiveClass.A ∨ k = TonhauserEtAl2013.ProjectiveClass.D)

def TonhauserEtAl2013.ProjectiveClass.ObligatoryLocalEffect (k : ProjectiveClass) : Prop

The contents of the class have obligatory local effect.

Equations

• k.ObligatoryLocalEffect = (k = TonhauserEtAl2013.ProjectiveClass.A ∨ k = TonhauserEtAl2013.ProjectiveClass.C)

@[instance_reducible]

instance TonhauserEtAl2013.ProjectiveClass.instDecidablePredStrongContextualFelicity : DecidablePred StrongContextualFelicity

Equations

• x✝.instDecidablePredStrongContextualFelicity = { decide := decide (x✝ = TonhauserEtAl2013.ProjectiveClass.A) || decide (x✝ = TonhauserEtAl2013.ProjectiveClass.D), reflects_decide := ⋯ }

@[instance_reducible]

instance TonhauserEtAl2013.ProjectiveClass.instDecidablePredObligatoryLocalEffect : DecidablePred ObligatoryLocalEffect

Equations

• x✝.instDecidablePredObligatoryLocalEffect = { decide := decide (x✝ = TonhauserEtAl2013.ProjectiveClass.A) || decide (x✝ = TonhauserEtAl2013.ProjectiveClass.C), reflects_decide := ⋯ }

theorem TonhauserEtAl2013.ProjectiveClass.eq_of_iff {k k' : ProjectiveClass} (hs : k.StrongContextualFelicity ↔ k'.StrongContextualFelicity) (ho : k.ObligatoryLocalEffect ↔ k'.ObligatoryLocalEffect) : k = k'

The two properties determine the class.

The diagnostics

inductive TonhauserEtAl2013.Test : Type

A diagnostic configuration. A member of the family of sentences of the trigger's sentence is uttered in a context with a given stance to the content, (12) and (24), or the sentence is the complement of a belief report whose holder's epistemic state has a given stance, (41).

• matrix (e : Presupposition.FamilyVariant) (s : Stance) : Test
• belief (s : Stance) : Test

def TonhauserEtAl2013.instDecidableEqTest.decEq (x✝ x✝¹ : Test) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• TonhauserEtAl2013.instDecidableEqTest.decEq (TonhauserEtAl2013.Test.matrix e s) (TonhauserEtAl2013.Test.belief s_1) = isFalse ⋯
• TonhauserEtAl2013.instDecidableEqTest.decEq (TonhauserEtAl2013.Test.belief s) (TonhauserEtAl2013.Test.matrix e s_1) = isFalse ⋯
• TonhauserEtAl2013.instDecidableEqTest.decEq (TonhauserEtAl2013.Test.belief a) (TonhauserEtAl2013.Test.belief b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TonhauserEtAl2013.instDecidableEqTest : DecidableEq Test

Equations

• TonhauserEtAl2013.instDecidableEqTest = TonhauserEtAl2013.instDecidableEqTest.decEq

@[instance_reducible]

instance TonhauserEtAl2013.instReprTest : Repr Test

Equations

• TonhauserEtAl2013.instReprTest = { reprPrec := TonhauserEtAl2013.instReprTest.repr }

def TonhauserEtAl2013.instReprTest.repr : Test → ℕ → Std.Format

Equations

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

def TonhauserEtAl2013.Test.Accepted {W : Type u_1} (m : Set W) (R : SetRel W W) (Acc : Presupposition.FamilyVariant → Set W → Prop) (AccB : Set W → Prop) : Test → Prop

An instance of the test is acceptable, where Acc e holds of the contexts in which the family member e is acceptable, AccB of those in which the belief report is, and R is the holder's doxastic accessibility, so that R.image {w} is the holder's epistemic state at w.

Equations

• TonhauserEtAl2013.Test.Accepted m R Acc AccB (TonhauserEtAl2013.Test.matrix e s) = ∃ (c : Set W), TonhauserEtAl2013.Stance.Holds c m s ∧ Acc e c
• TonhauserEtAl2013.Test.Accepted m R Acc AccB (TonhauserEtAl2013.Test.belief s) = ∃ (c : Set W), ∃ w ∈ c, TonhauserEtAl2013.Stance.Holds (R.image {w}) m s ∧ AccB c

def TonhauserEtAl2013.Excludes (k : ProjectiveClass) (t : Test) : Prop

A class excludes a test when no content with the properties of the class has an acceptable instance of it. A member of the family of sentences is acceptable only where its clause, whose acceptability is Acc₀, is acceptable in its local context, the image of the context under the member's relation. The modal's accessibility M is reflexive, what is the case being possible.

Equations

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

theorem TonhauserEtAl2013.excludes_matrix_iff {k : ProjectiveClass} {e : Presupposition.FamilyVariant} {s : Stance} : Excludes k (Test.matrix e s) ↔ k.StrongContextualFelicity ∧ s ≠ Stance.positive

A class excludes an utterance in a context exactly when its triggers impose the constraint and the context does not entail the content, (12).

theorem TonhauserEtAl2013.excludes_belief_iff {k : ProjectiveClass} {s : Stance} : Excludes k (Test.belief s) ↔ k.ObligatoryLocalEffect ∧ s ≠ Stance.positive

A class excludes a belief report exactly when its contents have obligatory local effect and the holder's epistemic state does not entail the content, (41).

@[instance_reducible]

instance TonhauserEtAl2013.instDecidablePredTestExcludes (k : ProjectiveClass) : DecidablePred (Excludes k)

Equations

• TonhauserEtAl2013.instDecidablePredTestExcludes k (TonhauserEtAl2013.Test.matrix e s) = decidable_of_iff' (k.StrongContextualFelicity ∧ s ≠ TonhauserEtAl2013.Stance.positive) ⋯
• TonhauserEtAl2013.instDecidablePredTestExcludes k (TonhauserEtAl2013.Test.belief s) = decidable_of_iff' (k.ObligatoryLocalEffect ∧ s ≠ TonhauserEtAl2013.Stance.positive) ⋯

theorem TonhauserEtAl2013.eq_of_excludes_iff {k : ProjectiveClass} {e : Presupposition.FamilyVariant} {s : Stance} {k' : ProjectiveClass} (hs : s ≠ Stance.positive) (hm : Excludes k (Test.matrix e Stance.neutral) ↔ Excludes k' (Test.matrix e Stance.neutral)) (hb : Excludes k (Test.belief s) ↔ Excludes k' (Test.belief s)) : k = k'

The two diagnostics separate the four classes, in that classes excluding the same utterances in a neutral context and the same belief reports are one class.

Local satisfaction

theorem TonhauserEtAl2013.Excludes.not_accepted_admits {W : Type} {t : Test} (h : Excludes ProjectiveClass.A t) (p : W → SignType) (M R : SetRel W W) [M.IsRefl] : ¬Test.Accepted (Function.support p) R (fun (e : Presupposition.FamilyVariant) (c : Set W) => (Presupposition.FamilyVariant.rel M e).image c ⊆ Function.support p) (fun (c : Set W) => R.image c ⊆ Function.support p) t

If a sentence is acceptable exactly where its local context entails its presupposition, as for Karttunen, Heim and Schlenker, the presupposition has the two properties of class A, so no instance of a test that class A excludes is acceptable. The local context of a family member is the image of the utterance context under the member's relation, and that of the complement of a belief report its image under the holder's doxastic accessibility.

The rows

def TonhauserEtAl2013.Stance.table : List (String × Stance)

The names of the stances as example rows record them.

Equations

• TonhauserEtAl2013.Stance.table = [("m-positive", TonhauserEtAl2013.Stance.positive), ("m-neutral", TonhauserEtAl2013.Stance.neutral), ("m-negative", TonhauserEtAl2013.Stance.negative)]

def TonhauserEtAl2013.class? (r : Datum) : Option ProjectiveClass

The class that Table 2 assigns to the content of a row.

Equations

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

def TonhauserEtAl2013.test? (r : Datum) : Option Test

The diagnostic configuration of a row, a belief report when the row records the stance of the holder's epistemic state and otherwise a family member in its utterance context.

Equations

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

theorem TonhauserEtAl2013.judgment_rows (r : Datum) : r ∈ Examples.all → ∀ k ∈ class? r, ∃ t ∈ test? r, r.judgment = Judgment.unacceptable ↔ Excludes k t

Each example of a content in Table 2 is unacceptable exactly when the class of the content excludes its configuration.

theorem TonhauserEtAl2013.exists_rows_of_class (k : ProjectiveClass) : (∃ r ∈ Examples.all, class? r = some k ∧ ∃ (e : Presupposition.FamilyVariant), test? r = some (Test.matrix e Stance.neutral)) ∧ ∃ r ∈ Examples.all, class? r = some k ∧ ∃ (s : Stance), s ≠ Stance.positive ∧ test? r = some (Test.belief s)

Each of the four classes has an example in a neutral context and an example of a belief report whose holder does not believe the content, the two judgments that fix a class.

theorem TonhauserEtAl2013.acceptable_rows_of_ne_A (k : ProjectiveClass) : k ≠ ProjectiveClass.A → ∃ r ∈ Examples.all, class? r = some k ∧ r.judgment = Judgment.acceptable ∧ ∃ t ∈ test? r, Excludes ProjectiveClass.A t

Each class other than A has an acceptable example in a configuration that class A excludes, so a theory of projection on which every projective content must be satisfied in its local context does not extend to it (section 8).