Linglib.Theories.Semantics.Dynamic.Comparisons.PLA

theorem Semantics.Dynamic.Comparisons.pla_dne_syntactic (φ : PLA.Formula) :

In PLA, ¬¬φ has the same domain as φ syntactically, but doesn't export witnesses semantically.

theorem Semantics.Dynamic.Comparisons.pla_existential_exports {E : Type u_1} [Nonempty E] (M : PLA.Model E) (x : PLA.VarIdx) (φ : PLA.Formula) (s : PLA.InfoState E) (p : PLA.Poss E) (hp : p ∈ PLA.Formula.update M (PLA.Formula.exists_ x φ) s) :

∃ (e : E), PLA.Formula.sat M (p.1[x ↦ e]) p.2 φ

PLA existential introduces witnesses that survive in the output.

source

theorem Semantics.Dynamic.Comparisons.pla_dne_has_domain {E : Type u_1} [Nonempty E] (x : PLA.VarIdx) (φ : PLA.Formula) :

x ∈ (∼∼PLA.Formula.exists_ x φ).domain

The problem: x is in the domain of ¬¬∃x.φ (syntactically present), but the update doesn't recover witnesses.

BUS Structure (from Core.Bilateral) #

In BUS, a denotation is a pair of update functions:

structure BilateralDen (W E : Type*) where
  positive : InfoState W E → InfoState W E
  negative : InfoState W E → InfoState W E

Negation swaps the dimensions:

def neg (φ : BilateralDen W E) : BilateralDen W E :=
  { positive := φ.negative, negative := φ.positive }

This gives DNE definitionally: neg (neg φ) = φ by rfl.

See Linglib.Theories.Semantics.Dynamic.Core.Bilateral for the full development.

source

theorem Semantics.Dynamic.Comparisons.bathroom_pla_has_unbound_pronoun :

0 ∈ PLA.bathroomSentence.range

PLA problem: the bathroom sentence has an unbound pronoun.

"Either there's no bathroom, or it's in a funny place." The pronoun "it" (index 0) appears in the range but the existential that would bind it is under negation.

source

theorem Semantics.Dynamic.Comparisons.bathroom_pla_has_domain :

PLA.bathroomSentence.domain.Nonempty

PLA problem: the domain is nonempty (existential is syntactically present).

BUS Solution (from BUS.FreeChoice) #

In BUS disjunction with modal semantics, the second disjunct receives the negative dimension of the first:

def disjPos2 (φ ψ : BilateralDen W E) (s : InfoState W E) : InfoState W E :=
  ψ.positive (φ.negative s)

For ¬∃x.φ ∨ ψ:

(¬∃x.φ).negative s = (∃x.φ).positive s
So ψ receives the existential's positive update, with x bound!

This is why bathroom sentences work in BUS: the pronoun in "it's in a funny place" gets bound because ∃x.bathroom is available in the negative dimension of ¬∃x.bathroom.

See Linglib.Theories.Semantics.Dynamic.BUS.FreeChoice for the full derivation.

Summary: PLA vs BUS #

Property	PLA	BUS
Negation	Test (s or ∅)	Swap (pos ↔ neg)
¬¬φ	≠ φ (returns s)	= φ (definitional)
∃x under ¬	Witness trapped	Witness in neg dim
Bathroom	Unbound pronoun	Bound via swap

PLA Negation (Test) #

s[¬φ] = s if s[φ] = ∅
      = ∅ otherwise

This is why ¬¬φ ≠ φ: double negation returns s, not s[φ].

BUS Negation (Swap) #

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

Swapping twice gives identity, so ¬¬φ = φ.

The structural difference in negation is the key:

PLA traps drefs under negation (eliminative test)
BUS preserves them in the other dimension (structural swap)

Documentation