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.matrix_local_context_is_global {W : Type u_1} (c : CommonGround.ContextSet W) : (Semantics.Presupposition.LocalContext.initialLocalCtx c).worlds = c

Matrix local context = global context.

In unembedded sentences, the local context is just the global context c, so a matrix presupposition must be entailed by the context set or project.

theorem Schlenker2009.belief_local_context_is_holder_beliefs {W : Type u_1} {Agent : Type u_2} (blc : Semantics.Presupposition.BeliefEmbedding.BeliefLocalCtx W Agent) (w_star : W) (h : blc.globalCtx w_star) : (Semantics.Presupposition.BeliefEmbedding.beliefToLocalCtx blc w_star h).worlds = blc.atWorld w_star

Local context under belief = attitude holder's beliefs.

Under "x believes φ", the local context at φ is determined by x's doxastic state ([Sch09a] §3.1.2).

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

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

theorem Schlenker2009.conditional_filters {W : Type u_1} (c : Semantics.Presupposition.LocalContext.LocalCtx W) (p q : Semantics.Presupposition.PartialProp W) (h : ∀ (w : W), c.worlds w → p.assertion w → q.presup w) : Semantics.Presupposition.LocalContext.presupFiltered (Semantics.Presupposition.LocalContext.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.LocalContext.presupFiltered (Semantics.Presupposition.LocalContext.localCtxConsequent (Semantics.Presupposition.LocalContext.initialLocalCtx 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.LocalContext.presupFiltered (Semantics.Presupposition.LocalContext.localCtxConsequent (Semantics.Presupposition.LocalContext.initialLocalCtx 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.