Update Semantics

[Vel96]

In Update Semantics:

• Information states are sets of worlds (not assignments)
• Sentences update states by eliminating incompatible worlds
• "Might φ" is a TEST: passes if some φ-worlds remain
• No discourse referents (simpler than DRT/DPL)

⟦φ⟧ : State → State where State = Set World

@[reducible, inline]

abbrev Semantics.Dynamic.UpdateSemantics.State (W : Type u_1) : Type u_1

Update Semantics state: a set of possible worlds.

Unlike DPL/DRT, no assignment component - US focuses on propositional content.

Equations

• Semantics.Dynamic.UpdateSemantics.State W = Set W

@[reducible, inline]

abbrev Semantics.Dynamic.UpdateSemantics.Update (W : Type u_1) : Type u_1

Update function: how a sentence modifies a state.

Equations

• Semantics.Dynamic.UpdateSemantics.Update W = (Semantics.Dynamic.UpdateSemantics.State W → Semantics.Dynamic.UpdateSemantics.State W)

def Semantics.Dynamic.UpdateSemantics.Update.prop {W : Type u_1} (φ : W → Prop) : Update W

Propositional update: eliminate worlds where φ fails.

⟦φ⟧(s) = { w ∈ s | φ(w) }

Equations

• Semantics.Dynamic.UpdateSemantics.Update.prop φ s = {w : W | w ∈ s ∧ φ w}

def Semantics.Dynamic.UpdateSemantics.Update.conj {W : Type u_1} (φ ψ : Update W) : Update W

Conjunction: sequential update.

⟦φ ∧ ψ⟧ = ⟦ψ⟧ ∘ ⟦φ⟧

Delegates to Core.CCP.seq.

Equations

• φ.conj ψ = Semantics.Dynamic.Core.CCP.seq φ ψ

def Semantics.Dynamic.UpdateSemantics.Update.neg {W : Type u_1} (φ : Update W) : Update W

Negation: complement within the input state.

⟦¬φ⟧(s) = s \ ⟦φ⟧(s) ([Vel96])

Delegates to Core.CCP.neg. The whole-state consistency test is Core.CCP.negTest.

Equations

• φ.neg = Semantics.Dynamic.Core.CCP.neg φ

noncomputable def Semantics.Dynamic.UpdateSemantics.Update.might {W : Type u_1} (φ : Update W) : Update W

Epistemic "might": compatibility test.

⟦might φ⟧(s) = s if ⟦φ⟧(s) ≠ ∅, else ∅

Delegates to Core.CCP.might.

Equations

• φ.might = Semantics.Dynamic.Core.CCP.might φ

noncomputable def Semantics.Dynamic.UpdateSemantics.Update.must {W : Type u_1} (φ : Update W) : Update W

Epistemic "must": universal test.

⟦must φ⟧(s) = s if ⟦φ⟧(s) = s, else ∅

Delegates to Core.CCP.must.

Equations

• φ.must = Semantics.Dynamic.Core.CCP.must φ

theorem Semantics.Dynamic.UpdateSemantics.might_is_test {W : Type u_1} (φ : Update W) (s : State W) (h : Set.Nonempty (φ s)) : φ.might s = s

Might is a TEST: it doesn't change the state (if it passes).

theorem Semantics.Dynamic.UpdateSemantics.might_order_matters {W : Type u_1} [DecidableEq W] [Nontrivial W] : ∃ (p : W → Prop) (x : DecidablePred p) (s : State W), (Update.prop p).conj (Update.prop fun (w : W) => ¬p w).might s = ∅ ∧ Set.Nonempty ((Update.prop fun (w : W) => ¬p w).might.conj (Update.prop p) s)

Order matters for epistemic might.

"It's raining and it might not be raining" is contradictory: after learning rain, the might-not-rain test fails (no ¬rain worlds remain). But "it might not be raining and it's raining" can succeed: the might test passes on the initial state, then learning eliminates ¬rain worlds.

Requires Nontrivial W: for empty or singleton W, no state has both p-worlds and ¬p-worlds, making the second conjunct unsatisfiable.

def Semantics.Dynamic.UpdateSemantics.supports {W : Type u_1} (s : State W) (φ : Update W) : Prop

State s supports φ iff updating with φ doesn't change s.

s ⊨ φ iff ⟦φ⟧(s) = s

Equations

• Semantics.Dynamic.UpdateSemantics.supports s φ = (φ s = s)

def Semantics.Dynamic.UpdateSemantics.accepts {W : Type u_1} (s : State W) (φ : Update W) : Prop

State s accepts φ iff updating with φ yields a non-empty state.

s accepts φ iff ⟦φ⟧(s) ≠ ∅

Equations

• Semantics.Dynamic.UpdateSemantics.accepts s φ = Set.Nonempty (φ s)

def Semantics.Dynamic.UpdateSemantics.valid₁ {W : Type u_1} (premises : List (Update W)) (conclusion : Update W) : Prop

Validity₁: updating the minimal state 0 with the premises in order yields a state that supports the conclusion.

ψ₁,...,ψₙ ⊩₁ φ iff 0[ψ₁]⋯[ψₙ] ⊨ φ

[Vel96], §1.2. This is the notion Veltman concentrates on: it captures the fact that default conclusions depend on exactly what information is available.

Equations

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

def Semantics.Dynamic.UpdateSemantics.valid₂ {W : Type u_1} (premises : List (Update W)) (conclusion : Update W) : Prop

Validity₂: for every state σ, updating with the premises in order yields a state that supports the conclusion.

ψ₁,...,ψₙ ⊩₂ φ iff ∀σ, σ[ψ₁]⋯[ψₙ] ⊨ φ

Equations

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

def Semantics.Dynamic.UpdateSemantics.valid₃ {W : Type u_1} (premises : List (Update W)) (conclusion : Update W) : Prop

Validity₃: one cannot accept all premises without accepting the conclusion. Closest to the classical notion.

ψ₁,...,ψₙ ⊩₃ φ iff ∀σ, (σ ⊨ ψ₁ ∧ ... ∧ σ ⊨ ψₙ) → σ ⊨ φ

Equations

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

theorem Semantics.Dynamic.UpdateSemantics.valid₂_imp_valid₁ {W : Type u_1} (premises : List (Update W)) (conclusion : Update W) : valid₂ premises conclusion → valid₁ premises conclusion

Validity₂ implies validity₁: specializing σ = 0.

[Vel96], Proposition 1.3 (one direction, unconditional).

theorem Semantics.Dynamic.UpdateSemantics.valid₃_monotone {W : Type u_1} (premises extra : List (Update W)) (conclusion : Update W) : valid₃ premises conclusion → valid₃ (premises ++ extra) conclusion

Validity₃ is monotonic: adding premises preserves validity.

[Vel96], §1.2: validity₃ is the only notion that is both left and right monotonic.

@[reducible, inline]

abbrev Semantics.Dynamic.UpdateSemantics.PState (W : Type u_1) : Type u_1

The designated undefined state: update failure.

[Yag25] Definition 5: when a presupposition is not satisfied, the update yields ∗. We model ∗ as none via Option (State W).

Equations

• Semantics.Dynamic.UpdateSemantics.PState W = Option (Semantics.Dynamic.UpdateSemantics.State W)

noncomputable def Semantics.Dynamic.UpdateSemantics.PUpdate.presup {W : Type u_1} (p φ : W → Prop) : PState W → PState W

Presuppositional update: update by φ_p is defined only when the presupposition p is supported (i.e. s[p] = s).

[Yag25] Definition 5: s[φ_p] = ∗ if s[p] ≠ s = s[φ] otherwise

[Hei82] [Bea01] [Vel96]

Equations

• Semantics.Dynamic.UpdateSemantics.PUpdate.presup p φ none = none
• Semantics.Dynamic.UpdateSemantics.PUpdate.presup p φ (some s) = if Semantics.Dynamic.UpdateSemantics.Update.prop p s = s then some (Semantics.Dynamic.UpdateSemantics.Update.prop φ s) else none

theorem Semantics.Dynamic.UpdateSemantics.PUpdate.presup_ne_none_iff_admits {W : Type u_1} (p φ : W → Prop) (s : State W) : presup p φ (some s) ≠ none ↔ (Core.PartialCCP.ofPartialProp { presup := p, assertion := φ }).admits s

PUpdate.presup is the Option-valued shadow of Core.PartialCCP.ofPartialProp: defined (≠ none) at some s exactly when s admits the corresponding partial update. PartialCCP is the canonical Part-based form; this clause survives for the [Yag25] disjunction machinery below.

noncomputable def Semantics.Dynamic.UpdateSemantics.PUpdate.neg {W : Type u_1} (φ : W → Prop) : PState W → PState W

Negation extended to PState: s[¬φ] = s/s[φ].

[Yag25] Definition 4: s[¬φ] = s \ s[φ].

Equations

• Semantics.Dynamic.UpdateSemantics.PUpdate.neg φ none = none
• Semantics.Dynamic.UpdateSemantics.PUpdate.neg φ (some s) = some (s \ Semantics.Dynamic.UpdateSemantics.Update.prop φ s)

noncomputable def Semantics.Dynamic.UpdateSemantics.PUpdate.disj {W : Type u_1} (φ ψ : W → Prop) : PState W → PState W

Disjunction extended to PState: s[φ ∨ ψ] = s[φ] ∪ s[¬φ][ψ].

[Yag25] Definition 4, [Hei82]. Extended with ∗ ∪ s = s ∪ ∗ = ∗.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Dynamic.UpdateSemantics.PUpdate.disj φ ψ none = none

noncomputable def Semantics.Dynamic.UpdateSemantics.PUpdate.disjPresup {W : Type u_1} (p φ q ψ : W → Prop) : PState W → PState W

Presuppositional disjunction: s[φ_p ∨ ψ_q]. Apply presupposition checks to each disjunct.

This is the standard Heim/Beaver definition: s[φ_p ∨ ψ_q] = s[φ_p] ∪ s[¬φ_p][ψ_q]

Both presuppositional updates must be defined for the result to be defined: s[φ_p] requires s ⊨ p, and s[¬φ_p][ψ_q] requires s[¬φ_p] ⊨ q.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Dynamic.UpdateSemantics.PUpdate.disjPresup p φ q ψ none = none

noncomputable def Semantics.Dynamic.UpdateSemantics.PUpdate.disjFlex {W : Type u_1} (χ φ_presup φ ω ψ_presup ψ : W → Prop) (_h_split : ∀ (s : State W), Update.prop χ s ∪ Update.prop ω s = s) : PState W → PState W

Flexible accommodation disjunction (dynamic version).

[Yag25] (13) / [Geu05] / [Alo22]: s[φ ∨ ψ] = s[χ][φ] ∪ s[ω][ψ], where s[χ] ∪ s[ω] = s

The propositions χ and ω split the state s into two substates. By default χ = ω = ⊤ (both tautological), but when the default violates genuineness ([Zim00]), the split becomes non-trivial: χ = ¬q and ω = ¬p for conflicting presuppositions.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Dynamic.UpdateSemantics.PUpdate.disjFlex χ φ_presup φ ω ψ_presup ψ _h_split none = none

theorem Semantics.Dynamic.UpdateSemantics.presup_disj_uninformative_when_supported {W : Type u_1} (p φ q ψ : W → Prop) (s : State W) (hp : Update.prop p s = s) (hq : Update.prop q s = s) (h_or : ∀ w ∈ s, φ w ∨ ψ w) : PUpdate.disjPresup p φ q ψ (some s) = some s

Presuppositional disjunction update is uninformative when both presuppositions are already supported: if s ⊨ p and s ⊨ q and the disjunction φ ∨ ψ is already true throughout s, the update returns s unchanged.

Note: this applies to non-conflicting presuppositions. When p ∧ q = ⊥, the hypotheses hp and hq are jointly unsatisfiable (unless s = ∅). For the conflicting case, see update_yields_undefined in the Yagi2025 study, which shows the update is undefined (∗) rather than uninformative.