Bilateral Update Semantics

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 partial (Flat E-valued), the carrier of State.lean's information states. ⊥ is the paper's ∗, so definedness is per-possibility and need not be uniform, which the paper's separation of assertability (54) from Heimian familiarity needs. Subsistence (Def. 3.3, after [GSV96]), familiarity (Def. 3.2) and random assignment (43) are State.lean's.

Main definitions

• 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.
• egli: Egli's theorem for the positive dimension, definitionally.

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.

References

• P. D. Elliott and Y. Sudo, Free choice with anaphora (2025)
• E. Krahmer and R. Muskens, Negation and disjunction in discourse representation theory (1995)
• J. Groenendijk, M. Stokhof and F. Veltman, Coreference and modality (1996)

Bilateral denotations

structure 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 (DynamicSemantics.Possibility W V (Flat E)) → Set (DynamicSemantics.Possibility W V (Flat E))

  Positive update: the result of asserting the sentence.

• negative : Set (DynamicSemantics.Possibility W V (Flat E)) → Set (DynamicSemantics.Possibility W V (Flat E))

  Negative update: the result of denying the sentence.

theorem 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 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 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 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 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 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

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

def 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

• BilateralDen.«term~_» = Lean.ParserDescr.node `BilateralDen.«term~_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 1024))

@[simp]

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

Double negation is the identity, definitionally.

@[instance_reducible]

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

Equations

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

The unknown update and assertability

def BilateralDen.unknownUpdate {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ : BilateralDen W V E) (s : Set (DynamicSemantics.Possibility W V (Flat E))) : Set (DynamicSemantics.Possibility W V (Flat 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 (Flat E) | p ∈ s ∧ p ∉ lowerClosure (φ.positive s) ∧ p ∉ lowerClosure (φ.negative s)}

def BilateralDen.assertable {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ : BilateralDen W V E) (c : Set (DynamicSemantics.Possibility W V (Flat 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 BilateralDen.unknownUpdate_neg {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ : BilateralDen W V E) (s : Set (DynamicSemantics.Possibility W V (Flat E))) : φ.neg.unknownUpdate s = φ.unknownUpdate s

The unknown update is invariant under negation.

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

Worldly atoms never gap.

theorem BilateralDen.partition {W : Type u_1} {V : Type u_2} {E : Type u_3} {s : Set (DynamicSemantics.Possibility W V (Flat E))} {p : DynamicSemantics.Possibility W V (Flat 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 BilateralDen.partition_assertable {W : Type u_1} {V : Type u_2} {E : Type u_3} {φ : BilateralDen W V E} {s : Set (DynamicSemantics.Possibility W V (Flat E))} {p : DynamicSemantics.Possibility W V (Flat 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 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 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

• BilateralDen.«term_⊙_» = Lean.ParserDescr.trailingNode `BilateralDen.«term_⊙_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊙ ") (Lean.ParserDescr.cat `term 66))

def 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 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

• BilateralDen.«term_⊕_» = Lean.ParserDescr.trailingNode `BilateralDen.«term_⊕_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ ") (Lean.ParserDescr.cat `term 61))

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

Conjunction associates in the positive dimension.

theorem BilateralDen.de_morgan_disj {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ ψ : BilateralDen W V E) (s : Set (DynamicSemantics.Possibility W V (Flat E))) : (φ.disj ψ).neg.positive s = (φ.neg.conj ψ.neg).positive s

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

theorem BilateralDen.de_morgan_conj {W : Type u_1} {V : Type u_2} {E : Type u_3} (φ ψ : BilateralDen W V E) (s : Set (DynamicSemantics.Possibility W V (Flat E))) : (φ.conj ψ).neg.positive s = (φ.neg.disj ψ.neg).positive s

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

Quantifiers

def 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 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

• BilateralDen.forall_ x φ = (BilateralDen.exists_ x φ.neg).neg

theorem BilateralDen.egli {W : Type u_1} {V : Type u_2} {E : Type u_3} [DecidableEq V] (x : V) (φ ψ : BilateralDen W V E) (s : Set (DynamicSemantics.Possibility W V (Flat E))) : ((exists_ x φ).conj ψ).positive s = (exists_ x (φ.conj ψ)).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 BilateralDen.supports {W : Type u_1} {V : Type u_2} {E : Type u_3} (s : Set (DynamicSemantics.Possibility W V (Flat E))) (φ : BilateralDen W V E) : Prop

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

Equations

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

def 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

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

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

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

Equations

• BilateralDen.«term_⊨ᵇ_» = Lean.ParserDescr.trailingNode `BilateralDen.«term_⊨ᵇ_» 50 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊨ᵇ ") (Lean.ParserDescr.cat `term 0))

Structural lemmas

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

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

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

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

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

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

theorem 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 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 BilateralDen.pred1_positive_eliminative {W : Type u_1} {V : Type u_2} {E : Type u_3} (P : E → W → Prop) (t : V) : DynamicSemantics.CCP.IsEliminative (pred1 P t).positive

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

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

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