Elliott & Sudo (2025): Free Choice with Anaphora #
Bilateral Update Semantics (BUS) applied to bathroom disjunctions.
The puzzle #
Bathroom disjunction: "Either there's no bathroom or it's in a funny place."
From this, we infer:
- It's possible there's no bathroom
- It's possible there's a bathroom AND it's in a funny place
The pronoun "it" in the second disjunct is bound by the existential in the negated first disjunct. This cross-disjunct anaphora is puzzling because:
- Standard FC: ◇(φ ∨ ψ) → ◇φ ∧ ◇ψ (no anaphoric connection)
- With anaphora: ◇(¬∃xφ ∨ ψ(x)) → ◇¬∃xφ ∧ ◇(∃x(φ ∧ ψ(x)))
Solution #
BUS + Modal Disjunction:
- Disjunction semantics: φ ∨ ψ entails ◇φ ∧ ◇ψ
- Negation swaps positive/negative: ¬∃xφ positive = ∃xφ negative
- Cross-disjunct binding: x introduced in ¬∃xφ is visible to ψ(x)
Key results #
- Modified FC: ◇(φ ∨ ψ) ⊨ ◇φ ∧ ◇(¬φ ∧ ψ)
- FC with anaphora: bathroom inference pattern
- Dual prohibition: ¬◇φ ∧ ¬◇ψ ⊨ ¬(φ ∨ ψ) (preserved)
The paper's general disjPos1/disjPos2 (eq. 92) simplify for the
bathroom case (eqs. 93-94):
Under these simplification conditions, the general FC preconditions (both disjPos nonempty) yield the bathroom inference.
Possibility: state s makes ◇φ true iff s[φ]⁺ is consistent.
Equivalent to checking (BUSDen.diamond φ).positive s is non-empty.
Equations
- ElliottSudo2025.possible φ s = (φ.positive s).consistent
Instances For
Necessity: state s makes □φ true iff s subsists in s[φ]⁺.
Equations
- ElliottSudo2025.necessary φ s = s.subsistsIn (φ.positive s)
Instances For
Impossibility: ¬◇φ iff s[φ]⁺ is empty.
Equations
- ElliottSudo2025.impossible φ s = ¬(φ.positive s).consistent
Instances For
Diamond positive = s when φ is possible, ∅ otherwise.
Standard disjunction: the basic bilateral disjunction without FC preconditions.
Equations
- ElliottSudo2025.disjStd φ ψ = φ ⊕ ψ
Instances For
The part of the standard disjunction positive update that the first disjunct is responsible for: the (1,*) row of the Strong Kleene truth table.
s[φ ∨ ψ]₁⁺ = s[φ]⁺[ψ]⁺ ∪ s[φ]⁺[ψ]⁻ ∪ s[φ]⁺[ψ]?
Every possibility in s[φ]⁺ is verified by φ, and then classified by ψ
into one of three truth values. (eq. 92a)
Equations
- ElliottSudo2025.disjPos1 φ ψ s = ψ.positive (φ.positive s) ∪ ψ.negative (φ.positive s) ∪ ψ.unknownUpdate (φ.positive s)
Instances For
The part of the standard disjunction positive update that the second disjunct is responsible for: the (*,1) column of the Strong Kleene truth table.
s[φ ∨ ψ]₂⁺ = s[φ]⁺[ψ]⁺ ∪ s[φ]⁻[ψ]⁺ ∪ s[φ]?[ψ]⁺
The key term for cross-disjunct anaphora is s[φ]⁻[ψ]⁺: when
φ = ¬∃x.P(x), s[φ]⁻ = s[∃x.P(x)]⁺ by DNE, introducing the
discourse referent for binding across disjuncts. (eq. 92b)
Equations
- ElliottSudo2025.disjPos2 φ ψ s = ψ.positive (φ.positive s) ∪ ψ.positive (φ.negative s) ∪ ψ.positive (φ.unknownUpdate s)
Instances For
Modal Disjunction (anaphora-sensitive version): semantic disjunction that validates FC with anaphora.
Modal disjunction adds a precondition to the positive update requiring that each disjunct contribute at least some possibilities. This semantically derives FC without pragmatic reasoning. (eq. 96)
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- ElliottSudo2025.«term_∨ᶠᶜ_» = Lean.ParserDescr.trailingNode `ElliottSudo2025.«term_∨ᶠᶜ_» 60 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∨ᶠᶜ ") (Lean.ParserDescr.cat `term 0))
Instances For
The partition property guarantees φ.positive s ⊆ disjPos1 φ ψ s:
every possibility verified by φ ends up in disjPos1 (classified by ψ as
true, false, or unknown).
Similarly, ψ.positive (φ.negative s) ⊆ disjPos2 φ ψ s via the middle
term.
FC preconditions: if the modal disjunction is possible, both disjuncts contribute possibilities. (eq. 96)
Extract disjPos1 nonemptiness from FC possibility.
Extract disjPos2 nonemptiness from FC possibility.
Dual prohibition via disjPos1: if disjPos1 is empty (first disjunct contributes nothing), modal disjunction is impossible.
Dual prohibition via disjPos2: if disjPos2 is empty (second disjunct contributes nothing), modal disjunction is impossible.
In BUS, negation swaps positive and negative updates.
Negated existential has existential in negative dimension.
DNE preserves binding.
Divergence from DPL on doubly negated indefinites. The discourse
Examples.double_negation ("It's not the case that John didn't see a
bird. It was singing.") is judged acceptable; BUS derives the binding
because ¬¬φ = φ (dne_preserves_binding), whereas in DPL negation is
a test, so ¬¬∃xφ ≠ ∃xφ and the discourse referent never escapes.
Egli's theorem (positive): (∃x.φ) ∧ ψ ⊆ ∃x(φ ∧ ψ) for positive
updates. The positive direction holds because conjunction sequences
through the existential's positive update.
The bathroom disjunction configuration.
"Either there's no bathroom or it's in a funny place"
- bathroom : Semantics.Dynamic.Core.BilateralDen W E
The existential: ∃x.bathroom(x)
- funnyPlace : Semantics.Dynamic.Core.BilateralDen W E
The predicate on x: funny-place(x)
- x : ℕ
The variable bound by the existential
Instances For
The bathroom disjunction sentence: ¬∃x.bathroom(x) ∨ᶠᶜ funny-place(x)
Equations
- ElliottSudo2025.bathroomSentence cfg = ~cfg.bathroom ∨ᶠᶜ cfg.funnyPlace
Instances For
DNE as structural equality: ¬¬φ = φ.
FC with anaphora: the bathroom disjunction inference.
Eqs. 93-94 show that for bathroom disjunctions, the general
disjPos1/disjPos2 (eq. 92) simplify so that:
disjPos1reduces tobath.negative s(possible there's no bathroom)disjPos2reduces tofunnyPlace.positive (bath.positive s)(possible there's a bathroom in a funny place)
The hypotheses h_dp1 and h_dp2 encode these simplifications: the
general forms are contained in the simplified forms, so nonemptiness
of the general forms transfers to the simplified forms.
These hold when funnyPlace is eliminative (output ⊆ input), as is the
case for atomic predicates (pred1).
- noBathroom : BathroomWorld
- bathroomNormal : BathroomWorld
- bathroomFunny : BathroomWorld
Instances For
Equations
- ElliottSudo2025.instDecidableEqBathroomWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Equations
- ElliottSudo2025.instDecidableEqBathroomEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.