structure Semantics.Dynamic.Core.BilateralDen (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A bilateral denotation: positive and negative update functions.

In bilateral semantics, a sentence φ denotes a pair of update functions:

• positive: s[φ]⁺ - the result of asserting φ in state s
• negative: s[φ]⁻ - the result of denying φ in state s

Standard dynamic semantics only has positive updates. The negative dimension is what enables DNE and proper treatment of cross-disjunct anaphora.

• positive : InfoState W E → InfoState W E

  Positive update: result of asserting the sentence

• negative : InfoState W E → InfoState W E

  Negative update: result of denying the sentence

theorem Semantics.Dynamic.Core.BilateralDen.ext {W : Type u_1} {E : Type u_2} {φ ψ : BilateralDen W E} (hp : φ.positive = ψ.positive) (hn : φ.negative = ψ.negative) : φ = ψ

theorem Semantics.Dynamic.Core.BilateralDen.ext_iff {W : Type u_1} {E : Type u_2} {φ ψ : BilateralDen W E} : φ = ψ ↔ φ.positive = ψ.positive ∧ φ.negative = ψ.negative

def Semantics.Dynamic.Core.BilateralDen.atom {W : Type u_1} {E : Type u_2} (pred : W → Bool) : BilateralDen W E

Atomic proposition: lift a classical proposition to bilateral form.

For an atomic proposition p:

• s[p]⁺ = { w ∈ s | p(w) } (keep worlds where p holds)
• s[p]⁻ = { w ∈ s | ¬p(w) } (keep worlds where p fails)

Equations

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

theorem Semantics.Dynamic.Core.BilateralDen.atom_complementary {W : Type u_1} {E : Type u_2} (pred : W → Bool) (s : InfoState W E) : (atom pred).positive s ∪ (atom pred).negative s = s

Atomic positive and negative are complementary

theorem Semantics.Dynamic.Core.BilateralDen.atom_disjoint {W : Type u_1} {E : Type u_2} (pred : W → Bool) (s : InfoState W E) : (atom pred).positive s ∩ (atom pred).negative s = ∅

Atomic positive and negative are disjoint

theorem Semantics.Dynamic.Core.BilateralDen.atom_positive_monotone {W : Type u_1} {E : Type u_2} (pred : W → Bool) : Monotone (atom pred).positive

Atomic positive update is monotone.

theorem Semantics.Dynamic.Core.BilateralDen.atom_negative_monotone {W : Type u_1} {E : Type u_2} (pred : W → Bool) : Monotone (atom pred).negative

Atomic negative update is monotone.

theorem Semantics.Dynamic.Core.BilateralDen.atom_positive_eliminative {W : Type u_1} {E : Type u_2} (pred : W → Bool) : IsEliminative (atom pred).positive

Atomic positive update is eliminative.

theorem Semantics.Dynamic.Core.BilateralDen.atom_negative_eliminative {W : Type u_1} {E : Type u_2} (pred : W → Bool) : IsEliminative (atom pred).negative

Atomic negative update is eliminative.

def Semantics.Dynamic.Core.BilateralDen.neg {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) : BilateralDen W E

Negation: swap positive and negative updates.

This is the key insight of bilateral semantics. Negation doesn't "push in" - it simply swaps which update is positive and which is negative.

s[¬φ]⁺ = s[φ]⁻ s[¬φ]⁻ = s[φ]⁺

Equations

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

def Semantics.Dynamic.Core.BilateralDen.«term~_» : Lean.ParserDescr

Notation for negation

Equations

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

@[simp]

theorem Semantics.Dynamic.Core.BilateralDen.neg_neg {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) : ~~φ = φ

Double negation is identity (DNE).

theorem Semantics.Dynamic.Core.BilateralDen.dne_positive {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) (s : InfoState W E) : (~~φ).positive s = φ.positive s

DNE for positive updates

theorem Semantics.Dynamic.Core.BilateralDen.dne_negative {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) (s : InfoState W E) : (~~φ).negative s = φ.negative s

DNE for negative updates

theorem Semantics.Dynamic.Core.BilateralDen.neg_involutive {W : Type u_1} {E : Type u_2} : Function.Involutive neg

Negation is involutive

def Semantics.Dynamic.Core.BilateralDen.unknownUpdate {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) (s : InfoState W E) : InfoState W E

Unknown update: possibilities in s that subsist in neither the positive nor the negative update.

This is the dynamic analog of the third truth value (#) in Strong Kleene logic. For atomic propositions, the unknown update is always empty. For existential statements, it captures possibilities where variable definedness introduces a gap.

Equation (53) of @cite{elliott-sudo-2025}.

Equations

• φ.unknownUpdate s = {p : Semantics.Dynamic.Core.Possibility W E | p ∈ s ∧ ¬p ∈ φ.positive s ∧ ¬p ∈ φ.negative s}

theorem Semantics.Dynamic.Core.BilateralDen.unknownUpdate_neg {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) (s : InfoState W E) : (~φ).unknownUpdate s = φ.unknownUpdate s

The unknown update of a negation equals the unknown update of the original.

theorem Semantics.Dynamic.Core.BilateralDen.unknownUpdate_atom {W : Type u_1} {E : Type u_2} (pred : W → Bool) (s : InfoState W E) : (atom pred).unknownUpdate s = ∅

For atomic propositions, the unknown update is empty.

def Semantics.Dynamic.Core.BilateralDen.assertable {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) (c : InfoState W E) : Prop

Assertability condition: φ is assertable at context c iff the unknown update is empty — every possibility is accounted for by either the positive or negative update.

Definition (54) of @cite{elliott-sudo-2025}.

Equations

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

theorem Semantics.Dynamic.Core.BilateralDen.partition {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) (s : InfoState W E) : s ⊆ φ.positive s ∪ φ.negative s ∪ φ.unknownUpdate s

Every possibility in s is either verified, falsified, or unknown. This is the partition property of the Strong Kleene truth table.

theorem Semantics.Dynamic.Core.BilateralDen.partition_assertable {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) (s : InfoState W E) (h : φ.assertable s) : s ⊆ φ.positive s ∪ φ.negative s

Assertability implies the positive and negative updates cover the state.

def Semantics.Dynamic.Core.BilateralDen.conj {W : Type u_1} {E : Type u_2} (φ ψ : BilateralDen W E) : BilateralDen W E

Conjunction: sequence positive updates, combine negative updates following the Strong Kleene truth table.

For conjunction φ ∧ ψ:

• s[φ ∧ ψ]⁺ = s[φ]⁺[ψ]⁺ (the (1,1) cell: both verified)
• s[φ ∧ ψ]⁻ = s[φ]⁻ (the (0,*) row: φ falsified) ∪ s[φ]⁺[ψ]⁻ (the (1,0) cell: φ verified, ψ falsified) ∪ s[φ]?[ψ]⁻ (the (#,0) cell: φ unknown, ψ falsified)

Equation (61) of @cite{elliott-sudo-2025}.

Equations

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

def Semantics.Dynamic.Core.BilateralDen.«term_⊙_» : Lean.TrailingParserDescr

Notation for conjunction

Equations

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

theorem Semantics.Dynamic.Core.BilateralDen.conj_assoc_positive {W : Type u_1} {E : Type u_2} (φ ψ χ : BilateralDen W E) (s : InfoState W E) : (φ ⊙ ψ ⊙ χ).positive s = (φ ⊙ (ψ ⊙ χ)).positive s

Conjunction associates (for positive updates)

def Semantics.Dynamic.Core.BilateralDen.disj {W : Type u_1} {E : Type u_2} (φ ψ : BilateralDen W E) : BilateralDen W E

Standard disjunction: dynamic Strong Kleene semantics.

For disjunction φ ∨ ψ, the positive update covers two verification routes:

• Verification via φ: s[φ]⁺ (φ is true, ψ is anything)
• Verification via ψ: s[φ]⁻[ψ]⁺ ∪ s[φ]?[ψ]⁺ (φ is false or unknown, ψ is true)

The negative update is sequential: s[φ ∨ ψ]⁻ = s[φ]⁻[ψ]⁻ (both must be denied in sequence, passing state dynamically).

The dynamic state-passing in the positive update is what makes bathroom disjunctions work: s[¬∃xP(x)]⁻[Q(x)]⁺ = s[∃xP(x)]⁺[Q(x)]⁺ (by DNE), introducing the discourse referent x for cross-disjunct anaphora.

Equations (64)/(67) of @cite{elliott-sudo-2025}.

Equations

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

def Semantics.Dynamic.Core.BilateralDen.«term_⊕_» : Lean.TrailingParserDescr

Notation for disjunction

Equations

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

theorem Semantics.Dynamic.Core.BilateralDen.de_morgan_disj {W : Type u_1} {E : Type u_2} (φ ψ : BilateralDen W E) (s : InfoState W E) : (~(φ ⊕ ψ)).positive s = (~φ ⊙ ~ψ).positive s

De Morgan: ¬(φ ∨ ψ) = ¬φ ∧ ¬ψ (positive dimension).

theorem Semantics.Dynamic.Core.BilateralDen.de_morgan_conj {W : Type u_1} {E : Type u_2} (φ ψ : BilateralDen W E) (s : InfoState W E) : (~(φ ⊙ ψ)).positive s = (~φ ⊕ ~ψ).positive s

De Morgan: ¬(φ ∧ ψ) = ¬φ ∨ ¬ψ (positive dimension).

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

Existential quantification: introduce a discourse referent.

For ∃x.φ:

• s[∃x.φ]⁺ = s[x:=?][φ]⁺ (introduce x, then assert φ)
• s[∃x.φ]⁻ = { p ∈ s | ∀e, p[x↦e] ∉ s[x:=?][φ]⁺ } (no witness makes φ true)

Equations

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

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

Existential with full domain

Equations

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

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

Universal quantification: ∀x.φ = ¬∃x.¬φ

In bilateral semantics, universal quantification is defined via de Morgan duality. This ensures proper interaction with negation.

Equations

• Semantics.Dynamic.Core.BilateralDen.forall_ x domain φ = ~(Semantics.Dynamic.Core.BilateralDen.exists_ x domain ~φ)

def Semantics.Dynamic.Core.BilateralDen.supports {W : Type u_1} {E : Type u_2} (s : InfoState W E) (φ : BilateralDen W E) : Prop

Bilateral support: state s supports φ iff positive update is non-empty and s subsists in s[φ]⁺.

Equations

• Semantics.Dynamic.Core.BilateralDen.supports s φ = ((φ.positive s).consistent ∧ s ⪯ φ.positive s)

def Semantics.Dynamic.Core.BilateralDen.entails {W : Type u_1} {E : Type u_2} (φ ψ : BilateralDen W E) : Prop

Bilateral entailment: φ entails ψ iff for all consistent states s, s[φ]⁺ supports ψ.

Equations

• (φ ⊨ᵇ ψ) = ∀ (s : Semantics.Dynamic.Core.InfoState W E), (φ.positive s).consistent → Semantics.Dynamic.Core.BilateralDen.supports (φ.positive s) ψ

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

Equations

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

theorem Semantics.Dynamic.Core.BilateralDen.egli {W : Type u_1} {E : Type u_2} (x : ℕ) (domain : Set E) (φ ψ : BilateralDen W E) (s : InfoState W E) : (exists_ x domain φ ⊙ ψ).positive s ⊆ (exists_ x domain (φ ⊙ ψ)).positive s

Egli's theorem: ∃x.φ ∧ ψ ⊨ ∃x[φ ∧ ψ]

When an existential takes wide scope over conjunction, the variable it introduces is accessible in the second conjunct. This is the key property for cross-sentential anaphora.

In bilateral semantics, this follows from the sequencing of updates.

def Semantics.Dynamic.Core.BilateralDen.pred1 {W : Type u_1} {E : Type u_2} (p : E → W → Prop) [(e : E) → (w : W) → Decidable (p e w)] (t : ℕ) : BilateralDen W E

Create bilateral from predicate over entities.

The predicate is Prop-valued (with per-point Decidable), following the project-wide migration of propositional positions from Bool to Prop.

Equations

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

def Semantics.Dynamic.Core.BilateralDen.pred2 {W : Type u_1} {E : Type u_2} (p : E → E → W → Prop) [(e₁ e₂ : E) → (w : W) → Decidable (p e₁ e₂ w)] (t₁ t₂ : ℕ) : BilateralDen W E

Create bilateral from binary predicate.

Equations

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

theorem Semantics.Dynamic.Core.BilateralDen.pred1_positive_monotone {W : Type u_1} {E : Type u_2} (p : E → W → Prop) [(e : E) → (w : W) → Decidable (p e w)] (t : ℕ) : Monotone (pred1 p t).positive

pred1 positive update is monotone.

theorem Semantics.Dynamic.Core.BilateralDen.pred1_negative_monotone {W : Type u_1} {E : Type u_2} (p : E → W → Prop) [(e : E) → (w : W) → Decidable (p e w)] (t : ℕ) : Monotone (pred1 p t).negative

pred1 negative update is monotone.

theorem Semantics.Dynamic.Core.BilateralDen.pred1_positive_eliminative {W : Type u_1} {E : Type u_2} (p : E → W → Prop) [(e : E) → (w : W) → Decidable (p e w)] (t : ℕ) : IsEliminative (pred1 p t).positive

pred1 positive update is eliminative.

theorem Semantics.Dynamic.Core.BilateralDen.pred1_negative_eliminative {W : Type u_1} {E : Type u_2} (p : E → W → Prop) [(e : E) → (w : W) → Decidable (p e w)] (t : ℕ) : IsEliminative (pred1 p t).negative

pred1 negative update is eliminative.

theorem Semantics.Dynamic.Core.BilateralDen.pred2_positive_monotone {W : Type u_1} {E : Type u_2} (p : E → E → W → Prop) [(e₁ e₂ : E) → (w : W) → Decidable (p e₁ e₂ w)] (t₁ t₂ : ℕ) : Monotone (pred2 p t₁ t₂).positive

pred2 positive update is monotone.

theorem Semantics.Dynamic.Core.BilateralDen.pred2_negative_monotone {W : Type u_1} {E : Type u_2} (p : E → E → W → Prop) [(e₁ e₂ : E) → (w : W) → Decidable (p e₁ e₂ w)] (t₁ t₂ : ℕ) : Monotone (pred2 p t₁ t₂).negative

pred2 negative update is monotone.

theorem Semantics.Dynamic.Core.BilateralDen.pred2_positive_eliminative {W : Type u_1} {E : Type u_2} (p : E → E → W → Prop) [(e₁ e₂ : E) → (w : W) → Decidable (p e₁ e₂ w)] (t₁ t₂ : ℕ) : IsEliminative (pred2 p t₁ t₂).positive

pred2 positive update is eliminative.

theorem Semantics.Dynamic.Core.BilateralDen.pred2_negative_eliminative {W : Type u_1} {E : Type u_2} (p : E → E → W → Prop) [(e₁ e₂ : E) → (w : W) → Decidable (p e₁ e₂ w)] (t₁ t₂ : ℕ) : IsEliminative (pred2 p t₁ t₂).negative

pred2 negative update is eliminative.

def Semantics.Dynamic.Core.BilateralDen.UnilateralDen (W : Type u_3) (E : Type u_4) : Type (max u_4 u_3)

Unilateral denotation: single update function

Equations

• Semantics.Dynamic.Core.BilateralDen.UnilateralDen W E = (Semantics.Dynamic.Core.InfoState W E → Semantics.Dynamic.Core.InfoState W E)

def Semantics.Dynamic.Core.BilateralDen.toPair {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) : (InfoState W E → InfoState W E) × (InfoState W E → InfoState W E)

View bilateral as pair of updates

Equations

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

def Semantics.Dynamic.Core.BilateralDen.ofPair {W : Type u_1} {E : Type u_2} (p : (InfoState W E → InfoState W E) × (InfoState W E → InfoState W E)) : BilateralDen W E

Construct bilateral from pair

Equations

• Semantics.Dynamic.Core.BilateralDen.ofPair p = { positive := p.fst, negative := p.snd }

theorem Semantics.Dynamic.Core.BilateralDen.toPair_ofPair {W : Type u_1} {E : Type u_2} (p : (InfoState W E → InfoState W E) × (InfoState W E → InfoState W E)) : (ofPair p).toPair = p

theorem Semantics.Dynamic.Core.BilateralDen.ofPair_toPair {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) : ofPair φ.toPair = φ

theorem Semantics.Dynamic.Core.BilateralDen.neg_eq_swap {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) : (~φ).toPair = φ.toPair.swap

Negation = swap on pairs

theorem Semantics.Dynamic.Core.BilateralDen.dne_from_swap {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) : (~~φ).toPair = φ.toPair

DNE follows from swap ∘ swap = id

def Semantics.Dynamic.Core.BilateralDen.toUnilateral {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) : UnilateralDen W E

Projection: bilateral → unilateral (forgets negative)

Equations

• φ.toUnilateral = φ.positive

@[implicit_reducible]

instance Semantics.Dynamic.Core.BilateralDen.instInvolutiveNeg {W : Type u_1} {E : Type u_2} : InvolutiveNeg (BilateralDen W E)

Equations

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

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

BUS's BilateralDen is itself a paraconsistent bilateral logic (Core.Logic.Bilateral.IsBilateral): the BilateralDen value IS the formula; positive and negative are the field projections; neg swaps them by definition. Both axioms reduce to rfl.

@[implicit_reducible]

instance Semantics.Dynamic.Core.BilateralDen.instPartialOrder {W : Type u_1} {E : Type u_2} : PartialOrder (BilateralDen W E)

Pointwise partial order on bilateral denotations: φ ≤ ψ iff both φ.positive s ⊆ ψ.positive s and φ.negative s ⊆ ψ.negative s for all s.

Equations

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

theorem Semantics.Dynamic.Core.BilateralDen.neg_monotone {W : Type u_1} {E : Type u_2} : Monotone neg

Negation is monotone: swapping dimensions preserves the pointwise order. ~φ ≤ ~ψ ↔ φ ≤ ψ because the pointwise order checks both components independently, and swap just rearranges them.

theorem Semantics.Dynamic.Core.BilateralDen.neg_le_neg_iff {W : Type u_1} {E : Type u_2} (φ ψ : BilateralDen W E) : ~φ ≤ ~ψ ↔ φ ≤ ψ

Negation reflects and preserves order: ~φ ≤ ~ψ ↔ φ ≤ ψ.