Local Context Computation

Local contexts for presupposition projection, stipulated per connective in the satisfaction tradition ([Kar74], [Hei83]). [Sch09a]'s contribution — deriving these local contexts from bivalent meanings plus incremental transparency — is not implemented here: the per-connective clauses below are the Karttunen/Heim stipulations that Schlenker's algorithm reconstructs.

Insight

The "local context" at a position in a sentence determines what presuppositions are filtered vs. projected, computed incrementally from left to right.

The Algorithm

For a sentence S with embedded clause φ at position i:

1. The local context c_i is the global context c updated with all material to the left of position i
2. A presupposition P of φ projects iff c_i ⊭ P
3. If c_i ⊧ P, the presupposition is "filtered" (locally satisfied)

Examples

"If the king exists, the king is bald"

• Global context: c
• Local context at "the king is bald": c + [the king exists]
• Presupposition "king exists" is entailed by local context
• Therefore: presupposition is filtered, doesn't project globally

"John stopped smoking"

• Global context: c
• No filtering material before "stopped"
• Presupposition "John used to smoke" projects globally

structure Semantics.Presupposition.LocalContext.LocalCtx (W : Type u_2) : Type u_2

A local context at a position in a sentence.

Tracks:

• The context set (worlds compatible with prior material)
• The embedding depth (for intermediate accommodation)

• worlds : CommonGround.ContextSet W

  The set of worlds at this position

• depth : ℕ

  Embedding depth (for intermediate accommodation)

@[implicit_reducible]

instance Semantics.Presupposition.LocalContext.instHasContextSetLocalCtx {W : Type u_1} : CommonGround.HasContextSet (LocalCtx W) W

Equations

• Semantics.Presupposition.LocalContext.instHasContextSetLocalCtx = { toContextSet := Semantics.Presupposition.LocalContext.LocalCtx.worlds }

def Semantics.Presupposition.LocalContext.initialLocalCtx {W : Type u_1} (c : CommonGround.ContextSet W) : LocalCtx W

Initial local context: the global context, unembedded.

Equations

• Semantics.Presupposition.LocalContext.initialLocalCtx c = { worlds := c }

def Semantics.Presupposition.LocalContext.localCtxConsequent {W : Type u_1} (c : LocalCtx W) (antecedent : PartialProp W) : LocalCtx W

Local context for the consequent of a conditional.

"If P then Q" — the local context at Q is c + P.assertion

This is why "If the king exists, the king is bald" doesn't presuppose king exists: the local context at "the king is bald" already entails it.

Equations

• Semantics.Presupposition.LocalContext.localCtxConsequent c antecedent = { worlds := c.worlds.update antecedent.assertion, depth := c.depth }

def Semantics.Presupposition.LocalContext.localCtxSecondConjunct {W : Type u_1} (c : LocalCtx W) (first : PartialProp W) : LocalCtx W

Local context for the second conjunct.

"P and Q" — the local context at Q is c + P.assertion

Equations

• Semantics.Presupposition.LocalContext.localCtxSecondConjunct c first = { worlds := c.worlds.update first.assertion, depth := c.depth }

def Semantics.Presupposition.LocalContext.localCtxNegation {W : Type u_1} (c : LocalCtx W) : LocalCtx W

Local context under negation.

"not P" — the local context at P is unchanged, but we track depth.

Equations

• Semantics.Presupposition.LocalContext.localCtxNegation c = { worlds := c.worlds, depth := c.depth + 1 }

def Semantics.Presupposition.LocalContext.localCtxSecondDisjunct {W : Type u_1} (c : LocalCtx W) (first : PartialProp W) : LocalCtx W

Local context for each disjunct.

"P or Q" — Schlenker: local context at Q is c + ¬P.assertion (and symmetrically for P)

Equations

• Semantics.Presupposition.LocalContext.localCtxSecondDisjunct c first = { worlds := fun (w : W) => c.worlds w ∧ ¬first.assertion w, depth := c.depth }

@[reducible, inline]

abbrev Semantics.Presupposition.LocalContext.presupProjects {W : Type u_1} (lc : LocalCtx W) (p : PartialProp W) : Prop

A presupposition projects at a local context if it's not entailed. Delegates to Semantics.Presupposition.Context.presupProjects.

Equations

• Semantics.Presupposition.LocalContext.presupProjects lc p = Semantics.Presupposition.Context.presupProjects lc.worlds p

@[reducible, inline]

abbrev Semantics.Presupposition.LocalContext.presupFiltered {W : Type u_1} (lc : LocalCtx W) (p : PartialProp W) : Prop

A presupposition is filtered (satisfied) at a local context if it IS entailed. Delegates to Semantics.Presupposition.Context.presupSatisfied.

Equations

• Semantics.Presupposition.LocalContext.presupFiltered lc p = Semantics.Presupposition.Context.presupSatisfied lc.worlds p

theorem Semantics.Presupposition.LocalContext.conditional_filters_when_entailed {W : Type u_1} (c : LocalCtx W) (p q : PartialProp W) (h : ∀ (w : W), c.worlds w → p.assertion w → q.presup w) : presupFiltered (localCtxConsequent c p) q

Presupposition of consequent is filtered when antecedent assertion entails the presupposition.

This formalizes the core insight of filtering semantics.

theorem Semantics.Presupposition.LocalContext.conditional_projects_when_not_entailed {W : Type u_1} (c : LocalCtx W) (p q : PartialProp W) (h : ∃ (w : W), c.worlds w ∧ p.assertion w ∧ ¬q.presup w) : presupProjects (localCtxConsequent c p) q

If antecedent assertion doesn't entail consequent presupposition, it projects.

theorem Semantics.Presupposition.LocalContext.negation_preserves_projection {W : Type u_1} (c : LocalCtx W) (p : PartialProp W) : presupProjects c p ↔ presupProjects (localCtxNegation c) p

Negation doesn't filter presuppositions.

theorem Semantics.Presupposition.LocalContext.local_context_matches_impFilter {W : Type u_1} (c : CommonGround.ContextSet W) (p q : PartialProp W) : (∀ (w : W), c w → (p.impFilter q).presup w) ↔ ∀ (w : W), c w → p.presup w ∧ (p.assertion w → q.presup w)

The local context theory derives the same result as the filtering connectives in Semantics.Presupposition.

This theorem shows the correspondence between:

• the stipulated local context computation
• the Karttunen filtering implication formula ([Kar73], [Pet79])

theorem Semantics.Presupposition.LocalContext.local_context_matches_disjFilterLeft {W : Type u_1} (c : CommonGround.ContextSet W) (firstDisjunct second : PartialProp W) : presupFiltered (localCtxSecondDisjunct (initialLocalCtx c) firstDisjunct) second ↔ ∀ (w : W), c w → (PartialProp.disjFilterLeft firstDisjunct.assertion second).presup w

Schlenker's local context at the second disjunct derives Karttunen's asymmetric disjunction filter (PartialProp.disjFilterLeft).

For "A ∨ B_ψ" in context c:

• Schlenker: local context at B is c ∧ ¬A; ψ filtered iff c ∧ ¬A ⊧ ψ
• Karttunen: residual presupposition is ¬A → ψ; satisfied iff ∀w∈c, ¬A(w) → ψ(w)

These are the same condition (currying/uncurrying the conjunction). Analogous to local_context_matches_impFilter for conditionals. [Sch09a], [Kar73]