Accommodation

@cite{lewis-1979} @cite{beaver-2001} @cite{van-der-sandt-1992}

Accommodation is the process by which a context is adjusted to satisfy a presupposition that is not already entailed. @cite{lewis-1979} introduced the concept: "If at time t something is said that requires presupposition P to be acceptable, and if P is not presupposed just before t, then — ceteris paribus — presupposition P comes into existence at t."

Three Levels (@cite{beaver-2001} Ch. 5)

• Global: presupposition is added to the top-level common ground
• Local: presupposition is satisfied within the embedded context
• Intermediate: presupposition is added at an intermediate level (into the restrictor of a quantifier or antecedent of a conditional)

Three Strategies

1. Heim/Lewis preference: prefer global > intermediate > local. Global preference + consistency constraint ≈ Gazdar's cancellation (@cite{beaver-2001} Ch. 5.8.1).
2. Van der Sandt structural: DRT-based move-α; presupposition DRS is moved to the highest accessible position (@cite{van-der-sandt-1992}).
3. Fauconnier flotation: presupposition floats upward through mental spaces, leaving a shadow at each level (@cite{beaver-2001} Ch. 5.8.3).

Constraints (@cite{beaver-2001} Ch. 5.3)

• Informativity: accommodation must be informative (add new information)
• Consistency: accommodated content must be consistent with the context
• Trapping: bound presuppositions cannot escape their binder's scope
• Binding preference: anaphoric resolution is preferred over accommodation

inductive Semantics.Presupposition.Accommodation.AccommodationLevel : Type

The level at which accommodation occurs. @cite{beaver-2001} Ch. 5, @cite{lewis-1979}, @cite{heim-1983}.

• global : AccommodationLevel

  Add presupposition to the global common ground.

• local : AccommodationLevel

  Satisfy presupposition within the local embedded context.

• intermediate (depth : ℕ) : AccommodationLevel

  Add presupposition at an intermediate level (e.g., restrictor of a quantifier, antecedent of a conditional). @cite{beaver-2001} Ch. 5.5 argues this is heavily restricted.

def Semantics.Presupposition.Accommodation.instDecidableEqAccommodationLevel.decEq (x✝ x✝¹ : AccommodationLevel) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Presupposition.Accommodation.instDecidableEqAccommodationLevel : DecidableEq AccommodationLevel

Equations

• Semantics.Presupposition.Accommodation.instDecidableEqAccommodationLevel = Semantics.Presupposition.Accommodation.instDecidableEqAccommodationLevel.decEq

def Semantics.Presupposition.Accommodation.instReprAccommodationLevel.repr : AccommodationLevel → ℕ → Std.Format

Equations

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

instance Semantics.Presupposition.Accommodation.instReprAccommodationLevel : Repr AccommodationLevel

Equations

• Semantics.Presupposition.Accommodation.instReprAccommodationLevel = { reprPrec := Semantics.Presupposition.Accommodation.instReprAccommodationLevel.repr }

def Semantics.Presupposition.Accommodation.globalAccommodate {W : Type u_1} (c : Core.CommonGround.ContextSet W) (presup : BProp W) : Core.CommonGround.ContextSet W

Global accommodation: update the context to include the presupposition. @cite{lewis-1979}: "presupposition P comes into existence."

Formally, this intersects the context set with the presupposition, removing worlds where the presupposition fails.

Equations

• Semantics.Presupposition.Accommodation.globalAccommodate c presup w = (c w ∧ presup w = true)

theorem Semantics.Presupposition.Accommodation.globalAccommodate_strengthens {W : Type u_1} (c : Core.CommonGround.ContextSet W) (presup : BProp W) (w : W) : globalAccommodate c presup w → c w

Global accommodation strengthens the context (is eliminative).

theorem Semantics.Presupposition.Accommodation.globalAccommodate_entails {W : Type u_1} (c : Core.CommonGround.ContextSet W) (presup : BProp W) : globalAccommodate c presup ⊧ presup

After global accommodation, the presupposition is entailed.

theorem Semantics.Presupposition.Accommodation.globalAccommodate_idempotent {W : Type u_1} (c : Core.CommonGround.ContextSet W) (presup : BProp W) (h : c ⊧ presup) (w : W) : globalAccommodate c presup w ↔ c w

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

theorem Semantics.Presupposition.Accommodation.globalAccommodate_eq_defined {W : Type u_1} (c : Core.CommonGround.ContextSet W) (p : Core.Presupposition.PrProp W) (w : W) : globalAccommodate c p.presup w ↔ c w ∧ Core.Presupposition.PrProp.defined w p

Accommodation via PrProp.defined: globalAccommodate c p.presup restricts the context to points where PrProp.defined holds. This is the structural connection between accommodation and PrProp — accommodation targets .presup by construction.

def Semantics.Presupposition.Accommodation.isInformative {W : Type u_1} (c : Core.CommonGround.ContextSet W) (presup : BProp W) : Prop

Informativity: the accommodated content must add new information. The context must not already entail the presupposition. @cite{beaver-2001} Ch. 5.3.

Equations

• Semantics.Presupposition.Accommodation.isInformative c presup = ¬c ⊧ presup

def Semantics.Presupposition.Accommodation.isConsistent {W : Type u_1} (c : Core.CommonGround.ContextSet W) (presup : BProp W) : Prop

Consistency: the result of accommodation must be non-empty. @cite{beaver-2001} Ch. 5.3.

Equations

• Semantics.Presupposition.Accommodation.isConsistent c presup = (Semantics.Presupposition.Accommodation.globalAccommodate c presup).nonEmpty

def Semantics.Presupposition.Accommodation.isTrapped (bindingDepth : ℕ) : AccommodationLevel → Bool

Trapping: a presupposition with a bound variable cannot be accommodated above its binder. @cite{beaver-2001} Ch. 5.3.

Modeled as a predicate on the accommodation level and a binding depth: accommodation at level l is trapped if the presupposition is bound at depth d and l would place it above d.

Equations

• Semantics.Presupposition.Accommodation.isTrapped bindingDepth Semantics.Presupposition.Accommodation.AccommodationLevel.global = true
• Semantics.Presupposition.Accommodation.isTrapped bindingDepth (Semantics.Presupposition.Accommodation.AccommodationLevel.intermediate d) = decide (d < bindingDepth)
• Semantics.Presupposition.Accommodation.isTrapped bindingDepth Semantics.Presupposition.Accommodation.AccommodationLevel.local = false

structure Semantics.Presupposition.Accommodation.AccommodationOK {W : Type u_1} (c : Core.CommonGround.ContextSet W) (presup : BProp W) : Prop

All constraints bundled together.

• informative : isInformative c presup
• consistent : isConsistent c presup

inductive Semantics.Presupposition.Accommodation.AccommodationStrategy : Type

An accommodation strategy determines which level of accommodation is preferred. @cite{beaver-2001} Ch. 5.8.

• heimPreference : AccommodationStrategy

  Heim/Lewis: prefer global, fall back to local if global is inconsistent. Global preference ≈ projection; local fallback ≈ cancellation. @cite{heim-1983}, @cite{lewis-1979}.

• vanDerSandt : AccommodationStrategy

  Van der Sandt: DRT-based move-α. Presupposition DRS is moved to the highest accessible position that satisfies binding constraints. @cite{van-der-sandt-1992}.

• fauconnierFlotation : AccommodationStrategy

  Fauconnier: presupposition floats upward through mental spaces, leaving a copy ("shadow") at each intermediate level. @cite{beaver-2001} Ch. 5.8.3.

instance Semantics.Presupposition.Accommodation.instDecidableEqAccommodationStrategy : DecidableEq AccommodationStrategy

Equations

• Semantics.Presupposition.Accommodation.instDecidableEqAccommodationStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Presupposition.Accommodation.instReprAccommodationStrategy : Repr AccommodationStrategy

Equations

• Semantics.Presupposition.Accommodation.instReprAccommodationStrategy = { reprPrec := Semantics.Presupposition.Accommodation.instReprAccommodationStrategy.repr }

def Semantics.Presupposition.Accommodation.instReprAccommodationStrategy.repr : AccommodationStrategy → ℕ → Std.Format

Equations

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

noncomputable def Semantics.Presupposition.Accommodation.heimSelect {W : Type u_1} (c : Core.CommonGround.ContextSet W) (presup : BProp W) : AccommodationLevel

Select accommodation level based on the Heim/Lewis strategy.

Try global first; if inconsistent, fall back to local.

@cite{heim-1983}: "by stipulating a ceteris paribus preference for global over local accommodation, we recapture the effect of Gazdar's assumption that presupposition cancellation occurs only under the threat of inconsistency."

Equations

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

theorem Semantics.Presupposition.Accommodation.heim_cancellation_equivalence {W : Type u_1} (c : Core.CommonGround.ContextSet W) (presup : BProp W) (h_inconsistent : ¬(globalAccommodate c presup).nonEmpty) : heimSelect c presup = AccommodationLevel.local

Heim's observation: global accommodation preference is equivalent to Gazdar's cancellation under threat of inconsistency.

When global accommodation would be inconsistent, we fall back to local accommodation — which has the same effect as Gazdar's presupposition cancellation.

@cite{beaver-2001} Ch. 5.8.1: "with one short remark buried in a terse paper, Heim offers a simple synthesis between the two antitheses of 1970s presupposition theory."

theorem Semantics.Presupposition.Accommodation.heim_projection_when_consistent {W : Type u_1} (c : Core.CommonGround.ContextSet W) (presup : BProp W) (h_consistent : (globalAccommodate c presup).nonEmpty) : heimSelect c presup = AccommodationLevel.global

When global accommodation IS consistent, Heim's strategy projects the presupposition globally — matching Karttunen's projection.

theorem Semantics.Presupposition.Accommodation.heim_never_intermediate {W : Type u_1} (c : Core.CommonGround.ContextSet W) (presup : BProp W) (d : ℕ) : heimSelect c presup ≠ AccommodationLevel.intermediate d

Intermediate accommodation is problematic.

@cite{beaver-2001} Ch. 5.5 argues that intermediate accommodation (accommodation into the restrictor of a quantifier or antecedent of a conditional) is heavily restricted and only occurs with generic/habitual statements. Without intermediate accommodation, both Heim's CCP and van der Sandt's DRT make better predictions.

This is formalized as: the Heim preference strategy never selects intermediate accommodation.

inductive Semantics.Presupposition.Accommodation.TriggerClass : Type

Van der Sandt vs. Fauconnier: the key difference is whether accommodation leaves shadows at intermediate levels.

• Van der Sandt: presupposition jumps to highest position, no trace at intermediate levels.
• Fauconnier: presupposition floats up, leaving a copy at each level it passes through.

@cite{beaver-2001} Ch. 5.8.3: Fauconnier's strategy correctly predicts that lexical triggers (factives) must hold at all intermediate levels, while anaphoric triggers (definites, 'too') only need to hold at the highest level.

• anaphoric : TriggerClass

  Anaphoric/resolution triggers: definites, 'too', 'again'. Collect entities from context. Use van der Sandt strategy.

• lexical : TriggerClass

  Lexical triggers: factives ('know', 'regret'). Impose conditions on concept application. Use Fauconnier strategy.

instance Semantics.Presupposition.Accommodation.instDecidableEqTriggerClass : DecidableEq TriggerClass

Equations

• Semantics.Presupposition.Accommodation.instDecidableEqTriggerClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Presupposition.Accommodation.instReprTriggerClass : Repr TriggerClass

Equations

• Semantics.Presupposition.Accommodation.instReprTriggerClass = { reprPrec := Semantics.Presupposition.Accommodation.instReprTriggerClass.repr }

def Semantics.Presupposition.Accommodation.instReprTriggerClass.repr : TriggerClass → ℕ → Std.Format

Equations

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

def Semantics.Presupposition.Accommodation.strategyForTrigger : TriggerClass → AccommodationStrategy

Select accommodation strategy based on trigger class. @cite{beaver-2001} Ch. 5.8, following Zeevat (1992).

Equations

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