Default Reasoning in Update Semantics

[Vel96]

[Vel96] extends update semantics with expectation patterns — normality orderings on worlds — and two new operators:

• Normally p: refines the expectation pattern so p-worlds are preferred
• Presumably p: a test that passes iff all optimal worlds satisfy p

The key insight is that defaults are dynamic: "normally p" does not eliminate worlds (like assertion does) but changes the normality ordering. This means defaults persist under information growth — learning q does not undo the expectation that p is normal.

What's here (§3)

This module formalizes Veltman's §3: expectation states, the operators "normally", "presumably", and "might", and the key results:

• Defaults create expectations (normally_creates_respect)
• Defaults persist under further updates (persistence_assert, persistence_normally)
• "Normally p; presumably p" succeeds (normally_presumably_succeeds)
• Conflicting defaults yield agnosticism (conflicting_defaults_iff_agree)
• Compatible defaults reinforce (compatible_defaults_optimal)
• Promotion is idempotent and commutative (promote_respects_idempotent, promote_comm)

What's not here (§5)

§5 proves which inference patterns are valid for the default conditional (contraposition fails, cautious monotonicity holds, etc.). Key patterns are verified as regression tests in Studies/Veltman1996.lean.

§4 (expectation frames, conditional defaults, specificity) is formalized in Studies/Veltman1996.lean.

Connection to existing infrastructure

• Basic.lean: Veltman's base language (§2) — states, updates, tests, might as consistency test — is formalized there. This module adds the default layer (§3).

• BeliefRevision.lean: PreferentialConsequence (System P) and PlausibilityOrder formalize the static characterization of default reasoning. Veltman's system is the dynamic realization: the default consequence relation it induces validates System P.

• Core/Order/Normality.lean: The normality ordering (mathlib Preorder W) and the refine operation are defined there as shared infrastructure. This module builds ExpState (expectation states) on top of that.

Expectation states

structure UpdateSemantics.Default.ExpState (W : Type u_2) : Type u_2

An expectation state: an information state paired with a normality ordering on worlds.

The information state tracks what is known (which worlds are compatible with the discourse so far). The normality ordering encodes expectations about what is normal (which worlds are most expected given the defaults processed so far).

Veltman's notation: σ = ⟨ε, s⟩ where ε is a preorder (expectation pattern) and s ⊆ W is the information state.

• info : Set W

  The information state: set of worlds compatible with the discourse

• order : Preorder W

  The normality ordering (expectation pattern)

def UpdateSemantics.Default.ExpState.init {W : Type u_1} : ExpState W

The initial expectation state: all worlds are possible and equally normal. No information, no expectations.

Equations

• UpdateSemantics.Default.ExpState.init = { info := Set.univ, order := Core.Order.Normality.total }

def UpdateSemantics.Default.ExpState.optimal {W : Type u_1} (σ : ExpState W) : Set W

Optimal worlds in the current state: the most normal worlds among those compatible with the discourse.

Equations

• σ.optimal = Core.Order.Normality.optimal σ.order σ.info

Update operations

def UpdateSemantics.Default.ExpState.assert {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : ExpState W

Assertion update (Veltman's factual update): eliminate non-φ-worlds, preserve the pattern. Information grows; expectations are unchanged. This is [Por18]'s +-update on the context set, and the standard eliminative update from Update.lean lifted to expectation states.

Equations

• σ.assert φ = { info := {w : W | w ∈ σ.info ∧ φ w}, order := σ.order }

def UpdateSemantics.Default.ExpState.promote {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : ExpState W

Promotion update (Veltman's normally φ): refine the pattern so φ-worlds are preferred. The information state is unchanged — we don't learn that φ is true, only that φ is expected.

This is the core innovation of [Vel96]: defaults operate on the expectation pattern, not on the information state. Read at the discourse level it is [Por18]'s ⋆-update (the To-Do-List update of [Por04]).

Equations

• σ.promote φ = { info := σ.info, order := Core.Order.Normality.refine σ.order φ }

noncomputable def UpdateSemantics.Default.presumablyTest {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : ExpState W

"Presumably p": a test that passes iff all optimal worlds satisfy p. Like CCP.might, this is a test — it either returns the state unchanged or crashes (empties the info state).

"Presumably p" checks whether p follows from current expectations.

Equations

• UpdateSemantics.Default.presumablyTest φ σ = if ∀ w ∈ σ.optimal, φ w then σ else { info := ∅, order := σ.order }

noncomputable def UpdateSemantics.Default.mightTest {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : ExpState W

"Might p": consistency test on the information state. Passes iff the information state has p-worlds. The expectation pattern is irrelevant — might is purely informational.

Equations

• UpdateSemantics.Default.mightTest φ σ = if ∃ w ∈ σ.info, φ w then σ else { info := ∅, order := σ.order }

Basic properties

@[simp]

theorem UpdateSemantics.Default.ExpState.assert_info {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : (σ.assert φ).info = {w : W | w ∈ σ.info ∧ φ w}

@[simp]

theorem UpdateSemantics.Default.ExpState.assert_order {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : (σ.assert φ).order = σ.order

Assertion preserves the normality ordering.

@[simp]

theorem UpdateSemantics.Default.ExpState.promote_info {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : (σ.promote φ).info = σ.info

Promotion preserves the information state.

@[simp]

theorem UpdateSemantics.Default.ExpState.promote_order {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : (σ.promote φ).order = Core.Order.Normality.refine σ.order φ

theorem UpdateSemantics.Default.ExpState.assert_info_subset {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : (σ.assert φ).info ⊆ σ.info

Assertion is eliminative: it can only shrink the info state.

Refinement order on expectation states: more constrained ≤ less constrained, componentwise — finer ≤ coarser, matching the Setoid convention. (NB [Vel96] orients his ≤ the other way, weaker below stronger; the content is the same.) Both updates are deflationary, monotone, and idempotent for this order, and acceptance — [Vel96]'s σ ⊩ φ iff σ[φ] = σ — is the fixpoint condition σ ≤ σ[φ].

@[instance_reducible]

instance UpdateSemantics.Default.ExpState.instPreorder {W : Type u_1} : Preorder (ExpState W)

Equations

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

theorem UpdateSemantics.Default.ExpState.le_iff {W : Type u_1} {σ τ : ExpState W} : σ ≤ τ ↔ σ.info ⊆ τ.info ∧ σ.order ≤ τ.order

theorem UpdateSemantics.Default.ExpState.assert_le_self {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : σ.assert φ ≤ σ

Assertion lands below the input.

theorem UpdateSemantics.Default.ExpState.promote_le_self {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : σ.promote φ ≤ σ

Promotion lands below the input.

theorem UpdateSemantics.Default.ExpState.assert_mono {W : Type u_1} {σ τ : ExpState W} (h : σ ≤ τ) (φ : W → Prop) : σ.assert φ ≤ τ.assert φ

theorem UpdateSemantics.Default.ExpState.promote_mono {W : Type u_1} {σ τ : ExpState W} (h : σ ≤ τ) (φ : W → Prop) : σ.promote φ ≤ τ.promote φ

theorem UpdateSemantics.Default.ExpState.mem_foldl_assert_info {W : Type u_1} (ps : List (W → Prop)) (σ : ExpState W) (v : W) : v ∈ (List.foldl assert σ ps).info ↔ v ∈ σ.info ∧ ∀ p ∈ ps, p v

Membership in the information state after a sequence of assertions: the input's information, filtered by every asserted proposition.

theorem UpdateSemantics.Default.ExpState.foldl_promote_order_le {W : Type u_1} (ps : List (W → Prop)) (σ : ExpState W) (w v : W) : w ≤ v ↔ w ≤ v ∧ ∀ p ∈ ps, p v → p w

The ordering after a sequence of promotions: the input's ordering, refined by the criterion preorder of every promoted proposition.

@[simp]

theorem UpdateSemantics.Default.ExpState.foldl_promote_info {W : Type u_1} (ps : List (W → Prop)) (σ : ExpState W) : (List.foldl promote σ ps).info = σ.info

Promotion sequences leave the information state fixed.

theorem UpdateSemantics.Default.ExpState.le_assert_iff {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : σ ≤ σ.assert φ ↔ ∀ w ∈ σ.info, φ w

Acceptance fixpoint for assertion ([Vel96], §1): the input refines its own assertion iff φ already holds throughout the information state.

theorem UpdateSemantics.Default.ExpState.le_promote_iff {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : σ ≤ σ.promote φ ↔ Core.Order.Normality.respects σ.order φ

Acceptance fixpoint for promotion ([Vel96]: e is a default in ε iff ε ∘ e = ε, his Def 4.2): the input refines its own promotion iff the ordering already respects φ. This is the support notion for the preferential component — "φ is already on the To-Do List" — distinct from truth at the best worlds.

theorem UpdateSemantics.Default.presumably_isTest {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : (presumablyTest φ σ).info = σ.info ∨ (presumablyTest φ σ).info = ∅

Presumably is a test: it either returns the state or empties info.

theorem UpdateSemantics.Default.might_isTest {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : (mightTest φ σ).info = σ.info ∨ (mightTest φ σ).info = ∅

Might is a test: it either returns the state or empties info.

theorem UpdateSemantics.Default.mightTest_preserves_order {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : (mightTest φ σ).order = σ.order

Tests preserve the ordering.

theorem UpdateSemantics.Default.presumablyTest_preserves_order {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : (presumablyTest φ σ).order = σ.order

"Normally p; presumably p" succeeds

theorem UpdateSemantics.Default.presumably_passes {W : Type u_1} (σ : ExpState W) (φ : W → Prop) (hresp : Core.Order.Normality.respects σ.order φ) (hconn : Core.Order.Normality.connected σ.order) (hex : ∃ w ∈ σ.info, φ w) : presumablyTest φ σ = σ

General presumably: if the ordering is connected, respects φ, and the info state has φ-worlds, then "presumably φ" passes.

This is the general form of Veltman's claim that defaults create valid presumptions. The connectedness condition is essential: without it, a non-φ-world can be optimal by being incomparable with all φ-worlds (see Normality.optimal_of_respects_connected).

theorem UpdateSemantics.Default.normally_presumably_succeeds {W : Type u_1} (φ : W → Prop) (d : Set W) (hex : ∃ w ∈ d, φ w) : have σ := { info := d, order := Core.Order.Normality.total }; presumablyTest φ (σ.promote φ) = σ.promote φ

The central result: after processing "normally p", the test "presumably p" passes — provided the information state has p-worlds.

Corollary of presumably_passes: "normally p" creates respect, and a single refinement from total preserves connectedness.

Persistence

theorem UpdateSemantics.Default.persistence_assert {W : Type u_1} (σ : ExpState W) (φ ψ : W → Prop) (h : Core.Order.Normality.respects σ.order φ) : Core.Order.Normality.respects (σ.assert ψ).order φ

Persistence under assertion: asserting any ψ preserves respect for φ — learning new facts does not undo expectations. Immediate, since assert leaves the ordering untouched (assert_order).

[Vel96], Proposition 3.6(iv).

theorem UpdateSemantics.Default.persistence_normally {W : Type u_1} (σ : ExpState W) (φ ψ : W → Prop) (h : Core.Order.Normality.respects σ.order φ) : Core.Order.Normality.respects (σ.promote ψ).order φ

Persistence under further defaults: if the ordering respects p, then processing "normally q" (for any q) preserves this. Later defaults do not undo earlier ones.

[Vel96], Proposition 3.6(iv).

theorem UpdateSemantics.Default.normally_creates_respect {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : Core.Order.Normality.respects (σ.promote φ).order φ

After "normally p", the ordering respects p. Combined with persistence, this means "normally p" creates a permanent expectation.

Idempotency and commutativity

theorem UpdateSemantics.Default.promote_respects_idempotent {W : Type u_1} (σ : ExpState W) (φ : W → Prop) (h : Core.Order.Normality.respects σ.order φ) : σ.promote φ = σ

Idempotency: if the state already accepts "normally φ" (the ordering respects φ), then processing "normally φ" again is a no-op.

[Vel96], Proposition 3.6(ii) at the state level.

theorem UpdateSemantics.Default.promote_promote_self {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : (σ.promote φ).promote φ = σ.promote φ

Corollary: "normally φ; normally φ" = "normally φ" from any state.

theorem UpdateSemantics.Default.promote_comm {W : Type u_1} (σ : ExpState W) (φ ψ : W → Prop) : (σ.promote φ).promote ψ = (σ.promote ψ).promote φ

Commutativity: the order of defaults doesn't matter. "Normally φ; normally ψ" = "normally ψ; normally φ".

Conflicting defaults

theorem UpdateSemantics.Default.conflicting_defaults_le {W : Type u_1} (φ : W → Prop) (w v : W) : w ≤ v ↔ (φ v → φ w) ∧ (¬φ v → ¬φ w)

Conflicting defaults produce agnosticism. After processing both "normally p" and "normally ¬p", the ordering relates worlds only when they agree on p. Both p-worlds and ¬p-worlds can be optimal, so neither "presumably p" nor "presumably ¬p" passes.

This is the degenerate (unconditional) case of conflicting defaults. The full Nixon Diamond — where the conflict arises from conditional defaults "if Quaker then normally pacifist" and "if Republican then normally not pacifist" — requires Veltman's §4 expectation frames.

theorem UpdateSemantics.Default.conflicting_defaults_iff_agree {W : Type u_1} (φ : W → Prop) (w v : W) : w ≤ v ↔ (φ w ↔ φ v)

The conflicting-default ordering is equivalent to p-agreement: w is at most as normal as v iff they agree on p.

Compatible defaults

theorem UpdateSemantics.Default.compatible_defaults_optimal {W : Type u_1} (φ ψ : W → Prop) (d : Set W) (hφψ : ∀ (w : W), φ w → ψ w) (hex : ∃ w ∈ d, φ w) : Core.Order.Normality.optimal (Core.Order.Normality.refine (Core.Order.Normality.refine Core.Order.Normality.total ψ) φ) d ⊆ {w : W | w ∈ d ∧ φ w}

When two defaults are compatible (p implies q), processing both in sequence makes p-worlds optimal: the expectations reinforce rather than conflict.