Update Semantics

@cite{veltman-1996}

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

def 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 → Bool) : Update W

Propositional update: eliminate worlds where φ fails.

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

Equations

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

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

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

Negation: test and possibly fail.

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

Delegates to Core.CCP.neg.

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} [Nontrivial W] : ∃ (p : W → Bool), ∃ (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[ψ₁]⋯[ψₙ] ⊨ φ

@cite{veltman-1996}, §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.

@cite{veltman-1996}, 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.

@cite{veltman-1996}, §1.2: validity₃ is the only notion that is both left and right monotonic.