Charlow (2019): Where Is the Destructive Update Problem?

[Cha19b]

Destructive update is not empirically problematic: assignment modification is shared between static and dynamic systems. The static/dynamic divide reduces to a single operator ↑ determining whether modified assignments are retained.

def Charlow2019.trueAt {E : Type u_1} (K : DPL.Rel E) (g : Assignment E) : Prop

Truth at an assignment: K True at g ⟺ ∃h. K g h (Charlow's (7)).

Equations

• Charlow2019.trueAt K g = ∃ (h : ℕ → E), K g h

theorem Charlow2019.destructive_preserves_truth {E : Type u_1} (P Q : E → Prop) (g : Assignment E) : trueAt ((DPL.Rel.exists_ 6 (DPL.Rel.atom fun (g' : ℕ → E) => P (g' 6))).conj (DPL.Rel.exists_ 6 (DPL.Rel.atom fun (g' : ℕ → E) => Q (g' 6)))) g ↔ (∃ (x : E), P x) ∧ ∃ (y : E), Q y

Destructive update preserves truth conditions (§4).

def Charlow2019.staticExists {E : Type u_1} (x : ℕ) (body : Assignment E → Prop) : DPL.Rel E

Static ↑: evaluates truth, discards modified assignment (Table 1, row 1).

Equations

• Charlow2019.staticExists x body = DPL.Rel.atom fun (g : ℕ → E) => ∃ (d : E), body (Function.update g x d)

def Charlow2019.dynamicExists {E : Type u_1} (x : ℕ) (body : Assignment E → Prop) : DPL.Rel E

Dynamic ↑: retains modified assignment (Table 1, row 2).

Equations

• Charlow2019.dynamicExists x body = DPL.Rel.exists_ x (DPL.Rel.atom fun (g : ℕ → E) => body g)

theorem Charlow2019.static_is_test {E : Type u_1} (x : ℕ) (body : Assignment E → Prop) (g h : Assignment E) : staticExists x body g h → g = h

Static existential is a test: output = input.

theorem Charlow2019.dynamic_changes_assignment {E : Type u_1} [Nontrivial E] : ∃ (x : ℕ) (body : Assignment E → Prop) (g : Assignment E) (h : Assignment E), dynamicExists x body g h ∧ g ≠ h

Dynamic existential can change the assignment.

theorem Charlow2019.static_dynamic_same_truth {E : Type u_1} (x : ℕ) (body : Assignment E → Prop) (g : Assignment E) : trueAt (staticExists x body) g ↔ trueAt (dynamicExists x body) g

Static and dynamic agree on truth conditions (§4, §7).

def Charlow2019.reachable {E : Type u_1} (g h : Assignment E) : Prop

Reachable: h is reachable from g via some DPL formula (Charlow's (24)).

Equations

• Charlow2019.reachable g h = ∃ (φ : DPL.Rel E), φ g h

theorem Charlow2019.reachable_refl {E : Type u_1} (g : Assignment E) : reachable g g

Reachability is reflexive.

theorem Charlow2019.reachable_trans {E : Type u_1} {g h k : Assignment E} (hgh : reachable g h) (hhk : reachable h k) : reachable g k

Reachability is transitive (via dynamic conjunction).

theorem Charlow2019.antisymmetry_fails {E : Type u_1} [Nontrivial E] : ∃ (g : Assignment E) (h : Assignment E), g ≠ h ∧ reachable g h ∧ reachable h g

Antisymmetry fails: distinct assignments can be mutually reachable (§8).

@[reducible, inline]

abbrev Charlow2019.State (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

Charlow's context type: a set of world-assignment pairs.

Equations

• Charlow2019.State W E = Set (W × Assignment E)

@[reducible, inline]

abbrev Charlow2019.State.CCP (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

Context change potential over Charlow's contexts.

Equations

• Charlow2019.State.CCP W E = DynamicSemantics.CCP (W × Assignment E)

def Charlow2019.stateNeg {W : Type u_1} {E : Type u_2} (φ : State.CCP W E) : State.CCP W E

Non-distributive negation (28): removes from s points that survive φ.

Equations

• Charlow2019.stateNeg φ s = {i : W × Assignment E | i ∈ s ∧ i ∉ φ s}

def Charlow2019.stateDistNeg {W : Type u_1} {E : Type u_2} (φ : State.CCP W E) : State.CCP W E

Distributive negation (29): tests each point individually.

Equations

• Charlow2019.stateDistNeg φ s = {i : W × Assignment E | i ∈ s ∧ φ {i} = ∅}

def Charlow2019.partByAssignment {W : Type u_1} {E : Type u_2} (s : State W E) : Set (State W E)

Partition by assignment: groups points sharing the same assignment (Charlow's (35)).

Equations

• Charlow2019.partByAssignment s = {t : Charlow2019.State W E | t ⊆ s ∧ Set.Nonempty t ∧ ∀ i ∈ t, ∀ j ∈ t, i.2 = j.2}

def Charlow2019.anaphoricallyDistributive {W : Type u_1} {E : Type u_2} (φ : State.CCP W E) : Prop

Anaphorically distributive: processes each assignment-group separately (Charlow's (39)).

Equations

• Charlow2019.anaphoricallyDistributive φ = ∀ (s : Set (W × Assignment E)), φ s = {p : W × Assignment E | ∃ t ∈ Charlow2019.partByAssignment s, p ∈ φ t}

theorem Charlow2019.distributive_implies_anaphoric {W : Type u_1} {E : Type u_2} (φ : State.CCP W E) : DynamicSemantics.CCP.IsDistributive φ → anaphoricallyDistributive φ

Every distributive meaning is anaphorically distributive.

Charlow's ↑ (liftPW) promotes a pointwise Update (Assignment E) (Dynamic Ty2, [Mus96]) to a context-level State.CCP W E; his ↓ (lowerPW) extracts a pointwise relation back. Lifted meanings are always distributive (liftPW_preserves_distributive), so pointwise meanings can never produce irreducibly context-level effects — cumulative readings require non-distributive updates, which live only in State.CCP.

def Charlow2019.liftPW {W : Type u_1} {E : Type u_2} (D : DynamicSemantics.Update (Assignment E)) : State.CCP W E

Charlow's ↑: lift a pointwise Update to an update on states. liftPW D s = {⟨w, h⟩ | ∃ ⟨w, g⟩ ∈ s, D g h} Each world-assignment pair in the output comes from applying D to some input assignment in s, preserving the world.

Equations

• Charlow2019.liftPW D s = {p : W × Assignment E | ∃ q ∈ s, p.1 = q.1 ∧ D q.2 p.2}

def Charlow2019.lowerPW {W : Type u_1} {E : Type u_2} (K : State.CCP W E) (w₀ : W) : DynamicSemantics.Update (Assignment E)

Charlow's ↓: extract a pointwise Update from a state update by evaluating K on a singleton context at an arbitrary world.

Equations

• Charlow2019.lowerPW K w₀ g h = ((w₀, h) ∈ K {(w₀, g)})

theorem Charlow2019.lowerPW_liftPW {W : Type u_1} {E : Type u_2} (D : DynamicSemantics.Update (Assignment E)) (w₀ : W) : lowerPW (liftPW D) w₀ = D

Round-trip identity: lowering a lifted Update recovers the original.

↓(↑D) = D because the singleton context {(w₀, g)} passes through ↑ with only (w₀, g) as witness, leaving exactly the pairs h with D g h.

theorem Charlow2019.liftPW_injective {W : Type u_1} {E : Type u_2} [Nonempty W] (D₁ D₂ : DynamicSemantics.Update (Assignment E)) (h : liftPW D₁ = liftPW D₂) : D₁ = D₂

↑ is injective: distinct DRSs yield distinct state updates.

Follows from the round-trip: D = ↓(↑D), so ↑D₁ = ↑D₂ implies D₁ = ↓(↑D₁) = ↓(↑D₂) = D₂. Requires W to be nonempty for the lowering witness world.

theorem Charlow2019.liftPW_preserves_distributive {W : Type u_1} {E : Type u_2} (D : DynamicSemantics.Update (Assignment E)) : DynamicSemantics.CCP.IsDistributive (liftPW D)

Lifted pointwise DRSs are always distributive.

↑D processes each element of the input state independently — the output at p depends only on whether some q ∈ s satisfies D q.2 p.2 with matching world p.1 = q.1. This is exactly the singleton decomposition (↑D)(s) = ⋃_{i∈s} (↑D)({i}), which is the definition of distributivity.

theorem Charlow2019.liftPW_lowerPW_not_id {W : Type u_1} {E : Type u_2} [Nonempty W] [Nonempty E] : ∃ (K : State.CCP W E) (w₀ : W), liftPW (lowerPW K w₀) ≠ K

↑↓ ≠ id: there exist irreducibly update-theoretic meanings K such that liftPW (lowerPW K w₀) ≠ K.

The simplest witness is K _ = {(w₀, g₀)} (constant function ignoring input). Then K ∅ = {(w₀, g₀)}, but liftPW (lowerPW K w₀) ∅ = ∅ because ↑ has no input pairs to draw.

Requires Nonempty W and Nonempty E to construct the witness.

@[instance_reducible]

instance Charlow2019.instCharlowHasFiberedLookup (W E : Type) : DynamicSemantics.HasFiberedLookup Set (State W E) ℕ W E

Charlow's State W E = Set (W × Assignment E) as the nondeterministic (M = Set) instance of the fibered lookup interface. The lookup at variable v at world w yields { g v | (w, g) ∈ s } — one alternative per assignment containing w. The empty set is the falsifier (no assignment defines v at w): Charlow rejects a value-level ⋆, so compositional negation is preserved by the empty-set convention. The fibered projection is lossy — the native joint state records which worlds pair with which assignments beyond what a single (v, w) query reveals; the supportCollapse bridge below collapses genuinely-uncertain states.

Equations

• Charlow2019.instCharlowHasFiberedLookup W E = { iLookup := fun (s : Charlow2019.State W E) (v : ℕ) (w : W) => {e : E | ∃ (g : Assignment E), (w, g) ∈ s ∧ g v = e} }

def Charlow2019.singletonLift {W E : Type} [Inhabited E] (worlds : Set W) (vars : Finset ℕ) (i : DynamicSemantics.ICDRT.Assignment W E) : State W E

Hofmann ↪ Charlow: lift an ICDRT.Assignment to a Charlow state on the worlds where every vars-listed variable has a non-⋆ referent. At such worlds the resulting state has exactly one alternative — the assignment forced by Hofmann's values on vars (free elsewhere). At ⋆-worlds for any vars-listed variable, the world contributes no alternatives.

Equations

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

noncomputable def Charlow2019.supportCollapse {W E : Type} (s : State W E) : DynamicSemantics.ICDRT.Assignment W E

Charlow ↠ Hofmann: collapse a Charlow state to a Hofmann-style assignment by "agreement-or-⋆". At each world, if all alternatives agree on v's value, that's v's value; otherwise ⋆. Propositional drefs are dropped (Charlow has no propositional-dref structure to preserve). The reverse-image singletonLift ∘ supportCollapse loses information whenever the Charlow state has genuine uncertainty.

Equations

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

theorem Charlow2019.supportCollapse_singletonLift {W E : Type} [Inhabited E] (worlds : Set W) (vars : Finset ℕ) (i : DynamicSemantics.ICDRT.Assignment W E) (v : DynamicSemantics.ICDRT.IVar) (w : W) (hw : w ∈ worlds) (hv : v.idx ∈ vars) (hall : ∀ u ∈ vars, i.indiv { idx := u } w ≠ DynamicSemantics.ICDRT.Entity.star) : (supportCollapse (singletonLift worlds vars i)).indiv v w = i.indiv v w

Bridge / section-retraction: on the deterministic image, supportCollapse ∘ singletonLift = id for individual variables in the lift's vars set, at worlds in the lift's worlds set, where every listed variable has a non-⋆ referent. (Outside this domain the maps behave differently — singletonLift produces an empty state at ⋆-worlds, and supportCollapse falls through to ⋆.)

This is a section/retraction relationship in the spirit of Function.LeftInverse, witnessing that singletonLift injects Hofmann states into Charlow states without information loss on its image. The reverse direction (singletonLift ∘ supportCollapse) is not the identity — collapsing genuine Charlow uncertainty to ⋆ and then re-singleton-lifting forgets which alternatives were possible.

Charlow's State W E = Set (W × Assignment E) deliberately carries no propositional-dref structure, so the bathroom-sentence blocking theorem (counterfactual_blocks_veridical, ICDRT/Basic.lean) — whose every hypothesis is about propositional drefs — has no analogue here. The same anaphora-under-negation phenomenon ("There isn't a bathroom. #It is upstairs.") is handled by alternative-set filtering — a negative antecedent yields an empty alternative set, which by the empty-set falsifier makes downstream lookup empty.

theorem Charlow2019.charlow_static_eq_cylindrify {E : Type u_1} (x : ℕ) (body : Assignment E → Prop) (g : Assignment E) : trueAt (staticExists x body) g ↔ CylindricAlgebra.cylindrify x body g

Static existential truth = cylindrification.

Charlow's staticExists x body tests whether ∃ d, body(g[x↦d]), which is exactly cylindrify x body.

theorem Charlow2019.charlow_dynamic_eq_cylindrify {E : Type u_1} (x : ℕ) (body : Assignment E → Prop) (g : Assignment E) : trueAt (dynamicExists x body) g ↔ CylindricAlgebra.cylindrify x body g

Dynamic existential truth = cylindrification (same truth conditions).