Schlenker (2009): Local Contexts

[Sch09a]

Projection predictions of the local-context theory, applied to the King and conditional examples from Studies.Heim1983. The per-connective local contexts are substrate (Semantics.Presupposition.LocalContext); belief embedding ([Sch09a] §3.1.2) is Semantics.Presupposition.BeliefEmbedding.

Main declarations

• matrix_local_context_is_global: at matrix position the local context is the global context, so unembedded presuppositions project.
• belief_local_context_is_holder_beliefs: under "x believes φ" the local context at φ is x's belief state.
• negation_projects / conditional_filters: the projection asymmetry between negation and conditionals.
• king_conditional_filters: "If the king exists, the king is bald" filters the existence presupposition.
• king_accounts_agree: the local-context prediction agrees with the Karttunen filtering connective (PartialProp.impFilter) on the king example.

theorem Schlenker2009.negation_projects {W : Type u_1} (c : CommonGround.ContextSet W) (p : Semantics.Presupposition.PartialProp W) : Semantics.Presupposition.Context.presupProjects (Semantics.Presupposition.Context.localCtxNegation c) p ↔ Semantics.Presupposition.Context.presupProjects c p

Negation projects: "not φ" has the same local context at φ as the unembedded sentence (the matrix local context being the global context itself), so φ's presupposition projects unless globally entailed.

theorem Schlenker2009.conditional_filters {W : Type u_1} (c : CommonGround.ContextSet W) (p q : Semantics.Presupposition.PartialProp W) (h : ∀ (w : W), c w → p.assertion w → q.presup w) : Semantics.Presupposition.Context.presupSatisfied (Semantics.Presupposition.Context.localCtxConsequent c p) q

Conditionals filter: in "if φ then ψ", the antecedent's assertion enters ψ's local context; when it entails ψ's presupposition, the presupposition is filtered.

theorem Schlenker2009.king_conditional_filters (c : CommonGround.ContextSet Heim1983.KingWorld) : Semantics.Presupposition.Context.presupSatisfied (Semantics.Presupposition.Context.localCtxConsequent c Heim1983.kingExists) Heim1983.kingBald

"If the king exists, the king is bald": the local context at "the king is bald" is c + [king exists], which entails the existence presupposition, so it is filtered.

theorem Schlenker2009.king_accounts_agree (c : CommonGround.ContextSet Heim1983.KingWorld) : Semantics.Presupposition.Context.presupSatisfied (Semantics.Presupposition.Context.localCtxConsequent c Heim1983.kingExists) Heim1983.kingBald ∧ Heim1983.ifKingThenBald.presup = fun (x : Heim1983.KingWorld) => True

On the king example, the local-context account and the Karttunen filtering connective agree: both pronounce the conditional presuppositionless.