Elliott & Sudo (2025): Free Choice with Anaphora

@cite{elliott-sudo-2025}

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:

1. It's possible there's no bathroom
2. 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:

1. Disjunction semantics: φ ∨ ψ entails ◇φ ∧ ◇ψ
2. Negation swaps positive/negative: ¬∃xφ positive = ∃xφ negative
3. 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):

• disjPos1 ⊆ s[∃ₓB(x)]⁻ (eq. 93)
• disjPos2 ⊆ s[∃ₓB(x)]⁺[F(x)]⁺ (eq. 94)

Under these simplification conditions, the general FC preconditions (both disjPos nonempty) yield the bathroom inference.

def Phenomena.Modality.Studies.ElliottSudo2025.possible {W : Type u_1} {E : Type u_2} (φ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) : Prop

Possibility: state s makes ◇φ true iff s[φ]⁺ is consistent. Equivalent to checking (BUSDen.diamond φ).positive s is non-empty.

Equations

• Phenomena.Modality.Studies.ElliottSudo2025.possible φ s = (φ.positive s).consistent

def Phenomena.Modality.Studies.ElliottSudo2025.necessary {W : Type u_1} {E : Type u_2} (φ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) : Prop

Necessity: state s makes □φ true iff s subsists in s[φ]⁺.

Equations

• Phenomena.Modality.Studies.ElliottSudo2025.necessary φ s = (s ⪯ φ.positive s)

def Phenomena.Modality.Studies.ElliottSudo2025.impossible {W : Type u_1} {E : Type u_2} (φ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) : Prop

Impossibility: ¬◇φ iff s[φ]⁺ is empty.

Equations

• Phenomena.Modality.Studies.ElliottSudo2025.impossible φ s = ¬(φ.positive s).consistent

theorem Phenomena.Modality.Studies.ElliottSudo2025.impossible_iff_empty {W : Type u_1} {E : Type u_2} (φ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) : impossible φ s ↔ φ.positive s = ∅

theorem Phenomena.Modality.Studies.ElliottSudo2025.diamond_positive_eq {W : Type u_1} {E : Type u_2} (φ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) : (◇ᵇφ).positive s = if possible φ s then s else ∅

Diamond positive = s when φ is possible, ∅ otherwise.

def Phenomena.Modality.Studies.ElliottSudo2025.disjStd {W : Type u_1} {E : Type u_2} (φ ψ : Semantics.Dynamic.Core.BilateralDen W E) : Semantics.Dynamic.Core.BilateralDen W E

Standard disjunction: the basic bilateral disjunction without FC preconditions.

Equations

• Phenomena.Modality.Studies.ElliottSudo2025.disjStd φ ψ = φ ⊕ ψ

def Phenomena.Modality.Studies.ElliottSudo2025.disjPos1 {W : Type u_1} {E : Type u_2} (φ ψ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) : Semantics.Dynamic.Core.InfoState W E

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

• Phenomena.Modality.Studies.ElliottSudo2025.disjPos1 φ ψ s = ψ.positive (φ.positive s) ∪ ψ.negative (φ.positive s) ∪ ψ.unknownUpdate (φ.positive s)

def Phenomena.Modality.Studies.ElliottSudo2025.disjPos2 {W : Type u_1} {E : Type u_2} (φ ψ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) : Semantics.Dynamic.Core.InfoState W E

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

• Phenomena.Modality.Studies.ElliottSudo2025.disjPos2 φ ψ s = ψ.positive (φ.positive s) ∪ ψ.positive (φ.negative s) ∪ ψ.positive (φ.unknownUpdate s)

def Phenomena.Modality.Studies.ElliottSudo2025.disjModal {W : Type u_1} {E : Type u_2} (φ ψ : Semantics.Dynamic.Core.BilateralDen W E) : Semantics.Dynamic.Core.BilateralDen W E

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.

def Phenomena.Modality.Studies.ElliottSudo2025.«term_∨ᶠᶜ_» : Lean.TrailingParserDescr

Equations

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

theorem Phenomena.Modality.Studies.ElliottSudo2025.subset_disjPos1 {W : Type u_1} {E : Type u_2} (φ ψ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) : φ.positive s ⊆ disjPos1 φ ψ s

The partition property guarantees φ.positive s ⊆ disjPos1 φ ψ s: every possibility verified by φ ends up in disjPos1 (classified by ψ as true, false, or unknown).

theorem Phenomena.Modality.Studies.ElliottSudo2025.neg_subset_disjPos2 {W : Type u_1} {E : Type u_2} (φ ψ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) : ψ.positive (φ.negative s) ⊆ disjPos2 φ ψ s

Similarly, ψ.positive (φ.negative s) ⊆ disjPos2 φ ψ s via the middle term.

theorem Phenomena.Modality.Studies.ElliottSudo2025.fc_preconditions {W : Type u_1} {E : Type u_2} (φ ψ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) (h : possible (φ ∨ᶠᶜ ψ) s) : Set.Nonempty (disjPos1 φ ψ s) ∧ Set.Nonempty (disjPos2 φ ψ s)

FC preconditions: if the modal disjunction is possible, both disjuncts contribute possibilities. (eq. 96)

theorem Phenomena.Modality.Studies.ElliottSudo2025.fc_disjPos1_nonempty {W : Type u_1} {E : Type u_2} (φ ψ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) (h : possible (φ ∨ᶠᶜ ψ) s) : Set.Nonempty (disjPos1 φ ψ s)

Extract disjPos1 nonemptiness from FC possibility.

theorem Phenomena.Modality.Studies.ElliottSudo2025.fc_disjPos2_nonempty {W : Type u_1} {E : Type u_2} (φ ψ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) (h : possible (φ ∨ᶠᶜ ψ) s) : Set.Nonempty (disjPos2 φ ψ s)

Extract disjPos2 nonemptiness from FC possibility.

theorem Phenomena.Modality.Studies.ElliottSudo2025.dual_prohibition_disjPos1 {W : Type u_1} {E : Type u_2} (φ ψ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) (h : ¬Set.Nonempty (disjPos1 φ ψ s)) : impossible (φ ∨ᶠᶜ ψ) s

Dual prohibition via disjPos1: if disjPos1 is empty (first disjunct contributes nothing), modal disjunction is impossible.

theorem Phenomena.Modality.Studies.ElliottSudo2025.dual_prohibition_disjPos2 {W : Type u_1} {E : Type u_2} (φ ψ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) (h : ¬Set.Nonempty (disjPos2 φ ψ s)) : impossible (φ ∨ᶠᶜ ψ) s

Dual prohibition via disjPos2: if disjPos2 is empty (second disjunct contributes nothing), modal disjunction is impossible.

theorem Phenomena.Modality.Studies.ElliottSudo2025.negation_swaps_dims {W : Type u_1} {E : Type u_2} (φ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) : (~φ).positive s = φ.negative s ∧ (~φ).negative s = φ.positive s

In BUS, negation swaps positive and negative updates.

theorem Phenomena.Modality.Studies.ElliottSudo2025.exists_in_neg_dimension {W : Type u_1} {E : Type u_2} (x : ℕ) (dom : Set E) (φ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) : (~(Semantics.Dynamic.Core.BilateralDen.exists_ x dom φ)).negative s = (Semantics.Dynamic.Core.BilateralDen.exists_ x dom φ).positive s

Negated existential has existential in negative dimension.

theorem Phenomena.Modality.Studies.ElliottSudo2025.dne_preserves_binding {W : Type u_1} {E : Type u_2} (x : ℕ) (dom : Set E) (φ ψ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) : (~~(Semantics.Dynamic.Core.BilateralDen.exists_ x dom φ) ⊙ ψ).positive s = (Semantics.Dynamic.Core.BilateralDen.exists_ x dom φ ⊙ ψ).positive s

DNE preserves binding.

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

Egli's theorem (positive): (∃x.φ) ∧ ψ ⊆ ∃x(φ ∧ ψ) for positive updates. The positive direction holds because conjunction sequences through the existential's positive update.

structure Phenomena.Modality.Studies.ElliottSudo2025.BathroomConfig (W : Type u_3) (E : Type u_4) : Type (max u_3 u_4)

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

def Phenomena.Modality.Studies.ElliottSudo2025.bathroomSentence {W : Type u_1} {E : Type u_2} (cfg : BathroomConfig W E) : Semantics.Dynamic.Core.BilateralDen W E

The bathroom disjunction sentence: ¬∃x.bathroom(x) ∨ᶠᶜ funny-place(x)

Equations

• Phenomena.Modality.Studies.ElliottSudo2025.bathroomSentence cfg = ~cfg.bathroom ∨ᶠᶜ cfg.funnyPlace

theorem Phenomena.Modality.Studies.ElliottSudo2025.anaphora_via_dne {W : Type u_1} {E : Type u_2} (cfg : BathroomConfig W E) : ~~cfg.bathroom = cfg.bathroom

DNE as structural equality: ¬¬φ = φ.

theorem Phenomena.Modality.Studies.ElliottSudo2025.fc_with_anaphora {W : Type u_1} {E : Type u_2} (cfg : BathroomConfig W E) (s : Semantics.Dynamic.Core.InfoState W E) (h_poss : possible (bathroomSentence cfg) s) (h_dp1 : disjPos1 (~cfg.bathroom) cfg.funnyPlace s ⊆ cfg.bathroom.negative s) (h_dp2 : disjPos2 (~cfg.bathroom) cfg.funnyPlace s ⊆ cfg.funnyPlace.positive (cfg.bathroom.positive s)) : Set.Nonempty (cfg.bathroom.negative s) ∧ Set.Nonempty (cfg.funnyPlace.positive (cfg.bathroom.positive s))

FC with anaphora: the bathroom disjunction inference.

Eqs. 93-94 show that for bathroom disjunctions, the general disjPos1/disjPos2 (eq. 92) simplify so that:

• disjPos1 reduces to bath.negative s (possible there's no bathroom)
• disjPos2 reduces to funnyPlace.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).

inductive Phenomena.Modality.Studies.ElliottSudo2025.BathroomWorld : Type

• noBathroom : BathroomWorld
• bathroomNormal : BathroomWorld
• bathroomFunny : BathroomWorld

@[implicit_reducible]

instance Phenomena.Modality.Studies.ElliottSudo2025.instDecidableEqBathroomWorld : DecidableEq BathroomWorld

Equations

• Phenomena.Modality.Studies.ElliottSudo2025.instDecidableEqBathroomWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Modality.Studies.ElliottSudo2025.instReprBathroomWorld.repr : BathroomWorld → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Modality.Studies.ElliottSudo2025.instReprBathroomWorld : Repr BathroomWorld

Equations

• Phenomena.Modality.Studies.ElliottSudo2025.instReprBathroomWorld = { reprPrec := Phenomena.Modality.Studies.ElliottSudo2025.instReprBathroomWorld.repr }

inductive Phenomena.Modality.Studies.ElliottSudo2025.BathroomEntity : Type

• theBathroom : BathroomEntity

@[implicit_reducible]

instance Phenomena.Modality.Studies.ElliottSudo2025.instDecidableEqBathroomEntity : DecidableEq BathroomEntity

Equations

• Phenomena.Modality.Studies.ElliottSudo2025.instDecidableEqBathroomEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Modality.Studies.ElliottSudo2025.instReprBathroomEntity.repr : BathroomEntity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Modality.Studies.ElliottSudo2025.instReprBathroomEntity : Repr BathroomEntity

Equations

• Phenomena.Modality.Studies.ElliottSudo2025.instReprBathroomEntity = { reprPrec := Phenomena.Modality.Studies.ElliottSudo2025.instReprBathroomEntity.repr }

def Phenomena.Modality.Studies.ElliottSudo2025.isBathroom : BathroomEntity → BathroomWorld → Prop

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Modality.Studies.ElliottSudo2025.isBathroom Phenomena.Modality.Studies.ElliottSudo2025.BathroomEntity.theBathroom x✝ = True

@[implicit_reducible]

instance Phenomena.Modality.Studies.ElliottSudo2025.instDecidableIsBathroom (e : BathroomEntity) (w : BathroomWorld) : Decidable (isBathroom e w)

Equations

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

def Phenomena.Modality.Studies.ElliottSudo2025.inFunnyPlace : BathroomEntity → BathroomWorld → Prop

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Modality.Studies.ElliottSudo2025.inFunnyPlace x✝¹ x✝ = False

@[implicit_reducible]

instance Phenomena.Modality.Studies.ElliottSudo2025.instDecidableInFunnyPlace (e : BathroomEntity) (w : BathroomWorld) : Decidable (inFunnyPlace e w)

Equations

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

def Phenomena.Modality.Studies.ElliottSudo2025.exampleBathroomConfig : BathroomConfig BathroomWorld BathroomEntity

Equations

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