Presupposition–Context Bridge

[Sta74] [Hei83] [Lew79b]

Canonical operations connecting presuppositions (PartialProp W) to contexts (ContextSet W): the shared vocabulary for projection, filtering, accommodation, and conceivability.

Main declarations

• presupSatisfied — the context entails the presupposition (filtering).
• presupSatisfiable — some context world satisfies it (conceivability).
• presupProjects — the context does not entail it (projection).
• accommodate — restrict the context to presupposition worlds.

Conceivability

presupSatisfiable is the conceivability check needed for [Eng24]'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.

Core operations

@[reducible, inline]

abbrev Semantics.Presupposition.Context.presupSatisfied {W : Type u_1} (c : CommonGround.ContextSet W) (p : PartialProp 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

• Semantics.Presupposition.Context.presupSatisfied c p = (c ⊆ p.presup)

@[reducible, inline]

abbrev Semantics.Presupposition.Context.presupSatisfiable {W : Type u_1} (c : CommonGround.ContextSet W) (p : PartialProp 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

• Semantics.Presupposition.Context.presupSatisfiable c p = Set.Nonempty (c ∩ p.presup)

@[reducible, inline]

abbrev Semantics.Presupposition.Context.presupProjects {W : Type u_1} (c : CommonGround.ContextSet W) (p : PartialProp W) : Prop

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

Equations

• Semantics.Presupposition.Context.presupProjects c p = ¬Semantics.Presupposition.Context.presupSatisfied c p

@[reducible, inline]

abbrev Semantics.Presupposition.Context.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.

[Lew79b]: "presupposition P comes into existence."

Equations

• Semantics.Presupposition.Context.accommodate c presup = c ∩ presup

@[reducible, inline]

abbrev Semantics.Presupposition.Context.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

• Semantics.Presupposition.Context.accommodationInformative c presup = ¬c ⊆ presup

@[reducible, inline]

abbrev Semantics.Presupposition.Context.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

• Semantics.Presupposition.Context.accommodationConsistent c presup = Set.Nonempty (Semantics.Presupposition.Context.accommodate c presup)

Theorems

theorem Semantics.Presupposition.Context.satisfied_implies_satisfiable {W : Type u_1} (c : CommonGround.ContextSet W) (p : PartialProp W) (hne : Set.Nonempty c) (hsat : presupSatisfied c p) : presupSatisfiable c p

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

theorem Semantics.Presupposition.Context.not_satisfiable_implies_projects {W : Type u_1} (c : CommonGround.ContextSet W) (p : PartialProp W) (hne : Set.Nonempty c) (h : ¬presupSatisfiable c p) : presupProjects c p

If the presupposition is not even satisfiable, it projects.

theorem Semantics.Presupposition.Context.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 Semantics.Presupposition.Context.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 Semantics.Presupposition.Context.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 Semantics.Presupposition.Context.accommodationConsistent_iff_satisfiable {W : Type u_1} (c : CommonGround.ContextSet W) (p : PartialProp W) : accommodationConsistent c p.presup ↔ presupSatisfiable c p

Accommodation consistency = presupposition satisfiable in context.

theorem Semantics.Presupposition.Context.accommodate_eq_defined {W : Type u_1} (c : CommonGround.ContextSet W) (p : PartialProp W) (w : W) : w ∈ accommodate c p.presup ↔ w ∈ c ∧ PartialProp.defined w p

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

Local contexts (satisfaction tradition)

Per-connective local contexts, stipulated in the satisfaction tradition ([Kar74a], [Hei83]); [Sch09a]'s algorithm reconstructs these clauses from bivalent meanings plus incremental transparency. A presupposition is filtered at a position iff the local context there satisfies it (presupSatisfied), and projects otherwise (presupProjects).

def Semantics.Presupposition.Context.localCtxConsequent {W : Type u_1} (c : CommonGround.ContextSet W) (antecedent : PartialProp W) : CommonGround.ContextSet W

Local context for the consequent of a conditional — and equally for the second conjunct: "If P then Q" / "P and Q" give Q the local context c + P.assertion (the shared rule behind PartialProp.impFilter_presup_eq_andFilter_presup).

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.Context.localCtxConsequent c antecedent = c.update antecedent.assertion

def Semantics.Presupposition.Context.localCtxSecondDisjunct {W : Type u_1} (c : CommonGround.ContextSet W) (first : PartialProp W) : CommonGround.ContextSet W

Local context for the second disjunct: "P or Q" gives Q the local context c + ¬P.assertion ([Sch09a], reconstructing [Kar73]'s asymmetric disjunction rule).

Equations

• Semantics.Presupposition.Context.localCtxSecondDisjunct c first w = (c w ∧ ¬first.assertion w)

def Semantics.Presupposition.Context.localCtxNegation {W : Type u_1} (c : CommonGround.ContextSet W) : CommonGround.ContextSet W

Local context under negation: unchanged — negation is a hole ([Kar73]).

Equations

• Semantics.Presupposition.Context.localCtxNegation c = c

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

Presupposition of the consequent is filtered when the antecedent's assertion entails the presupposition throughout the context.

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

If the antecedent's assertion doesn't entail the consequent's presupposition somewhere in the context, it projects.

theorem Semantics.Presupposition.Context.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 stipulated local-context computation agrees with the Karttunen filtering implication formula ([Kar73], [Pet79]).

theorem Semantics.Presupposition.Context.local_context_matches_disjFilterLeft {W : Type u_1} (c : CommonGround.ContextSet W) (firstDisjunct second : PartialProp W) : presupSatisfied (localCtxSecondDisjunct 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]