Partial Context Change Potentials

Heim's context change potentials are partial functions on contexts: the domain condition IS the presupposition ([heim-1983]'s "c admits φ", [karttunen-1974-presupposition]'s "c satisfies-the-presuppositions-of φ"). CCP.Partial P := Set P →. Set P grounds this in mathlib's PFun: Part.Dom is admittance, and the satisfaction law for conjunction — "c admits φ∧ψ iff c admits φ and c[φ] admits ψ" — is the domain condition of partial-function composition, true by construction (admits_seq).

This is partiality of the arrow, and it is orthogonal to the partiality of the points: DRT's embeddings are partial assignments of discourse referents (Possibility.domain, Part-valued — Dynamic/State.lean), which encodes referential growth, not presupposition. The two compose in Dynamic/FileChange.lean, where FCP is CCP.Partial at partial-point states. ([haug-2014]'s "partial dynamic semantics" is the point sense.)

ofPartialProp sends a static partial proposition to its Heimian update: defined iff the context globally satisfies the presupposition (whole-state admittance, NOT per-world filtering), updating by intersecting with the assertion. Under this bridge the filtering connectives of Presupposition/Basic.lean stop being stipulations: andFilter, impFilter, and orFilter are derived as the admittance conditions of dynamic conjunction, conditional, and disjunction (admits_seq_ofPartialProp etc.).

Main declarations

• CCP.Partial, admits, ofTotal, ofPartialProp
• seq, neg, cond, disj — the partial-update clauses ([heim-1983] gives CCPs for not/and/if; the disjunction clause with ¬φ local context follows [beaver-2001])
• seq_eq_kleisliComp — sequencing is Kleisli composition for Part: the partiality column of the effect view, beside Collapse.lean's powerset column
• admits_seq — the Karttunen satisfaction law, by construction
• neg_eliminative, seq_eliminative — Heim's Principle (A), and its closure under sequencing
• admits_ofPartialProp — admittance is Context.presupSatisfied
• mem_ofPartialProp_self — a context is a fixed point of an atomic update iff presupposition and assertion hold throughout it ([heim-1992]'s c + φ = same)
• admits_seq_ofPartialProp, admits_cond_ofPartialProp, admits_disj_ofPartialProp — the filtering connectives, derived

@[reducible, inline]

abbrev DynamicSemantics.CCP.Partial (S : Type u_1) : Type u_1

A partial context change potential: a partial function on information states, the partial variant of the CCP API. The domain condition is the presupposition; Part.Dom is [heim-1983]'s admittance.

Equations

• DynamicSemantics.CCP.Partial S = (Set S →. Set S)

def DynamicSemantics.CCP.Partial.admits {P : Type u_1} (u : Partial P) (s : Set P) : Prop

u.admits s: the update is defined at s ([heim-1983]'s "s admits u", [karttunen-1974-presupposition]'s satisfaction). This is Part.Dom.

Equations

• u.admits s = (u s).Dom

def DynamicSemantics.CCP.Partial.ofTotal {P : Type u_1} (φ : CCP P) : Partial P

Total CCPs are partial CCPs with trivial presupposition.

Equations

• DynamicSemantics.CCP.Partial.ofTotal φ s = Part.some (φ s)

@[simp]

theorem DynamicSemantics.CCP.Partial.admits_ofTotal {P : Type u_1} (φ : CCP P) (s : Set P) : (ofTotal φ).admits s

def DynamicSemantics.CCP.Partial.ofPartialProp {W : Type u_2} (p : Presupposition.PartialProp W) : Partial W

The Heimian update of a static partial proposition: defined iff the context globally satisfies the presupposition (Context.presupSatisfied), updating by intersecting with the assertion.

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

Equations

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

@[simp]

theorem DynamicSemantics.CCP.Partial.ofPartialProp_get {W : Type u_2} (p : Presupposition.PartialProp W) (s : Set W) (h : (ofPartialProp p s).Dom) : (ofPartialProp p s).get h = {w : W | w ∈ s ∧ p.assertion w}

theorem DynamicSemantics.CCP.Partial.mem_ofPartialProp_self {W : Type u_2} (p : Presupposition.PartialProp W) (s : Set W) : s ∈ ofPartialProp p s ↔ s ⊆ p.presup ∧ s ⊆ p.assertion

A context is a fixed point of an atomic update iff the presupposition and the assertion hold throughout it ([heim-1992]'s c + φ = same).

Connectives

def DynamicSemantics.CCP.Partial.seq {P : Type u_1} (φ ψ : Partial P) : Partial P

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

Equations

• φ.seq ψ = PFun.comp ψ φ

theorem DynamicSemantics.CCP.Partial.seq_eq_kleisliComp {P : Type u_1} (φ ψ : Set P → Part (Set P)) : seq φ ψ = φ >=> ψ

Sequencing is Kleisli composition for the Part monad: a partial CCP is a Kleisli arrow Set P → Part (Set P), definitionally — the partiality column of the effect view of dynamic semantics, beside the powerset column in Collapse.lean ([Mog91], [Sha01]).

def DynamicSemantics.CCP.Partial.neg {P : Type u_1} (φ : Partial P) : Partial P

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

Equations

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

def DynamicSemantics.CCP.Partial.cond {P : Type u_1} (φ ψ : Partial P) : Partial P

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

Equations

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

def DynamicSemantics.CCP.Partial.disj {P : Type u_1} (φ ψ : Partial P) : Partial P

Disjunction with ¬φ local context for the second disjunct ([beaver-2001]; [heim-1983] gives CCPs only for not/and/if): s[φ ∨ ψ] = s[φ] ∪ (s \ s[φ])[ψ].

Equations

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

Eliminativity

theorem DynamicSemantics.CCP.Partial.neg_eliminative {P : Type u_1} (φ : Partial P) {s s' : Set P} (h : s' ∈ φ.neg s) : s' ⊆ s

Negation is eliminative: defined outputs shrink the input.

theorem DynamicSemantics.CCP.Partial.seq_eliminative {P : Type u_1} {φ ψ : Partial P} (hφ : ∀ (s s' : Set P), s' ∈ φ s → s' ⊆ s) (hψ : ∀ (s s' : Set P), s' ∈ ψ s → s' ⊆ s) {s s' : Set P} (h : s' ∈ φ.seq ψ s) : s' ⊆ s

Eliminativity ([heim-1982]'s Principle (A); [groenendijk-stokhof-1990]'s ↓-direction) is closed under sequencing.

The satisfaction law

theorem DynamicSemantics.CCP.Partial.admits_seq {P : Type u_1} (φ ψ : Partial P) (s : Set P) : (φ.seq ψ).admits s ↔ ∃ (h : φ.admits s), ψ.admits ((φ s).get h)

The Karttunen satisfaction law ([karttunen-1974-presupposition]), by construction: s admits φ ∧ ψ iff s admits φ and s[φ] admits ψ. The statement is the domain condition of Part.bind.

theorem DynamicSemantics.CCP.Partial.admits_seq_iff {P : Type u_1} (φ ψ : Partial P) (s : Set P) (h : φ.admits s) : (φ.seq ψ).admits s ↔ ψ.admits ((φ s).get h)

The satisfaction law, with admittance of the first conjunct given.

@[simp]

theorem DynamicSemantics.CCP.Partial.admits_neg {P : Type u_1} (φ : Partial P) (s : Set P) : φ.neg.admits s ↔ φ.admits s

Negation projects: s admits ¬φ iff s admits φ.

theorem DynamicSemantics.CCP.Partial.admits_cond {P : Type u_1} (φ ψ : Partial P) (s : Set P) : (φ.cond ψ).admits s ↔ ∃ (h : φ.admits s), ψ.admits ((φ s).get h)

Conditional admittance: s admits if φ, ψ iff s admits φ and s[φ] admits ψ — the same condition as conjunction ([karttunen-1974-presupposition]).

theorem DynamicSemantics.CCP.Partial.admits_disj {P : Type u_1} (φ ψ : Partial P) (s : Set P) : (φ.disj ψ).admits s ↔ ∃ (h : φ.admits s), ψ.admits (s \ (φ s).get h)

Disjunction admittance: s admits φ ∨ ψ iff s admits φ and the ¬φ local context s \ s[φ] admits ψ.

The Stalnaker bridge

theorem DynamicSemantics.CCP.Partial.admits_ofPartialProp {W : Type u_2} (p : Presupposition.PartialProp W) (s : Set W) : (ofPartialProp p).admits s ↔ Presupposition.Context.presupSatisfied s p

Admittance of an atomic update is the static layer's Context.presupSatisfied, by construction: the dynamic definedness condition and the satisfaction-theoretic context condition are one notion.

Filtering connectives, derived

Under ofPartialProp, the admittance conditions of the dynamic connectives are pointwise exactly the presuppositions of the filtering connectives of Presupposition/Basic.lean — Karttunen filtering is the composition law of partial updates, not a stipulation.

theorem DynamicSemantics.CCP.Partial.admits_seq_ofPartialProp {W : Type u_2} (p q : Presupposition.PartialProp W) (s : Set W) : ((ofPartialProp p).seq (ofPartialProp q)).admits s ↔ ∀ w ∈ s, (p.andFilter q).presup w

Dynamic conjunction admits s iff s satisfies andFilter's presupposition pointwise.

theorem DynamicSemantics.CCP.Partial.admits_cond_ofPartialProp {W : Type u_2} (p q : Presupposition.PartialProp W) (s : Set W) : ((ofPartialProp p).cond (ofPartialProp q)).admits s ↔ ∀ w ∈ s, (p.impFilter q).presup w

Dynamic conditional admits s iff s satisfies impFilter's presupposition pointwise.

theorem DynamicSemantics.CCP.Partial.admits_disj_ofPartialProp {W : Type u_2} (p q : Presupposition.PartialProp W) (s : Set W) : ((ofPartialProp p).disj (ofPartialProp q)).admits s ↔ ∀ w ∈ s, (p.orFilter q).presup w

Dynamic disjunction admits s iff s satisfies orFilter's presupposition pointwise: the ¬φ local context is Karttunen's negative-antecedent filtering.

theorem DynamicSemantics.CCP.Partial.admits_neg_ofPartialProp {W : Type u_2} (p : Presupposition.PartialProp W) (s : Set W) : (ofPartialProp p).neg.admits s ↔ ∀ w ∈ s, p.presup w

Negation projects the atomic presupposition unchanged.