Expectation Frames — @cite{veltman-1996} §4

@cite{veltman-1996}

Veltman calls §4 "the heart of the paper." Where §3 uses a single normality ordering for all domains, §4 introduces expectation frames: functions assigning a per-domain normality ordering. This enables conditional defaults — "if φ then normally ψ" — where the ordering is refined only for the φ-domain.

The key insight is the definition of normal worlds (Definition 4.3): a world w is normal in πd not just when w is optimal in d under πd, but when w is top-ranked in every subdomain d' ⊆ d containing w, under πd'. This is how specificity works — a more specific exception (governing a subdomain) can override a general default (governing a superdomain) without the general default needing to "know about" the exception.

Key definitions

• ExpFrame W: function Set W → NormalityOrder W
• ExpFrame.normal: Def 4.3 — check all subdomains, not just d
• ExpFrame.coherent: Def 4.3(iii) — every non-empty d has normals
• ExpFrame.refineAt: Def 4.5 — refine pattern at domain d only
• FrameState: expectation state with a frame
• condDefault: Def 4.6 — conditional default update

Key results

• refineAt_preserves_coherent: Prop 4.7 — coherence characterization
• refineAt_comm_same: refinement at one domain commutes
• refineAt_comm_diff: refinements at different domains commute

Connection to §3

The unconditional "normally ψ" is "(ψ ∨ ¬ψ) ⇝ ψ", so it refines the frame at d = W. The ExpState from Basic.lean corresponds to a FrameState with a constant frame. For constant frames with connected orderings, the §4 normal definition reduces to §3's optimal (since optimal and "top in all subdomains" coincide when every ordering is connected).

structure Semantics.Dynamic.Default.ExpFrame (W : Type u_2) : Type u_2

An expectation frame: a function assigning a normality ordering to each domain (subset of worlds).

@cite{veltman-1996}, Definition 4.2: π assigns to every d ⊆ W an expectation pattern πd. Different domains may have different orderings — this is what enables conditional defaults.

• pattern : Set W → Core.Order.NormalityOrder W

  The per-domain normality ordering

theorem Semantics.Dynamic.Default.ExpFrame.ext {W : Type u_1} {π₁ π₂ : ExpFrame W} (h : ∀ (d : Set W), π₁.pattern d = π₂.pattern d) : π₁ = π₂

Extensionality for frames: two frames are equal iff they assign the same ordering to every domain.

theorem Semantics.Dynamic.Default.ExpFrame.ext_iff {W : Type u_1} {π₁ π₂ : ExpFrame W} : π₁ = π₂ ↔ ∀ (d : Set W), π₁.pattern d = π₂.pattern d

def Semantics.Dynamic.Default.ExpFrame.normal {W : Type u_1} (π : ExpFrame W) (d : Set W) : Set W

The normal worlds in a domain under the frame.

@cite{veltman-1996}, Definition 4.3(i–ii): w is normal in πd iff w ∈ d and for every subdomain d' ⊆ d such that w ∈ d', w is at least as normal as every v ∈ d' under πd'.

This is stronger than just being optimal in d under πd: w must be top-ranked in every subdomain's pattern, not just the top-level one. This is how specificity works — a more specific exception (governing a subdomain) overrides a general default by making the world non-normal at the subdomain level.

Equations

• π.normal d = {w : W | w ∈ d ∧ ∀ (d' : Set W), d' ⊆ d → w ∈ d' → ∀ (v : W), v ∈ d' → (π.pattern d').le w v}

def Semantics.Dynamic.Default.ExpFrame.coherent {W : Type u_1} (π : ExpFrame W) : Prop

A frame is coherent if every non-empty domain has at least one normal world.

@cite{veltman-1996}, Definition 4.3(iii).

Equations

• π.coherent = ∀ (d : Set W), d.Nonempty → (π.normal d).Nonempty

def Semantics.Dynamic.Default.ExpFrame.isDefault {W : Type u_1} (π : ExpFrame W) (d : Set W) (e : W → Prop) : Prop

e is a default in πd iff d ∩ e ≠ ∅ and πd already respects e.

@cite{veltman-1996}, Definition 4.2(ii): e is a default in πd iff d ∩ e ≠ ∅ and πd ∘ e = πd. Since refine_of_respects gives the latter iff respects, we use respects directly.

Equations

• π.isDefault d e = ((∃ (w : W), w ∈ d ∧ e w) ∧ (π.pattern d).respects e)

def Semantics.Dynamic.Default.ExpFrame.const {W : Type u_1} (no : Core.Order.NormalityOrder W) : ExpFrame W

The constant frame: assigns the same ordering to every domain. This embeds §3's single-ordering setup into the §4 framework.

Equations

• Semantics.Dynamic.Default.ExpFrame.const no = { pattern := fun (x : Set W) => no }

def Semantics.Dynamic.Default.ExpFrame.total {W : Type u_1} : ExpFrame W

The total frame: assigns the total ordering to every domain. The initial state before any defaults have been processed.

Equations

• Semantics.Dynamic.Default.ExpFrame.total = Semantics.Dynamic.Default.ExpFrame.const Core.Order.NormalityOrder.total

noncomputable def Semantics.Dynamic.Default.ExpFrame.refineAt {W : Type u_1} (π : ExpFrame W) (d : Set W) (e : W → Prop) : ExpFrame W

Frame refinement: refine the ordering at domain d only.

@cite{veltman-1996}, Definition 4.5(ii):

• π_{d∘e}(d') = πd' if d' ≠ d
• π_{d∘e}(d) = πd ∘ e

Unlike our earlier (incorrect) version that refined all d' ⊇ d, this modifies only the pattern at d. The effect on superdomains comes automatically through the normal computation, which checks all subdomains — so a refinement at d changes which worlds count as normal in any d' ⊇ d.

Equations

• π.refineAt d e = { pattern := fun (d' : Set W) => if d' = d then (π.pattern d).refine e else π.pattern d' }

theorem Semantics.Dynamic.Default.ExpFrame.refineAt_unchanged {W : Type u_1} (π : ExpFrame W) (d : Set W) (e : W → Prop) (d' : Set W) (h : d' ≠ d) : (π.refineAt d e).pattern d' = π.pattern d'

Domains other than d are unchanged by refinement.

theorem Semantics.Dynamic.Default.ExpFrame.refineAt_target {W : Type u_1} (π : ExpFrame W) (d : Set W) (e : W → Prop) : (π.refineAt d e).pattern d = (π.pattern d).refine e

The target domain gets its ordering refined.

structure Semantics.Dynamic.Default.FrameState (W : Type u_2) : Type u_2

An expectation state with frame: an information state paired with an expectation frame.

Veltman's §4 notation: σ = ⟨π, s⟩ where π is a frame and s ⊆ W is the information state. This generalizes ExpState from §3 (which uses a single ordering).

• info : Set W

  The information state

• frame : ExpFrame W

  The expectation frame

def Semantics.Dynamic.Default.FrameState.normal {W : Type u_1} (σ : FrameState W) : Set W

Normal worlds in the current state: the most normal worlds in the info state according to the frame.

Equations

• σ.normal = σ.frame.normal σ.info

def Semantics.Dynamic.Default.FrameState.init {W : Type u_1} : FrameState W

The initial frame state: all worlds possible, total frame.

Equations

• Semantics.Dynamic.Default.FrameState.init = { info := Set.univ, frame := Semantics.Dynamic.Default.ExpFrame.total }

def Semantics.Dynamic.Default.FrameState.ofExpState {W : Type u_1} (σ : ExpState W) : FrameState W

Embed a §3 ExpState as a FrameState with constant frame.

Equations

• Semantics.Dynamic.Default.FrameState.ofExpState σ = { info := σ.info, frame := Semantics.Dynamic.Default.ExpFrame.const σ.order }

noncomputable def Semantics.Dynamic.Default.condDefault {W : Type u_1} (φ ψ : W → Prop) (σ : FrameState W) : FrameState W

Conditional default update: "if φ then normally ψ".

@cite{veltman-1996}, Definition 4.6. Given σ = ⟨π, s⟩:

• Let d = ‖φ‖ — the set of all φ-worlds (not just those in s)
• If d ∩ ‖ψ‖ = ∅, crash (the default is vacuous)
• If π_{d∘ψ} is incoherent, crash
• Otherwise, result is ⟨π_{d∘ψ}, s⟩

Note: d = ‖φ‖ over all of W, not ‖φ‖ ∩ s. The frame is about the space of possible worlds; the info state restricts which are epistemically accessible but doesn't determine the default domain.

Equations

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

noncomputable def Semantics.Dynamic.Default.normallyFrame {W : Type u_1} (ψ : W → Prop) (σ : FrameState W) : FrameState W

Unconditional default: "normally ψ" = "(ψ ∨ ¬ψ) ⇝ ψ".

Refines the frame at d = W (all worlds).

Equations

• Semantics.Dynamic.Default.normallyFrame ψ σ = Semantics.Dynamic.Default.condDefault (fun (x : W) => True) ψ σ

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

Assertion in the frame setting: eliminate non-φ-worlds.

Equations

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

noncomputable def Semantics.Dynamic.Default.presumablyFrame {W : Type u_1} (φ : W → Prop) (σ : FrameState W) : FrameState W

Presumably test in the frame setting: passes iff all normal worlds satisfy φ.

Equations

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

theorem Semantics.Dynamic.Default.assertFrame_preserves_frame {W : Type u_1} (φ : W → Prop) (σ : FrameState W) : (assertFrame φ σ).frame = σ.frame

Assertion preserves the frame.

theorem Semantics.Dynamic.Default.ExpFrame.normal_subset {W : Type u_1} (π : ExpFrame W) (d : Set W) : π.normal d ⊆ d

Normal worlds are in the domain.

theorem Semantics.Dynamic.Default.ExpFrame.refineAt_comm_same {W : Type u_1} (π : ExpFrame W) (d : Set W) (e₁ e₂ : W → Prop) : (π.refineAt d e₁).refineAt d e₂ = (π.refineAt d e₂).refineAt d e₁

Commutativity at one domain: refining by e₁ then e₂ at the same domain gives the same result as the reverse order.

theorem Semantics.Dynamic.Default.ExpFrame.refineAt_comm_diff {W : Type u_1} (π : ExpFrame W) (da db : Set W) (ea eb : W → Prop) (h : da ≠ db) : (π.refineAt da ea).refineAt db eb = (π.refineAt db eb).refineAt da ea

Commutativity at different domains: refinements at da ≠ db commute trivially — they modify different entries.

theorem Semantics.Dynamic.Default.ExpFrame.refineAt_idempotent {W : Type u_1} (π : ExpFrame W) (d : Set W) (e : W → Prop) : (π.refineAt d e).refineAt d e = π.refineAt d e

Idempotency at frame level: refining at d by e twice is the same as refining once.

theorem Semantics.Dynamic.Default.ExpFrame.refineAt_of_respects {W : Type u_1} (π : ExpFrame W) (d : Set W) (e : W → Prop) (h : (π.pattern d).respects e) : π.refineAt d e = π

If πd already respects e, refinement at d is a no-op.

theorem Semantics.Dynamic.Default.ExpFrame.refineAt_creates_respect {W : Type u_1} (π : ExpFrame W) (d : Set W) (e : W → Prop) : ((π.refineAt d e).pattern d).respects e

After refinement at d, the pattern at d respects e.

theorem Semantics.Dynamic.Default.ExpFrame.refineAt_normal_mono {W : Type u_1} (π : ExpFrame W) (d : Set W) (e : W → Prop) (d₀ : Set W) : (π.refineAt d e).normal d₀ ⊆ π.normal d₀

Refinement can only remove normal worlds, never add them. Because refineAt either preserves or strengthens the ordering at each subdomain, the normal condition is harder to satisfy.

theorem Semantics.Dynamic.Default.ExpFrame.refineAt_coherent_iff {W : Type u_1} (π : ExpFrame W) (d : Set W) (e : W → Prop) (hcoh : π.coherent) (hne : ∃ (w : W), w ∈ d ∧ e w) : (π.refineAt d e).coherent ↔ ¬∃ (d' : Set W), d ⊆ d' ∧ π.normal d' ⊆ {w : W | w ∈ d ∧ ¬e w}

Coherence characterization (Proposition 4.7): given coherent π with d ∩ e ≠ ∅, the refined frame π_{d∘e} is coherent iff there is no d' ⊇ d such that nπd' ⊆ d \ e.

The condition "nπd' ⊆ d \ e" means all normal d'-worlds are in d but fail e. If this holds, refinement at d makes those worlds non-top (they don't satisfy e), potentially leaving no normals in the refined frame.

Note: nπd' here uses the original frame π's normals, not the refined frame's.

theorem Semantics.Dynamic.Default.ExpFrame.const_normal_of_connected {W : Type u_1} (no : Core.Order.NormalityOrder W) (d : Set W) (hconn : no.connected) : (const no).normal d = no.optimal d

For a constant frame with a connected ordering, the §4 normal worlds in d coincide with §3's optimal worlds. This is because for connected orderings, "top in every subdomain" reduces to "optimal in d" — since optimal = top when the ordering is total or connected.

def Semantics.Dynamic.Default.ExpFrame.applies {W : Type u_1} (π : ExpFrame W) (d : Set W) (e : W → Prop) (s : Set W) : Prop

Applicability: a default e applies to s within frame π.

@cite{veltman-1996}, Definition 4.9: the d-default e applies to s iff there is no d' ⊇ s such that nπd' ⊆ d and the normal d'-worlds all fail e. Simplified for a single default: e applies to s if the frame can be coherently refined by e at d (from s's perspective).

Equations

• π.applies d e s = (s ⊆ d → ¬∃ (d' : Set W), s ⊆ d' ∧ π.normal d' ⊆ {w : W | w ∈ d ∧ ¬e w})