def Semantics.Dynamic.Charlow2019.trueAt {E : Type u_1} (K : DPL.DPLRel E) (g : Core.Assignment E) : Prop

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

Equations

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

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

Destructive update preserves truth conditions (§4).

def Semantics.Dynamic.Charlow2019.staticExists {E : Type u_1} (x : ℕ) (body : Core.Assignment E → Prop) : DPL.DPLRel E

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

Equations

• Semantics.Dynamic.Charlow2019.staticExists x body = Semantics.Dynamic.DPL.atom fun (g : ℕ → E) => ∃ (d : E), body (Core.Assignment.update g x d)

def Semantics.Dynamic.Charlow2019.dynamicExists {E : Type u_1} (x : ℕ) (body : Core.Assignment E → Prop) : DPL.DPLRel E

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

Equations

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

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

Static existential is a test: output = input.

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

Dynamic existential can change the assignment.

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

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

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

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

Equations

• Semantics.Dynamic.Charlow2019.reachable g h = ∃ (φ : Semantics.Dynamic.DPL.DPLRel E), φ g h

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

Reachability is reflexive.

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

Reachability is transitive (via dynamic conjunction).

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

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

def Semantics.Dynamic.Charlow2019.stateNeg {W : Type u_1} {E : Type u_2} (φ : Core.StateCCP W E) : Core.StateCCP W E

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

Equations

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

def Semantics.Dynamic.Charlow2019.stateDistNeg {W : Type u_1} {E : Type u_2} (φ : Core.StateCCP W E) : Core.StateCCP W E

Distributive negation (29): tests each point individually.

Equations

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

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

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

Equations

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

def Semantics.Dynamic.Charlow2019.anaphoricallyDistributive {W : Type u_1} {E : Type u_2} (φ : Core.StateCCP W E) : Prop

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

Equations

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

theorem Semantics.Dynamic.Charlow2019.distributive_implies_anaphoric {W : Type u_1} {E : Type u_2} (φ : Core.StateCCP W E) : Core.IsDistributive φ → anaphoricallyDistributive φ

Every distributive meaning is anaphorically distributive.

@[implicit_reducible]

instance Semantics.Dynamic.Charlow2019.instCharlowHasFiberedLookup (W E : Type) : Context.HasFiberedLookup Set (Core.State W E) ℕ W E

Charlow's State W E = Set (W × Assignment E) as the nondeterministic (M = Set) instance of the unified lookup interface. The lookup at variable v at world w yields { g v | (w, g) ∈ s } — one alternative per assignment containing w. Empty set is the falsifier (no assignment defines v at w).

SEAM (Falsifier, Seam 1): Charlow commits to ∅ as the no-referent

case. Bivalence is rejected — there is no Entity.star analog at the value level. Compositional negation is preserved by the empty-set convention; bridge to Hofmann via supportCollapse collapses genuinely-uncertain states.

Equations

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

@[implicit_reducible]

instance Semantics.Dynamic.Charlow2019.instCharlowHasJointState (W E : Type) : Context.HasJointState Set (Core.State W E) ℕ W E

Charlow as joint-state: State W E = Set (W × Assignment E) is natively a joint set over (world, assignment) pairs — no marginalization needed. The joint field is essentially the identity, modulo rendering Assignment E = Nat → E as the function V → E expected by the typeclass.

SEAM (Seam 2): This declaration commits Charlow empirically to having

joint structure to lose. The fibered iLookup projection of this state is lossy — it discards which worlds were paired with which assignments beyond what a single (v, w) query reveals.

Equations

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

def Semantics.Dynamic.Charlow2019.singletonLift {W E : Type} [Inhabited E] (worlds : Set W) (vars : Finset ℕ) (i : Core.ICDRTAssignment W E) : Core.State W E

Hofmann ↪ Charlow: lift an ICDRTAssignment 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 Semantics.Dynamic.Charlow2019.supportCollapse {W E : Type} (s : Core.State W E) : Core.ICDRTAssignment 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 Semantics.Dynamic.Charlow2019.supportCollapse_singletonLift {W E : Type} [Inhabited E] (worlds : Set W) (vars : Finset ℕ) (i : Core.ICDRTAssignment W E) (v : Core.IVar) (w : W) (hw : w ∈ worlds) (hv : v.idx ∈ vars) (hall : ∀ u ∈ vars, i.indiv { idx := u } w ≠ Core.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. Anaphora-under-negation phenomena that ICDRT solves by propositional drefs (e.g. the bathroom-sentence theorem Semantics.Dynamic.Context.counterfactual_blocks_veridical) are solved here by alternative-set filtering — a negative antecedent yields an empty alternative set, which by the empty-set falsifier (Seam 1) makes downstream lookup empty.

Concretely: Charlow does not instantiate HasPropDrefs, and the typeclass theorem counterfactual_blocks_veridical (which lives over [HasPropDrefs Ctx P W] only — independent of the effect functor M) does not apply here. Attempting to write HasPropDrefs (State W E) P W would require inventing a pLookup that doesn't exist in Charlow's framework.

This is the seam working as intended: the unification at HasFiberedLookup (the lookup signature) is honest, and the divergence at the resolution-mechanism layer is preserved as a typeclass-instance gap, not papered over by a phony pLookup definition. The ICDRT and Charlow analyses of the same empirical phenomenon (e.g. "There isn't a bathroom. #It is upstairs.") thus live as non-interreducible theorems in their respective files.

theorem Semantics.Dynamic.Charlow2019.charlow_static_eq_cylindrify {E : Type u_1} (x : ℕ) (body : Core.Assignment E → Prop) (g : Core.Assignment E) : trueAt (staticExists x body) g ↔ Core.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 Semantics.Dynamic.Charlow2019.charlow_dynamic_eq_cylindrify {E : Type u_1} (x : ℕ) (body : Core.Assignment E → Prop) (g : Core.Assignment E) : trueAt (dynamicExists x body) g ↔ Core.CylindricAlgebra.cylindrify x body g

Dynamic existential truth = cylindrification (same truth conditions).