Presupposition–Context Bridge

@cite{stalnaker-1974} @cite{heim-1983} @cite{lewis-1979}

Canonical operations connecting presuppositions (PrProp W) to contexts (ContextSet W). Before this module, every downstream file that needed both reimplemented the same bridge with different names:

• LocalContext.presupFiltered = c ⊆ p.presup
• Accommodation.globalAccommodate = c ∩ presup
• Accommodation.isInformative = ¬ c ⊆ presup

This module provides a shared vocabulary so that projection, filtering, accommodation, and conceivability are defined once and reused everywhere.

Core Operations

Operation	Meaning	Use site
presupSatisfied	presup entailed by context	filtering
presupSatisfiable	∃ world in context with presup	conceivability
presupProjects	presup NOT entailed	projection
accommodate	restrict context to presup worlds	accommodation

Conceivability

presupSatisfiable is the conceivability check needed for @cite{enguehard-2024}'s conceivability presupposition: a number feature's presupposition is conceivable in the common ground iff there exists some world in the context set satisfying it.

@[reducible, inline]

abbrev Core.PresuppositionContext.presupSatisfied {W : Type u_1} (c : CommonGround.ContextSet W) (p : Presupposition.PrProp W) : Prop

A presupposition is satisfied (filtered) in context c iff the context entails it: every world in the context satisfies the presupposition.

This is Karttunen's filtering condition and Schlenker's local satisfaction.

Equations

• Core.PresuppositionContext.presupSatisfied c p = (c ⊆ p.presup)

@[reducible, inline]

abbrev Core.PresuppositionContext.presupSatisfiable {W : Type u_1} (c : CommonGround.ContextSet W) (p : Presupposition.PrProp W) : Prop

A presupposition is satisfiable (conceivable) in context c iff some world in the context satisfies it.

This is Enguehard's conceivability condition: a singular indefinite's number presupposition is conceivable iff the common ground contains a world where the witness set has the right cardinality.

Equations

• Core.PresuppositionContext.presupSatisfiable c p = Set.Nonempty (c ∩ p.presup)

@[reducible, inline]

abbrev Core.PresuppositionContext.presupProjects {W : Type u_1} (c : CommonGround.ContextSet W) (p : Presupposition.PrProp W) : Prop

A presupposition projects from context c iff it is NOT satisfied (not filtered). Projection is the complement of filtering.

Equations

• Core.PresuppositionContext.presupProjects c p = ¬Core.PresuppositionContext.presupSatisfied c p

@[reducible, inline]

abbrev Core.PresuppositionContext.accommodate {W : Type u_1} (c : CommonGround.ContextSet W) (presup : Set W) : CommonGround.ContextSet W

Accommodate a presupposition: restrict the context to worlds where the presupposition holds.

@cite{lewis-1979}: "presupposition P comes into existence."

Equations

• Core.PresuppositionContext.accommodate c presup = c ∩ presup

@[reducible, inline]

abbrev Core.PresuppositionContext.accommodationInformative {W : Type u_1} (c : CommonGround.ContextSet W) (presup : Set W) : Prop

Accommodation is informative iff the presupposition is not already entailed — accommodation actually changes the context.

Equations

• Core.PresuppositionContext.accommodationInformative c presup = ¬c ⊆ presup

@[reducible, inline]

abbrev Core.PresuppositionContext.accommodationConsistent {W : Type u_1} (c : CommonGround.ContextSet W) (presup : Set W) : Prop

Accommodation is consistent iff the restricted context is non-empty — the presupposition is compatible with the context.

Equations

• Core.PresuppositionContext.accommodationConsistent c presup = Set.Nonempty (Core.PresuppositionContext.accommodate c presup)

theorem Core.PresuppositionContext.projects_iff_not_satisfied {W : Type u_1} (c : CommonGround.ContextSet W) (p : Presupposition.PrProp W) : presupProjects c p ↔ ¬presupSatisfied c p

Projection and filtering are complementary.

theorem Core.PresuppositionContext.satisfied_implies_satisfiable {W : Type u_1} (c : CommonGround.ContextSet W) (p : Presupposition.PrProp W) (hne : Set.Nonempty c) (hsat : presupSatisfied c p) : presupSatisfiable c p

Satisfaction implies satisfiability (when the context is non-empty).

theorem Core.PresuppositionContext.not_satisfiable_implies_projects {W : Type u_1} (c : CommonGround.ContextSet W) (p : Presupposition.PrProp W) (hne : Set.Nonempty c) (h : ¬presupSatisfiable c p) : presupProjects c p

If the presupposition is not even satisfiable, it projects.

theorem Core.PresuppositionContext.accommodate_entails_presup {W : Type u_1} (c : CommonGround.ContextSet W) (presup : Set W) : accommodate c presup ⊆ presup

After accommodation, the presupposition is satisfied.

theorem Core.PresuppositionContext.accommodate_idempotent {W : Type u_1} (c : CommonGround.ContextSet W) (presup : Set W) (h : c ⊆ presup) : accommodate c presup = c

Accommodation is idempotent: accommodating what's already satisfied doesn't change the context.

theorem Core.PresuppositionContext.accommodate_strengthens {W : Type u_1} (c : CommonGround.ContextSet W) (presup : Set W) : accommodate c presup ⊆ c

Accommodation strengthens the context: fewer worlds survive.

theorem Core.PresuppositionContext.accommodationConsistent_iff_satisfiable {W : Type u_1} (c : CommonGround.ContextSet W) (p : Presupposition.PrProp W) : accommodationConsistent c p.presup ↔ presupSatisfiable c p

Accommodation consistency = presupposition satisfiable in context.

theorem Core.PresuppositionContext.accommodate_eq_defined {W : Type u_1} (c : CommonGround.ContextSet W) (p : Presupposition.PrProp W) (w : W) : w ∈ accommodate c p.presup ↔ w ∈ c ∧ Presupposition.PrProp.defined w p

Accommodation via PrProp.defined: accommodating p.presup restricts to worlds where p.defined holds.

@[reducible, inline]

abbrev Core.PresuppositionContext.presupSatisfiedIn {W : Type u_1} {S : Type u_2} [CommonGround.HasContextSet S W] (s : S) (p : Presupposition.PrProp W) : Prop

Presupposition satisfied relative to any discourse state with a context set. Works with CG W, Commitment.CommitmentSlate W, LocalCtx W, and any other state implementing HasContextSet.

Equations

• Core.PresuppositionContext.presupSatisfiedIn s p = Core.PresuppositionContext.presupSatisfied (Core.CommonGround.HasContextSet.toContextSet s) p

@[reducible, inline]

abbrev Core.PresuppositionContext.presupSatisfiableIn {W : Type u_1} {S : Type u_2} [CommonGround.HasContextSet S W] (s : S) (p : Presupposition.PrProp W) : Prop

Presupposition satisfiable (conceivable) relative to any discourse state.

Equations

• Core.PresuppositionContext.presupSatisfiableIn s p = Core.PresuppositionContext.presupSatisfiable (Core.CommonGround.HasContextSet.toContextSet s) p

@[reducible, inline]

abbrev Core.PresuppositionContext.presupProjectsFrom {W : Type u_1} {S : Type u_2} [CommonGround.HasContextSet S W] (s : S) (p : Presupposition.PrProp W) : Prop

Presupposition projects from any discourse state.

Equations

• Core.PresuppositionContext.presupProjectsFrom s p = Core.PresuppositionContext.presupProjects (Core.CommonGround.HasContextSet.toContextSet s) p