Partial updates

import Linglib.Semantics.Dynamic.Partial

A partial update PartialUpdate α := α →. α is a partial function on states, and a state admits the update when the update is defined there. Heim's context change potentials are the partial updates of sets of worlds (CCP.Partial), whose domain condition is the presupposition, so that Karttunen's satisfaction law for conjunction is the domain condition of composition and holds by construction. A trivalent proposition gives the update defined on the contexts where it is defined throughout, and under this update the filtering connectives, Peters' Middle Kleene connectives, are the admittance conditions of the dynamic connectives. More strongly, the update map is an isomorphism from trivalent propositions to the updates it reaches, carrying the constant truth, Peters' conjunction and the Weak Kleene difference, disjunction and conjunction to the null update, sequencing, difference, union and intersection (George 2014 §2). Every update built from these operations out of trivalentisable ones is therefore trivalentisable, and Heim's connectives are Peters'.

Main definitions

PartialUpdate.seq: sequencing, the composition of partial functions.
PartialUpdate.IsEliminative: Heim's Principle (A), that an update never adds information.
PartialUpdate.supports: a state supports an update of which it is a fixed point.
PartialUpdate.Presupposes: every state admitting the first update supports the second.
CCP.Partial.ofTrivalent: the update of a trivalent proposition.
CCP.Partial.neg, CCP.Partial.cond, CCP.Partial.disj: Heim's negation and conditional, and the disjunction that updates its second disjunct with the negation of the first.
CCP.Partial.diff, CCP.Partial.union, CCP.Partial.inter: the difference, union and intersection of updates, defined where both updates are.
CCP.Partial.IsTrivalentisable: an update given by a trivalent proposition.
CCP.Partial.ofTrivalentEquiv: trivalent propositions are the trivalentisable updates.

Main results

PartialUpdate.admits_seq: the satisfaction law.
PartialUpdate.seq_eq_kleisliComp: sequencing is Kleisli composition for Part.
PartialUpdate.entails_bind_iff_seq_eq: entailment is absorption under sequencing.
PartialUpdate.Presupposes.seq_right: a presupposition of the second conjunct projects conditionalised on the first.
CCP.Partial.admits_seq_ofTrivalent, CCP.Partial.admits_cond_ofTrivalent, CCP.Partial.admits_disj_ofTrivalent: the filtering connectives, derived.
CCP.Partial.ofTrivalent_injective, CCP.Partial.ofTrivalent_one, CCP.Partial.ofTrivalent_meetMiddle, CCP.Partial.ofTrivalent_diff, CCP.Partial.ofTrivalent_joinWeak, CCP.Partial.ofTrivalent_meetWeak: the update map is an isomorphism of the trivalent operations onto the operations on updates.
CCP.Partial.ofTrivalent_neg, CCP.Partial.ofTrivalent_cond, CCP.Partial.ofTrivalent_joinMiddle, CCP.Partial.ofTrivalent_joinMiddle_eq_neg_seq_neg: Heim's connectives, and both Beaver's disjunction and its De Morgan form, are Peters'.

Implementation notes

The partiality is of the update and not of the points. The partial assignments of Dynamic/State.lean encode referential growth rather than presupposition, the sense of partial dynamic semantics in Haug's work, and the two kinds compose in Dynamic/FileChange.lean. Heim gives context change potentials for negation, conjunction and the conditional only, and the disjunction follows Beaver. George 2014's error context # is the undefinedness of a Part, so every update sends # to #; updates that recover from #, such as his (6a), are not representable, but every trivalentisable update is of this kind.

References

Heim 1982, The Semantics of Definite and Indefinite Noun Phrases formalized
Heim 1983, On the Projection Problem for Presuppositions formalized
Heim 1992, Presupposition Projection and the Semantics of Attitude Verbs formalized
Karttunen 1974, Presupposition and Linguistic Context formalized
Beaver 2001, Presupposition and Assertion in Dynamic Semantics formalized
Beaver & Krahmer 2001, A Partial Account of Presupposition Projection formalized
Coppock & Beaver 2015, Definiteness and determinacy formalized
Veltman 1996, Defaults in Update Semantics formalized
Groenendijk & Stokhof 1990, Two Theories of Dynamic Semantics
Moggi 1991, Notions of Computation and Monads
Shan 2001, Monads for Natural Language Semantics
Haug 2014, Partial Dynamic Semantics for Anaphora: Compositionality without Syntactic Coindexation
George 2014, Some Remarks on Certain Trivalent Accounts of Presupposition Projection

Declarations

A partial update of states of type α. The domain condition is the presupposition; Part.Dom is Heim 1983's admittance.

@[reducible, inline] abbrev DynamicSemantics.PartialUpdate L87–89

(α : Type u_1) :

Type u_1

DynamicSemantics.PartialUpdate α = (α →. α)

Used in Semantics/Dynamic/FileChange

L95–97

L99–100

L102–103

Sequencing, dynamic conjunction, is s[φ ∧ ψ] = s[φ][ψ]. This is PFun.comp; the projection behavior of conjunction is the composition law of partial functions.

def DynamicSemantics.PartialUpdate.seq L105–108

{α : Type u_1} (φ ψ : PartialUpdate α) :

PartialUpdate α

φ.seq ψ = PFun.comp ψ φ

Built from

Used in Semantics/Dynamic/FileChange, Semantics/Presupposition/Formula, Beaver2001, BeaverKrahmer2001, Heim1982 and 3 more

Sequencing is Kleisli composition for the Part monad, since a partial update is definitionally a Kleisli arrow α → Part α. This is the partiality column of the effect view of dynamic semantics, beside the powerset column in Collapse.lean (Moggi 1991, Shan 2001).

theorem DynamicSemantics.PartialUpdate.seq_eq_kleisliComp L110–115

{α : Type u_1} (φ ψ : α → Part α) :

seq φ ψ = φ >=> ψ

Built from

Eliminativity

A partial update is eliminative if its defined outputs are at least as informative as the input (Heim 1982's Principle (A); Groenendijk & Stokhof 1990's ↓-direction).

def DynamicSemantics.PartialUpdate.IsEliminative L119–121

{α : Type u_1} [LE α] (φ : PartialUpdate α) :

Prop

φ.IsEliminative = ∀ (s s' : α), s' ∈ φ s → s' ≤ s

Built from

Used by DynamicSemantics.PartialUpdate.isEliminative_id, DynamicSemantics.PartialUpdate.IsEliminative.seq, DynamicSemantics.CCP.Partial.isEliminative_ofTrivalent, DynamicSemantics.CCP.Partial.isEliminative_neg, DynamicSemantics.CCP.Partial.isEliminative_cond

Used in Semantics/Dynamic/FileChange, Heim1982

L123–124

L126–129

Support and entailment

s supports φ when the update changes nothing (Heim 1992's c + φ = c, Veltman 1996's acceptance).

def DynamicSemantics.PartialUpdate.supports L133–135

{α : Type u_1} (s : α) (φ : PartialUpdate α) :

Prop

DynamicSemantics.PartialUpdate.supports s φ = (s ∈ φ s)

Built from

Used by DynamicSemantics.PartialUpdate.supports_iff_mem, DynamicSemantics.PartialUpdate.supports_iff_eq_some, DynamicSemantics.PartialUpdate.supports.seq_apply, DynamicSemantics.PartialUpdate.supports_iff_isFixedPt, DynamicSemantics.PartialUpdate.entails_bind_iff, DynamicSemantics.PartialUpdate.Presupposes, DynamicSemantics.PartialUpdate.supports.admits

Used in Semantics/Dynamic/FileChange, Beaver2001, Heim1982

Dynamic entailment between partial updates, every defined update with φ supporting ψ (Veltman 1996's acceptance consequence; Heim 1982's entailment between file change potentials), is Entails of their extensions along Part.bind. It is absorption, sequencing ψ after φ changing nothing.

theorem DynamicSemantics.PartialUpdate.entails_bind_iff_seq_eq L148–157

{α : Type u_1} {φ ψ : PartialUpdate α} :

(Entails [fun (x : Part α) => x >>= φ] fun (x : Part α) => x >>= ψ) ↔ φ.seq ψ = φ

Built from ,

L159–168

Presupposition

φ presupposes ψ when every state admitting φ supports ψ. This is Heim 1983's presupposition when ψ is the update of a plain proposition (presupposes_ofProp_iff), and Beaver 2001's presupposition between sentences.

def DynamicSemantics.PartialUpdate.Presupposes L172–175

{α : Type u_1} (φ ψ : PartialUpdate α) :

Prop

φ.Presupposes ψ = ∀ (s : α), φ.Admits s → DynamicSemantics.PartialUpdate.supports s ψ

Built from , ,

Used by DynamicSemantics.PartialUpdate.Presupposes.trans, DynamicSemantics.PartialUpdate.Presupposes.seq_left, DynamicSemantics.CCP.Partial.presupposes_ofProp_iff, DynamicSemantics.CCP.Partial.presupposes_ofTrivalent, DynamicSemantics.PartialUpdate.Presupposes.neg, DynamicSemantics.PartialUpdate.Presupposes.cond_left, DynamicSemantics.PartialUpdate.Presupposes.seq_right, DynamicSemantics.PartialUpdate.Presupposes.cond_right

Used in Beaver2001, Heim1983

L177

L179–181

L183–184

The satisfaction law

The Karttunen satisfaction law (Karttunen 1974), that s admits φ ∧ ψ iff s admits φ and s[φ] admits ψ, holds by construction as the domain condition of Part.bind.

theorem DynamicSemantics.PartialUpdate.admits_seq L188–193

{α : Type u_1} (φ ψ : PartialUpdate α) (s : α) :

(φ.seq ψ).Admits s ↔ ∃ (h : φ.Admits s), ψ.Admits ((φ s).get h)

Built from , ,

L195–198

L200–208

L210–214

Heim's partial context change potentials

A partial context change potential is a partial update of sets of possibilities, the partial variant of the CCP API.

@[reducible, inline] abbrev DynamicSemantics.CCP.Partial L220–222

(S : Type u_1) :

Type u_1

DynamicSemantics.CCP.Partial S = DynamicSemantics.PartialUpdate (Set S)

Built from

Used in Semantics/Presupposition/Formula, Beaver2001, Heim1983, Heim1992, WangDavidson2026 and 1 more

The Heimian update of a trivalent proposition is defined iff the proposition is defined throughout the context, and keeps the worlds where it is true. This is the update relation of Beaver & Krahmer 2001 §5.3 read as a partial function (mem_ofTrivalent), and the context update of Coppock & Beaver 2015.

The whole-state domain condition is what separates admittance from per-world filtering (the static update CCP.up). A context containing a single presupposition-failing world admits nothing, rather than silently discarding the world.

def DynamicSemantics.CCP.Partial.ofTrivalent L230–239

{W : Type u_2} (p : W → SignType) :

Partial W

DynamicSemantics.CCP.Partial.ofTrivalent p s = { Dom := s ⊆ Function.support p, get := fun (x : s ⊆ Function.support p) => {w : W | w ∈ s ∧ p w = 1} }

Built from

Used in Semantics/Presupposition/Formula, Beaver2001, BeaverKrahmer2001, CoppockBeaver2015, Heim1983 and 4 more

Connectives

Heim negation is s[¬φ] = s \ s[φ], defined iff s[φ] is.

def DynamicSemantics.CCP.Partial.neg L269–270

{P : Type u_1} (φ : Partial P) :

Partial P

φ.neg s = Part.map (fun (x : Set P) => s \ x) (φ s)

Built from

Used by DynamicSemantics.CCP.Partial.neg_eq_diff, DynamicSemantics.CCP.Partial.cond_eq_neg_seq_neg, DynamicSemantics.CCP.Partial.isEliminative_neg, DynamicSemantics.CCP.Partial.admits_neg, DynamicSemantics.CCP.Partial.ofTrivalent_neg, DynamicSemantics.CCP.Partial.ofTrivalent_joinMiddle_eq_neg_seq_neg, DynamicSemantics.CCP.Partial.disj_ofTrivalent, DynamicSemantics.CCP.Partial.IsTrivalentisable.neg, DynamicSemantics.PartialUpdate.Presupposes.neg

Used in Semantics/Dynamic/FileChange, Semantics/Presupposition/Formula, Beaver2001, Heim1983, Heim1992 and 2 more

The Heim conditional is s[if φ, ψ] = s \ (s[φ] \ s[φ][ψ]), defined iff s[φ] and s[φ][ψ] are.

def DynamicSemantics.CCP.Partial.cond L272–275

{P : Type u_1} (φ ψ : Partial P) :

Partial P

φ.cond ψ s = (φ s).bind fun (sφ : Set P) => Part.map (fun (sφψ : Set P) => s \ (sφ \ sφψ)) (ψ sφ)

Built from

Used in Semantics/Presupposition/Formula, Beaver2001

Disjunction, after Beaver 2001, is s[φ ∨ ψ] = s[φ] ∪ (s \ s[φ])[ψ], evaluating its second disjunct in the ¬φ local context.

def DynamicSemantics.CCP.Partial.disj L277–280

{P : Type u_1} (φ ψ : Partial P) :

Partial P

φ.disj ψ s = (φ s).bind fun (sφ : Set P) => Part.map (fun (sψ : Set P) => sφ ∪ sψ) (ψ (s \ sφ))

Built from

Used by DynamicSemantics.CCP.Partial.admits_disj, DynamicSemantics.CCP.Partial.admits_disj_ofTrivalent_iff, DynamicSemantics.CCP.Partial.admits_disj_ofTrivalent, DynamicSemantics.CCP.Partial.ofTrivalent_joinMiddle, DynamicSemantics.CCP.Partial.disj_ofTrivalent, DynamicSemantics.CCP.Partial.IsTrivalentisable.disj

Used in Semantics/Presupposition/Formula, WangDavidson2026, Yagi2025

The difference of updates is s[φ \ ψ] = s[φ] \ s[ψ], defined iff both updates are (George 2014, Definition 7).

def DynamicSemantics.CCP.Partial.diff L282–284

{P : Type u_1} (φ ψ : Partial P) :

Partial P

φ.diff ψ s = φ s \ ψ s

Built from

Used by DynamicSemantics.CCP.Partial.admits_diff, DynamicSemantics.CCP.Partial.neg_eq_diff, DynamicSemantics.CCP.Partial.cond_eq_diff, DynamicSemantics.CCP.Partial.ofTrivalent_diff, DynamicSemantics.CCP.Partial.IsTrivalentisable.diff

The union of updates is s[φ ∪ ψ] = s[φ] ∪ s[ψ], defined iff both updates are (George 2014, Definition 7).

def DynamicSemantics.CCP.Partial.union L286–288

{P : Type u_1} (φ ψ : Partial P) :

Partial P

φ.union ψ s = φ s ∪ ψ s

Built from

Used by DynamicSemantics.CCP.Partial.admits_union, DynamicSemantics.CCP.Partial.ofTrivalent_joinWeak, DynamicSemantics.CCP.Partial.IsTrivalentisable.union

The intersection of updates is s[φ ∩ ψ] = s[φ] ∩ s[ψ], defined iff both updates are (George 2014, Definition 7).

def DynamicSemantics.CCP.Partial.inter L290–292

{P : Type u_1} (φ ψ : Partial P) :

Partial P

φ.inter ψ s = φ s ∩ ψ s

Built from

Used by DynamicSemantics.CCP.Partial.admits_inter, DynamicSemantics.CCP.Partial.ofTrivalent_meetWeak, DynamicSemantics.CCP.Partial.IsTrivalentisable.inter

Eliminativity

Local contexts

The connectives evaluate their second argument in Karttunen 1974's local context (Presupposition.Connective.localContext): conjunction and the conditional in the context updated with the first argument, disjunction in the context updated with its negation.

L355–358

L360–363

L365–372

Filtering connectives, derived

Under ofTrivalent, the admittance conditions of the dynamic connectives are exactly the definedness conditions of the filtering connectives, Peters' Middle Kleene connectives: both are satisfaction in the local contexts (Presupposition.subset_support_meetMiddle_iff and its siblings), so Karttunen filtering is the composition law of partial updates, not a stipulation.

Dynamic conjunction admits s iff the Middle Kleene conjunction is defined throughout it.

theorem DynamicSemantics.CCP.Partial.admits_seq_ofTrivalent L382–386

{W : Type u_2} (p q : W → SignType) (s : Set W) :

(PartialUpdate.seq (ofTrivalent p) (ofTrivalent q)).Admits s ↔ s ⊆ Function.support fun (w : W) => (p w).meetMiddle (q w)

Built from , ,

The dynamic conditional admits s iff the Middle Kleene conditional is defined throughout it.

theorem DynamicSemantics.CCP.Partial.admits_cond_ofTrivalent L388–393

{W : Type u_2} (p q : W → SignType) (s : Set W) :

PartialUpdate.Admits ((ofTrivalent p).cond (ofTrivalent q)) s ↔ s ⊆ Function.support fun (w : W) => (-p w).joinMiddle (q w)

Built from , ,

Dynamic disjunction admits s iff the Middle Kleene disjunction is defined throughout it, the ¬φ local context being Karttunen's negative-antecedent filtering.

theorem DynamicSemantics.CCP.Partial.admits_disj_ofTrivalent L395–400

{W : Type u_2} (p q : W → SignType) (s : Set W) :

PartialUpdate.Admits ((ofTrivalent p).disj (ofTrivalent q)) s ↔ s ⊆ Function.support fun (w : W) => (p w).joinMiddle (q w)

Built from , ,

The update isomorphism

George 2014's Proposition 1: the update map is injective (Remark 1) and carries the constant truth, Peters' conjunction and the Weak Kleene difference meetWeak p (-q), disjunction and conjunction to the null update, sequencing, difference, union and intersection. The trivalentisable updates are therefore closed under these operations (Corollary 1), and reading Heim's connectives off their isomorphic images shows that they are Peters' (footnote 15).

The trivalentisable updates contain the null update and are closed under the operations of the toolbox (George 2014, Corollary 1) and Heim's connectives (Proposition 2).

An update is trivalentisable when it is the update of a trivalent proposition (George 2014, Definition 11).

def DynamicSemantics.CCP.Partial.IsTrivalentisable L410–412

{W : Type u_2} (φ : Partial W) :

Prop

φ.IsTrivalentisable = (φ ∈ Set.range DynamicSemantics.CCP.Partial.ofTrivalent)

Built from ,

Used by DynamicSemantics.CCP.Partial.isTrivalentisable_ofTrivalent, DynamicSemantics.CCP.Partial.isTrivalentisable_id, DynamicSemantics.CCP.Partial.IsTrivalentisable.seq, DynamicSemantics.CCP.Partial.IsTrivalentisable.diff, DynamicSemantics.CCP.Partial.IsTrivalentisable.union, DynamicSemantics.CCP.Partial.IsTrivalentisable.inter, DynamicSemantics.CCP.Partial.IsTrivalentisable.neg, DynamicSemantics.CCP.Partial.IsTrivalentisable.cond, DynamicSemantics.CCP.Partial.IsTrivalentisable.disj

L414–415

Distinct trivalent propositions give distinct updates, as the update of a singleton context recovers the value at its world (George 2014, Remark 1).

theorem DynamicSemantics.CCP.Partial.ofTrivalent_injective L417–429

{W : Type u_2} :

Function.Injective ofTrivalent

Built from

The constant truth gives the null update.

@[simp] theorem DynamicSemantics.CCP.Partial.ofTrivalent_one L431–434

{W : Type u_2} :

ofTrivalent 1 = PFun.id (Set W)

Built from

Peters' conjunction gives sequencing.

theorem DynamicSemantics.CCP.Partial.ofTrivalent_meetMiddle L436–444

{W : Type u_2} (p q : W → SignType) :

(ofTrivalent fun (w : W) => (p w).meetMiddle (q w)) = PartialUpdate.seq (ofTrivalent p) (ofTrivalent q)

Built from ,

L446–453

The Weak Kleene difference gives the difference of updates.

theorem DynamicSemantics.CCP.Partial.ofTrivalent_diff L455–469

{W : Type u_2} (p q : W → SignType) :

(ofTrivalent fun (w : W) => (p w).meetWeak (-q w)) = (ofTrivalent p).diff (ofTrivalent q)

Built from ,

Weak Kleene disjunction gives the union of updates.

theorem DynamicSemantics.CCP.Partial.ofTrivalent_joinWeak L471–485

{W : Type u_2} (p q : W → SignType) :

(ofTrivalent fun (w : W) => (p w).joinWeak (q w)) = (ofTrivalent p).union (ofTrivalent q)

Built from ,

Weak Kleene conjunction gives the intersection of updates.

theorem DynamicSemantics.CCP.Partial.ofTrivalent_meetWeak L487–497

{W : Type u_2} (p q : W → SignType) :

(ofTrivalent fun (w : W) => (p w).meetWeak (q w)) = (ofTrivalent p).inter (ofTrivalent q)

Built from ,

Heim negation is Kleene negation, read off the isomorphic images of ε \ φ (George 2014, footnote 15).

theorem DynamicSemantics.CCP.Partial.ofTrivalent_neg L499–504

{W : Type u_2} (p : W → SignType) :

(ofTrivalent fun (w : W) => -p w) = (ofTrivalent p).neg

Built from ,

The Heim conditional is Peters' conditional, read off the isomorphic images of ε \ (φ \ (φ; ψ)) (George 2014, footnote 15).

theorem DynamicSemantics.CCP.Partial.ofTrivalent_cond L506–515

{W : Type u_2} (p q : W → SignType) :

(ofTrivalent fun (w : W) => (-p w).joinMiddle (q w)) = (ofTrivalent p).cond (ofTrivalent q)

Built from ,

Beaver's disjunction is Peters' disjunction. It is not built from the toolbox, so this is proved directly; ofTrivalent_joinMiddle_eq_neg_seq_neg reads off the De Morgan form.

theorem DynamicSemantics.CCP.Partial.ofTrivalent_joinMiddle L517–530

{W : Type u_2} (p q : W → SignType) :

(ofTrivalent fun (w : W) => (p w).joinMiddle (q w)) = (ofTrivalent p).disj (ofTrivalent q)

Built from ,

George 2014's disjunction ¬(¬φ; ¬ψ) (Definition 9) is Peters' disjunction, read off the isomorphic images (footnote 15).

theorem DynamicSemantics.CCP.Partial.ofTrivalent_joinMiddle_eq_neg_seq_neg L532–540

{W : Type u_2} (p q : W → SignType) :

(ofTrivalent fun (w : W) => (p w).joinMiddle (q w)) = neg (PartialUpdate.seq (ofTrivalent p).neg (ofTrivalent q).neg)

Built from , ,

L542–547

Trivalent propositions are the trivalentisable updates.

DynamicSemantics.CCP.Partial.ofTrivalentEquiv L549–551

noncomputable def DynamicSemantics.CCP.Partial.ofTrivalentEquiv {W : Type u_2} :

(W → SignType) ≃ ↑(Set.range ofTrivalent)

DynamicSemantics.CCP.Partial.ofTrivalentEquiv = Equiv.ofInjective DynamicSemantics.CCP.Partial.ofTrivalent ⋯

Built from

Presupposition

L600–603

L605–607

Projection

Negation and the first argument of the conjunction and the conditional pass a presupposition on unchanged; the second argument passes it on conditionalised on the first.

L620

L622–623

A presupposition of the second conjunct projects conditionalised on the first.

theorem DynamicSemantics.PartialUpdate.Presupposes.seq_right L625–628

{P : Type u_1} {φ ψ χ : CCP.Partial P} (h : Presupposes φ ψ) :

(seq χ φ).Presupposes (χ.cond ψ)

Built from , , ,

L630–632