Elliott and Sudo (2025): Free choice with anaphora

This file formalizes [ES25a]'s account of free choice with anaphora in Bilateral Update Semantics. A bathroom disjunction, either there's no bathroom or it's in a funny place, embedded under an existential modal yields the inferences that possibly there is no bathroom and that possibly there is a bathroom in a funny place, an inference that the classical schema ◇(φ ∨ ψ) ⊨ ◇φ ∧ ◇ψ ([Kam73], [Zim00]) cannot state, since its second conjunct would contain a free pronoun. The modified schema ◇(φ ∨ ψ) ⊨ ◇φ ∧ ◇(¬φ ∧ ψ) together with Double Negation Elimination and Egli's theorem derives it, and neither exhaustification over structurally simpler alternatives ([BLF20], [FK11], [TH15]) nor classical update semantics ([Hei82a], [Vel96], [GS91a]), where negation blocks anaphora and DNE fails, validates all three. In Bilateral Update Semantics ([KM95]) every sentence has a positive and a negative update over Heimian states, negation swaps them, so DNE is definitional; an existential introduces its referent by random assignment in the positive dimension only; the connectives compose the dimensions along the Strong Kleene tables, so the negation of a negated existential in the first disjunct makes the referent available to the second, and a bathroom disjunction gets existential truth conditions; epistemic modals are tests on the state after [Vel96], with subsistence ([GSV96]) for the negative update; and modal disjunction adds to the positive update the precondition that each disjunct be responsible for some possibilities, which validates free choice ([Sim05], [Alo22]) while leaving dual prohibition intact. The same precondition on the negative update of conjunction gives negative free choice, and the dual universal gives distributive inferences, both with anaphora.

Implementation notes

• The substrate BilateralDen supplies the dimensions, the connectives (61) and (64), the existential (44)–(45), the unknown update (53) and assertability (54); this file adds the modals (73) and (77), the two parts of a disjunction's positive update (92), modal disjunction (96) and its conjunctive counterpart (132).
• The derivations (93), (94) and (70) hold at states where the referent is novel, the article's initial states; the bivalence of an existential, that its unknown update is empty, needs a nonempty domain. Free choice with anaphora (24) is then derived from the preconditions of modal disjunction rather than assumed.
• The comparison with DPL ([GS91a]) is the substrate's definitional DNE against GroenendijkStokhof1991.dne_fails_anaphora.
• The examples are Data.Examples.ElliottSudo2025.

TODO

• The flavour-neutral modals (89), simplification of disjunctive antecedents (127) and wide free choice with anaphora (110) are not represented.

References

• [ES25a]
• [KM95]
• [GS91a]
• [GSV96]
• [Vel96]
• [Hei82a]
• [Kam73]
• [Zim00]
• [Sim05]
• [Alo22]
• [BLF20]
• [FK11]
• [TH15]

@[reducible, inline]

abbrev ElliottSudo2025.BUSDen (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A BUS denotation: a bilateral denotation over possibilities with natural-number variables.

Equations

• ElliottSudo2025.BUSDen W E = BilateralDen W ℕ E

@[reducible, inline]

abbrev ElliottSudo2025.BUSState (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

A Heimian information state (Def. 3.1).

Equations

• ElliottSudo2025.BUSState W E = Set (DynamicSemantics.Possibility W ℕ (Flat E))

Novel referents and atomic predications (§3.2–3.3)

theorem ElliottSudo2025.pred1_positive_of_novel {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (Q : E → W → Prop) (hx : DynamicSemantics.State.Novel s x) : (BilateralDen.pred1 Q x).positive s = ∅

Where the referent is novel, an atomic predication of it survives in neither dimension.

theorem ElliottSudo2025.pred1_negative_of_novel {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (Q : E → W → Prop) (hx : DynamicSemantics.State.Novel s x) : (BilateralDen.pred1 Q x).negative s = ∅

theorem ElliottSudo2025.pred1_unknownUpdate_of_novel {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (Q : E → W → Prop) (hx : DynamicSemantics.State.Novel s x) : (BilateralDen.pred1 Q x).unknownUpdate s = s

Where the referent is novel, every possibility is unknown for the predication.

theorem ElliottSudo2025.pred1_positive_empty {W : Type u_1} {E : Type u_2} {x : ℕ} (Q : E → W → Prop) : (BilateralDen.pred1 Q x).positive ∅ = ∅

theorem ElliottSudo2025.pred1_negative_empty {W : Type u_1} {E : Type u_2} {x : ℕ} (Q : E → W → Prop) : (BilateralDen.pred1 Q x).negative ∅ = ∅

theorem ElliottSudo2025.exists_negative_subset {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (φ : BUSDen W E) : (BilateralDen.exists_ x φ).negative s ⊆ s

The negative update of an existential keeps possibilities of the input state, (45).

theorem ElliottSudo2025.novel_exists_negative {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (hx : DynamicSemantics.State.Novel s x) (φ : BUSDen W E) : DynamicSemantics.State.Novel ((BilateralDen.exists_ x φ).negative s) x

The negative update of an existential introduces no anaphoric information: the referent stays novel.

theorem ElliottSudo2025.mem_lowerClosure_exists_positive_iff {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (Q : E → W → Prop) {p : DynamicSemantics.Possibility W ℕ (Flat E)} (hp : p ∈ s) (hx : DynamicSemantics.State.Novel s x) : p ∈ lowerClosure ((BilateralDen.exists_ x (BilateralDen.pred1 Q x)).positive s) ↔ ∃ (e : E), Q e p.world

A novel possibility subsists in the random-assignment update of a predication exactly when its world has a witness, (76).

theorem ElliottSudo2025.exists_unknownUpdate_of_novel {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (Q : E → W → Prop) [Nonempty E] (hx : DynamicSemantics.State.Novel s x) : (BilateralDen.exists_ x (BilateralDen.pred1 Q x)).unknownUpdate s = ∅

Bivalence of an existential statement, (55): at a state where its referent is novel, every possibility subsists in the positive or the negative update, so the unknown update is empty and the statement is assertable.

theorem ElliottSudo2025.exists_assertable {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (Q : E → W → Prop) [Nonempty E] (hx : DynamicSemantics.State.Novel s x) : (BilateralDen.exists_ x (BilateralDen.pred1 Q x)).assertable s

Epistemic modals (§3.5)

def ElliottSudo2025.Possible {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : BUSState W E) : Prop

◇φ passes positively when the positive update is consistent, (73a).

Equations

• ElliottSudo2025.Possible φ s = (φ.positive s).Nonempty

def ElliottSudo2025.Settled {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : BUSState W E) : Prop

◇φ passes negatively when ¬φ is already implicit in the state modulo anaphoric information: the state subsists in the negative update, (73b).

Equations

• ElliottSudo2025.Settled φ s = (lowerClosure s ≤ lowerClosure (φ.negative s))

def ElliottSudo2025.diamond {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : BUSDen W E

Epistemic possibility (73): both updates are tests, returning the state or the absurd state.

Equations

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

def ElliottSudo2025.box {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : BUSDen W E

Epistemic necessity (77), the dual □φ = ¬◇¬φ.

Equations

• □ᵇφ = BilateralDen.neg ◇ᵇ(BilateralDen.neg φ)

def ElliottSudo2025.«term◇ᵇ_» : Lean.ParserDescr

Epistemic possibility (73): both updates are tests, returning the state or the absurd state.

Equations

• ElliottSudo2025.«term◇ᵇ_» = Lean.ParserDescr.node `ElliottSudo2025.«term◇ᵇ_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◇ᵇ") (Lean.ParserDescr.cat `term 1024))

def ElliottSudo2025.«term□ᵇ_» : Lean.ParserDescr

Epistemic necessity (77), the dual □φ = ¬◇¬φ.

Equations

• ElliottSudo2025.«term□ᵇ_» = Lean.ParserDescr.node `ElliottSudo2025.«term□ᵇ_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□ᵇ") (Lean.ParserDescr.cat `term 1024))

theorem ElliottSudo2025.box_positive {W : Type u_1} {E : Type u_2} {s : BUSState W E} (φ : BUSDen W E) : (□ᵇφ).positive s = (◇ᵇ(BilateralDen.neg φ)).negative s

(77a): s[□φ]⁺ = s[◇¬φ]⁻.

theorem ElliottSudo2025.diamond_neg_exists_positive {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (B : E → W → Prop) : (◇ᵇ(BilateralDen.exists_ x (BilateralDen.pred1 B x)).neg).positive s = {_i : DynamicSemantics.Possibility W ℕ (Flat E) | _i ∈ s ∧ ((BilateralDen.exists_ x (BilateralDen.pred1 B x)).negative s).Nonempty}

(75): maybe there isn't a bathroom passes positively when some possibility has none.

theorem ElliottSudo2025.settled_neg_exists_iff {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (B : E → W → Prop) (hx : DynamicSemantics.State.Novel s x) : Settled (BilateralDen.exists_ x (BilateralDen.pred1 B x)).neg s ↔ ∀ p ∈ s, ∃ (e : E), B e p.world

(76): it passes negatively when the state subsists in the positive update of the existential, which at a state where the referent is novel means that every possibility has a bathroom.

Modal disjunction (§3.6–3.7)

def ElliottSudo2025.disjPos1 {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) (s : BUSState W E) : BUSState W E

The part of a disjunction's positive update the first disjunct is responsible for, (92a): the verifying row of the Strong Kleene table.

Equations

• ElliottSudo2025.disjPos1 φ ψ s = ψ.positive (φ.positive s) ∪ ψ.negative (φ.positive s) ∪ BilateralDen.unknownUpdate ψ (φ.positive s)

def ElliottSudo2025.disjPos2 {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) (s : BUSState W E) : BUSState W E

The part the second disjunct is responsible for, (92b): the verifying column. The term ψ.positive (φ.negative s) carries cross-disjunct anaphora.

Equations

• ElliottSudo2025.disjPos2 φ ψ s = ψ.positive (φ.positive s) ∪ ψ.positive (φ.negative s) ∪ ψ.positive (BilateralDen.unknownUpdate φ s)

theorem ElliottSudo2025.disj_positive_eq {W : Type u_1} {E : Type u_2} {s : BUSState W E} (φ ψ : BUSDen W E) : (BilateralDen.disj φ ψ).positive s = disjPos1 φ ψ s ∪ disjPos2 φ ψ s

(92c): the positive update of disjunction (64) is the union of the two parts.

noncomputable def ElliottSudo2025.disjModal {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) : BUSDen W E

Modal disjunction, anaphora-sensitive version (96): the positive update requires each disjunct to be responsible for some possibilities; the negative update is that of plain disjunction.

Equations

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

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

Modal disjunction, anaphora-sensitive version (96): the positive update requires each disjunct to be responsible for some possibilities; the negative update is that of plain disjunction.

Equations

• ElliottSudo2025.«term_∨ᶠᶜ_» = Lean.ParserDescr.trailingNode `ElliottSudo2025.«term_∨ᶠᶜ_» 60 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∨ᶠᶜ ") (Lean.ParserDescr.cat `term 0))

theorem ElliottSudo2025.fc_preconditions {W : Type u_1} {E : Type u_2} {s : BUSState W E} (φ ψ : BUSDen W E) (h : Possible (φ ∨ᶠᶜ ψ) s) : Set.Nonempty (disjPos1 φ ψ s) ∧ Set.Nonempty (disjPos2 φ ψ s)

The preconditions of modal disjunction: a possible modal disjunction has both parts consistent.

theorem ElliottSudo2025.disjPos1_atom {W : Type u_1} {E : Type u_2} {s : BUSState W E} (c t : W → Prop) : disjPos1 (BilateralDen.atom c) (BilateralDen.atom t) s = (BilateralDen.atom c).positive s

For worldly atoms the first part is the first disjunct's positive update: the second disjunct partitions it.

theorem ElliottSudo2025.disjPos2_atom {W : Type u_1} {E : Type u_2} {s : BUSState W E} (c t : W → Prop) : disjPos2 (BilateralDen.atom c) (BilateralDen.atom t) s = (BilateralDen.atom t).positive s

For worldly atoms the second part is the second disjunct's positive update.

theorem ElliottSudo2025.possible_disjModal_atom_iff {W : Type u_1} {E : Type u_2} {s : BUSState W E} (c t : W → Prop) : Possible (BilateralDen.atom c ∨ᶠᶜ BilateralDen.atom t) s ↔ Possible (BilateralDen.atom c) s ∧ Possible (BilateralDen.atom t) s

Free choice (84): there might be coffee or tea passes exactly when some possibility has coffee and some has tea.

theorem ElliottSudo2025.lowerClosure_le_sep_iff {W : Type u_1} {E : Type u_2} {s : BUSState W E} (pred : W → Prop) : lowerClosure s ≤ lowerClosure {p : DynamicSemantics.Possibility W ℕ (Flat E) | p ∈ s ∧ pred p.world} ↔ ∀ p ∈ s, pred p.world

Subsistence into a worldly restriction of the state is that restriction's holding throughout, since descendants share their world.

theorem ElliottSudo2025.settled_disjModal_atom_iff {W : Type u_1} {E : Type u_2} {s : BUSState W E} (c t : W → Prop) : Settled (BilateralDen.atom c ∨ᶠᶜ BilateralDen.atom t) s ↔ ∀ p ∈ s, ¬c p.world ∧ ¬t p.world

(88): it's impossible that there's coffee or tea passes exactly when no possibility has coffee or tea.

theorem ElliottSudo2025.dual_prohibition {W : Type u_1} {E : Type u_2} {s : BUSState W E} (c t : W → Prop) (h : Settled (BilateralDen.atom c ∨ᶠᶜ BilateralDen.atom t) s) : Settled (BilateralDen.atom c) s ∧ Settled (BilateralDen.atom t) s

Dual prohibition (80) is preserved: the negative update of modal disjunction is untouched.

The bathroom disjunction and free choice with anaphora (§3.4.2, §3.7)

theorem ElliottSudo2025.disjPos1_bathroom {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (P Q : E → W → Prop) (hx : DynamicSemantics.State.Novel s x) : disjPos1 (BilateralDen.exists_ x (BilateralDen.pred1 P x)).neg (BilateralDen.pred1 Q x) s = (BilateralDen.exists_ x (BilateralDen.pred1 P x)).negative s

(93): where the referent is novel, the first part of the bathroom disjunction is the negative update of the existential, since the second disjunct introduces no anaphoric information.

theorem ElliottSudo2025.disjPos2_bathroom {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (P Q : E → W → Prop) [Nonempty E] (hx : DynamicSemantics.State.Novel s x) : disjPos2 (BilateralDen.exists_ x (BilateralDen.pred1 P x)).neg (BilateralDen.pred1 Q x) s = (BilateralDen.pred1 Q x).positive ((BilateralDen.exists_ x (BilateralDen.pred1 P x)).positive s)

(94): the second part is the positive update of the existential followed by the second disjunct, by DNE at the negative update of the negated existential.

theorem ElliottSudo2025.bathroom_positive {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (P Q : E → W → Prop) [Nonempty E] (hx : DynamicSemantics.State.Novel s x) : ((BilateralDen.exists_ x (BilateralDen.pred1 P x)).neg.disj (BilateralDen.pred1 Q x)).positive s = (BilateralDen.exists_ x (BilateralDen.pred1 P x)).negative s ∪ (BilateralDen.pred1 Q x).positive ((BilateralDen.exists_ x (BilateralDen.pred1 P x)).positive s)

(70): the bathroom disjunction's positive update keeps the possibilities without a P, with no referent introduced, and those with a P that is Q, with the referent introduced: existential truth conditions.

theorem ElliottSudo2025.bathroom_negative {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (P Q : E → W → Prop) : ((BilateralDen.exists_ x (BilateralDen.pred1 P x)).neg.disj (BilateralDen.pred1 Q x)).negative s = (BilateralDen.pred1 Q x).negative ((BilateralDen.exists_ x (BilateralDen.pred1 P x)).positive s)

(66): its negative update is the positive update of the existential followed by the denial of the second disjunct, the positive update of ∃x(P(x) ∧ ¬Q(x)).

theorem ElliottSudo2025.fc_with_anaphora {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (P Q : E → W → Prop) [Nonempty E] (hx : DynamicSemantics.State.Novel s x) (h : Possible ((BilateralDen.exists_ x (BilateralDen.pred1 P x)).neg ∨ᶠᶜ BilateralDen.pred1 Q x) s) : ((BilateralDen.exists_ x (BilateralDen.pred1 P x)).negative s).Nonempty ∧ ((BilateralDen.pred1 Q x).positive ((BilateralDen.exists_ x (BilateralDen.pred1 P x)).positive s)).Nonempty

Free choice with anaphora, (24) and (99): a possible modalized bathroom disjunction makes it possible that there is no P and possible that there is a P that is Q.

theorem ElliottSudo2025.classical_conclusion_impossible {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} (Q : E → W → Prop) (hx : DynamicSemantics.State.Novel s x) : ¬Possible (BilateralDen.pred1 Q x) s

(25), (90c): the classical schema's second conclusion ◇Q(x) is unsatisfiable at the same states, its pronoun being free.

Double negation and Egli's theorem (§2.1, §3.3–3.4)

theorem ElliottSudo2025.dne_bus_not_dpl {W : Type u_1} {E : Type u_2} [Nontrivial E] : (∀ (φ : BUSDen W E), (BilateralDen.neg φ).neg = φ) ∧ ∃ (x : ℕ) (φ : DynamicSemantics.Update (Assignment E)), DynamicSemantics.Update.test (DynamicSemantics.Update.test (DynamicSemantics.Update.dexists x φ).neg).neg ≠ DynamicSemantics.Update.dexists x φ

DNE is definitional in BUS (49), whereas in DPL a doubly negated existential differs from the existential, so no discourse referent escapes ([GS91a]).

theorem ElliottSudo2025.negative_egli_fails : ∃ (W : Type) (E : Type) (x : ℕ) (P : E → W → Prop) (Q : E → W → Prop) (s : BUSState W E), (BilateralDen.exists_ x ((BilateralDen.pred1 P x).conj (BilateralDen.pred1 Q x))).negative s ≠ ((BilateralDen.exists_ x (BilateralDen.pred1 P x)).conj (BilateralDen.pred1 Q x)).negative s

Egli's positive equivalence (59) is the substrate's egli; its negative counterpart (62) fails: the negative update of ∃x(P(x) ∧ Q(x)) introduces no referent, while that of ∃xP(x) ∧ Q(x) contains possibilities with the referent defined.

Partial familiarity (§3.3, (56)–(57))

inductive ElliottSudo2025.PWorld : Type

The worlds of (56)–(57): a is P at wa, b at wb, nothing at w0.

• wa : PWorld
• wb : PWorld
• w0 : PWorld

@[instance_reducible]

instance ElliottSudo2025.instDecidableEqPWorld : DecidableEq PWorld

Equations

• ElliottSudo2025.instDecidableEqPWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive ElliottSudo2025.PEntity : Type

• a : PEntity
• b : PEntity

@[instance_reducible]

instance ElliottSudo2025.instDecidableEqPEntity : DecidableEq PEntity

Equations

• ElliottSudo2025.instDecidableEqPEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def ElliottSudo2025.pHolds : PEntity → PWorld → Prop

Equations

• ElliottSudo2025.pHolds ElliottSudo2025.PEntity.a ElliottSudo2025.PWorld.wa = True
• ElliottSudo2025.pHolds ElliottSudo2025.PEntity.b ElliottSudo2025.PWorld.wb = True
• ElliottSudo2025.pHolds x✝¹ x✝ = False

def ElliottSudo2025.xTo (e : PEntity) : ℕ → Flat PEntity

The assignment [x → e]: register 0 defined, all else ∗.

Equations

• ElliottSudo2025.xTo e n = if n = 0 then ↑e else ⊥

def ElliottSudo2025.blank : ℕ → Flat PEntity

The initial assignment [].

Equations

• ElliottSudo2025.blank x✝ = ⊥

def ElliottSudo2025.s56 : BUSState PWorld PEntity

The state of (56), where x is defined at the P-worlds only.

Equations

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

theorem ElliottSudo2025.mem_positive_s56 : { world := PWorld.wa, assignment := xTo PEntity.a } ∈ (BilateralDen.pred1 pHolds 0).positive s56

(56a): (wa, [x → a]) survives assertion.

theorem ElliottSudo2025.gap_mem_unknownUpdate_s56 : { world := PWorld.w0, assignment := blank } ∈ (BilateralDen.pred1 pHolds 0).unknownUpdate s56

(56c): (w0, []) subsists in neither dimension, so it is unknown.

theorem ElliottSudo2025.not_assertable_s56 : ¬(BilateralDen.pred1 pHolds 0).assertable s56

(56): P(x) is not assertable at a partially familiar state, and x is not familiar.

theorem ElliottSudo2025.not_familiar_s56 : ¬DynamicSemantics.State.Familiar s56 0

def ElliottSudo2025.s57 : BUSState PWorld PEntity

The state of (57): x is undefined at some possibility of each world but defined at another with the same world.

Equations

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

theorem ElliottSudo2025.assertable_s57_not_familiar : (BilateralDen.pred1 pHolds 0).assertable s57 ∧ ¬DynamicSemantics.State.Familiar s57 0

Assertability is strictly weaker than familiarity (57): P(x) is assertable at s57, every possibility subsisting in the positive update, although x is not familiar there.

Distributive inferences with anaphora (§5.2)

theorem ElliottSudo2025.distributive_preconditions {W : Type u_1} {E : Type u_2} {s : BUSState W E} (φ ψ : BUSDen W E) (y : ℕ) (h : Possible (BilateralDen.forall_ y (φ ∨ᶠᶜ ψ)) s) : Set.Nonempty (disjPos1 φ ψ (DynamicSemantics.State.randomAssign s y)) ∧ Set.Nonempty (disjPos2 φ ψ (DynamicSemantics.State.randomAssign s y))

(121): a possible universal over a modal disjunction has both parts consistent at the random-assignment update, so some individual verifies the first disjunct and some the second.

Negative free choice (§5.4)

def ElliottSudo2025.conjNeg1 {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) (s : BUSState W E) : BUSState W E

The part of a conjunction's negative update the first conjunct is responsible for: the falsifying row of the Strong Kleene table (61).

Equations

• ElliottSudo2025.conjNeg1 φ ψ s = ψ.positive (φ.negative s) ∪ ψ.negative (φ.negative s) ∪ BilateralDen.unknownUpdate ψ (φ.negative s)

def ElliottSudo2025.conjNeg2 {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) (s : BUSState W E) : BUSState W E

The part the second conjunct is responsible for: the falsifying column.

Equations

• ElliottSudo2025.conjNeg2 φ ψ s = ψ.negative (φ.negative s) ∪ ψ.negative (φ.positive s) ∪ ψ.negative (BilateralDen.unknownUpdate φ s)

theorem ElliottSudo2025.conj_negative_eq {W : Type u_1} {E : Type u_2} {s : BUSState W E} (φ ψ : BUSDen W E) : (BilateralDen.conj φ ψ).negative s = conjNeg1 φ ψ s ∪ conjNeg2 φ ψ s

The negative update of conjunction (61) is the union of the two parts.

noncomputable def ElliottSudo2025.conjModal {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) : BUSDen W E

Negative modal conjunction (132): the negative update requires each conjunct to be responsible for some possibilities.

Equations

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

theorem ElliottSudo2025.negative_modal_conjunction {W : Type u_1} {E : Type u_2} {s : BUSState W E} (φ ψ : BUSDen W E) (h : Possible (BilateralDen.neg (conjModal φ ψ)) s) : Set.Nonempty (conjNeg1 φ ψ s) ∧ Set.Nonempty (conjNeg2 φ ψ s)

(130): a possible negated modal conjunction has both parts consistent.

theorem ElliottSudo2025.dual_permission {W : Type u_1} {E : Type u_2} {s : BUSState W E} (φ ψ : BUSDen W E) (hφ : DynamicSemantics.CCP.IsEliminative φ.positive) (hm : Monotone ψ.positive) (he : DynamicSemantics.CCP.IsEliminative ψ.positive) (h : Possible (BilateralDen.conj φ ψ) s) : Possible φ s ∧ Possible ψ s

Dual permission (131) holds for eliminative conjuncts with a monotone second conjunct: a possible conjunction has both conjuncts possible.

theorem ElliottSudo2025.negative_fc_with_anaphora {W : Type u_1} {E : Type u_2} {s : BUSState W E} {x : ℕ} [Nonempty E] (A B : E → W → Prop) (hx : DynamicSemantics.State.Novel s x) (h : Possible (BilateralDen.neg (conjModal (BilateralDen.exists_ x (BilateralDen.pred1 A x)) (BilateralDen.pred1 B x))) s) : ((BilateralDen.exists_ x (BilateralDen.pred1 A x)).negative s).Nonempty ∧ ((BilateralDen.pred1 B x).negative ((BilateralDen.exists_ x (BilateralDen.pred1 A x)).positive s)).Nonempty

Negative free choice with anaphora, (129): a possible not required that you include an appendix and keep it to a single page makes it possible that no appendix is included and possible that an appendix is included and not kept to a page.