Charlow (2019): Where is the destructive update problem?

This file formalizes [Cha19b], "Where is the destructive update problem?", which argues that overwriting the value an assignment gives a variable is not a problem peculiar to dynamic semantics. In the dynamic system of [GS91a] two indefinites with the same index leave only the second as a discourse referent, the first update being destroyed, at no cost to truth conditions. The static system overwrites assignments in the same way: a superscripted expression is a scope-taker that evaluates its scope at a shifted assignment, and the two systems differ only in the operator ↑ that closes off the part of a sentence that does not care about assignments, the static one discarding the shifted assignment and the dynamic one returning it. The dynamic ↑ is the test of the static one, so the two agree on truth.

What destructive update does cost is antisymmetry: an assignment reachable from another by some formula reaches it back, reachability being the relation of differing at finitely many variables. That is a problem only for a negation defined by descent along an order on points. Over states of world-assignment pairs, the negation that tests each point is distributive whatever its prejacent, which collapses negated possibility and negated necessity, and the one that removes the surviving points fails once points are modified. Processing a state cell by cell, a cell being its points with one assignment, gives a possibility modal and a negation that are distributive over assignments and not over worlds, and the negation is the pointwise one on the updates that only change assignments.

Main definitions

• sup, pro, upStatic, upDynamic: the superscript, the pronoun, and the two operators ↑.
• reachable: reachability of an assignment from another by a formula.
• distNeg, descNeg: the pointwise negation and the negation by descent.
• Part, slice, IsAnaphoricallyDistributive, anaMight, anaNeg: the cells of a state, processing a state cell by cell, and the possibility modal and negation defined that way.

Main results

• mem_indefinites_iff: the second of two coindexed indefinites overwrites the first.
• upDynamic_eq_test, nonempty_upDynamic_iff: the dynamic ↑ is the test of the static one.
• pollyAnnaStatic_eq, pollyAnnaDynamic_eq: the static and the dynamic meaning of a sentence with two names competing for one index.
• reachable_iff_finite, reachable_symm, antisymmetry_fails: reachability is differing at finitely many variables, so it is symmetric and no partial order.
• isDistributive_distNeg, distNeg_might_eq_distNeg_must: the pointwise negation is distributive and conflates the two modals.
• isAnaphoricallyDistributive_slice, not_isDistributive_anaMight, anaNeg_image: slicing is distributive over assignments only, and its negation is pointwise on anaphoric updates.

Implementation notes

A dynamic proposition is an Update (Assignment E), the paper's functions from assignments to sets of assignments uncurried; the operators of the modular analysis are stated in the paper's curried form, with upDynamic_eq_test relating the two. The paper's cells are the maximal subsets of a state with one assignment, which are the nonempty fibres of the projection to assignments. Descent needs an order on assignments, which total assignments do not have, so descNeg is stated over any preordered type of anaphoric contexts.

References

• [Cha19b]
• [GS91a]

Destructive update, sections 3 and 4

theorem Charlow2019.mem_indefinites_iff {E : Type u_1} {P Q : E → Prop} {g h : Assignment E} (n : ℕ) : (g, h) ∈ SetRel.comp (DynamicSemantics.Update.dexists n (DynamicSemantics.Update.test {k : Assignment E | P (k n)})) (DynamicSemantics.Update.dexists n (DynamicSemantics.Update.test {k : Assignment E | Q (k n)})) ↔ (∃ (x : E), P x) ∧ ∃ (y : E), Q y ∧ h = Function.update g n y

A linguist⁶ entered the room. A linguist⁶ was already there: the outputs map the index to a witness of the second indefinite, the value the first gave it being overwritten.

theorem Charlow2019.mem_dom_indefinites_iff {E : Type u_1} {P Q : E → Prop} {g : Assignment E} (n : ℕ) : g ∈ (SetRel.comp (DynamicSemantics.Update.dexists n (DynamicSemantics.Update.test {k : Assignment E | P (k n)})) (DynamicSemantics.Update.dexists n (DynamicSemantics.Update.test {k : Assignment E | Q (k n)}))).dom ↔ (∃ (x : E), P x) ∧ ∃ (y : E), Q y

Overwriting costs no truth conditions: the text is true iff each indefinite has a witness.

The static/dynamic divide, section 7

A logical form is cleaved at ↑: below it nothing looks at the assignment, above it superscripted expressions shift the assignment and pronouns read it. The shifting is the same in the static and the dynamic system.

def Charlow2019.sup {E : Type u_1} {ρ : Type u_2} (n : ℕ) (x : E) (c : E → Assignment E → ρ) : Assignment E → ρ

A superscripted individual is a scope-taker that evaluates its scope at the assignment shifted to map its index to it.

Equations

• Charlow2019.sup n x c g = c x (Function.update g n x)

def Charlow2019.pro {E : Type u_1} {ρ : Type u_2} (n : ℕ) (c : E → Assignment E → ρ) : Assignment E → ρ

A pronoun passes the value of its index to its scope (18).

Equations

• Charlow2019.pro n c g = c (g n) g

def Charlow2019.upStatic {E : Type u_1} (p : Prop) : Assignment E → Prop

The static ↑ returns the truth value and drops the assignment.

Equations

• Charlow2019.upStatic p x✝ = p

def Charlow2019.upDynamic {E : Type u_1} (p : Prop) : Assignment E → Set (Assignment E)

The dynamic ↑ returns the assignment, conditional on the truth value.

Equations

• Charlow2019.upDynamic p g = {h : Assignment E | h = g ∧ p}

theorem Charlow2019.upDynamic_eq_test {E : Type u_1} (p : Prop) : {i : Assignment E × Assignment E | i.2 ∈ upDynamic p i.1} = DynamicSemantics.Update.test {g : Assignment E | upStatic p g}

The dynamic ↑ is the test of the static one.

theorem Charlow2019.nonempty_upDynamic_iff {E : Type u_1} (p : Prop) (g : Assignment E) : (upDynamic p g).Nonempty ↔ upStatic p g

A dynamic proposition built with ↑ is true where the static one is.

def Charlow2019.pollyAnnaStatic {E : Type u_1} (gave : E → E → E → Prop) (polly anna : E) : Assignment E → Prop

Polly⁵ gave Anna⁵ her₅ paper (20), statically: gave x y z says x gave y the paper of z.

Equations

• Charlow2019.pollyAnnaStatic gave polly anna = Charlow2019.sup 5 polly fun (x : E) => Charlow2019.sup 5 anna fun (y : E) => Charlow2019.pro 5 fun (z : E) => Charlow2019.upStatic (gave x y z)

def Charlow2019.pollyAnnaDynamic {E : Type u_1} (gave : E → E → E → Prop) (polly anna : E) : Assignment E → Set (Assignment E)

Polly⁵ gave Anna⁵ her₅ paper (20), dynamically.

Equations

• Charlow2019.pollyAnnaDynamic gave polly anna = Charlow2019.sup 5 polly fun (x : E) => Charlow2019.sup 5 anna fun (y : E) => Charlow2019.pro 5 fun (z : E) => Charlow2019.upDynamic (gave x y z)

theorem Charlow2019.pollyAnnaStatic_eq {E : Type u_1} (gave : E → E → E → Prop) (polly anna : E) : pollyAnnaStatic gave polly anna = fun (x : Assignment E) => gave polly anna anna

The static meaning (22): the pronoun is Anna, and the shifted assignment is gone.

theorem Charlow2019.pollyAnnaDynamic_eq {E : Type u_1} (gave : E → E → E → Prop) (polly anna : E) (g : Assignment E) : pollyAnnaDynamic gave polly anna g = {h : ℕ → E | h = Function.update g 5 anna ∧ gave polly anna anna}

The dynamic meaning (23): the same truth condition, with the doubly shifted assignment returned, in which Polly's update is overwritten by Anna's.

Antisymmetry, section 8

def Charlow2019.reachable (L : FirstOrder.Language) {E : Type u_1} [L.Structure E] (g h : Assignment E) : Prop

An assignment is reachable from another when some formula of dynamic predicate logic takes the one to the other (24).

Equations

• Charlow2019.reachable L g h = ∃ (φ : DPL.Formula L ℕ), (g, h) ∈ DPL.Formula.eval E φ

theorem Charlow2019.reachable_refl {L : FirstOrder.Language} {E : Type u_1} [L.Structure E] (g : Assignment E) : reachable L g g

Reachability is reflexive, by the tautology.

theorem Charlow2019.reachable_trans {L : FirstOrder.Language} {E : Type u_1} [L.Structure E] {g h k : Assignment E} (hgh : reachable L g h) (hhk : reachable L h k) : reachable L g k

Reachability is transitive, by conjunction.

theorem Charlow2019.reachable_iff_finite {L : FirstOrder.Language} {E : Type u_1} [L.Structure E] {g h : Assignment E} : reachable L g h ↔ {x : ℕ | g x ≠ h x}.Finite

The assignments reachable from one another are those that differ at finitely many variables: a formula changes only its active quantifier variables, and resetting the variables where two assignments differ takes the one to the other.

theorem Charlow2019.reachable_symm {L : FirstOrder.Language} {E : Type u_1} [L.Structure E] {g h : Assignment E} (hgh : reachable L g h) : reachable L h g

Reachability is symmetric, so it is a partial order only if it is trivial.

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

Antisymmetry fails: distinct assignments are reachable from one another, an overwritten variable being overwritten again with its old value.

Negation and distributivity

Over states, the possibility modal is the substrate's CCP.might, which is not distributive (CCP.might_not_isDistributive), and the negation (28) that removes the surviving points is CCP.neg.

def Charlow2019.distNeg {S : Type u_1} (φ : DynamicSemantics.CCP S) : DynamicSemantics.CCP S

The pointwise negation (29) keeps the points whose singleton the prejacent rejects.

Equations

• Charlow2019.distNeg φ s = {i : S | i ∈ s ∧ φ {i} = ∅}

theorem Charlow2019.distNeg_eq_image {S : Type u_1} (φ : DynamicSemantics.CCP S) : distNeg φ = SetRel.image (DynamicSemantics.Update.test φ.lower.neg)

The pointwise negation is the image of a test, of the points with no output.

theorem Charlow2019.isDistributive_distNeg {S : Type u_1} (φ : DynamicSemantics.CCP S) : (distNeg φ).IsDistributive

The pointwise negation is distributive, whatever its prejacent.

theorem Charlow2019.neg_might_of_nonempty {S : Type u_1} {φ : DynamicSemantics.CCP S} {s : Set S} (h : (φ s).Nonempty) : φ.might.neg s = ∅

The negation that removes survivors gets a negated possibility right: it rejects a state compatible with the prejacent and accepts one that is not.

theorem Charlow2019.neg_might_of_eq_empty {S : Type u_1} {φ : DynamicSemantics.CCP S} {s : Set S} (h : φ s = ∅) : φ.might.neg s = s

theorem Charlow2019.neg_eq_self_of_disjoint {S : Type u_1} {φ : DynamicSemantics.CCP S} {s : Set S} (h : Disjoint s (φ s)) : φ.neg s = s

Once an update modifies points, so that none of the input survives in the output, the negation that removes survivors removes nothing.

theorem Charlow2019.distNeg_might_eq_distNeg_must {S : Type u_1} {φ : DynamicSemantics.CCP S} (hφ : φ.IsEliminative) : distNeg φ.might = distNeg φ.must

The pointwise negation conflates negated possibility and negated necessity: on an eliminative prejacent both keep the points the prejacent rejects.

Descent and slicing

A state is a set of points, pairs of a world and an anaphoric context.

def Charlow2019.descNeg {W : Type u_1} {A : Type u_2} [Preorder A] (φ : DynamicSemantics.CCP (W × A)) : DynamicSemantics.CCP (W × A)

The negation by descent (33) removes the points with a descendant among the outputs, a descendant (34) having the same world and an anaphoric context above.

Equations

• Charlow2019.descNeg φ s = {i : W × A | i ∈ s ∧ ¬∃ i' ∈ φ s, i.1 = i'.1 ∧ i.2 ≤ i'.2}

theorem Charlow2019.descNeg_subset_neg {W : Type u_1} {A : Type u_2} [Preorder A] (φ : DynamicSemantics.CCP (W × A)) (s : Set (W × A)) : descNeg φ s ⊆ φ.neg s

Descent removes at least the surviving points.

theorem Charlow2019.descNeg_image_subset {W : Type u_1} {A : Type u_2} [Preorder A] {D : DynamicSemantics.Update (W × A)} (hD : ∀ ⦃i j : W × A⦄, (i, j) ∈ D → i.1 = j.1 ∧ i.2 ≤ j.2) (s : Set (W × A)) : descNeg (SetRel.image D) s ⊆ s \ SetRel.dom D

Descent removes the points that subsist in the output without being in it: a point with an output, under an update that keeps the world and grows the anaphoric context.

def Charlow2019.Part {W : Type u_1} {A : Type u_2} (s : Set (W × A)) : Set (Set (W × A))

The cells of a state (35): its nonempty sets of points with one anaphoric context.

Equations

• Charlow2019.Part s = {t : Set (W × A) | t.Nonempty ∧ ∃ (g : A), t = {i : W × A | i ∈ s ∧ i.2 = g}}

def Charlow2019.slice {W : Type u_1} {A : Type u_2} (ψ : DynamicSemantics.CCP (W × A)) : DynamicSemantics.CCP (W × A)

Slicing processes a state cell by cell.

Equations

• Charlow2019.slice ψ s = ⋃ t ∈ Charlow2019.Part s, ψ t

def Charlow2019.IsAnaphoricallyDistributive {W : Type u_1} {A : Type u_2} (φ : DynamicSemantics.CCP (W × A)) : Prop

A transformer is anaphorically distributive (39) when it processes a state cell by cell.

Equations

• Charlow2019.IsAnaphoricallyDistributive φ = (Charlow2019.slice φ = φ)

theorem Charlow2019.subset_of_mem_part {W : Type u_1} {A : Type u_2} {s t : Set (W × A)} (ht : t ∈ Part s) : t ⊆ s

theorem Charlow2019.mem_part_of_mem {W : Type u_1} {A : Type u_2} {s : Set (W × A)} {i : W × A} (hi : i ∈ s) : {j : W × A | j ∈ s ∧ j.2 = i.2} ∈ Part s

Every point of a state lies in the cell of its anaphoric context.

theorem Charlow2019.part_of_mem_part {W : Type u_1} {A : Type u_2} {s t : Set (W × A)} (ht : t ∈ Part s) : Part t = {t}

A cell is its own only cell.

theorem Charlow2019.isAnaphoricallyDistributive_slice {W : Type u_1} {A : Type u_2} (ψ : DynamicSemantics.CCP (W × A)) : IsAnaphoricallyDistributive (slice ψ)

Slicing is anaphorically distributive.

theorem DynamicSemantics.CCP.IsDistributive.isAnaphoricallyDistributive {W : Type u_1} {A : Type u_2} {φ : CCP (W × A)} (hφ : φ.IsDistributive) : Charlow2019.IsAnaphoricallyDistributive φ

A distributive transformer is anaphorically distributive.

def Charlow2019.anaMight {W : Type u_1} {A : Type u_2} (φ : DynamicSemantics.CCP (W × A)) : DynamicSemantics.CCP (W × A)

The possibility modal that tests each cell (36).

Equations

• Charlow2019.anaMight φ = Charlow2019.slice φ.might

def Charlow2019.anaNeg {W : Type u_1} {A : Type u_2} (φ : DynamicSemantics.CCP (W × A)) : DynamicSemantics.CCP (W × A)

The negation that removes from each cell the points whose world survives in its update (37), sameness of world (38) standing in for descent.

Equations

• Charlow2019.anaNeg φ = Charlow2019.slice fun (t : Set (W × A)) => {i : W × A | i ∈ t ∧ ¬∃ i' ∈ φ t, i'.1 = i.1}

theorem Charlow2019.not_isDistributive_anaMight : ∃ (W : Type) (A : Type) (φ : DynamicSemantics.CCP (W × A)), ¬(anaMight φ).IsDistributive

The sliced modal is not distributive (40): with one anaphoric context and two worlds, one of which verifies the prejacent, it keeps both points, and point by point it keeps one.

theorem Charlow2019.anaNeg_image {W : Type u_1} {A : Type u_2} {D : DynamicSemantics.Update (W × A)} (hD : ∀ ⦃i j : W × A⦄, (i, j) ∈ D → i.1 = j.1) (s : Set (W × A)) : anaNeg (SetRel.image D) s = s \ SetRel.dom D

On an update that only changes the anaphoric context, the sliced negation is the pointwise one: within a cell a world identifies its point, so a surviving world is a surviving point.