Linglib.Theories.Semantics.Dynamic.Systems.PLA.Update

"It's not the case that no man came. He sat down." - "He" is problematic. Negation "traps" drefs: ∃x.P(x) exports x, but ¬¬∃x.P(x) only tests existence. This motivates bilateral semantics (BUS), where DNE holds structurally.

source

theorem Semantics.Dynamic.PLA.update_taut {E : Type u_1} [Nonempty E] (M : Model E) (s : InfoState E) (φ : Formula) (htaut : ∀ (g : Assignment E) (ê : WitnessSeq E), Formula.sat M g ê φ) :

Formula.update M φ s = s

Updating with a tautology leaves state unchanged

source

theorem Semantics.Dynamic.PLA.update_contra {E : Type u_1} [Nonempty E] (M : Model E) (s : InfoState E) (φ : Formula) (hcontra : ∀ (g : Assignment E) (ê : WitnessSeq E), ¬Formula.sat M g ê φ) :

Formula.update M φ s = ∅

Updating with a contradiction yields empty state

source

theorem Semantics.Dynamic.PLA.update_elim {E : Type u_1} [Nonempty E] (M : Model E) (s : InfoState E) (φ : Formula) (h : s ⊫[M] φ) :

Formula.update M φ s = s

Update elimination: if s already supports φ, update is identity

source

theorem Semantics.Dynamic.PLA.update_eq_updateFromSat {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) :

Formula.update M φ s = Core.updateFromSat (satisfiesPLA M) φ s

PLA formula update equals Core.updateFromSat via satPoss.

source

theorem Semantics.Dynamic.PLA.update_eliminative {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) :

Formula.update M φ s ⊆ s

Eliminativity: updates never add possibilities, only remove them.

This is the fundamental property of dynamic semantics: information only grows. Every update is a subset of the input state.

This follows from Core.updateFromSat_eliminative.

source

theorem Semantics.Dynamic.PLA.update_isEliminative {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) :

Core.IsEliminative (Formula.update M φ)

PLA's formula update is eliminative in the Core sense.

source

theorem Semantics.Dynamic.PLA.update_monotone {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s t : InfoState E) (h : s ⊆ t) :

Formula.update M φ s ⊆ Formula.update M φ t

Monotonicity of update: larger input states yield larger output states.

If s ⊆ t, then φ.update(s) ⊆ φ.update(t).

This follows from Core.updateFromSat_monotone.

source

theorem Semantics.Dynamic.PLA.support_downward_closed {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s t : InfoState E) (h : t ⊆ s) (hs : s ⊫[M] φ) :

t ⊫[M] φ

Support is downward closed: if t ⊆ s and s supports φ, then t supports φ.

Smaller states have "more information" (fewer possibilities = more certainty).

source

theorem Semantics.Dynamic.PLA.support_inter {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s t : InfoState E) (hs : s ⊫[M] φ) (_ht : t ⊫[M] φ) :

s ∩ t ⊫[M] φ

Intersection preserves support: if s and t both support φ, so does s ∩ t.

source

theorem Semantics.Dynamic.PLA.support_union_iff {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s t : InfoState E) :

(s ∪ t ⊫[M] φ) ↔ (s ⊫[M] φ) ∧ t ⊫[M] φ

Union and support: s ∪ t supports φ iff both s and t support φ.

source

theorem Semantics.Dynamic.PLA.update_inter {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s t : InfoState E) :

Formula.update M φ (s ∩ t) = Formula.update M φ s ∩ Formula.update M φ t

Update distributes over intersection: φ.update(s ∩ t) = φ.update(s) ∩ φ.update(t)

source

theorem Semantics.Dynamic.PLA.dynConj_subset_inter {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ : Formula) (s : InfoState E) :

Formula.dynConj M φ ψ s ⊆ Formula.update M φ s ∩ Formula.update M ψ s

Sequential composition with intersection: (φ; ψ)(s) ⊆ φ(s) ∩ ψ(s)

Note: this is not equality in general due to the dynamic nature of sequencing.

source

theorem Semantics.Dynamic.PLA.ccp_reducibility {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) :

Formula.update M φ s = s ∩ Formula.content M φ

CCP Reducibility: updates = intersection with content.

source

theorem Semantics.Dynamic.PLA.static_seq_is_intersection {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ : Formula) (s : InfoState E) (_hφ : φ.domain = ∅) (_hψ : ψ.domain = ∅) :

(Formula.update M φ ;; Formula.update M ψ) s = s ∩ Formula.content M φ ∩ Formula.content M ψ

Sequential composition = nested intersection of contents.

source

theorem Semantics.Dynamic.PLA.dynamicity_source_exists (x : VarIdx) (φ : Formula) :

x ∈ (Formula.exists_ x φ).domain

Only ∃ introduces discourse referents.

source

theorem Semantics.Dynamic.PLA.dynamicity_source_neg (φ : Formula) :

(∼φ).domain = φ.domain

source

theorem Semantics.Dynamic.PLA.dynamicity_source_conj (φ ψ : Formula) :

(φ ⋀ ψ).domain = φ.domain ∪ ψ.domain

source

theorem Semantics.Dynamic.PLA.dynamicity_source_atom (name : String) (ts : List Term) :

(Formula.atom name ts).domain = ∅

source

theorem Semantics.Dynamic.PLA.domain_empty_iff_no_exists (φ : Formula) :

φ.domain = ∅ ↔ ∀ (x : VarIdx), x ∉ φ.domain

Domain empty iff no variables bound.

source

theorem Semantics.Dynamic.PLA.ccp_reduces_to_static {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ : Formula) (s : InfoState E) (hφ : φ.domain = ∅) (hψ : ψ.domain = ∅) :

(Formula.update M φ ;; Formula.update M ψ) s = Formula.update M (φ ⋀ ψ) s

CCP reducibility: for dref-free formulas, φ; ψ = φ ∧ ψ.

source

theorem Semantics.Dynamic.PLA.updates_are_tests {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) :

Formula.update M φ s ⊆ s

Updates are eliminative: they only filter, never add.

source

theorem Semantics.Dynamic.PLA.same_content_same_update {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ : Formula) (hcontent : Formula.content M φ = Formula.content M ψ) (s : InfoState E) :

Formula.update M φ s = Formula.update M ψ s

Same content implies same update.

source

theorem Semantics.Dynamic.PLA.dekker_minimalism {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) (s : InfoState E) :

Formula.update M φ s = {p : Assignment E × WitnessSeq E | p ∈ s ∧ p ∈ Formula.content M φ}

Updates are intersection with content: φ.update s = { p ∈ s | p ∈ φ.content }.

source

def Semantics.Dynamic.PLA.dynamicEntails {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ : Formula) :

Prop

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

This is the fundamental semantic consequence relation for dynamic semantics.

Equations

(φ ⊨[M]_dyn ψ) = ∀ (s : Semantics.Dynamic.PLA.InfoState E), Semantics.Dynamic.PLA.Formula.update M φ s ⊫[M] ψ

Instances For

source

def Semantics.Dynamic.PLA.«term_⊨[_]_dyn_» :

Lean.TrailingParserDescr

Equations

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

Instances For

source

theorem Semantics.Dynamic.PLA.dynamicEntails_refl {E : Type u_1} [Nonempty E] (M : Model E) (φ : Formula) :

φ ⊨[M]_dyn φ

Reflexivity of dynamic entailment: φ ⊨_dyn φ.

Updating with φ yields a state that supports φ.

source

theorem Semantics.Dynamic.PLA.dynamicEntails_trans {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ χ : Formula) (h1 : φ ⊨[M]_dyn ψ) (h2 : ψ ⊨[M]_dyn χ) :

φ ⊨[M]_dyn χ

Chaining dynamic entailment: if φ ⊨_dyn ψ and ψ ⊨_dyn χ, then φ ⊨_dyn χ.

Note: This holds because update is eliminative - if φ entails ψ, then updating with φ produces a state that supports ψ, and since that state is a subset of the original, it also supports χ if ψ ⊨_dyn χ.

source

theorem Semantics.Dynamic.PLA.dynamicEntails_weakening {E : Type u_1} [Nonempty E] (M : Model E) (φ ψ : Formula) (s : InfoState E) (hent : φ ⊨[M]_dyn ψ) :

Formula.update M φ s ⊫[M] ψ

Weakening: if s supports φ and φ ⊨_dyn ψ, then φ.update(s) supports ψ.