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 UpdateSemantics.State (W : Type u_2) : Type u_2

Update Semantics state: a set of possible worlds.

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

Equations

• UpdateSemantics.State W = Set W

@[reducible, inline]

abbrev UpdateSemantics.Update (W : Type u_2) : Type u_2

Update function: how a sentence modifies a state. This is the spine's CCP W (set-transformer context change potential) under Veltman's name.

Equations

• UpdateSemantics.Update W = DynamicSemantics.CCP W

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

Propositional update: eliminate worlds where φ fails.

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

Equations

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

@[reducible, inline]

abbrev UpdateSemantics.Update.conj {W : Type u_1} (φ ψ : Update W) : Update W

Conjunction: sequential update.

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

Delegates to DynamicSemantics.CCP.seq.

Equations

• φ.conj ψ = DynamicSemantics.CCP.seq φ ψ

@[reducible, inline]

abbrev UpdateSemantics.Update.neg {W : Type u_1} (φ : Update W) : Update W

Negation: complement within the input state.

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

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

Equations

• φ.neg = DynamicSemantics.CCP.neg φ

@[reducible, inline]

noncomputable abbrev UpdateSemantics.Update.might {W : Type u_1} (φ : Update W) : Update W

Epistemic "might": compatibility test.

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

Delegates to DynamicSemantics.CCP.might.

Equations

• φ.might = DynamicSemantics.CCP.might φ

@[reducible, inline]

noncomputable abbrev UpdateSemantics.Update.must {W : Type u_1} (φ : Update W) : Update W

Epistemic "must": universal test.

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

Delegates to DynamicSemantics.CCP.must.

Equations

• φ.must = DynamicSemantics.CCP.must φ

theorem UpdateSemantics.Update.might_eq_self_of_nonempty {W : Type u_1} (φ : Update W) (s : State W) (h : (φ s).Nonempty) : φ.might s = s

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

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

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 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

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

def 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

• UpdateSemantics.accepts s φ = (φ s).Nonempty

Three notions of validity

def 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

• UpdateSemantics.valid₁ premises conclusion = UpdateSemantics.supports (List.foldl (fun (s : UpdateSemantics.State W) (u : UpdateSemantics.Update W) => u s) Set.univ premises) conclusion

def 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 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

• UpdateSemantics.valid₃ premises conclusion = ∀ (σ : UpdateSemantics.State W), (∀ p ∈ premises, UpdateSemantics.supports σ p) → UpdateSemantics.supports σ conclusion

theorem 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 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.