PLA dynamic update semantics

Information update and support for PLA, after [Dek12]: three equivalent perspectives on dynamic meaning — contents (sets of assignment-witness pairs), updates (context change potentials over PLA possibilities, instantiating DynamicSemantics.CCP), and support (a state supports a formula when the formula holds throughout it).

Main definitions

• PLA.InfoState, PLA.Formula.content, PLA.Formula.update, PLA.InfoState.supports
• PLA.Formula.dynConj: sequential update
• PLA.dynamicEntails: dynamic entailment, scoped notation φ ⊨[M]_dyn ψ

Main results

• PLA.contents_updates_equiv (Observation 16): update is intersection with content
• PLA.updates_support_equiv (Observation 17): support means update is the identity
• PLA.update_eliminative: updates only filter the input state; consequently dynamic conjunction here is commutative and static-reducible (PLA.dynConj_static) — [Dek12]'s non-commutativity claims concern witness-sequence dynamics this formalization does not render
• PLA.obs10_dynamic_eq_classical_entailment: dynamic entailment is conservative over classical entailment

@[reducible, inline]

abbrev PLA.InfoState (E : Type u_2) : Type u_2

An information state is a set of (assignment, witness) pairs.

This represents the current state of the discourse: all ways the conversation could be going given what's been said.

Using abbrev makes this a transparent alias so all Set instances apply directly.

Equations

• PLA.InfoState E = Set (PLA.Assignment E × PLA.WitnessSeq E)

def PLA.InfoState.univ {E : Type u_1} : InfoState E

The trivial state: all possibilities

Equations

• PLA.InfoState.univ = Set.univ

def PLA.InfoState.empty {E : Type u_1} : InfoState E

The absurd state: no possibilities

Equations

• PLA.InfoState.empty = ∅

def PLA.InfoState.consistent {E : Type u_1} (s : InfoState E) : Prop

State is consistent (non-empty)

Equations

• s.consistent = Set.Nonempty s

def PLA.InfoState.restrict {E : Type u_1} (s : InfoState E) (M : Model E) (φ : Formula) : InfoState E

Restrict state to pairs where formula is satisfied

Equations

• s.restrict M φ = {p : PLA.Assignment E × PLA.WitnessSeq E | p ∈ s ∧ PLA.Formula.sat M p.1 p.2 φ}

@[reducible, inline]

abbrev PLA.Poss (E : Type u_2) : Type u_2

PLA Possibility type: (assignment, witness sequence) pairs.

This instantiates the generic DynamicSemantics.CCP framework for PLA.

Equations

• PLA.Poss E = (PLA.Assignment E × PLA.WitnessSeq E)

def PLA.possEquivMerged {E : Type u_2} : Poss E ≃ MergedAssignment E

A PLA possibility is a merged assignment (MergedAssignment, the sum-indexed carrier of the Ty2 embedding): mathlib's sum-arrow equivalence, componentwise.

Equations

• PLA.possEquivMerged = (Equiv.sumArrowEquivProdArrow PLA.VarIdx PLA.PronIdx E).symm

@[reducible, inline]

abbrev PLA.Update (E : Type u_2) : Type u_2

An update is a context change potential over PLA possibilities.

Equations

• PLA.Update E = DynamicSemantics.CCP (PLA.Poss E)

def PLA.satisfiesPLA {E : Type u_1} (M : Model E) : Poss E → Formula → Prop

PLA satisfaction relation: possibility satisfies formula.

This bridges PLA to the DynamicSemantics.CCP infrastructure, matching the signature P → φ → Prop expected by DynamicSemantics.updateFromSat.

Equations

• PLA.satisfiesPLA M p φ = PLA.Formula.sat M p.1 p.2 φ

def PLA.Formula.content {E : Type u_1} (M : Model E) (φ : Formula) : InfoState E

The content of a formula: set of (g, ê) pairs where φ is satisfied — the spine's contentOf at satisfiesPLA.

⟦φ⟧^M = { (g, ê) | M, g, ê ⊨ φ }

This is the "static" meaning - what information φ conveys.

Equations

• PLA.Formula.content M φ = DynamicSemantics.contentOf (PLA.satisfiesPLA M) φ

theorem PLA.Formula.mem_content {E : Type u_1} (M : Model E) (φ : Formula) (g : Assignment E) (ê : WitnessSeq E) : (g, ê) ∈ content M φ ↔ sat M g ê φ

theorem PLA.Formula.content_neg {E : Type u_1} (M : Model E) (φ : Formula) : content M (∼φ) = (content M φ)ᶜ

Content of negation is complement

theorem PLA.Formula.content_conj {E : Type u_1} (M : Model E) (φ ψ : Formula) : content M (φ ⋀ ψ) = content M φ ∩ content M ψ

Content of conjunction is intersection

def PLA.Formula.update {E : Type u_1} (M : Model E) (φ : Formula) : Update E

The update of a formula: filter state to satisfying pairs.

⟦φ⟧ : InfoState → InfoState ⟦φ⟧(s) = { (g, ê) ∈ s | M, g, ê ⊨ φ }

Equations

• PLA.Formula.update M φ s = PLA.InfoState.restrict s M φ

theorem PLA.Formula.mem_update {E : Type u_1} (M : Model E) (φ : Formula) (s : InfoState E) (g : Assignment E) (ê : WitnessSeq E) : (g, ê) ∈ update M φ s ↔ (g, ê) ∈ s ∧ sat M g ê φ

theorem PLA.contents_updates_equiv {E : Type u_1} (M : Model E) (φ : Formula) (s : InfoState E) : Formula.update M φ s = s ∩ Formula.content M φ

Observation 16 (Proper Update, [Dek12] §3.2, p.60).

The update of φ is intersection with the content of φ:

⟦φ⟧(s) = s ∩ ⟦φ⟧^M

This shows Contents and Updates are equivalent perspectives.

def PLA.InfoState.supports {E : Type u_1} (M : Model E) (s : InfoState E) (φ : Formula) : Prop

A state supports a formula iff the formula is satisfied throughout the state — the spine's supportOf at satisfiesPLA.

s ⊨ φ iff ∀(g, ê) ∈ s, M, g, ê ⊨ φ

This is the evidential perspective: the speaker's evidence supports φ.

Equations

• PLA.InfoState.supports M s φ = DynamicSemantics.supportOf (PLA.satisfiesPLA M) s φ

def PLA.«term_⊫[_]_» : Lean.TrailingParserDescr

Equations

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

theorem PLA.InfoState.empty_supports {E : Type u_1} (M : Model E) (φ : Formula) : supports M ∅ φ

Empty state supports everything (vacuously)

theorem PLA.InfoState.supports_mono {E : Type u_1} (M : Model E) (s t : InfoState E) (φ : Formula) (h : s ⊆ t) (ht : supports M t φ) : supports M s φ

Support is monotonic: if s ⊆ t and t supports φ, then s supports φ

theorem PLA.InfoState.supports_conj {E : Type u_1} (M : Model E) (s : InfoState E) (φ ψ : Formula) : supports M s (φ ⋀ ψ) ↔ supports M s φ ∧ supports M s ψ

Support and conjunction

theorem PLA.updates_support_equiv {E : Type u_1} (M : Model E) (φ : Formula) (s : InfoState E) : InfoState.supports M s φ ↔ Formula.update M φ s = s

Observation 17 (Proper Support, [Dek12] §3.2, p.61).

A state supports φ iff updating with φ leaves it unchanged:

s ⊫[M] φ ↔ ⟦φ⟧(s) = s

This shows Updates and Support are equivalent perspectives.

def PLA.Formula.dynConj {E : Type u_1} (M : Model E) (φ ψ : Formula) : Update E

Dynamic conjunction: sequential update, φ then ψ.

In this eliminative formalization both conjuncts act as filters, so dynamic conjunction is commutative and reduces to static conjunction (dynConj_static). [Dek12]'s non-commutativity and non-idempotence claims (Observation 9, §2.2, p.32) concern the witness-sequence dynamics, which this formalization does not render: existentials certify witnesses in the membership condition without exporting them to output states.

Equations

• PLA.Formula.dynConj M φ ψ = DynamicSemantics.CCP.seq (PLA.Formula.update M φ) (PLA.Formula.update M ψ)

theorem PLA.Formula.dynConj_eq {E : Type u_1} (M : Model E) (φ ψ : Formula) (s : InfoState E) : dynConj M φ ψ s = update M ψ (update M φ s)

Dynamic conjunction update rule

theorem PLA.Formula.mem_dynConj {E : Type u_1} (M : Model E) (φ ψ : Formula) (s : InfoState E) (g : Assignment E) (ê : WitnessSeq E) : (g, ê) ∈ dynConj M φ ψ s ↔ (g, ê) ∈ s ∧ sat M g ê φ ∧ sat M g ê ψ

Dynamic conjunction membership

theorem PLA.dynConj_static {E : Type u_1} (M : Model E) (φ ψ : Formula) (s : InfoState E) : Formula.dynConj M φ ψ s = Formula.update M (φ ⋀ ψ) s

Dynamic conjunction reduces to static conjunction. [Dek12] restricts this to dref-free formulas; here updates are eliminative, so it holds unconditionally.

theorem PLA.exists_domain_idempotent (x : VarIdx) (φ : Formula) : (Formula.exists_ x φ ⋀ Formula.exists_ x φ).domain = (Formula.exists_ x φ).domain

Existentials are not idempotent ([Dek12] Observation 9, §2.2, p.32).

"A man came. A man sat down." - may be different men. Each ∃x.φ independently chooses a witness.

theorem PLA.dne_syntactic (φ : Formula) : (∼∼φ).domain = φ.domain

DNE failure for dref-introducing formulas (discussed in [Dek12] §2.2, around Observation 9).

"It's not the case that no man came. He sat down." - "He" is problematic. In Dekker's PLA, negation "traps" drefs: ∃x.P(x) introduces a witness to the output state while ¬¬∃x.P(x) only tests existence. In this eliminative formalization both are filters (see update_eliminative), and the contrast survives at the domain/range level. This motivates bilateral semantics (BUS), where DNE holds structurally.

theorem PLA.update_taut {E : Type u_1} (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

theorem PLA.update_contra {E : Type u_1} (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

theorem PLA.update_elim {E : Type u_1} (M : Model E) (s : InfoState E) (φ : Formula) (h : InfoState.supports M s φ) : Formula.update M φ s = s

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

theorem PLA.update_eq_updateFromSat {E : Type u_1} (M : Model E) (φ : Formula) (s : InfoState E) : Formula.update M φ s = DynamicSemantics.updateFromSat (satisfiesPLA M) φ s

PLA formula update equals DynamicSemantics.updateFromSat via satisfiesPLA.

theorem PLA.update_eliminative {E : Type u_1} (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 DynamicSemantics.updateFromSat_eliminative.

theorem PLA.update_isEliminative {E : Type u_1} (M : Model E) (φ : Formula) : DynamicSemantics.CCP.IsEliminative (Formula.update M φ)

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

theorem PLA.update_monotone {E : Type u_1} (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 DynamicSemantics.updateFromSat_monotone.

theorem PLA.support_downward_closed {E : Type u_1} (M : Model E) (φ : Formula) (s t : InfoState E) (h : t ⊆ s) (hs : InfoState.supports M s φ) : InfoState.supports M t φ

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

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

theorem PLA.support_inter {E : Type u_1} (M : Model E) (φ : Formula) (s t : InfoState E) (hs : InfoState.supports M s φ) (_ht : InfoState.supports M t φ) : InfoState.supports M (s ∩ t) φ

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

theorem PLA.support_union_iff {E : Type u_1} (M : Model E) (φ : Formula) (s t : InfoState E) : InfoState.supports M (s ∪ t) φ ↔ InfoState.supports M s φ ∧ InfoState.supports M t φ

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

theorem PLA.update_inter {E : Type u_1} (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)

theorem PLA.dynConj_subset_inter {E : Type u_1} (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.

theorem PLA.static_seq_is_intersection {E : Type u_1} (M : Model E) (φ ψ : Formula) (s : InfoState E) : DynamicSemantics.CCP.seq (Formula.update M φ) (Formula.update M ψ) s = s ∩ Formula.content M φ ∩ Formula.content M ψ

Sequential composition is nested intersection of contents.

theorem PLA.dynamicity_source_exists (x : VarIdx) (φ : Formula) : x ∈ (Formula.exists_ x φ).domain

Only ∃ introduces discourse referents.

theorem PLA.dynamicity_source_neg (φ : Formula) : (∼φ).domain = φ.domain

theorem PLA.dynamicity_source_conj (φ ψ : Formula) : (φ ⋀ ψ).domain = φ.domain ∪ ψ.domain

theorem PLA.dynamicity_source_atom (name : String) (ts : List Term) : (Formula.atom name ts).domain = ∅

theorem PLA.domain_empty_iff_no_exists (φ : Formula) : φ.domain = ∅ ↔ ∀ (x : VarIdx), x ∉ φ.domain

Domain empty iff no variables bound.

theorem PLA.same_content_same_update {E : Type u_1} (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.

def PLA.dynamicEntails {E : Type u_1} (M : Model E) (φ ψ : Formula) : Prop

Dynamic entailment: φ dynamically entails ψ if updating with φ always yields a state that supports ψ — the spine's dynamicEntailsOf at satisfiesPLA.

Equations

• PLA.dynamicEntails M φ ψ = DynamicSemantics.dynamicEntailsOf (PLA.satisfiesPLA M) φ ψ

def PLA.«term_⊨[_]_dyn_» : Lean.TrailingParserDescr

Equations

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

theorem PLA.dynamicEntails_refl {E : Type u_1} (M : Model E) (φ : Formula) : dynamicEntails M φ φ

Reflexivity of dynamic entailment: φ ⊨_dyn φ.

Updating with φ yields a state that supports φ.

theorem PLA.dynamicEntails_trans {E : Type u_1} (M : Model E) (φ ψ χ : Formula) (h1 : dynamicEntails M φ ψ) (h2 : dynamicEntails M ψ χ) : dynamicEntails M φ χ

Transitivity of dynamic entailment; holds because update is eliminative.

theorem PLA.dynamicEntails_weakening {E : Type u_1} (M : Model E) (φ ψ : Formula) (s : InfoState E) (hent : dynamicEntails M φ ψ) : InfoState.supports M (Formula.update M φ s) ψ

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

theorem PLA.obs10_dynamic_eq_classical_entailment {E : Type u_1} (M : Model E) (φ ψ : Formula) : dynamicEntails M φ ψ ↔ ∀ (g : Assignment E) (ê : WitnessSeq E), Formula.sat M g ê φ → Formula.sat M g ê ψ

Observation 10 ([Dek12] §2.3, p.33): Conservative Entailment.

Dynamic entailment coincides with classical pointwise entailment: φ ⊨_dyn ψ iff for all g, ê, M,g,ê ⊨ φ implies M,g,ê ⊨ ψ.

This shows that PLA's dynamic consequence relation is conservative over classical PL consequence.

theorem PLA.obs11_deduction_theorem {E : Type u_1} (M : Model E) (φ χ ψ : Formula) : dynamicEntails M (φ ⋀ χ) ψ ↔ dynamicEntails M φ (χ.impl ψ)

Observation 11 ([Dek12] §2.3, p.34): Deduction Theorem.

φ ∧ χ ⊨_dyn ψ ↔ φ ⊨_dyn χ → ψ

The classical deduction theorem holds in PLA's dynamic system.

Update-composition and domain API

Membership characterizations for sequenced updates, and structural facts about Formula.domain / Formula.range under negation and existentials. Note the eliminative character these make explicit: updates only filter the input state (update_eliminative), so an existential's witness values figure in the membership condition, not in the surviving possibilities.

theorem PLA.exists_update_characterization {E : Type u_1} (M : Model E) (x : VarIdx) (φ : Formula) (s : InfoState E) : Formula.update M (Formula.exists_ x φ) s = {p : Assignment E × WitnessSeq E | p ∈ s ∧ ∃ (e : E), Formula.sat M (Function.update p.1 x e) p.2 φ}

Existential update output characterization.

theorem PLA.dne_range_same (φ : Formula) : (∼∼φ).range = φ.range

Double negation preserves range.

theorem PLA.exists_domain_nonempty (x : VarIdx) (φ : Formula) : (Formula.exists_ x φ).domain.Nonempty

Existential domain is nonempty.

theorem PLA.seq_update_eq {E : Type u_1} (M : Model E) (φ ψ : Formula) (s : InfoState E) : DynamicSemantics.CCP.seq (Formula.update M φ) (Formula.update M ψ) s = {p : Assignment E × WitnessSeq E | p ∈ s ∧ Formula.sat M p.1 p.2 φ ∧ Formula.sat M p.1 p.2 ψ}

Sequential update as set comprehension.

theorem PLA.static_conjunction_commutes {E : Type u_1} (M : Model E) (φ ψ : Formula) (s : InfoState E) : DynamicSemantics.CCP.seq (Formula.update M φ) (Formula.update M ψ) s = DynamicSemantics.CCP.seq (Formula.update M ψ) (Formula.update M φ) s

Sequential update commutes: eliminative updates are filters, so order is irrelevant. ([Dek12] restricts this to dref-free formulas.)

theorem PLA.static_existential_local_scope (x : VarIdx) (φ ψ : Formula) : x ∈ (Formula.exists_ x φ).domain ∧ (Formula.exists_ x φ ⋀ ψ).domain = (Formula.exists_ x φ).domain ∪ ψ.domain

The existential marks its variable in the domain; conjunction unions domains, leaving the second conjunct's domain unaffected.