Default Reasoning in Update Semantics

@cite{veltman-1996}

@cite{veltman-1996} 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)
• "Normally" is idempotent and commutative (normallyUpdate_idempotent, normallyUpdate_comm)

What's not here (§4–5)

Veltman's §4 — which he calls "the heart of the paper" — introduces expectation frames for conditional defaults: "if φ then normally ψ" (written φ ⇝ ψ). This enables specificity, the full Nixon Diamond, and the Tweety Triangle. §5 proves which inference patterns are valid for the default conditional (contraposition fails, cautious monotonicity holds, etc.). These require substantially more infrastructure and are left for future work.

Connection to existing infrastructure

• CCP.lean: Veltman's base language (§2) — CCPs, tests, might as consistency test — is already 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 NormalityOrder type and refine operation are defined there as shared infrastructure. This module builds ExpState (expectation states) on top of that.

structure Semantics.Dynamic.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 : Core.Order.NormalityOrder W

  The normality ordering (expectation pattern)

def Semantics.Dynamic.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

• Semantics.Dynamic.Default.ExpState.init = { info := Set.univ, order := Core.Order.NormalityOrder.total }

def Semantics.Dynamic.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 = σ.order.optimal σ.info

def Semantics.Dynamic.Default.assertUpdate {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : ExpState W

Assertion update: eliminate non-p-worlds, preserve pattern.

This is the standard eliminative update from CCP.lean, lifted to expectation states. Information grows; expectations are unchanged.

Equations

• Semantics.Dynamic.Default.assertUpdate φ σ = { info := {w : W | w ∈ σ.info ∧ φ w}, order := σ.order }

def Semantics.Dynamic.Default.normallyUpdate {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : ExpState W

"Normally p": refine the pattern so p-worlds are preferred. The information state is unchanged — we don't learn that p is true, only that p is expected.

This is the core innovation of @cite{veltman-1996}: defaults operate on the expectation pattern, not on the information state.

Equations

• Semantics.Dynamic.Default.normallyUpdate φ σ = { info := σ.info, order := σ.order.refine φ }

noncomputable def Semantics.Dynamic.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

• Semantics.Dynamic.Default.presumablyTest φ σ = if ∀ (w : W), w ∈ σ.optimal → φ w then σ else { info := ∅, order := σ.order }

noncomputable def Semantics.Dynamic.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

• Semantics.Dynamic.Default.mightTest φ σ = if ∃ (w : W), w ∈ σ.info ∧ φ w then σ else { info := ∅, order := σ.order }

theorem Semantics.Dynamic.Default.assertUpdate_preserves_order {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : (assertUpdate φ σ).order = σ.order

Assertion preserves the normality ordering.

theorem Semantics.Dynamic.Default.normallyUpdate_preserves_info {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : (normallyUpdate φ σ).info = σ.info

"Normally" preserves the information state.

theorem Semantics.Dynamic.Default.assertUpdate_eliminative {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : (assertUpdate φ σ).info ⊆ σ.info

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

theorem Semantics.Dynamic.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 Semantics.Dynamic.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 Semantics.Dynamic.Default.mightTest_preserves_order {W : Type u_1} (φ : W → Prop) (σ : ExpState W) : (mightTest φ σ).order = σ.order

Tests preserve the ordering.

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

theorem Semantics.Dynamic.Default.presumably_passes {W : Type u_1} (σ : ExpState W) (φ : W → Prop) (hresp : σ.order.respects φ) (hconn : σ.order.connected) (hex : ∃ (w : W), 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 NormalityOrder.optimal_of_respects_connected).

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

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.

theorem Semantics.Dynamic.Default.persistence_assert {W : Type u_1} (σ : ExpState W) (φ ψ : W → Prop) (h : σ.order.respects φ) : (assertUpdate ψ σ).order.respects φ

Persistence under assertion: if the ordering respects p (i.e., the state has accepted "normally p"), then asserting any q preserves this. Learning new facts does not undo expectations.

@cite{veltman-1996}, Proposition 3.6(iv).

theorem Semantics.Dynamic.Default.persistence_normally {W : Type u_1} (σ : ExpState W) (φ ψ : W → Prop) (h : σ.order.respects φ) : (normallyUpdate ψ σ).order.respects φ

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.

@cite{veltman-1996}, Proposition 3.6(iv).

theorem Semantics.Dynamic.Default.normally_creates_respect {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : (normallyUpdate φ σ).order.respects φ

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

theorem Semantics.Dynamic.Default.normallyUpdate_idempotent {W : Type u_1} (σ : ExpState W) (φ : W → Prop) (h : σ.order.respects φ) : normallyUpdate φ σ = σ

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

@cite{veltman-1996}, Proposition 3.6(ii) at the state level.

theorem Semantics.Dynamic.Default.normallyUpdate_normally_idempotent {W : Type u_1} (σ : ExpState W) (φ : W → Prop) : normallyUpdate φ (normallyUpdate φ σ) = normallyUpdate φ σ

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

theorem Semantics.Dynamic.Default.normallyUpdate_comm {W : Type u_1} (σ : ExpState W) (φ ψ : W → Prop) : normallyUpdate ψ (normallyUpdate φ σ) = normallyUpdate φ (normallyUpdate ψ σ)

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

theorem Semantics.Dynamic.Default.conflicting_defaults_le {W : Type u_1} (φ : W → Prop) (w v : W) : ((Core.Order.NormalityOrder.total.refine φ).refine fun (x : W) => ¬φ x).le 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 Semantics.Dynamic.Default.conflicting_defaults_iff_agree {W : Type u_1} (φ : W → Prop) [DecidablePred φ] (w v : W) : ((Core.Order.NormalityOrder.total.refine φ).refine fun (x : W) => ¬φ x).le 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.

theorem Semantics.Dynamic.Default.compatible_defaults_optimal {W : Type u_1} (φ ψ : W → Prop) (d : Set W) (hφψ : ∀ (w : W), φ w → ψ w) (hex : ∃ (w : W), w ∈ d ∧ φ w) : ((Core.Order.NormalityOrder.total.refine ψ).refine φ).optimal 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.