Dekker (2012): Predicate Logic with Anaphora vs Bilateral Update Semantics #
PLA (Semantics/Dynamic/PLA/, originating in [Dek94]) is the
foundational system for dynamic semantics with explicit pronoun indices.
This study verifies the formalized PLA's behavior on the canonical anaphora
puzzles and contrasts it with Bilateral Update Semantics (BUS,
UpdateSemantics/Bilateral.lean and Studies/ElliottSudo2025.lean), which solves
anaphora cases that PLA structurally cannot.
Caveat on the formalization: the PLA substrate as formalized is
eliminative — every update filters the input state
(update_eliminative), and existentials certify witness satisfiability in
their membership condition without storing the witness in the output
possibilities. Dekker's own PLA exports witnesses to output states;
anaphora resolution here goes through an explicit Resolution instead.
The theorems below are therefore facts about satisfiability and formula
structure (domain/range), not about witness export.
The Core Difference #
PLA has only positive updates (eliminative CCPs); BUS has both positive and negative dimensions.
- In PLA:
¬φtests ifφ.update(s) ≠ ∅, returnssor∅. Double negation preserves the domain of bound variables (syntactically the same) but not their witnesses (semantically lost). - In BUS:
¬φswaps positive/negative, so¬¬φ = φdefinitionally. Witnesses introduced by∃survive in the negative dimension and become available in cross-disjunct contexts.
This is the bilateral DNE strategy listed in
Dynamic/Update.lean's "three incompatible DNE solutions" table;
ICDRT (Studies/Hofmann2025.lean §7) is the third
strategy and dominates BUS on disagreement, modal subordination, and
three-way veridicality.
What this file proves #
§ 1 — PLA-side analysis of the bathroom sentence and double negation.
§ 2 — Architectural divergence summary; the BUS side is documented as
prose because BUS and PLA use different Core infrastructures that
cannot be co-imported.
PLA double negation: ¬¬φ has the same domain as φ. The
syntactic presence of the existentially-bound variable is preserved
because Formula.domain is computed from the formula structure, not
the update behavior.
Surviving an existential update certifies a witness: if p is in
(∃x.φ).update M s, some value for x satisfies φ at p.
Note what this does not say: p itself is unchanged (updates are
eliminative), so the witness is certified but not exported to the output
state — the formalized PLA's existential is a satisfiability test.
Surviving a sequenced update ∃x.φ then ψ means surviving the
existential update and satisfying ψ — the possibility is filtered by
both conjuncts. Since the state is only filtered, this records
satisfiability of both conjuncts at p; it does not link ψ's pronouns
to the existential's witness (that would require witness export, which
the eliminative formalization lacks).
Combining the two: a possibility surviving ∃x.φ then ψ certifies a
witness for φ and satisfies ψ.
The PLA puzzle: x is in the domain of ¬¬∃x.φ (syntactically
present, by pla_dne_syntactic) — but the update behavior of ¬¬
discards the actual witnesses. The discourse referent looks bound
syntactically yet is unavailable for anaphora.
Bathroom sentence (Partee): "Either there's no bathroom, or it's
upstairs" — ¬∃x.Bathroom(x) ∨ Upstairs(p₀).
Equations
- Dekker2012.bathroomSentence = (∼PLA.Formula.exists_ 0 (PLA.Formula.atom "Bathroom" [PLA.Term.var 0]) ⋁ PLA.Formula.atom "Upstairs" [PLA.Term.pron 0])
Instances For
Bathroom sentence in PLA: the pronoun "it" (index 0) appears in the range because the existential that would bind it sits under negation.
The bathroom sentence has nonempty domain (the existential is syntactically present) — PLA can write the formula but cannot resolve the pronoun against any introduced witness.
BUS's bilateral substrate lives in Semantics/Dynamic/UpdateSemantics/Bilateral.lean
with the type
structure BilateralDen (W V E : Type*) where
positive negative :
Set (Possibility W V (Part E)) → Set (Possibility W V (Part E))
and negation as def neg φ := { positive := φ.negative, negative := φ.positive }.
The DNE law neg (neg φ) = φ then holds by rfl
(BilateralDen.neg_neg in UpdateSemantics/Bilateral.lean).
PLA states (assignment-witness pairs) and BUS states (Part-partial
possibility sets) are different carriers, so a single file cannot state
both side-by-side. The BUS-side facts are stated
abstractly here and verified in their home file.
Bathroom sentence in BUS #
For ¬∃x.φ ∨ ψ:
(¬∃x.φ).negative s = (∃x.φ).positive s— the witness is in the negative dimension of the negated existential.- BUS disjunction routes
ψthrough the negative dimension of the first disjunct:disjPos2 φ ψ s := ψ.positive (φ.negative s). - So
ψreceives the existential's positive update, withxbound — the pronoun in "it's in a funny place" finds its referent.
This is why bathroom sentences work in BUS and fail in PLA: BUS routes the witness through the swap, while PLA discards it via the eliminative test.
Summary #
| Property | PLA | BUS |
|---|---|---|
| Negation | Test (s or ∅) | Swap (pos ↔ neg) |
¬¬φ semantics | Returns s, not s[φ] | = φ definitionally |
∃x under negation | Witness trapped | Witness in negative dimension |
| Bathroom sentence | Pronoun unbound | Pronoun bound via dimension swap |
The structural difference in negation is the key architectural choice: PLA's eliminative test traps drefs under negation; BUS's structural swap preserves them in the other dimension.