Bilateral Update Semantics

[ES25a], [KM95]

Bilateral Update Semantics (BUS, [ES25a]'s formulation, with [KM95]'s bilateral DRT as ancestor): update semantics where each sentence carries a positive and a negative update dimension, validating Double Negation Elimination (negation swaps the dimensions) and cross-disjunct anaphora.

States are Heimian (the paper's Def. 3.1): sets of world-assignment pairs whose assignments are Part E-valued — ⊥ is the paper's ∗, so definedness is per-possibility and non-uniform. This is strictly more expressive than the indexed State of State.lean: a uniform base cannot represent partially familiar states, on which the paper's separation of assertability (54) from Heimian familiarity rests.

Main definitions

• subsistence (Def. 3.3, after [GSV96]), rendered as the lower closure: membership for points, ≤ of closures for states.
• State.Familiar: familiarity (Def. 3.2) — defined at every possibility, values free; worldly information (Def. 3.1's 𝒲) is the image Possibility.world '' s.
• randomAssign: the paper's s[εₓ] (43); novelty is not encoded.
• BilateralDen with atom, pred1, pred2, neg (~), conj (⊙, (61)), disj (⊕, (64)), exists_ ((44)–(45)), forall_.
• unknownUpdate (s[φ]?, (53)) and assertable ((54)).
• supports, entails (⊨ᵇ): subsistence-based support.

Main results

• neg_neg: DNE is definitional.
• partition, partition_assertable: every possibility subsists positively, subsists negatively, or is unknown.
• de_morgan_disj, de_morgan_conj: de Morgan's laws, unlike in standard dynamic semantics. (Descendance, subsistence, State.Familiar, and random assignment now live at the root, in State.lean — this file's vocabulary became the module's.)
• egli: Egli's theorem for the positive dimension, definitionally.
• isBilateral: the update algebra is a bilateral logic in the sense of Core.Logic.Bilateral.

Implementation notes

Descent requires the larger point to extend the assignment, per [GSV96]; [ES25a]'s Def. 3.3 phrases the clause as domain inclusion, and their examples do not discriminate. The paper overloads ≺ for possibility-in-state and state-in-state subsistence (their fn. on (73)); here both are the lower closure — membership for points, ≤ of closures for states.

The empirical comparison against full ICDRT is in Studies/Hofmann2025.lean; against PLA in Studies/Dekker2012.lean.

Bilateral denotations

structure DynamicSemantics.BilateralDen (W : Type u_4) (V : Type u_5) (E : Type u_6) : Type (max (max u_4 u_5) u_6)

A bilateral denotation: a positive dimension s[φ]⁺ (what survives assertion) and a negative dimension s[φ]⁻ (what survives denial). Standard dynamic semantics has only the former; the latter is what makes DNE and cross-disjunct anaphora work.

• positive : Set (Possibility W V (Part E)) → Set (Possibility W V (Part E))

  Positive update: the result of asserting the sentence.

• negative : Set (Possibility W V (Part E)) → Set (Possibility W V (Part E))

  Negative update: the result of denying the sentence.

theorem DynamicSemantics.BilateralDen.ext_iff {W : Type u_4} {V : Type u_5} {E : Type u_6} {x y : BilateralDen W V E} : x = y ↔ x.positive = y.positive ∧ x.negative = y.negative

theorem DynamicSemantics.BilateralDen.ext {W : Type u_4} {V : Type u_5} {E : Type u_6} {x y : BilateralDen W V E} (positive : x.positive = y.positive) (negative : x.negative = y.negative) : x = y

def DynamicSemantics.BilateralDen.atom {W : Type u_1} {V : Type u_2} {E : Type u_3} (pred : W → Prop) : BilateralDen W V E

Worldly atom: keep the possibilities where the proposition holds (positively) or fails (negatively).

Equations

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

def DynamicSemantics.BilateralDen.pred1 {W : Type u_1} {V : Type u_2} {E : Type u_3} (P : E → W → Prop) (t : V) : BilateralDen W V E

Unary atomic predication at t. Atoms are partial: a possibility where t is undefined survives in neither dimension ([ES25a]'s definedness clause for atomic sentences).

Equations

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

def DynamicSemantics.BilateralDen.pred2 {W : Type u_1} {V : Type u_2} {E : Type u_3} (P : E → E → W → Prop) (t₁ t₂ : V) : BilateralDen W V E

Binary atomic predication at t₁, t₂; partial like pred1.

Equations

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

def DynamicSemantics.BilateralDen.neg {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ : BilateralDen W V E) : BilateralDen W V E

Negation swaps the dimensions: s[¬φ]⁺ = s[φ]⁻ and s[¬φ]⁻ = s[φ]⁺. Negation does not "push in" — this is the key insight of bilateralism.

Equations

• ~φ = { positive := φ.negative, negative := φ.positive }

def DynamicSemantics.BilateralDen.«term~_» : Lean.ParserDescr

Negation swaps the dimensions: s[¬φ]⁺ = s[φ]⁻ and s[¬φ]⁻ = s[φ]⁺. Negation does not "push in" — this is the key insight of bilateralism.

Equations

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

@[simp]

theorem DynamicSemantics.BilateralDen.neg_neg {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ : BilateralDen W V E) : ~~φ = φ

Double negation is the identity, definitionally.

theorem DynamicSemantics.BilateralDen.dne_positive {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ : BilateralDen W V E) (s : Set (Possibility W V (Part E))) : (~~φ).positive s = φ.positive s

theorem DynamicSemantics.BilateralDen.dne_negative {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ : BilateralDen W V E) (s : Set (Possibility W V (Part E))) : (~~φ).negative s = φ.negative s

theorem DynamicSemantics.BilateralDen.neg_involutive {W : Type u_1} {V : Type u_2} {E : Type u_3} : Function.Involutive neg

The unknown update and assertability

def DynamicSemantics.BilateralDen.unknownUpdate {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ : BilateralDen W V E) (s : Set (Possibility W V (Part E))) : Set (Possibility W V (Part E))

The unknown update s[φ]? ([ES25a], (53)): the possibilities of s that subsist in neither dimension — the dynamic analogue of the third Strong Kleene truth value.

Equations

• φ.unknownUpdate s = {p : DynamicSemantics.Possibility W V (Part E) | p ∈ s ∧ p ∉ lowerClosure (φ.positive s) ∧ p ∉ lowerClosure (φ.negative s)}

def DynamicSemantics.BilateralDen.assertable {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ : BilateralDen W V E) (c : Set (Possibility W V (Part E))) : Prop

Assertability ([ES25a], (54)): the unknown update is empty — every possibility is accounted for by one of the dimensions. Strictly weaker than Heimian familiarity.

Equations

• φ.assertable c = (φ.unknownUpdate c = ∅)

theorem DynamicSemantics.BilateralDen.unknownUpdate_neg {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ : BilateralDen W V E) (s : Set (Possibility W V (Part E))) : (~φ).unknownUpdate s = φ.unknownUpdate s

The unknown update is invariant under negation.

theorem DynamicSemantics.BilateralDen.unknownUpdate_atom {W : Type u_1} {V : Type u_2} {E : Type u_3} (pred : W → Prop) (s : Set (Possibility W V (Part E))) : (atom pred).unknownUpdate s = ∅

Worldly atoms never gap.

theorem DynamicSemantics.BilateralDen.partition {W : Type u_1} {V : Type u_2} {E : Type u_3} {s : Set (Possibility W V (Part E))} {p : Possibility W V (Part E)} (φ : BilateralDen W V E) (hp : p ∈ s) : p ∈ lowerClosure (φ.positive s) ∨ p ∈ lowerClosure (φ.negative s) ∨ p ∈ φ.unknownUpdate s

Every possibility subsists positively, subsists negatively, or is unknown.

theorem DynamicSemantics.BilateralDen.partition_assertable {W : Type u_1} {V : Type u_2} {E : Type u_3} {φ : BilateralDen W V E} {s : Set (Possibility W V (Part E))} {p : Possibility W V (Part E)} (h : φ.assertable s) (hp : p ∈ s) : p ∈ lowerClosure (φ.positive s) ∨ p ∈ lowerClosure (φ.negative s)

Under assertability, every possibility subsists in one of the dimensions.

Connectives

def DynamicSemantics.BilateralDen.conj {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ ψ : BilateralDen W V E) : BilateralDen W V E

Conjunction ([ES25a], (61)): the positive update sequences the positive dimensions (the one verifying Strong Kleene cell); the negative update is the union of the dynamic falsifications, one per falsifying cell.

Equations

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

def DynamicSemantics.BilateralDen.«term_⊙_» : Lean.TrailingParserDescr

Conjunction ([ES25a], (61)): the positive update sequences the positive dimensions (the one verifying Strong Kleene cell); the negative update is the union of the dynamic falsifications, one per falsifying cell.

Equations

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

def DynamicSemantics.BilateralDen.disj {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ ψ : BilateralDen W V E) : BilateralDen W V E

Disjunction ([ES25a], (64)): verification via the first disjunct (the s[φ]⁺ row) or via the second (the [ψ]⁺ column); denial is sequential. The state-passing ψ.positive (φ.negative s) term is what makes bathroom disjunctions work: by DNE, s[¬∃xP(x)]⁻ = s[∃xP(x)]⁺ introduces the referent for the second disjunct.

Equations

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

def DynamicSemantics.BilateralDen.«term_⊕_» : Lean.TrailingParserDescr

Disjunction ([ES25a], (64)): verification via the first disjunct (the s[φ]⁺ row) or via the second (the [ψ]⁺ column); denial is sequential. The state-passing ψ.positive (φ.negative s) term is what makes bathroom disjunctions work: by DNE, s[¬∃xP(x)]⁻ = s[∃xP(x)]⁺ introduces the referent for the second disjunct.

Equations

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

theorem DynamicSemantics.BilateralDen.conj_assoc_positive {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ ψ χ : BilateralDen W V E) (s : Set (Possibility W V (Part E))) : (φ ⊙ ψ ⊙ χ).positive s = (φ ⊙ (ψ ⊙ χ)).positive s

Conjunction associates in the positive dimension.

theorem DynamicSemantics.BilateralDen.de_morgan_disj {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ ψ : BilateralDen W V E) (s : Set (Possibility W V (Part E))) : (~(φ ⊕ ψ)).positive s = (~φ ⊙ ~ψ).positive s

De Morgan: ¬(φ ∨ ψ) and ¬φ ∧ ¬ψ agree positively, definitionally.

theorem DynamicSemantics.BilateralDen.de_morgan_conj {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ ψ : BilateralDen W V E) (s : Set (Possibility W V (Part E))) : (~(φ ⊙ ψ)).positive s = (~φ ⊕ ~ψ).positive s

De Morgan: ¬(φ ∧ ψ) and ¬φ ∨ ¬ψ agree positively.

Quantifiers

def DynamicSemantics.BilateralDen.exists_ {W : Type u_1} {V : Type u_2} {E : Type u_3} [DecidableEq V] (x : V) (φ : BilateralDen W V E) : BilateralDen W V E

Existential quantification ([ES25a], (44)–(45)): the positive update introduces the referent by random assignment and asserts the scope; the negative update merely removes possibilities — it retains those of s whose world falsifies the existential classically, and introduces no anaphoric information.

Equations

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

def DynamicSemantics.BilateralDen.forall_ {W : Type u_1} {V : Type u_2} {E : Type u_3} [DecidableEq V] (x : V) (φ : BilateralDen W V E) : BilateralDen W V E

Universal quantification, by de Morgan duality: ∀x φ = ¬∃x ¬φ.

Equations

• DynamicSemantics.BilateralDen.forall_ x φ = ~(DynamicSemantics.BilateralDen.exists_ x ~φ)

theorem DynamicSemantics.BilateralDen.egli {W : Type u_1} {V : Type u_2} {E : Type u_3} [DecidableEq V] (x : V) (φ ψ : BilateralDen W V E) (s : Set (Possibility W V (Part E))) : (exists_ x φ ⊙ ψ).positive s = (exists_ x (φ ⊙ ψ)).positive s

Egli's theorem, definitionally: an existential scoping over a conjunction binds into the second conjunct, (∃x φ) ∧ ψ = ∃x (φ ∧ ψ) in the positive dimension — the key property for cross-sentential anaphora.

Support and entailment

def DynamicSemantics.BilateralDen.supports {W : Type u_1} {V : Type u_2} {E : Type u_3} (s : Set (Possibility W V (Part E))) (φ : BilateralDen W V E) : Prop

Bilateral support: the positive update is consistent and the state subsists in it.

Equations

• DynamicSemantics.BilateralDen.supports s φ = ((φ.positive s).Nonempty ∧ lowerClosure s ≤ lowerClosure (φ.positive s))

def DynamicSemantics.BilateralDen.entails {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ ψ : BilateralDen W V E) : Prop

Bilateral entailment: every consistent positive update of φ supports ψ.

Equations

• (φ ⊨ᵇ ψ) = ∀ (s : Set (DynamicSemantics.Possibility W V (Part E))), (φ.positive s).Nonempty → DynamicSemantics.BilateralDen.supports (φ.positive s) ψ

def DynamicSemantics.BilateralDen.«term_⊨ᵇ_» : Lean.TrailingParserDescr

Bilateral entailment: every consistent positive update of φ supports ψ.

Equations

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

Structural lemmas

theorem DynamicSemantics.BilateralDen.atom_complementary {W : Type u_1} {V : Type u_2} {E : Type u_3} (pred : W → Prop) (s : Set (Possibility W V (Part E))) : (atom pred).positive s ∪ (atom pred).negative s = s

theorem DynamicSemantics.BilateralDen.atom_disjoint {W : Type u_1} {V : Type u_2} {E : Type u_3} (pred : W → Prop) (s : Set (Possibility W V (Part E))) : (atom pred).positive s ∩ (atom pred).negative s = ∅

theorem DynamicSemantics.BilateralDen.atom_positive_monotone {W : Type u_1} {V : Type u_2} {E : Type u_3} (pred : W → Prop) : Monotone (atom pred).positive

theorem DynamicSemantics.BilateralDen.atom_negative_monotone {W : Type u_1} {V : Type u_2} {E : Type u_3} (pred : W → Prop) : Monotone (atom pred).negative

theorem DynamicSemantics.BilateralDen.atom_positive_eliminative {W : Type u_1} {V : Type u_2} {E : Type u_3} (pred : W → Prop) : CCP.IsEliminative (atom pred).positive

theorem DynamicSemantics.BilateralDen.atom_negative_eliminative {W : Type u_1} {V : Type u_2} {E : Type u_3} (pred : W → Prop) : CCP.IsEliminative (atom pred).negative

theorem DynamicSemantics.BilateralDen.pred1_positive_monotone {W : Type u_1} {V : Type u_2} {E : Type u_3} (P : E → W → Prop) (t : V) : Monotone (pred1 P t).positive

theorem DynamicSemantics.BilateralDen.pred1_negative_monotone {W : Type u_1} {V : Type u_2} {E : Type u_3} (P : E → W → Prop) (t : V) : Monotone (pred1 P t).negative

theorem DynamicSemantics.BilateralDen.pred1_positive_eliminative {W : Type u_1} {V : Type u_2} {E : Type u_3} (P : E → W → Prop) (t : V) : CCP.IsEliminative (pred1 P t).positive

theorem DynamicSemantics.BilateralDen.pred1_negative_eliminative {W : Type u_1} {V : Type u_2} {E : Type u_3} (P : E → W → Prop) (t : V) : CCP.IsEliminative (pred1 P t).negative

theorem DynamicSemantics.BilateralDen.pred2_positive_eliminative {W : Type u_1} {V : Type u_2} {E : Type u_3} (P : E → E → W → Prop) (t₁ t₂ : V) : CCP.IsEliminative (pred2 P t₁ t₂).positive

theorem DynamicSemantics.BilateralDen.pred2_negative_eliminative {W : Type u_1} {V : Type u_2} {E : Type u_3} (P : E → E → W → Prop) (t₁ t₂ : V) : CCP.IsEliminative (pred2 P t₁ t₂).negative

The bilateral algebra

def DynamicSemantics.BilateralDen.toPair {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ : BilateralDen W V E) : (Set (Possibility W V (Part E)) → Set (Possibility W V (Part E))) × (Set (Possibility W V (Part E)) → Set (Possibility W V (Part E)))

View a bilateral denotation as a pair of updates.

Equations

• φ.toPair = (φ.positive, φ.negative)

def DynamicSemantics.BilateralDen.ofPair {W : Type u_1} {V : Type u_2} {E : Type u_3} (u : (Set (Possibility W V (Part E)) → Set (Possibility W V (Part E))) × (Set (Possibility W V (Part E)) → Set (Possibility W V (Part E)))) : BilateralDen W V E

Construct a bilateral denotation from a pair of updates.

Equations

• DynamicSemantics.BilateralDen.ofPair u = { positive := u.1, negative := u.2 }

theorem DynamicSemantics.BilateralDen.toPair_ofPair {W : Type u_1} {V : Type u_2} {E : Type u_3} (u : (Set (Possibility W V (Part E)) → Set (Possibility W V (Part E))) × (Set (Possibility W V (Part E)) → Set (Possibility W V (Part E)))) : (ofPair u).toPair = u

theorem DynamicSemantics.BilateralDen.ofPair_toPair {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ : BilateralDen W V E) : ofPair φ.toPair = φ

theorem DynamicSemantics.BilateralDen.neg_eq_swap {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ : BilateralDen W V E) : (~φ).toPair = φ.toPair.swap

Negation is the swap on pairs; DNE is swap ∘ swap = id.

@[implicit_reducible]

instance DynamicSemantics.BilateralDen.instInvolutiveNeg {W : Type u_1} {V : Type u_2} {E : Type u_3} : InvolutiveNeg (BilateralDen W V E)

Equations

• DynamicSemantics.BilateralDen.instInvolutiveNeg = { neg := DynamicSemantics.BilateralDen.neg, neg_neg := ⋯ }

theorem DynamicSemantics.BilateralDen.isBilateral {W : Type u_1} {V : Type u_2} {E : Type u_3} : Core.Logic.Bilateral.IsBilateral (fun (x : BilateralDen W V E) => x.positive) (fun (x : BilateralDen W V E) => x.negative) neg

BUS is a paraconsistent bilateral logic (Core.Logic.Bilateral): the denotation is the formula, the dimensions are the projections, and neg swaps them by definition.

@[implicit_reducible]

instance DynamicSemantics.BilateralDen.instPartialOrder {W : Type u_1} {V : Type u_2} {E : Type u_3} : PartialOrder (BilateralDen W V E)

The pointwise order: both dimensions componentwise.

Equations

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

theorem DynamicSemantics.BilateralDen.neg_monotone {W : Type u_1} {V : Type u_2} {E : Type u_3} : Monotone neg

Negation is monotone: the swap rearranges the componentwise checks.

theorem DynamicSemantics.BilateralDen.neg_le_neg_iff {W : Type u_1} {V : Type u_2} {E : Type u_3} {φ ψ : BilateralDen W V E} : ~φ ≤ ~ψ ↔ φ ≤ ψ

Negation preserves and reflects the order.