Partial Context Change Potentials

[Kar74] [Hei83]

Heim's context change potentials are partial functions on contexts: the domain condition IS the presupposition ([Hei83]'s "c admits φ", [Kar74]'s "c satisfies-the-presuppositions-of φ"). PartialCCP P := InfoStateOf P →. InfoStateOf 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_pseq).

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_pseq_ofPartialProp etc.).

Main declarations

• PartialCCP, admits, ofCCP, ofPartialProp
• pseq, pneg, pcond, pdisj — the partial-update clauses ([Hei83] gives CCPs for not/and/if; the disjunction clause with ¬φ local context follows [Bea01])
• admits_pseq — the Karttunen satisfaction law, by construction
• admits_ofPartialProp_iff_presupSatisfied — admittance is Context.presupSatisfied
• admits_pseq_ofPartialProp, admits_pcond_ofPartialProp, admits_pdisj_ofPartialProp — the filtering connectives, derived

@[reducible, inline]

abbrev Semantics.Dynamic.Core.PartialCCP (P : Type u_1) : Type u_1

A partial context change potential: a partial function on information states. The domain condition is the presupposition; Part.Dom is [Hei83]'s admittance.

Equations

• Semantics.Dynamic.Core.PartialCCP P = (Semantics.Dynamic.Core.InfoStateOf P →. Semantics.Dynamic.Core.InfoStateOf P)

def Semantics.Dynamic.Core.PartialCCP.admits {P : Type u_1} (u : PartialCCP P) (s : InfoStateOf P) : Prop

u.admits s: the update is defined at s ([Hei83]'s "s admits u", [Kar74]'s satisfaction). This is Part.Dom.

Equations

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

def Semantics.Dynamic.Core.PartialCCP.ofCCP {P : Type u_1} (φ : CCP P) : PartialCCP P

Total CCPs are partial CCPs with trivial presupposition.

Equations

• Semantics.Dynamic.Core.PartialCCP.ofCCP φ s = Part.some (φ s)

@[simp]

theorem Semantics.Dynamic.Core.PartialCCP.admits_ofCCP {P : Type u_1} (φ : CCP P) (s : InfoStateOf P) : (ofCCP φ).admits s

def Semantics.Dynamic.Core.PartialCCP.ofPartialProp {W : Type u_2} (p : Presupposition.PartialProp W) : PartialCCP W

The Heimian update of a static partial proposition: defined iff every world of the input satisfies the presupposition, 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

• Semantics.Dynamic.Core.PartialCCP.ofPartialProp p s = { Dom := ∀ w ∈ s, p.presup w, get := fun (x : ∀ w ∈ s, p.presup w) => {w : W | w ∈ s ∧ p.assertion w} }

@[simp]

theorem Semantics.Dynamic.Core.PartialCCP.ofPartialProp_get {W : Type u_2} (p : Presupposition.PartialProp W) (s : InfoStateOf W) (h : (ofPartialProp p s).Dom) : (ofPartialProp p s).get h = {w : W | w ∈ s ∧ p.assertion w}

Connectives

def Semantics.Dynamic.Core.PartialCCP.pseq {P : Type u_1} (φ ψ : PartialCCP P) : PartialCCP P

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

Equations

• φ.pseq ψ = PFun.comp ψ φ

def Semantics.Dynamic.Core.PartialCCP.pneg {P : Type u_1} (φ : PartialCCP P) : PartialCCP P

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

Equations

• φ.pneg s = Part.map (fun (x : Semantics.Dynamic.Core.InfoStateOf P) => s \ x) (φ s)

def Semantics.Dynamic.Core.PartialCCP.pcond {P : Type u_1} (φ ψ : PartialCCP P) : PartialCCP P

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

Equations

• φ.pcond ψ s = (φ s).bind fun (sφ : Semantics.Dynamic.Core.InfoStateOf P) => Part.map (fun (sφψ : Semantics.Dynamic.Core.InfoStateOf P) => s \ (sφ \ sφψ)) (ψ sφ)

def Semantics.Dynamic.Core.PartialCCP.pdisj {P : Type u_1} (φ ψ : PartialCCP P) : PartialCCP P

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

Equations

• φ.pdisj ψ s = (φ s).bind fun (sφ : Semantics.Dynamic.Core.InfoStateOf P) => Part.map (fun (sψ : Semantics.Dynamic.Core.InfoStateOf P) => sφ ∪ sψ) (ψ (s \ sφ))

The satisfaction law

theorem Semantics.Dynamic.Core.PartialCCP.admits_pseq {P : Type u_1} (φ ψ : PartialCCP P) (s : InfoStateOf P) : (φ.pseq ψ).admits s ↔ ∃ (h : φ.admits s), ψ.admits ((φ s).get h)

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

theorem Semantics.Dynamic.Core.PartialCCP.admits_pseq_iff {P : Type u_1} (φ ψ : PartialCCP P) (s : InfoStateOf P) (h : φ.admits s) : (φ.pseq ψ).admits s ↔ ψ.admits ((φ s).get h)

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

@[simp]

theorem Semantics.Dynamic.Core.PartialCCP.admits_pneg {P : Type u_1} (φ : PartialCCP P) (s : InfoStateOf P) : φ.pneg.admits s ↔ φ.admits s

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

theorem Semantics.Dynamic.Core.PartialCCP.admits_pcond {P : Type u_1} (φ ψ : PartialCCP P) (s : InfoStateOf P) : (φ.pcond ψ).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 ([Kar74]).

theorem Semantics.Dynamic.Core.PartialCCP.admits_pdisj {P : Type u_1} (φ ψ : PartialCCP P) (s : InfoStateOf P) : (φ.pdisj ψ).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 Semantics.Dynamic.Core.PartialCCP.admits_ofPartialProp {W : Type u_2} (p : Presupposition.PartialProp W) (s : InfoStateOf W) : (ofPartialProp p).admits s ↔ ∀ w ∈ s, p.presup w

Admittance of an atomic update is global presupposition satisfaction.

theorem Semantics.Dynamic.Core.PartialCCP.admits_ofPartialProp_iff_presupSatisfied {W : Type u_2} (p : Presupposition.PartialProp W) (c : CommonGround.ContextSet W) : (ofPartialProp p).admits c ↔ Presupposition.Context.presupSatisfied c p

Admittance is the static layer's Context.presupSatisfied: 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 Semantics.Dynamic.Core.PartialCCP.admits_pseq_ofPartialProp {W : Type u_2} (p q : Presupposition.PartialProp W) (s : InfoStateOf W) : ((ofPartialProp p).pseq (ofPartialProp q)).admits s ↔ ∀ w ∈ s, (p.andFilter q).presup w

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

theorem Semantics.Dynamic.Core.PartialCCP.admits_pcond_ofPartialProp {W : Type u_2} (p q : Presupposition.PartialProp W) (s : InfoStateOf W) : ((ofPartialProp p).pcond (ofPartialProp q)).admits s ↔ ∀ w ∈ s, (p.impFilter q).presup w

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

theorem Semantics.Dynamic.Core.PartialCCP.admits_pdisj_ofPartialProp {W : Type u_2} (p q : Presupposition.PartialProp W) (s : InfoStateOf W) : ((ofPartialProp p).pdisj (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 Semantics.Dynamic.Core.PartialCCP.admits_pneg_ofPartialProp {W : Type u_2} (p : Presupposition.PartialProp W) (s : InfoStateOf W) : (ofPartialProp p).pneg.admits s ↔ ∀ w ∈ s, p.presup w

Negation projects the atomic presupposition unchanged.