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 position in the sentence
• Whether we're under an operator that affects projection

• worlds : Core.CommonGround.ContextSet W

  The set of worlds at this position

• position : ℕ

  Position in the sentence (for tracking)

• depth : ℕ

  Embedding depth (for intermediate accommodation)

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

Initial local context: the global context at position 0.

Equations

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

def Semantics.Presupposition.LocalContext.localCtxConsequent {W : Type u_1} (c : LocalCtx W) (antecedent : Core.Presupposition.PrProp 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, position := c.position + 1, depth := c.depth }

def Semantics.Presupposition.LocalContext.localCtxSecondConjunct {W : Type u_1} (c : LocalCtx W) (first : Core.Presupposition.PrProp 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, position := c.position + 1, 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, position := c.position + 1, depth := c.depth + 1 }

def Semantics.Presupposition.LocalContext.localCtxSecondDisjunct {W : Type u_1} (c : LocalCtx W) (first : Core.Presupposition.PrProp 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 = false, position := c.position + 1, depth := c.depth }

def Semantics.Presupposition.LocalContext.presupProjects {W : Type u_1} (lc : LocalCtx W) (p : Core.Presupposition.PrProp W) : Prop

A presupposition projects at a local context if it's not entailed.

Projection is the default. Filtering (non-projection) happens when the local context already satisfies the presupposition.

Equations

• Semantics.Presupposition.LocalContext.presupProjects lc p = ¬lc.worlds ⊧ p.presup

def Semantics.Presupposition.LocalContext.presupFiltered {W : Type u_1} (lc : LocalCtx W) (p : Core.Presupposition.PrProp W) : Prop

A presupposition is filtered at a local context if it IS entailed.

Equations

• Semantics.Presupposition.LocalContext.presupFiltered lc p = (lc.worlds ⊧ p.presup)

theorem Semantics.Presupposition.LocalContext.projects_iff_not_filtered {W : Type u_1} (lc : LocalCtx W) (p : Core.Presupposition.PrProp W) : presupProjects lc p ↔ ¬presupFiltered lc p

Projection and filtering are complementary.

theorem Semantics.Presupposition.LocalContext.conditional_filters_when_entailed {W : Type u_1} (c : LocalCtx W) (p q : Core.Presupposition.PrProp W) (h : ∀ (w : W), c.worlds w → p.assertion w = true → q.presup w = true) : 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 : Core.Presupposition.PrProp W) (h : ∃ (w : W), c.worlds w ∧ p.assertion w = true ∧ q.presup w = false) : 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 : Core.Presupposition.PrProp W) : presupProjects c p ↔ presupProjects (localCtxNegation c) p

Negation doesn't filter presuppositions.

inductive Semantics.Presupposition.LocalContext.KingWorld' : Type

Formalization of "If the king exists, the king is bald".

World type: whether a king exists.

• kingExists : KingWorld'
• noKing : KingWorld'

instance Semantics.Presupposition.LocalContext.instDecidableEqKingWorld' : DecidableEq KingWorld'

Equations

• Semantics.Presupposition.LocalContext.instDecidableEqKingWorld' x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Presupposition.LocalContext.kingExists' : Core.Presupposition.PrProp KingWorld'

"The king exists" — no presupposition.

Equations

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

def Semantics.Presupposition.LocalContext.kingBald' : Core.Presupposition.PrProp KingWorld'

"The king is bald" — presupposes king exists.

Equations

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

theorem Semantics.Presupposition.LocalContext.king_conditional_filters (c : Core.CommonGround.ContextSet KingWorld') (h : c KingWorld'.noKing ∨ c KingWorld'.kingExists) : presupFiltered (localCtxConsequent (initialLocalCtx c) kingExists') kingBald'

In the conditional, the presupposition is filtered.

The local context at "the king is bald" is c + [king exists], which entails the presupposition [king exists].

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

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

This theorem shows the correspondence between:

• Schlenker's local context computation
• Kracht's filtering implication formula

Tower Depth = Local Context Depth

LocalCtx.depth tracks embedding depth for intermediate accommodation. ContextTower.depth tracks the number of context shifts. These two quantities coincide when each embedding operator (negation, attitude verb, conditional) pushes exactly one shift onto the tower.

The bridge is stated as a definitional correspondence rather than a universally quantified theorem, because the alignment depends on the particular sentence structure (each operator must push one shift).

theorem Semantics.Presupposition.LocalContext.negation_depth_matches_tower_push {W : Type u_1} (lc : LocalCtx W) : (localCtxNegation lc).depth = lc.depth + 1

When each embedding operator pushes exactly one shift onto the tower, the local context depth at the corresponding position equals the tower depth. This connects @cite{schlenker-2009}'s incremental depth tracking to the tower's structural depth.

Concretely: localCtxNegation increments depth by 1, and pushing a shift onto a tower increments depth by 1. The bridge holds by construction when the sentence structure is faithfully mirrored.

def Semantics.Presupposition.LocalContext.beliefTower {C : Type u_2} (rootCtx : C) (attShift : Core.Context.ContextShift C) : Core.Context.ContextTower C

A belief embedding tower: root context (speech-act context) plus one attitude shift (the belief operator). The tower has depth 1, matching the local context depth after one embedding.

Equations

• Semantics.Presupposition.LocalContext.beliefTower rootCtx attShift = (Core.Context.ContextTower.root rootCtx).push attShift

theorem Semantics.Presupposition.LocalContext.beliefTower_depth {C : Type u_2} (rootCtx : C) (attShift : Core.Context.ContextShift C) : (beliefTower rootCtx attShift).depth = 1

The belief tower has depth 1.