Beaver (2001) @cite{beaver-2001}

Presupposition and Assertion in Dynamic Semantics: A Critical Review of Linguistic Theories of Presupposition. CSLI Publications.

Overview

Beaver's monograph compares four families of presupposition theory in Part I, then develops his own dynamic theory (PUL) in Part II:

Part I: A Critical Review (Chs. 1-5)

1. Ch. 1: Introduction — presupposition identification, basic data
2. Ch. 2 Multivalence: Strong Kleene, Weak Kleene, Middle Kleene (§1-2)
3. Ch. 3 Cancellation and filtering: Karttunen's heritage functions, Heim's CCP, the convergence of heritage/filtering/CCP (§3)
4. Ch. 4 Common ground: Stalnaker's context sets, File Change Semantics, DPL — all compute from PrProp.presup and PrProp.assertion (§4)
5. Ch. 5 Accommodation: Lewis 1979, van der Sandt 1992, Heim's global-preference synthesis, conditional presuppositions (§5-6)

Part II: A Dynamic Theory (Chs. 6-10) 6. Ch. 6 PUL: Presuppositional Update Logic — Beaver's formalism (§7) 7. Ch. 7 ABLE: "A Bit Like English" — fragment mapping English to PUL 8. Ch. 8 Quantification: Presupposition projection under quantifiers 9. Ch. 9 Accommodation in ABLE: Accommodation within PUL 10. Ch. 10 Conclusion: Summary and open problems

Structural Connection to PrProp

The central insight formalized here: Karttunen's heritage functions, Heim's filtering connectives, and CCP-based local contexts all compute projection from the same source — PrProp.presup.

• Heritage function for p → q = (impFilter p q).presup (by construction)
• Local context for q in p → q = { w ∈ c | p.assertion w } (from PrProp)
• Accommodation operates on p.presup directly

PrProp IS the two-dimensional representation of @cite{karttunen-peters-1979}: .presup = their P-function, .assertion = their A-function. The filtering connectives resolve the "binding problem" (variables not linked between dimensions) by computing compound presuppositions from BOTH .presup and .assertion fields of the same PrProp W — the shared type parameter W ensures variables range over the same domain.

No separate heritage type is needed. Filtering connectives ARE heritage functions — the .presup field of a filtering connective IS the heritage function output.

Formalization Coverage

This file formalizes key results from Chs. 2-7. The ABLE fragment (Ch. 7) is formalized in Theories.Semantics.Dynamic.ABLE.Basic and demonstrated here via worked examples (§8). Quantifier projection (Ch. 8) and ABLE accommodation (Ch. 9) are not yet formalized. Quantifier projection is partially addressed by the QuantifierProjection type in PresuppositionPolarity.lean.

SK vs MK: Symmetry and Presupposition Projection

Strong Kleene disjunction is symmetric: join a b = join b a. Middle Kleene disjunction is NOT: joinMiddle a b ≠ joinMiddle b a in general. Natural language disjunction appears to be symmetric for presupposition projection, which favors the SK/heritage prediction over CCP.

Fact 2.1: SK Projection Predictions

@cite{beaver-2001} Fact 2.1 gives the SK projection predictions for all binary connectives. The hallmark of SK is uniformity: every binary connective (∧, ∨, →) predicts the same presupposition — π(φ) ∧ π(ψ) — and symmetry: swapping φ and ψ does not change the projection.

This uniformity is empirically too strong: "if p then q" presupposes π(p) ∧ (A(p) → π(q)), not π(p) ∧ π(q). The filtering connectives (PrProp.impFilter, etc.) capture this asymmetry.

theorem Phenomena.Presupposition.Studies.Beaver2001.sk_disjunction_symmetric (a b : Core.Duality.Truth3) : a.join b = b.join a

SK disjunction is symmetric for presupposition projection. @cite{beaver-2001} Ch. 2: the correct empirical prediction.

theorem Phenomena.Presupposition.Studies.Beaver2001.mk_disjunction_asymmetric : ∃ (a : Core.Duality.Truth3) (b : Core.Duality.Truth3), a.joinMiddle b ≠ b.joinMiddle a

MK disjunction is NOT symmetric. @cite{beaver-2001} Ch. 2: MK captures left-to-right processing but overpredicts asymmetry for disjunction.

theorem Phenomena.Presupposition.Studies.Beaver2001.sk_neg_presup {W : Type u_1} (p : Core.Presupposition.PrProp W) : p.neg.presup = p.presup

Fact 2.1, negation: SK negation preserves presupposition. The presupposition of ¬φ is exactly π(φ).

theorem Phenomena.Presupposition.Studies.Beaver2001.sk_binary_presup_uniform {W : Type u_1} (p q : Core.Presupposition.PrProp W) : (p.and q).presup = (p.or q).presup ∧ (p.or q).presup = (p.imp q).presup

Fact 2.1, uniformity: all SK binary connectives produce the SAME presupposition — π(φ) ∧ π(ψ) — regardless of the connective. This is the hallmark of the SK approach: conjunction, disjunction, and implication are indistinguishable from the presupposition's perspective.

theorem Phenomena.Presupposition.Studies.Beaver2001.sk_presup_symmetric {W : Type u_1} (p q : Core.Presupposition.PrProp W) : (p.and q).presup = (q.and p).presup

Fact 2.1, symmetry: SK binary presuppositions are symmetric. Swapping φ and ψ does not change the presupposition.

theorem Phenomena.Presupposition.Studies.Beaver2001.filtering_presup_not_symmetric : ∃ (p : Core.Presupposition.PrProp Bool) (q : Core.Presupposition.PrProp Bool), (p.andFilter q).presup ≠ (q.andFilter p).presup

Filtering presuppositions are NOT symmetric: there exist p, q where swapping the operands changes the presupposition. This is the empirically correct prediction — "if p then q" and "if q then p" have different presuppositions.

The Two-Dimensional Approach

@cite{karttunen-peters-1979} proposed parallel translation functions A(·) and P(·) that compute assertion and presupposition separately. This is structurally identical to PrProp:

• PrProp.assertion = A(·) (assertion translation)
• PrProp.presup = P(·) (presupposition translation)

The binding problem (@cite{beaver-2001} Ch. 2): in Karttunen & Peters' system, quantifier variables in the assertion dimension are not linked to variables in the presupposition dimension. For example, in "Every student stopped smoking", the student bound by "every" in the assertion should be the same student bound in the presupposition — but the two translation functions compute independently.

PrProp resolves this by construction: both .presup and .assertion are functions from the SAME type W. When W includes variable assignments (as in W = World × Assignment), the binding is shared. The filtering connectives explicitly reference both fields of a single PrProp, ensuring the variables agree across dimensions.

theorem Phenomena.Presupposition.Studies.Beaver2001.filtering_links_dimensions {W : Type u_1} (p q : Core.Presupposition.PrProp W) (w : W) : (p.impFilter q).presup w = (p.presup w && (!p.assertion w || q.presup w))

Filtering connectives reference BOTH .presup and .assertion, resolving the binding problem. The presupposition of impFilter p q depends on p.assertion (assertion of the antecedent) — linking the two dimensions.

theorem Phenomena.Presupposition.Studies.Beaver2001.sk_ignores_assertion {W : Type u_1} (p q : Core.Presupposition.PrProp W) (w : W) : (p.and q).presup w = (p.presup w && q.presup w)

SK connectives do NOT link dimensions: they reference only .presup, ignoring .assertion. This means they cannot capture filtering.

Karttunen's heritage function for a connective is the presupposition that the compound inherits from its parts. For filtering connectives, this IS the .presup field — no separate heritage type needed.

The convergence of heritage, filtering, and CCP is @cite{beaver-2001}'s central result for Chs. 2-4. We show it holds by construction: all three read from the same PrProp.presup and PrProp.assertion fields.

theorem Phenomena.Presupposition.Studies.Beaver2001.filtering_weaker_than_sk {W : Type u_1} (p q : Core.Presupposition.PrProp W) (h : ∀ (w : W), p.assertion w = true → q.presup w = true) : (p.andFilter q).presup = p.presup

Filtering vs SK: filtering conjunction is strictly weaker than SK conjunction in its presupposition requirements. When p's assertion entails q's presupposition, filtering drops q's presupposition entirely — SK never does.

The static filtering connectives and the dynamic CCP approach agree for conditionals. Both compute projection from PrProp.presup and PrProp.assertion — when the context entails p's presupposition, filtering holds iff the local context (from p.assertion) entails q's presupposition (from q.presup).

Connection to Common Ground and File Change Semantics

@cite{beaver-2001} Ch. 4 discusses @cite{stalnaker-1974}'s common ground and @cite{heim-1983}'s File Change Semantics in detail. The ContextSet W type used here IS the context set from Core.Semantics.CommonGround. ContextSet.update IS Heim's FCS update: intersect the context set with a proposition, keeping only worlds where the proposition holds.

The local context at position q in p → q is ContextSet.update c p.assertion — exactly Semantics.Presupposition.LocalContext.localCtxConsequent.

theorem Phenomena.Presupposition.Studies.Beaver2001.static_dynamic_agreement {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)

Static filtering = dynamic local context for conditionals. Both derive from PrProp fields: .presup and .assertion. This is the cornerstone theorem connecting three approaches:

1. Static filtering (@cite{karttunen-1973})
2. Heim's CCP / File Change Semantics (@cite{heim-1983})
3. Local contexts (@cite{schlenker-2009})

Heim's observation: global accommodation preference ≈ Gazdar cancellation. Accommodation operates on p.presup directly — the structural connection to PrProp is by construction.

theorem Phenomena.Presupposition.Studies.Beaver2001.heim_synthesis_projection {W : Type u_1} (c : Core.CommonGround.ContextSet W) (p : Core.Presupposition.PrProp W) (h : (Semantics.Presupposition.Accommodation.globalAccommodate c p.presup).nonEmpty) : Semantics.Presupposition.Accommodation.heimSelect c p.presup = Semantics.Presupposition.Accommodation.AccommodationLevel.global

Heim's synthesis: global preference selects global when consistent. Accommodation input is p.presup — structurally connected to PrProp.

theorem Phenomena.Presupposition.Studies.Beaver2001.heim_synthesis_cancellation {W : Type u_1} (c : Core.CommonGround.ContextSet W) (p : Core.Presupposition.PrProp W) (h : ¬(Semantics.Presupposition.Accommodation.globalAccommodate c p.presup).nonEmpty) : Semantics.Presupposition.Accommodation.heimSelect c p.presup = Semantics.Presupposition.Accommodation.AccommodationLevel.local

Heim's synthesis: global preference selects local when inconsistent. This matches Gazdar's cancellation prediction.

@cite{beaver-2001} argues that presuppositions can themselves be conditional. The Spaceman Spiff example:

"If Spaceman Spiff lands on Planet X, he will be bothered by the fact that his weight is greater than it would be on Earth."

The presupposition (Spiff's weight > Earth weight) is not an unconditional global presupposition — it is conditional on the antecedent. Neither filtering nor CCP can systematically produce conditional presuppositions.

inductive Phenomena.Presupposition.Studies.Beaver2001.SpiffWorld : Type

• onEarth : SpiffWorld
• onPlanetX_heavy : SpiffWorld
• onPlanetX_light : SpiffWorld
• inSpace : SpiffWorld

instance Phenomena.Presupposition.Studies.Beaver2001.instDecidableEqSpiffWorld : DecidableEq SpiffWorld

Equations

• Phenomena.Presupposition.Studies.Beaver2001.instDecidableEqSpiffWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Presupposition.Studies.Beaver2001.instReprSpiffWorld.repr : SpiffWorld → ℕ → Std.Format

Equations

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

instance Phenomena.Presupposition.Studies.Beaver2001.instReprSpiffWorld : Repr SpiffWorld

Equations

• Phenomena.Presupposition.Studies.Beaver2001.instReprSpiffWorld = { reprPrec := Phenomena.Presupposition.Studies.Beaver2001.instReprSpiffWorld.repr }

instance Phenomena.Presupposition.Studies.Beaver2001.instInhabitedSpiffWorld : Inhabited SpiffWorld

Equations

• Phenomena.Presupposition.Studies.Beaver2001.instInhabitedSpiffWorld = { default := Phenomena.Presupposition.Studies.Beaver2001.instInhabitedSpiffWorld.default }

def Phenomena.Presupposition.Studies.Beaver2001.instInhabitedSpiffWorld.default : SpiffWorld

Equations

• Phenomena.Presupposition.Studies.Beaver2001.instInhabitedSpiffWorld.default = Phenomena.Presupposition.Studies.Beaver2001.SpiffWorld.onEarth

def Phenomena.Presupposition.Studies.Beaver2001.spiffLands : Core.Presupposition.PrProp SpiffWorld

"Spiff lands on Planet X" — no presupposition.

Equations

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

def Phenomena.Presupposition.Studies.Beaver2001.weightGreater : Core.Presupposition.PrProp SpiffWorld

"Spiff's weight is greater than on Earth" — presupposes being somewhere with weight (not in space).

Equations

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

theorem Phenomena.Presupposition.Studies.Beaver2001.spiff_conditional_filters (w : SpiffWorld) : spiffLands.presup w = true → spiffLands.assertion w = true → weightGreater.presup w = true

Filtering correctly predicts: the antecedent filters the consequent's presupposition.

def Phenomena.Presupposition.Studies.Beaver2001.conditionalPresup : BProp SpiffWorld

The actual presupposition people infer is CONDITIONAL: "IF Spiff lands on Planet X, his weight > Earth weight." This is stronger than what filtering predicts.

Equations

• Phenomena.Presupposition.Studies.Beaver2001.conditionalPresup Phenomena.Presupposition.Studies.Beaver2001.SpiffWorld.onPlanetX_heavy = true
• Phenomena.Presupposition.Studies.Beaver2001.conditionalPresup Phenomena.Presupposition.Studies.Beaver2001.SpiffWorld.onPlanetX_light = false
• Phenomena.Presupposition.Studies.Beaver2001.conditionalPresup w = true

theorem Phenomena.Presupposition.Studies.Beaver2001.conditional_presup_stronger_than_filtering : ∃ (w : SpiffWorld), (spiffLands.impFilter weightGreater).presup w = true ∧ conditionalPresup w = false

The conditional presupposition is NOT equivalent to the filtering prediction. Filtering predicts weight-is-defined; the conditional presupposition additionally requires weight > Earth.

Beaver's Dynamic Theory

PUL is Beaver's own formal system from Part II. It combines partial semantics with dynamic update: presuppositions cause undefinedness of context updates. The core operations map to ContextSet operations:

• Atomic update σ[p] = σ ∩ {w | p(w)} = ContextSet.update σ p
• Negation σ[-φ] = σ \ σ[φ] (set complement within input)
• Conjunction σ[φ ∧ ψ] = σ[φ][ψ] (sequential update)
• Conditional σ[φ → ψ] = σ \ (σ[φ] \ σ[φ][ψ]) (residual)

PUL conjunction is exactly CCP sequential composition (CCP.seq from Theories.Semantics.Dynamic.Core.CCP). PUL negation differs from CCP's test-based negation: PUL computes the complement within the input state, while CCP negation passes or fails the entire state.

Partiality

In Beaver's book, PUL updates are PARTIAL — presupposition failure causes the update to be undefined. Here we define the total operations (the defined cases). The presupposition check is modeled separately through PrProp.presup: a PUL update from a PrProp sentence p is defined at context σ iff ∀ w, σ w → p.presup w = true.

def Phenomena.Presupposition.Studies.Beaver2001.pulUpdate {W : Type u_1} (p : BProp W) (σ : Core.CommonGround.ContextSet W) : Core.CommonGround.ContextSet W

PUL atomic update: intersect context with proposition. @cite{beaver-2001} Ch. 6. Equivalent to ContextSet.update.

Equations

• Phenomena.Presupposition.Studies.Beaver2001.pulUpdate p σ = σ.update p

def Phenomena.Presupposition.Studies.Beaver2001.pulNeg {W : Type u_1} (φ : Core.CommonGround.ContextSet W → Core.CommonGround.ContextSet W) (σ : Core.CommonGround.ContextSet W) : Core.CommonGround.ContextSet W

PUL negation: complement within the input state. σ[-φ] = σ \ σ[φ]. Note: this differs from CCP.neg, which is test-based (pass/fail). PUL negation selects worlds where φ does NOT hold.

Equations

• Phenomena.Presupposition.Studies.Beaver2001.pulNeg φ σ w = (σ w ∧ ¬φ σ w)

def Phenomena.Presupposition.Studies.Beaver2001.pulConj {W : Type u_1} (φ ψ : Core.CommonGround.ContextSet W → Core.CommonGround.ContextSet W) : Core.CommonGround.ContextSet W → Core.CommonGround.ContextSet W

PUL conjunction: sequential update. σ[φ ∧ ψ] = σ[φ][ψ]. This is CCP.seq by construction.

Equations

• Phenomena.Presupposition.Studies.Beaver2001.pulConj φ ψ = ψ ∘ φ

def Phenomena.Presupposition.Studies.Beaver2001.pulImpl {W : Type u_1} (φ ψ : Core.CommonGround.ContextSet W → Core.CommonGround.ContextSet W) (σ : Core.CommonGround.ContextSet W) : Core.CommonGround.ContextSet W

PUL conditional: residual. σ[φ → ψ] = σ \ (σ[φ] \ σ[φ][ψ]). Worlds in σ that survive are those where: if φ holds, then ψ holds in the φ-updated context.

Equations

• Phenomena.Presupposition.Studies.Beaver2001.pulImpl φ ψ σ w = (σ w ∧ ¬(φ σ w ∧ ¬ψ (φ σ) w))

theorem Phenomena.Presupposition.Studies.Beaver2001.pulUpdate_eq {W : Type u_1} (p : BProp W) (σ : Core.CommonGround.ContextSet W) : pulUpdate p σ = σ.update p

PUL atomic update is ContextSet.update (by construction).

theorem Phenomena.Presupposition.Studies.Beaver2001.pulNeg_eliminative {W : Type u_1} (φ : Core.CommonGround.ContextSet W → Core.CommonGround.ContextSet W) (σ : Core.CommonGround.ContextSet W) (w : W) : pulNeg φ σ w → σ w

PUL negation is eliminative: it only removes worlds.

theorem Phenomena.Presupposition.Studies.Beaver2001.pulConj_update {W : Type u_1} (p q : BProp W) (σ : Core.CommonGround.ContextSet W) : pulConj (pulUpdate p) (pulUpdate q) σ = (σ.update p).update q

PUL conjunction of atomic updates equals iterated context update.

theorem Phenomena.Presupposition.Studies.Beaver2001.pulImpl_atomic {W : Type u_1} (p q : BProp W) (σ : Core.CommonGround.ContextSet W) (w : W) : pulImpl (pulUpdate p) (pulUpdate q) σ w ↔ σ w ∧ (p w = true → q w = true)

PUL conditional on atomic propositions: a world survives iff it is in σ and the material conditional holds. When φ = pulUpdate p and ψ = pulUpdate q, the conditional simplifies to the classical material conditional on the proposition values.

ABLE Fragment Demonstrations

The ABLE formalization in Theories.Semantics.Dynamic.ABLE.Basic provides the Formula type and its evaluation semantics. Here we instantiate it with the Spaceman Spiff scenario from §6 to demonstrate projection through negation and conditionals.

Key correspondences to PUL:

• Formula.presup (∂) = CCP.must — full support test (D59)
• Formula.and = CCP.seq — sequential composition
• Formula.might = CCP.might — compatibility test
• Formula.not ≠ CCP.neg — PUL negation is set complement, not pass/fail

Structural Admittance (D54)

Admittance is the mechanism by which presuppositions project. A context σ admits a formula φ iff every subformula's presupposition is satisfied at its local context (the context that results from processing prior material). This is why presupposition projection is asymmetric for conjunction: in φ AND ψ, σ must admit φ, and σ[φ] must admit ψ — so ψ's presupposition can be "filtered" by φ's content.

def Phenomena.Presupposition.Studies.Beaver2001.spiffState : Set SpiffWorld

Represent the Spiff scenario as a set-based info state. Each element of the set is a possible world.

Equations

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

def Phenomena.Presupposition.Studies.Beaver2001.ableLands : Semantics.Dynamic.ABLE.Formula SpiffWorld

ABLE formula: "Spiff lands on Planet X" (no presupposition).

Equations

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

def Phenomena.Presupposition.Studies.Beaver2001.ableWeightGreater : Semantics.Dynamic.ABLE.Formula SpiffWorld

ABLE formula: "Spiff's weight > Earth weight" with presupposition ∂(has-weight).

Equations

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

theorem Phenomena.Presupposition.Studies.Beaver2001.spiff_full_state_rejects_weight : ¬ableWeightGreater.pulAdmits spiffState

Admitting "weight > Earth" requires the context to entail has-weight. The full info state does NOT admit it (space is included).

theorem Phenomena.Presupposition.Studies.Beaver2001.spiff_lands_then_weight_admits : ableWeightGreater.pulAdmits (ableLands.eval spiffState)

After learning "Spiff lands on Planet X", the state admits "weight > Earth". This is Fact 8.3: the conditional presupposition is satisfied.