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

Update state with proposition: keep only possibilities where φ holds.

Equations

• s⟦φ⟧ = {p : Semantics.Dynamic.Core.Possibility W E | p ∈ s ∧ φ p.world = true}

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.update_mono {W : Type u_1} {E : Type u_2} {s s' : InfoState W E} (h : s ⊆ s') (φ : W → Bool) : s⟦φ⟧ ⊆ s'⟦φ⟧

Update is monotonic: larger states give larger results

theorem Semantics.Dynamic.Core.InfoState.update_update {W : Type u_1} {E : Type u_2} (s : InfoState W E) (φ : W → Bool) : s⟦φ⟧⟦φ⟧ = s⟦φ⟧

Update is idempotent

theorem Semantics.Dynamic.Core.InfoState.update_seq {W : Type u_1} {E : Type u_2} (s : InfoState W E) (φ ψ : W → Bool) : s⟦φ⟧⟦ψ⟧ = s⟦fun (w : W) => φ w && ψ w⟧

Sequential update = conjunction

theorem Semantics.Dynamic.Core.InfoState.update_preserves_defined {W : Type u_1} {E : Type u_2} (s : InfoState W E) (φ : W → Bool) (x : ℕ) (h : s.definedAt x) : s⟦φ⟧.definedAt x

Update preserves definedness

theorem Semantics.Dynamic.Core.InfoState.update_supports {W : Type u_1} {E : Type u_2} (s : InfoState W E) (φ : W → Bool) : s⟦φ⟧ ⊫ φ

s[φ] ⊫ φ

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

Dynamic entailment for propositions.

Equations

• Semantics.Dynamic.Core.InfoState.dynamicEntails φ ψ = ∀ (s : Semantics.Dynamic.Core.InfoState W E), s⟦φ⟧.consistent → s⟦φ⟧ ⊫ ψ

theorem Semantics.Dynamic.Core.InfoState.dynamicEntails_refl {W : Type u_1} {E : Type u_2} (φ : W → Bool) : dynamicEntails φ φ

Any proposition dynamically entails itself

theorem Semantics.Dynamic.Core.InfoState.dynamicEntails_conj {W : Type u_1} {E : Type u_2} (φ ψ : W → Bool) (h : dynamicEntails φ ψ) : dynamicEntails φ fun (w : W) => φ w && ψ w

φ dynamically entails φ ∧ ψ when φ entails ψ

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

Random assignment: introduce new discourse referent at variable x.

Equations

• s.randomAssign x domain = {p' : Semantics.Dynamic.Core.Possibility W E | ∃ (p : Semantics.Dynamic.Core.Possibility W E), p ∈ s ∧ ∃ (e : E), e ∈ domain ∧ p' = p.extend x e}

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

Random assignment with full domain

Equations

• s.randomAssignFull x = {p' : Semantics.Dynamic.Core.Possibility W E | ∃ (p : Semantics.Dynamic.Core.Possibility W E), p ∈ s ∧ ∃ (e : E), p' = p.extend x e}

theorem Semantics.Dynamic.Core.InfoState.randomAssign_makes_novel {W : Type u_1} {E : Type u_2} (s : InfoState W E) (x : ℕ) (domain : Set E) (hs : s.consistent) (hdom : ∃ (e₁ : E), ∃ (e₂ : E), e₁ ∈ domain ∧ e₂ ∈ domain ∧ e₁ ≠ e₂) : (s.randomAssign x domain).novelAt x

Random assignment makes x novel (when domain has multiple elements)

theorem Semantics.Dynamic.Core.InfoState.randomAssign_preserves_defined {W : Type u_1} {E : Type u_2} (s : InfoState W E) (x y : ℕ) (domain : Set E) (h : s.definedAt y) (hne : y ≠ x) : (s.randomAssign x domain).definedAt y

Random assignment preserves other defined variables

def Semantics.Dynamic.Core.CCP.exists_ {W : Type u_1} {E : Type u_2} (x : ℕ) (domain : Set E) (φ : CCP (Possibility W E)) : CCP (Possibility W E)

Existential CCP: ∃x.φ introduces x then updates with φ.

Equations

• Semantics.Dynamic.Core.CCP.exists_ x domain φ s = φ (s.randomAssign x domain)

def Semantics.Dynamic.Core.CCP.existsFull {W : Type u_1} {E : Type u_2} (x : ℕ) (φ : CCP (Possibility W E)) : CCP (Possibility W E)

Existential with full domain

Equations

• Semantics.Dynamic.Core.CCP.existsFull x φ s = φ (s.randomAssignFull x)

def Semantics.Dynamic.Core.CCP.ofProp {W : Type u_1} {E : Type u_2} (φ : W → Bool) : CCP (Possibility W E)

Lift a classical proposition to a CCP.

Equations

• Semantics.Dynamic.Core.CCP.ofProp φ s = s⟦φ⟧

def Semantics.Dynamic.Core.CCP.ofPred1 {W : Type u_1} {E : Type u_2} (p : E → W → Bool) (x : ℕ) : CCP (Possibility W E)

Lift a predicate on entities (via variable lookup).

Equations

• Semantics.Dynamic.Core.CCP.ofPred1 p x s = {poss : Semantics.Dynamic.Core.Possibility W E | poss ∈ s ∧ p (poss.assignment x) poss.world = true}

def Semantics.Dynamic.Core.CCP.ofPred2 {W : Type u_1} {E : Type u_2} (p : E → E → W → Bool) (x y : ℕ) : CCP (Possibility W E)

Lift a binary predicate.

Equations

• Semantics.Dynamic.Core.CCP.ofPred2 p x y s = {poss : Semantics.Dynamic.Core.Possibility W E | poss ∈ s ∧ p (poss.assignment x) (poss.assignment y) poss.world = true}