Beaver (2001): Presupposition and Assertion in Dynamic Semantics

[Bea01] reviews the theories of presupposition (Part I) and develops a dynamic one (Part II): partial update logic, [Vel96]'s update logic — atomic updates eliminate worlds, not removes the worlds the negated sentence keeps, and sequences, and might/must test the state — with a presupposition operator ∂ whose update is defined only in contexts that already satisfy its argument (Ch. 6), then extended to the first-order fragment ABLE (Ch. 7). This file formalizes the propositional core over the substrate's partial context change potentials: a sentence denotes a partial function on information states (Formula.eval : CCP.Partial W), a state satisfies a sentence when it is a fixed point (D29, Satisfies), admits it when the update is defined (D30, CCP.Partial.admits), one sentence presupposes another when every admitting state satisfies it (D31, D46, Presupposes), and entails it when every update with it lands in a satisfying state (D26, D45, Entails). Discourse markers, determiners and accommodation (Chs. 7–9) are outside the propositional fragment.

Two results from Part I are stated on the static side: under the Strong Kleene connectives presuppositions are conditionalised rather than projected or filtered — φ ∧ ψ presupposes ψ → π and φ ∨ ψ presupposes ¬ψ → π when φ presupposes π, maximally so when ψ is bivalent (Fact 2.1: andStrong_presup_iff, orStrong_presup_iff). On the dynamic side: must is the dual of might (Fact 6.1, eval_must); every update is eliminative (Fact 7.1, eval_eliminative); presuppositions project through negation, conjunction, the conditional and the modals, and compose (Facts 8.1, 8.2, 8.8: Presupposes.not, .and_left, .implies_left, .might, .must, .trans); a presupposition of the second conjunct or the consequent projects conditionalised on the first conjunct or the antecedent (Fact 8.3: Presupposes.and_right, .implies_right) — so 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 (E154) presupposes that if he lands there his weight is greater, and not that it is (e154, e154_not_unconditional); might is a consistency test and must a satisfaction test (D61, Fact 8.5, Lemma 8.6, Fact 8.7). Finally, on the sentences without modals Peters' trivalent semantics (D70–D71, tval: the middle Kleene connectives, ∂φ undefined unless φ is true) and the update semantics agree world by world (Lemma 10.1, trueAt_iff, falseAt_iff), the non-modal updates are distributive (Fact A.2, mem_eval_iff), and the two entailment notions coincide (Lemma 10.2, Fact 10.3: entails_iff, entails_iff_tval), whence a non-modal sentence presupposes exactly what both it and its negation entail (presupposes_iff).

Strong Kleene conditionalises presuppositions (Fact 2.1)

theorem Beaver2001.andStrong_presup_iff {W : Type u_1} (p q : Semantics.Presupposition.PartialProp W) {w : W} (hq : q.presup w) : (p.andStrong q).presup w ↔ q.assertion w → p.presup w

Under Strong Kleene conjunction, if φ presupposes π then φ ∧ ψ presupposes ψ → π, and when ψ is bivalent this is its presupposition.

theorem Beaver2001.orStrong_presup_iff {W : Type u_1} (p q : Semantics.Presupposition.PartialProp W) {w : W} (hq : q.presup w) : (p.orStrong q).presup w ↔ ¬q.assertion w → p.presup w

Under Strong Kleene disjunction, if φ presupposes π then φ ∨ ψ presupposes ¬ψ → π, and when ψ is bivalent this is its presupposition.

Partial update logic (Ch. 6)

inductive Beaver2001.Formula (W : Type u_2) : Type u_2

The sentences of partial update logic (D22, D34), with atoms interpreted directly as sets of worlds.

• atom {W : Type u_2} (p : Set W) : Formula W
• not {W : Type u_2} (φ : Formula W) : Formula W
• and {W : Type u_2} (φ ψ : Formula W) : Formula W
• might {W : Type u_2} (φ : Formula W) : Formula W
• must {W : Type u_2} (φ : Formula W) : Formula W
• presup {W : Type u_2} (φ : Formula W) : Formula W

def Beaver2001.Formula.implies {W : Type u_1} (φ ψ : Formula W) : Formula W

φ implies ψ is not (φ and not ψ) (D25).

Equations

• φ.implies ψ = (φ.and ψ.not).not

def Beaver2001.Formula.or {W : Type u_1} (φ ψ : Formula W) : Formula W

φ or ψ is not (not φ and not ψ) (D52).

Equations

• φ.or ψ = (φ.not.and ψ.not).not

noncomputable def Beaver2001.Formula.eval {W : Type u_1} : Formula W → DynamicSemantics.CCP.Partial W

The update a sentence denotes (D25, D35): a partial function on information states, defined for ∂φ only at states that are fixed points of φ.

Equations

• (Beaver2001.Formula.atom p).eval = fun (σ : Set W) => Part.some {w : W | w ∈ σ ∧ w ∈ p}
• φ.not.eval = φ.eval.neg
• (φ.and ψ).eval = φ.eval.seq ψ.eval
• φ.might.eval = fun (σ : Set W) => Part.map (fun (υ : Set W) => if υ.Nonempty then σ else ∅) (φ.eval σ)
• φ.must.eval = fun (σ : Set W) => Part.map (fun (υ : Set W) => if υ = σ then σ else ∅) (φ.eval σ)
• φ.presup.eval = fun (σ : Set W) => { Dom := σ ∈ φ.eval σ, get := fun (x : σ ∈ φ.eval σ) => σ }

theorem Beaver2001.Formula.mem_eval_atom {W : Type u_1} {σ τ p : Set W} : τ ∈ (atom p).eval σ ↔ τ = {w : W | w ∈ σ ∧ w ∈ p}

theorem Beaver2001.Formula.mem_eval_not {W : Type u_1} {φ : Formula W} {σ τ : Set W} : τ ∈ φ.not.eval σ ↔ ∃ υ ∈ φ.eval σ, σ \ υ = τ

theorem Beaver2001.Formula.mem_eval_and {W : Type u_1} {φ ψ : Formula W} {σ τ : Set W} : τ ∈ (φ.and ψ).eval σ ↔ ∃ υ ∈ φ.eval σ, τ ∈ ψ.eval υ

theorem Beaver2001.Formula.mem_eval_might {W : Type u_1} {φ : Formula W} {σ τ : Set W} : τ ∈ φ.might.eval σ ↔ ∃ υ ∈ φ.eval σ, (if υ.Nonempty then σ else ∅) = τ

theorem Beaver2001.Formula.mem_eval_must {W : Type u_1} {φ : Formula W} {σ τ : Set W} : τ ∈ φ.must.eval σ ↔ ∃ υ ∈ φ.eval σ, (if υ = σ then σ else ∅) = τ

theorem Beaver2001.Formula.mem_eval_presup {W : Type u_1} {φ : Formula W} {σ τ : Set W} : τ ∈ φ.presup.eval σ ↔ σ ∈ φ.eval σ ∧ τ = σ

theorem Beaver2001.Formula.eval_eliminative {W : Type u_1} (φ : Formula W) {σ τ : Set W} : τ ∈ φ.eval σ → τ ⊆ σ

Every update is eliminative (Fact 7.1, Fact A.1): outputs are subsets of the input.

theorem Beaver2001.Formula.empty_mem_eval_empty {W : Type u_1} (φ : Formula W) : ∅ ∈ φ.eval ∅

The absurd state admits every sentence and is its own update.

def Beaver2001.Formula.Satisfies {W : Type u_1} (σ : Set W) (φ : Formula W) : Prop

σ satisfies φ (D29): σ[φ]σ.

Equations

• Beaver2001.Formula.Satisfies σ φ = (σ ∈ φ.eval σ)

def Beaver2001.Formula.Presupposes {W : Type u_1} (φ ψ : Formula W) : Prop

φ presupposes ψ (D31, D46): every state admitting φ satisfies ψ.

Equations

• φ.Presupposes ψ = ∀ (σ : Set W), φ.eval.admits σ → Beaver2001.Formula.Satisfies σ ψ

def Beaver2001.Formula.Entails {W : Type u_1} (φ ψ : Formula W) : Prop

φ entails ψ (D26, D45): every update with φ yields a state satisfying ψ.

Equations

• φ.Entails ψ = ∀ (σ τ : Set W), τ ∈ φ.eval σ → Beaver2001.Formula.Satisfies τ ψ

def Beaver2001.Formula.ConsistentWith {W : Type u_1} (σ : Set W) (φ : Formula W) : Prop

σ is consistent with φ (MP7): updating does not reach the absurd state.

Equations

• Beaver2001.Formula.ConsistentWith σ φ = ∃ τ ∈ φ.eval σ, τ.Nonempty

def Beaver2001.Formula.IsTest {W : Type u_1} (φ : Formula W) : Prop

A test (D61): its only outputs are the input and the absurd state.

Equations

• φ.IsTest = ∀ (σ τ : Set W), τ ∈ φ.eval σ → τ = σ ∨ τ = ∅

theorem Beaver2001.Formula.admits_of_mem {W : Type u_1} {φ : Formula W} {σ τ : Set W} (h : τ ∈ φ.eval σ) : φ.eval.admits σ

theorem Beaver2001.Formula.Satisfies.admits {W : Type u_1} {φ : Formula W} {σ : Set W} (h : Satisfies σ φ) : φ.eval.admits σ

theorem Beaver2001.Formula.eval_must {W : Type u_1} (φ : Formula W) : φ.must.eval = φ.not.might.not.eval

must is the dual of might (Fact 6.1).

Projection (Facts 8.1–8.3, 8.8)

theorem Beaver2001.Formula.Presupposes.not {W : Type u_1} {φ ψ : Formula W} (h : φ.Presupposes ψ) : φ.not.Presupposes ψ

theorem Beaver2001.Formula.Presupposes.and_left {W : Type u_1} {φ ψ χ : Formula W} (h : φ.Presupposes ψ) : (φ.and χ).Presupposes ψ

theorem Beaver2001.Formula.Presupposes.implies_left {W : Type u_1} {φ ψ χ : Formula W} (h : φ.Presupposes ψ) : (φ.implies χ).Presupposes ψ

theorem Beaver2001.Formula.Presupposes.might {W : Type u_1} {φ ψ : Formula W} (h : φ.Presupposes ψ) : φ.might.Presupposes ψ

theorem Beaver2001.Formula.Presupposes.must {W : Type u_1} {φ ψ : Formula W} (h : φ.Presupposes ψ) : φ.must.Presupposes ψ

theorem Beaver2001.Formula.Presupposes.trans {W : Type u_1} {φ ψ χ : Formula W} (h₁ : φ.Presupposes ψ) (h₂ : ψ.Presupposes χ) : φ.Presupposes χ

Presupposition composes (Fact 8.2).

theorem Beaver2001.Formula.presup_and_presupposes {W : Type u_1} (ψ χ : Formula W) : (ψ.presup.and χ).Presupposes ψ

∂ψ and χ presupposes ψ.

theorem Beaver2001.Formula.Presupposes.and_right {W : Type u_1} {φ ψ χ : Formula W} (h : φ.Presupposes ψ) : (χ.and φ).Presupposes (χ.implies ψ)

A presupposition of the second conjunct projects conditionalised on the first (Fact 8.3).

theorem Beaver2001.Formula.Presupposes.implies_right {W : Type u_1} {φ ψ χ : Formula W} (h : φ.Presupposes ψ) : (χ.implies φ).Presupposes (χ.implies ψ)

A presupposition of the consequent projects conditionalised on the antecedent (Fact 8.3).

theorem Beaver2001.Formula.e154 {W : Type u_1} (lands weight bothered : Set W) : ((atom lands).implies ((atom weight).presup.and (atom bothered))).Presupposes ((atom lands).implies (atom weight))

E154: the conditional presupposes that if Spiff lands on Planet X his weight is greater than on Earth.

theorem Beaver2001.Formula.e154_not_unconditional : ∃ (lands : Set Bool) (weight : Set Bool) (bothered : Set Bool), ¬((atom lands).implies ((atom weight).presup.and (atom bothered))).Presupposes (atom weight)

E154 does not presuppose that Spiff's weight is greater than on Earth: a state in which he may be weightless in space admits it.

Epistemic modality (D61, Facts 8.5–8.7)

theorem Beaver2001.Formula.might_isTest {W : Type u_1} (φ : Formula W) : φ.might.IsTest

theorem Beaver2001.Formula.must_isTest {W : Type u_1} (φ : Formula W) : φ.must.IsTest

theorem Beaver2001.Formula.satisfies_might_iff {W : Type u_1} {φ : Formula W} {σ : Set W} (hσ : σ.Nonempty) : Satisfies σ φ.might ↔ ConsistentWith σ φ

might is a consistency test (Fact 8.5): a non-absurd state is a fixed point of might φ iff it is consistent with φ.

theorem Beaver2001.Formula.satisfies_iff_not_consistentWith_not {W : Type u_1} {φ : Formula W} {σ : Set W} (h : φ.eval.admits σ) : Satisfies σ φ ↔ ¬ConsistentWith σ φ.not

A state admitting φ satisfies it iff it is inconsistent with not φ (Lemma 8.6).

theorem Beaver2001.Formula.satisfies_must_iff {W : Type u_1} {φ : Formula W} {σ : Set W} (hσ : σ.Nonempty) : Satisfies σ φ.must ↔ Satisfies σ φ

must is a satisfaction test (Fact 8.7): a non-absurd state is a fixed point of must φ iff it satisfies φ.

The trivalent connection (Ch. 10)

inductive Beaver2001.Formula.NonModal {W : Type u_1} : Formula W → Prop

The non-modal sentences, PL+∂.

• atom {W : Type u_1} (p : Set W) : (Formula.atom p).NonModal
• not {W : Type u_1} {φ : Formula W} : φ.NonModal → φ.not.NonModal
• and {W : Type u_1} {φ ψ : Formula W} : φ.NonModal → ψ.NonModal → (φ.and ψ).NonModal
• presup {W : Type u_1} {φ : Formula W} : φ.NonModal → φ.presup.NonModal

noncomputable def Beaver2001.Formula.tval {W : Type u_1} : Formula W → W → Trivalent

Peters' trivalent semantics (D70–D71): bivalent atoms, the middle Kleene connectives, and ∂φ true when φ is and undefined otherwise. Modal sentences are not covered.

Equations

• (Beaver2001.Formula.atom p).tval x✝ = if x✝ ∈ p then Trivalent.true else Trivalent.false
• φ.not.tval x✝ = (φ.tval x✝).neg
• (φ.and ψ).tval x✝ = (φ.tval x✝).meetMiddle (ψ.tval x✝)
• φ.presup.tval x✝ = if φ.tval x✝ = Trivalent.true then Trivalent.true else Trivalent.indet
• φ.might.tval x✝ = Trivalent.indet
• φ.must.tval x✝ = Trivalent.indet

def Beaver2001.Formula.TrueAt {W : Type u_1} (w : W) (φ : Formula W) : Prop

Update truth in a world (D76): {w}[φ]{w}.

Equations

• Beaver2001.Formula.TrueAt w φ = ({w} ∈ φ.eval {w})

def Beaver2001.Formula.FalseAt {W : Type u_1} (w : W) (φ : Formula W) : Prop

Update falsity in a world (D77): {w}[φ]∅.

Equations

• Beaver2001.Formula.FalseAt w φ = (∅ ∈ φ.eval {w})

theorem Beaver2001.Formula.eq_singleton_or_eq_empty {W : Type u_1} {φ : Formula W} {τ : Set W} {w : W} (h : τ ∈ φ.eval {w}) : τ = {w} ∨ τ = ∅

theorem Beaver2001.Formula.trueAt_atom {W : Type u_1} {w : W} {p : Set W} : TrueAt w (atom p) ↔ w ∈ p

theorem Beaver2001.Formula.falseAt_atom {W : Type u_1} {w : W} {p : Set W} : FalseAt w (atom p) ↔ w ∉ p

theorem Beaver2001.Formula.trueAt_not {W : Type u_1} {φ : Formula W} {w : W} : TrueAt w φ.not ↔ FalseAt w φ

theorem Beaver2001.Formula.falseAt_not {W : Type u_1} {φ : Formula W} {w : W} : FalseAt w φ.not ↔ TrueAt w φ

theorem Beaver2001.Formula.trueAt_and {W : Type u_1} {φ ψ : Formula W} {w : W} : TrueAt w (φ.and ψ) ↔ TrueAt w φ ∧ TrueAt w ψ

theorem Beaver2001.Formula.falseAt_and {W : Type u_1} {φ ψ : Formula W} {w : W} : FalseAt w (φ.and ψ) ↔ FalseAt w φ ∨ TrueAt w φ ∧ FalseAt w ψ

theorem Beaver2001.Formula.trueAt_presup {W : Type u_1} {φ : Formula W} {w : W} : TrueAt w φ.presup ↔ TrueAt w φ

theorem Beaver2001.Formula.not_falseAt_presup {W : Type u_1} {φ : Formula W} {w : W} : ¬FalseAt w φ.presup

theorem Beaver2001.Formula.trueAt_or_falseAt {W : Type u_1} {φ : Formula W} {w : W} (h : φ.eval.admits {w}) : TrueAt w φ ∨ FalseAt w φ

A world admitting φ makes it true or false.

theorem Beaver2001.Formula.admits_presup_singleton {W : Type u_1} {φ : Formula W} {w : W} : φ.presup.eval.admits {w} ↔ TrueAt w φ

theorem Beaver2001.Formula.not_trueAt_of_falseAt {W : Type u_1} {φ : Formula W} {w : W} (h : FalseAt w φ) : ¬TrueAt w φ

theorem Beaver2001.Formula.trueAt_falseAt_iff {W : Type u_1} {φ : Formula W} (hφ : φ.NonModal) (w : W) : (TrueAt w φ ↔ φ.tval w = Trivalent.true) ∧ (FalseAt w φ ↔ φ.tval w = Trivalent.false)

Trivalent and update truth and falsity coincide world by world (Lemma 10.1).

theorem Beaver2001.Formula.trueAt_iff {W : Type u_1} {φ : Formula W} {w : W} (hφ : φ.NonModal) : TrueAt w φ ↔ φ.tval w = Trivalent.true

theorem Beaver2001.Formula.falseAt_iff {W : Type u_1} {φ : Formula W} {w : W} (hφ : φ.NonModal) : FalseAt w φ ↔ φ.tval w = Trivalent.false

theorem Beaver2001.Formula.admits_and_singleton {W : Type u_1} {φ ψ : Formula W} {w : W} : (φ.and ψ).eval.admits {w} ↔ φ.eval.admits {w} ∧ (TrueAt w φ → ψ.eval.admits {w})

Admittance of a conjunction at a world.

theorem Beaver2001.Formula.mem_eval_iff {W : Type u_1} {φ : Formula W} (hφ : φ.NonModal) (σ τ : Set W) : τ ∈ φ.eval σ ↔ (∀ w ∈ σ, φ.eval.admits {w}) ∧ τ = {w : W | w ∈ σ ∧ TrueAt w φ}

Non-modal updates are distributive (Fact A.2): an update is defined iff it is defined at every world of the state, and keeps exactly the worlds at which the sentence is true.

theorem Beaver2001.Formula.satisfies_iff {W : Type u_1} {φ : Formula W} {σ : Set W} (hφ : φ.NonModal) : Satisfies σ φ ↔ ∀ w ∈ σ, TrueAt w φ

A non-modal sentence is satisfied iff it is true at every world of the state.

theorem Beaver2001.Formula.admits_iff {W : Type u_1} {φ : Formula W} {σ : Set W} (hφ : φ.NonModal) : φ.eval.admits σ ↔ ∀ w ∈ σ, φ.eval.admits {w}

A non-modal sentence is admitted iff it is admitted at every world of the state.

theorem Beaver2001.Formula.entails_iff {W : Type u_1} {φ ψ : Formula W} (hφ : φ.NonModal) (hψ : ψ.NonModal) : φ.Entails ψ ↔ ∀ (w : W), TrueAt w φ → TrueAt w ψ

For non-modal sentences, entailment is entailment at every world (Lemma 10.2).

theorem Beaver2001.Formula.entails_iff_satisfies {W : Type u_1} {φ ψ : Formula W} (hφ : φ.NonModal) (hψ : ψ.NonModal) : φ.Entails ψ ↔ ∀ (σ : Set W), Satisfies σ φ → Satisfies σ ψ

For non-modal sentences, entailment is preservation of fixed points (D73).

theorem Beaver2001.Formula.entails_iff_tval {W : Type u_1} {φ ψ : Formula W} (hφ : φ.NonModal) (hψ : ψ.NonModal) : φ.Entails ψ ↔ ∀ (w : W), φ.tval w = Trivalent.true → ψ.tval w = Trivalent.true

The update and trivalent entailment notions coincide on PL+∂ (Fact 10.3).

theorem Beaver2001.Formula.presupposes_iff {W : Type u_1} {φ ψ : Formula W} (hφ : φ.NonModal) (hψ : ψ.NonModal) : φ.Presupposes ψ ↔ φ.Entails ψ ∧ φ.not.Entails ψ

A non-modal sentence presupposes exactly what both it and its negation entail, Peters' characterisation of trivalent presupposition.