@[reducible, inline]

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

An InfoState is a set of possibilities.

Different theories instantiate P differently:

• PLA: Assignment × WitnessSeq
• DRT: Assignment
• Intensional: World × Assignment

Equations

• Semantics.Dynamic.Core.InfoStateOf P = Set P

@[reducible, inline]

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

A Context Change Potential (CCP) is a function from states to states.

This is the semantic type for dynamic meanings.

Equations

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

def Semantics.Dynamic.Core.CCP.id {P : Type u_1} : CCP P

Identity CCP: leaves state unchanged

Equations

• Semantics.Dynamic.Core.CCP.id s = s

def Semantics.Dynamic.Core.CCP.absurd {P : Type u_1} : CCP P

Absurd CCP: yields empty state

Equations

• Semantics.Dynamic.Core.CCP.absurd x✝ = ∅

def Semantics.Dynamic.Core.CCP.seq {P : Type u_1} (u v : CCP P) : CCP P

Sequential composition of CCPs

Equations

• u.seq v s = v (u s)

def Semantics.Dynamic.Core.CCP.«term_;;_» : Lean.TrailingParserDescr

Equations

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

theorem Semantics.Dynamic.Core.CCP.seq_assoc {P : Type u_1} (u v w : CCP P) : (u.seq v).seq w = u.seq (v.seq w)

theorem Semantics.Dynamic.Core.CCP.id_seq {P : Type u_1} (u : CCP P) : id.seq u = u

theorem Semantics.Dynamic.Core.CCP.seq_id {P : Type u_1} (u : CCP P) : u.seq id = u

@[implicit_reducible]

instance Semantics.Dynamic.Core.CCP.instMonoid {P : Type u_1} : Monoid (CCP P)

CCPs form a monoid under sequential composition

Equations

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

theorem Semantics.Dynamic.Core.CCP.seq_absurd {P : Type u_1} (u : CCP P) : u.seq absurd = absurd

seq_absurd: anything followed by absurd is absurd

def Semantics.Dynamic.Core.CCP.conj {P : Type u_1} (u v : CCP P) : CCP P

Dynamic conjunction: alias for sequential composition

Equations

• u.conj v = u.seq v

noncomputable def Semantics.Dynamic.Core.CCP.neg {P : Type u_1} (φ : CCP P) : CCP P

Test-based negation: passes (returns input) iff φ yields ∅.

This is the standard dynamic negation of @cite{heim-1982}, @cite{veltman-1996}: ¬φ(s) = s if φ(s) = ∅, else ∅. Does not validate DNE.

Equations

• φ.neg s = if Set.Nonempty (φ s) then ∅ else s

noncomputable def Semantics.Dynamic.Core.CCP.might {P : Type u_1} (φ : CCP P) : CCP P

Compatibility test ("might"): passes iff φ yields a nonempty result.

might(φ)(s) = s if φ(s) ≠ ∅, else ∅

Equations

• φ.might s = if Set.Nonempty (φ s) then s else ∅

noncomputable def Semantics.Dynamic.Core.CCP.must {P : Type u_1} (φ : CCP P) : CCP P

Full support test ("must"): passes iff φ returns input unchanged.

must(φ)(s) = s if φ(s) = s, else ∅

Equations

• φ.must s = if φ s = s then s else ∅

noncomputable def Semantics.Dynamic.Core.CCP.impl {P : Type u_1} (φ ψ : CCP P) : CCP P

Dynamic implication test: passes iff output of φ is preserved by ψ.

impl(φ,ψ)(s) = s if φ(s) ⊆ ψ(φ(s)), else ∅

Equations

• φ.impl ψ s = if φ s ⊆ ψ (φ s) then s else ∅

noncomputable def Semantics.Dynamic.Core.CCP.disj {P : Type u_1} (φ ψ : CCP P) : CCP P

Dynamic disjunction via De Morgan: φ ∨ ψ = ¬(¬φ ; ¬ψ).

@cite{heim-1983}: the local context for the second disjunct is the global context updated with ¬φ. This yields the standard Karttunen projection pattern for inclusive disjunction.

Equations

• φ.disj ψ = (φ.neg.seq ψ.neg).neg

def Semantics.Dynamic.Core.CCP.entails {P : Type u_1} (φ ψ : CCP P) : Prop

Dynamic entailment: φ entails ψ iff ψ adds no information after φ.

Equations

• φ.entails ψ = ∀ (s : Semantics.Dynamic.Core.InfoStateOf P), Set.Nonempty (φ s) → ψ (φ s) = φ s

theorem Semantics.Dynamic.Core.CCP.entails_id {P : Type u_1} (φ : CCP P) : φ.entails id

Entailment is reflexive

def Semantics.Dynamic.Core.IsEliminative {P : Type u_1} (u : CCP P) : Prop

An update is eliminative if it never adds possibilities.

This is the fundamental property of dynamic semantics: information only grows (possibilities only decrease).

Equations

• Semantics.Dynamic.Core.IsEliminative u = ∀ (s : Semantics.Dynamic.Core.InfoStateOf P), u s ⊆ s

theorem Semantics.Dynamic.Core.eliminative_id {P : Type u_1} : IsEliminative CCP.id

Identity is eliminative

theorem Semantics.Dynamic.Core.eliminative_seq {P : Type u_1} (u v : CCP P) (hu : IsEliminative u) (hv : IsEliminative v) : IsEliminative (u.seq v)

Sequential composition preserves eliminativity

def Semantics.Dynamic.Core.IsExpansive {P : Type u_1} (u : CCP P) : Prop

An update is expansive if it never removes possibilities.

Expansive operations include discourse referent introduction (DRT/DPL), modal horizon expansion (@cite{kirkpatrick-2024}), and accommodation. These are the dual of eliminative operations: where eliminative updates can only shrink the state, expansive updates can only grow it.

Equations

• Semantics.Dynamic.Core.IsExpansive u = ∀ (s : Semantics.Dynamic.Core.InfoStateOf P), s ⊆ u s

theorem Semantics.Dynamic.Core.expansive_id {P : Type u_1} : IsExpansive CCP.id

Identity is expansive

theorem Semantics.Dynamic.Core.expansive_seq {P : Type u_1} (u v : CCP P) (hu : IsExpansive u) (hv : IsExpansive v) : IsExpansive (u.seq v)

Sequential composition preserves expansiveness

theorem Semantics.Dynamic.Core.eliminative_expansive_id {P : Type u_1} (u : CCP P) (he : IsEliminative u) (hx : IsExpansive u) (s : InfoStateOf P) : u s = s

A CCP that is both eliminative and expansive is the identity on every input.

theorem Semantics.Dynamic.Core.isEliminative_iff_le_id {P : Type u_1} (u : CCP P) : IsEliminative u ↔ ∀ (s : InfoStateOf P), u s ≤ s

Eliminative ↔ antitone on the identity: u s ≤ s for all s.

theorem Semantics.Dynamic.Core.isExpansive_iff_id_le {P : Type u_1} (u : CCP P) : IsExpansive u ↔ ∀ (s : InfoStateOf P), s ≤ u s

Expansive ↔ identity below: s ≤ u s for all s.

theorem Semantics.Dynamic.Core.IsEliminative.le_id {P : Type u_1} {u : CCP P} (h : IsEliminative u) (s : InfoStateOf P) : u s ≤ s

Eliminative updates are antitone at the identity: u ≤ id in the pointwise order.

theorem Semantics.Dynamic.Core.IsExpansive.id_le {P : Type u_1} {u : CCP P} (h : IsExpansive u) (s : InfoStateOf P) : s ≤ u s

Expansive updates satisfy id ≤ u in the pointwise order.

def Semantics.Dynamic.Core.IsTest {P : Type u_1} (u : CCP P) : Prop

A test is a CCP that either passes (returns input) or fails (returns ∅).

Tests don't change information - they check compatibility. Examples: might, must, presupposition triggers.

Equations

• Semantics.Dynamic.Core.IsTest u = ∀ (s : Semantics.Dynamic.Core.InfoStateOf P), u s = s ∨ u s = ∅

theorem Semantics.Dynamic.Core.test_eliminative {P : Type u_1} (u : CCP P) (h : IsTest u) : IsEliminative u

Tests are eliminative

theorem Semantics.Dynamic.Core.CCP.neg_isTest {P : Type u_1} (φ : CCP P) : IsTest φ.neg

theorem Semantics.Dynamic.Core.CCP.might_isTest {P : Type u_1} (φ : CCP P) : IsTest φ.might

theorem Semantics.Dynamic.Core.CCP.must_isTest {P : Type u_1} (φ : CCP P) : IsTest φ.must

theorem Semantics.Dynamic.Core.CCP.impl_isTest {P : Type u_1} (φ ψ : CCP P) : IsTest (φ.impl ψ)

theorem Semantics.Dynamic.Core.CCP.might_eq_neg_neg {P : Type u_1} (φ : CCP P) : φ.might = φ.neg.neg

Duality: might φ = ¬(¬φ)

def Semantics.Dynamic.Core.supportOf {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (s : InfoStateOf P) (ψ : φ) : Prop

Support relation: s supports ψ if all possibilities in s satisfy ψ.

This is the fundamental entailment relation of dynamic semantics.

Equations

• Semantics.Dynamic.Core.supportOf sat s ψ = ∀ (p : P), p ∈ s → sat p ψ

def Semantics.Dynamic.Core.contentOf {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) : InfoStateOf P

Content of a formula: all possibilities satisfying it.

Equations

• Semantics.Dynamic.Core.contentOf sat ψ = {p : P | sat p ψ}

theorem Semantics.Dynamic.Core.support_iff_subset_content {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (s : InfoStateOf P) (ψ : φ) : supportOf sat s ψ ↔ s ⊆ contentOf sat ψ

Galois connection: s ⊆ content ψ ↔ s supports ψ

This is the fundamental duality of dynamic semantics.

theorem Semantics.Dynamic.Core.support_mono {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (s t : InfoStateOf P) (ψ : φ) (h : t ⊆ s) (hs : supportOf sat s ψ) : supportOf sat t ψ

Support is downward closed: smaller states support more.

theorem Semantics.Dynamic.Core.empty_supports {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) : supportOf sat ∅ ψ

Empty state supports everything (vacuously).

theorem Semantics.Dynamic.Core.content_mono {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ₁ ψ₂ : φ) (h : ∀ (p : P), sat p ψ₁ → sat p ψ₂) : contentOf sat ψ₁ ⊆ contentOf sat ψ₂

Content is antitone in entailment.

theorem Semantics.Dynamic.Core.sep_monotone {P : Type u_1} (pred : P → Prop) : Monotone fun (s : Set P) => {p : P | p ∈ s ∧ pred p}

Filtering a set by a predicate is monotone. This is the shared foundation for monotonicity of updateFromSat, atom, pred1, pred2, etc.

theorem Semantics.Dynamic.Core.sep_eliminative {P : Type u_1} (pred : P → Prop) : IsEliminative fun (s : Set P) => {p : P | p ∈ s ∧ pred p}

Filtering a set by a predicate is eliminative.

def Semantics.Dynamic.Core.updateFromSat {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) : CCP P

The standard update construction: filter by satisfaction.

This is how PLA, DRT, DPL all define updates.

Equations

• Semantics.Dynamic.Core.updateFromSat sat ψ s = {p : P | p ∈ s ∧ sat p ψ}

theorem Semantics.Dynamic.Core.updateFromSat_eliminative {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) : IsEliminative (updateFromSat sat ψ)

Standard updates are eliminative

theorem Semantics.Dynamic.Core.mem_updateFromSat {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) (s : InfoStateOf P) (p : P) : p ∈ updateFromSat sat ψ s ↔ p ∈ s ∧ sat p ψ

Standard update membership

theorem Semantics.Dynamic.Core.updateFromSat_eq_inter_content {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) (s : InfoStateOf P) : updateFromSat sat ψ s = s ∩ contentOf sat ψ

Update equals intersection with content

theorem Semantics.Dynamic.Core.support_iff_update_eq {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) (s : InfoStateOf P) : supportOf sat s ψ ↔ updateFromSat sat ψ s = s

Support-Update equivalence

def Semantics.Dynamic.Core.dynamicEntailsOf {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ₁ ψ₂ : φ) : Prop

Dynamic entailment: φ dynamically entails ψ if updating with φ always yields a state that supports ψ.

Equations

• Semantics.Dynamic.Core.dynamicEntailsOf sat ψ₁ ψ₂ = ∀ (s : Semantics.Dynamic.Core.InfoStateOf P), Semantics.Dynamic.Core.supportOf sat (Semantics.Dynamic.Core.updateFromSat sat ψ₁ s) ψ₂

theorem Semantics.Dynamic.Core.dynamicEntails_refl {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) : dynamicEntailsOf sat ψ ψ

Dynamic entailment is reflexive

theorem Semantics.Dynamic.Core.dynamicEntails_trans {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ₁ ψ₂ ψ₃ : φ) (h1 : dynamicEntailsOf sat ψ₁ ψ₂) (h2 : dynamicEntailsOf sat ψ₂ ψ₃) : dynamicEntailsOf sat ψ₁ ψ₃

Dynamic entailment is transitive

theorem Semantics.Dynamic.Core.updateFromSat_monotone {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) : Monotone (updateFromSat sat ψ)

updateFromSat is monotone in the state argument: larger input states yield larger output states. Uses mathlib's Monotone (i.e., s ≤ t → f s ≤ f t where ≤ on Set is ⊆).

structure Semantics.Dynamic.Core.Possibility (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A possibility: world paired with variable assignment.

This is the concrete state type for world-sensitive dynamic semantics (DPL, DRT, CDRT, PLA). The assignment field uses Assignment E from the CCP infrastructure.

• world : W
• assignment : Assignment E

def Semantics.Dynamic.Core.Possibility.agreeOn {W : Type u_1} {E : Type u_2} (p q : Possibility W E) (vars : Set ℕ) : Prop

Two possibilities agree on all variables in a set.

Equations

• p.agreeOn q vars = ∀ (x : ℕ), x ∈ vars → p.assignment x = q.assignment x

def Semantics.Dynamic.Core.Possibility.sameWorld {W : Type u_1} {E : Type u_2} (p q : Possibility W E) : Prop

Same world, possibly different assignment.

Equations

• p.sameWorld q = (p.world = q.world)

def Semantics.Dynamic.Core.Possibility.extend {W : Type u_1} {E : Type u_2} (p : Possibility W E) (x : ℕ) (e : E) : Possibility W E

Extend an assignment at a single variable, using Assignment.update.

Equations

• p.extend x e = { world := p.world, assignment := p.assignment.update x e }

@[simp]

theorem Semantics.Dynamic.Core.Possibility.extend_at {W : Type u_1} {E : Type u_2} (p : Possibility W E) (x : ℕ) (e : E) : (p.extend x e).assignment x = e

@[simp]

theorem Semantics.Dynamic.Core.Possibility.extend_other {W : Type u_1} {E : Type u_2} (p : Possibility W E) (x y : ℕ) (e : E) (h : y ≠ x) : (p.extend x e).assignment y = p.assignment y

@[simp]

theorem Semantics.Dynamic.Core.Possibility.extend_world {W : Type u_1} {E : Type u_2} (p : Possibility W E) (x : ℕ) (e : E) : (p.extend x e).world = p.world

@[reducible, inline]

abbrev Semantics.Dynamic.Core.InfoState (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

Information state: set of possibilities.

This is InfoStateOf (Possibility W E) — a specialization of the generic InfoStateOf to world-assignment possibilities.

Equations

• Semantics.Dynamic.Core.InfoState W E = Set (Semantics.Dynamic.Core.Possibility W E)

def Semantics.Dynamic.Core.InfoState.univ {W : Type u_1} {E : Type u_2} : InfoState W E

The trivial state: all possibilities.

Equations

• Semantics.Dynamic.Core.InfoState.univ = Set.univ

def Semantics.Dynamic.Core.InfoState.empty {W : Type u_1} {E : Type u_2} : InfoState W E

The absurd state: no possibilities.

Equations

• Semantics.Dynamic.Core.InfoState.empty = ∅

def Semantics.Dynamic.Core.InfoState.consistent {W : Type u_1} {E : Type u_2} (s : InfoState W E) : Prop

State is consistent (non-empty).

Equations

• s.consistent = Set.Nonempty s

def Semantics.Dynamic.Core.InfoState.trivial {W : Type u_1} {E : Type u_2} (s : InfoState W E) : Prop

State is trivial (all possibilities).

Equations

• s.trivial = (s = Set.univ)

def Semantics.Dynamic.Core.InfoState.definedAt {W : Type u_1} {E : Type u_2} (s : InfoState W E) (x : ℕ) : Prop

Variable x is defined in state s iff all possibilities agree on x's value.

Equations

• s.definedAt x = ∀ (p q : Semantics.Dynamic.Core.Possibility W E), p ∈ s → q ∈ s → p.assignment x = q.assignment x

def Semantics.Dynamic.Core.InfoState.definedVars {W : Type u_1} {E : Type u_2} (s : InfoState W E) : Set ℕ

The set of defined variables in a state.

Equations

• s.definedVars = {x : ℕ | s.definedAt x}

def Semantics.Dynamic.Core.InfoState.novelAt {W : Type u_1} {E : Type u_2} (s : InfoState W E) (x : ℕ) : Prop

Variable x is novel in state s iff x is not defined.

Equations

• s.novelAt x = ¬s.definedAt x

theorem Semantics.Dynamic.Core.InfoState.novelAt_iff_disagree {W : Type u_1} {E : Type u_2} (s : InfoState W E) (x : ℕ) (hs : s.consistent) : s.novelAt x ↔ ∃ (p : Possibility W E), ∃ (q : Possibility W E), p ∈ s ∧ q ∈ s ∧ p.assignment x ≠ q.assignment x

In a consistent state, novel means assignments actually disagree.

def Semantics.Dynamic.Core.InfoState.worlds {W : Type u_1} {E : Type u_2} (s : InfoState W E) : Set W

Project to the set of worlds in the state.

Equations

• s.worlds = {w : W | ∃ (p : Semantics.Dynamic.Core.Possibility W E), p ∈ s ∧ p.world = w}

def Semantics.Dynamic.Core.InfoState.filterWorlds {W : Type u_1} {E : Type u_2} (s : InfoState W E) (pred : W → Bool) : InfoState W E

Filter state by a world predicate.

Equations

• s.filterWorlds pred = {p : Semantics.Dynamic.Core.Possibility W E | p ∈ s ∧ pred p.world = true}

def Semantics.Dynamic.Core.InfoState.filterAssign {W : Type u_1} {E : Type u_2} (s : InfoState W E) (pred : (ℕ → E) → Bool) : InfoState W E

Filter state by an assignment predicate.

Equations

• s.filterAssign pred = {p : Semantics.Dynamic.Core.Possibility W E | p ∈ s ∧ pred p.assignment = true}

structure Semantics.Dynamic.Core.Context (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Context extends InfoState with metadata.

• state : InfoState W E
• definedVars : Set ℕ
• domain : Set E

def Semantics.Dynamic.Core.Context.initial {W : Type u_1} {E : Type u_2} : Context W E

Empty context with all possibilities.

Equations

• Semantics.Dynamic.Core.Context.initial = { state := Semantics.Dynamic.Core.InfoState.univ }

def Semantics.Dynamic.Core.Context.consistent {W : Type u_1} {E : Type u_2} (c : Context W E) : Prop

Context is consistent iff its state is.

Equations

• c.consistent = c.state.consistent

def Semantics.Dynamic.Core.Context.introduce {W : Type u_1} {E : Type u_2} (c : Context W E) (x : ℕ) : Context W E

Mark a variable as defined.

Equations

• c.introduce x = { state := c.state, definedVars := c.definedVars ∪ {x}, domain := c.domain }

def Semantics.Dynamic.Core.Context.narrow {W : Type u_1} {E : Type u_2} (c : Context W E) (s : InfoState W E) : Context W E

Narrow the state.

Equations

• c.narrow s = { state := c.state ∩ s, definedVars := c.definedVars, domain := c.domain }

def Semantics.Dynamic.Core.InfoState.subsistsIn {W : Type u_1} {E : Type u_2} (s s' : InfoState W E) : Prop

State subsistence: s subsists in s' iff every possibility in s has a descendant in s'.

Equations

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

def Semantics.Dynamic.Core.«term_⪯_» : Lean.TrailingParserDescr

Equations

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

theorem Semantics.Dynamic.Core.InfoState.subsistsIn_refl {W : Type u_1} {E : Type u_2} (s : InfoState W E) : s ⪯ s

Subsistence is reflexive.

theorem Semantics.Dynamic.Core.InfoState.subset_subsistsIn {W : Type u_1} {E : Type u_2} {s s' : InfoState W E} (h : s ⊆ s') : s ⪯ s'

Subset implies subsistence.

def Semantics.Dynamic.Core.InfoState.supports {W : Type u_1} {E : Type u_2} (s : InfoState W E) (φ : W → Bool) : Prop

State s supports proposition φ iff φ holds at all worlds in s.

Equations

• (s ⊫ φ) = ∀ (p : Semantics.Dynamic.Core.Possibility W E), p ∈ s → φ p.world = true

def Semantics.Dynamic.Core.InfoState.«term_⊫_» : Lean.TrailingParserDescr

Equations

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

theorem Semantics.Dynamic.Core.InfoState.supports_mono {W : Type u_1} {E : Type u_2} {s s' : InfoState W E} (h : s ⊆ s') (φ : W → Bool) (hsupp : s' ⊫ φ) : s ⊫ φ

Support is preserved by subset.

@[reducible, inline]

abbrev Semantics.Dynamic.Core.State (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

State: set of world-assignment pairs.

Isomorphic to InfoState W E but uses a flat product instead of the Possibility structure. Prefer InfoState for new code.

Equations

• Semantics.Dynamic.Core.State W E = Set (W × Core.Assignment E)

@[reducible, inline]

abbrev Semantics.Dynamic.Core.StateCCP (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

State-level CCP: context change potential over world-assignment states. Definitionally equal to CCP (W × Assignment E), so all CCP infrastructure (monoid, neg, might, tests, entailment, Galois connection) applies.

Equations

• Semantics.Dynamic.Core.StateCCP W E = Semantics.Dynamic.Core.CCP (W × Core.Assignment E)

def Semantics.Dynamic.Core.IsDistributive {P : Type u_1} (φ : CCP P) : Prop

A CCP is distributive when it processes each element of the input independently: φ(s) = ⋃_{i∈s} φ({i}).

Equations

• Semantics.Dynamic.Core.IsDistributive φ = ∀ (s : Semantics.Dynamic.Core.InfoStateOf P), φ s = {p : P | ∃ (i : P), i ∈ s ∧ p ∈ φ {i}}

theorem Semantics.Dynamic.Core.updateFromSat_isDistributive {P : Type u_1} {φ : Type u_2} (sat : P → φ → Prop) (ψ : φ) : IsDistributive (updateFromSat sat ψ)

updateFromSat is always distributive: it filters per-element.

theorem Semantics.Dynamic.Core.might_not_isDistributive : ∃ (P : Type), ∃ (φ : CCP P), ¬IsDistributive φ.might

CCP.might is not distributive: the whole-context test can pass while individual-element tests fail.

Witness: P = Bool, φ keeps only true. might φ {true, false} = {true, false} (whole-context test passes), but per-singleton: might φ {false} = ∅ (test fails on false-only context). So false is in the whole-context result but not the distributive union.

The relational type DRS S = S → S → Prop from DynProp is the primary dynamic semantic type. Every DRS gives rise to a distributive CCP via the relational image (lift), and every distributive CCP arises this way (lower). The round-trip is the identity in both directions (for distributive CCPs).

Non-distributive CCP operations (neg, might, must) test the whole input state and have no direct DRS counterpart — they are genuine additions of the set-transformer perspective.

def Semantics.Dynamic.Core.lift {S : Type u_1} (R : DynProp.DRS S) : CCP S

Lift a relational DRS meaning to a CCP (set transformer).

This is the relational image: given input state σ, collect all outputs reachable from any element of σ. The resulting CCP is always distributive (lift_isDistributive).

Equations

• Semantics.Dynamic.Core.lift R σ = {j : S | ∃ (i : S), i ∈ σ ∧ R i j}

def Semantics.Dynamic.Core.lower {S : Type u_1} (φ : CCP S) : DynProp.DRS S

Lower a CCP to a relational DRS meaning.

lower φ i j holds iff j is in the output of the singleton {i}. This is the inverse of lift for distributive CCPs.

Equations

• Semantics.Dynamic.Core.lower φ i j = (j ∈ φ {i})

theorem Semantics.Dynamic.Core.lift_dseq {S : Type u_1} (R₁ R₂ : DynProp.DRS S) : lift (R₁ ⨟ R₂) = (lift R₁).seq (lift R₂)

Lifting preserves sequential composition: lift (R₁ ⨟ R₂) = lift R₁ ;; lift R₂.

theorem Semantics.Dynamic.Core.lift_test {S : Type u_1} (C : DynProp.Condition S) : lift [C] = fun (σ : InfoStateOf S) => {i : S | i ∈ σ ∧ C i}

Lifting a test produces a per-element filter: lift (test C) σ = { i ∈ σ | C i }.

theorem Semantics.Dynamic.Core.lift_isDistributive {S : Type u_1} (R : DynProp.DRS S) : IsDistributive (lift R)

Lifted CCPs are always distributive.

theorem Semantics.Dynamic.Core.lower_lift {S : Type u_1} (R : DynProp.DRS S) : lower (lift R) = R

Round-trip: lower (lift R) = R. The relational type loses no information when lifted and lowered.

theorem Semantics.Dynamic.Core.lift_lower {S : Type u_1} (φ : CCP S) (hd : IsDistributive φ) : lift (lower φ) = φ

Round-trip: lift (lower φ) = φ for distributive CCPs. Distributive CCPs are exactly the relational images.

theorem Semantics.Dynamic.Core.lift_test_isEliminative {S : Type u_1} (C : DynProp.Condition S) : IsEliminative (lift [C])

lift (test C) is eliminative: it only removes elements.

theorem Semantics.Dynamic.Core.updateFromSat_eq_lift_test {P : Type u_2} {φ : Type u_3} (sat : P → φ → Prop) (ψ : φ) : updateFromSat sat ψ = lift [fun (p : P) => sat p ψ]

updateFromSat is the lifting of test applied to a satisfaction relation. This connects the CCP-native updateFromSat to the primary relational algebra.