Del Pinal, Bassi and Sauerland (2024): Free choice and presuppositional exhaustification

Del Pinal, Bassi and Sauerland's operator pex^{IE+II} asserts its prejacent and presupposes that the relevant includable alternatives are homogeneous. On ◇(p ∨ q) it presupposes ◇p ↔ ◇q, so free choice is the presupposition and the assertion together, while negation denies only the assertion and leaves double prohibition. The flat exh^{IE+II} of Bar-Lev and Fox yields the same overall content without the split, and the paper's puzzles about free choice under negative factives, in disjunctions and under quantifiers all turn on the split.

Main results

• basic_scalar: pex presupposes the negation of a non-entailed alternative, (11a).
• free_choice, double_prohibition, negative_free_choice, negative_free_choice_under_negation: the readings (14), (16), (19a) and (20), exactly.
• pexPossOr_eq_barePlural, homogeneity_gap: pex[◇(p ∨ q)] is Križ's homogeneous plural predication over the disjuncts, the structure the paper compares with Goldstein's in §2.2, with the presupposition failures of fn. 2.
• pex_and_exh_agree: with every alternative relevant, pex and exh agree, (12e)–(13).
• free_choice_presupposed, unaware_disbelieves_each_disjunct: negative factives, §3.
• free_choice_filtered, negative_free_choice_filtered: Karttunen's filtering disjunction filters free choice, (53), (57c), unlike flat exh or local accommodation.
• universal_free_choice, universal_double_prohibition, existential_free_choice_bound, exactly_one_free_choice: free choice under quantifiers, with Fox's strong Kleene existential for (75) and the readings of Gotzner, Romoli and Santorio for (83), (84).

Implementation notes

Each pex uses the paper's relevance set, which leaves out the conjunctive alternative of ◇(p ∨ q) and the disjunctive one of □(p ∧ q); with every alternative relevant, ¬pex[□(T ∧ B)] would entail ¬□(T ∨ B). ¬□(p ∧ q) is rendered as ◇(¬p ∨ ¬q). The witness hypotheses supply the worlds that make the alternatives independent, which the paper assumes implicitly. Negation is - on trivalent propositions and the filtering disjunction (45) is Middle Kleene SignType.joinMiddle. Negative factives use the transparent projection rule (30b), as ConventionalImplicature.TwoDim.negFactive does, on pex read as a two-dimensional meaning, since the factive denies belief in the at-issue prejacent. Quantifiers over S project the presupposition universally, as the Weak Kleene quantifiers over the subtype of S, and exactly one is ∃! with the same projection.

References

• [DPBS24]
• [BLF20]
• [GRS20]
• [Gol19]
• [Kri16]
• [Fox13]
• [Kar73]

Basic scalar sentences, §2.1

theorem DelPinalBassiSauerland2024.basic_scalar {W : Type u_1} {φ ψ : Set W} (h : ¬φ ⊆ ψ) {w : W} : Exhaustification.pexIEII {φ, ψ} φ {φ, ψ} w ≠ 0 ↔ w ∉ ψ

On a prejacent with one other alternative, which it does not entail, as some has all, pex^{IE+II} presupposes that the alternative is false, (10)–(11a).

pex^{IE+II} on ◇(p ∨ q), §2.2

noncomputable def DelPinalBassiSauerland2024.pexPossOr {W : Type u_1} (R : SetRel W W) (a b : Set W) : W → SignType

pexPossOr R a b is pex^{IE+II}[◇(a ∨ b)] with the conjunctive alternative irrelevant, as in (12) and (14).

Equations

• DelPinalBassiSauerland2024.pexPossOr R a b = Exhaustification.pexIEII (BarLevFox2020.fcAlts R a b) (R.preimage (a ∪ b)) {R.preimage (a ∪ b), R.preimage a, R.preimage b}

theorem DelPinalBassiSauerland2024.double_prohibition {W : Type u_1} {R : SetRel W W} {a b : Set W} {w : W} : pexPossOr R a b w = -1 ↔ w ∉ R.preimage a ∧ w ∉ R.preimage b

Negation denies the prejacent of pex^{IE+II}[◇(a ∨ b)] and leaves its presupposition, so pex is false, and its negation true, exactly where double prohibition holds, (16); the presupposition holds there whatever the includable alternatives are.

theorem DelPinalBassiSauerland2024.II_fcAlts_sdiff {W : Type u_1} {R : SetRel W W} {a b : Set W} (hF : BarLevFox2020.FreeChoiceWitnesses R a b) : Exhaustification.II (BarLevFox2020.fcAlts R a b) (R.preimage (a ∪ b)) \ {R.preimage (a ∪ b)} = {R.preimage a, R.preimage b}

Apart from the prejacent, the innocently includable alternatives of ◇(a ∨ b) are ◇a and ◇b, (12d).

theorem DelPinalBassiSauerland2024.pexPossOr_ne_zero_iff {W : Type u_1} {R : SetRel W W} {a b : Set W} {w : W} (hF : BarLevFox2020.FreeChoiceWitnesses R a b) : pexPossOr R a b w ≠ 0 ↔ (w ∈ R.preimage a ↔ w ∈ R.preimage b)

pex^{IE+II}[◇(a ∨ b)] presupposes ◇a ↔ ◇b, (14); its one excludable alternative, ◇(a ∧ b) (12c), is irrelevant.

theorem DelPinalBassiSauerland2024.free_choice {W : Type u_1} {R : SetRel W W} {a b : Set W} {w : W} (hF : BarLevFox2020.FreeChoiceWitnesses R a b) : pexPossOr R a b w = 1 ↔ w ∈ R.preimage a ∧ w ∈ R.preimage b

pex^{IE+II}[◇(a ∨ b)] is true exactly where free choice holds, (14), since ◇(a ∨ b) lies between ◇a ∧ ◇b and ◇a ∨ ◇b.

theorem DelPinalBassiSauerland2024.pexPossOr_eq_barePlural {W : Type u_1} {R : SetRel W W} {a b : Set W} (hF : BarLevFox2020.FreeChoiceWitnesses R a b) : pexPossOr R a b = Homogeneity.barePlural (fun (x : Set W) (w : W) => w ∈ R.preimage x) {a, b}

pex^{IE+II}[◇(a ∨ b)] is the plural predication that a and b are permitted, true where both are, false where neither is, and undefined in between.

theorem DelPinalBassiSauerland2024.homogeneity_gap {W : Type u_1} {R : SetRel W W} {a b : Set W} (hF : BarLevFox2020.FreeChoiceWitnesses R a b) : Trivalent.gapExt (pexPossOr R a b) = symmDiff (R.preimage a) (R.preimage b)

pex^{IE+II}[◇(a ∨ b)] is undefined exactly where one of ◇a and ◇b holds without the other, the presupposition failure fn. 2 predicts.

theorem DelPinalBassiSauerland2024.homogeneity_gap_neg {W : Type u_1} {R : SetRel W W} {a b : Set W} (hF : BarLevFox2020.FreeChoiceWitnesses R a b) : Trivalent.gapExt (-pexPossOr R a b) = symmDiff (R.preimage a) (R.preimage b)

The negation ¬pex^{IE+II}[◇(a ∨ b)] is undefined at the same worlds, fn. 2.

theorem DelPinalBassiSauerland2024.gapExt_pexPossOr_nonempty {W : Type u_1} {R : SetRel W W} {a b : Set W} (hF : BarLevFox2020.FreeChoiceWitnesses R a b) : (Trivalent.gapExt (pexPossOr R a b)).Nonempty

A world permitting only a lies in the gap of pex^{IE+II}[◇(a ∨ b)].

theorem DelPinalBassiSauerland2024.pex_and_exh_agree {W : Type u_1} {R : SetRel W W} {a b : Set W} {w : W} (hF : BarLevFox2020.FreeChoiceWitnesses R a b) : Exhaustification.pexIEII (BarLevFox2020.fcAlts R a b) (R.preimage (a ∪ b)) (BarLevFox2020.fcAlts R a b) w = 1 ↔ w ∈ Exhaustification.exhIEII (BarLevFox2020.fcAlts R a b) (R.preimage (a ∪ b))

With every alternative relevant, pex^{IE+II}[◇(a ∨ b)] is true exactly where exh^{IE+II}[◇(a ∨ b)] is, (12e) and (13); the two differ only in what they presuppose.

theorem DelPinalBassiSauerland2024.fcAlts_compl {W : Type u_1} (R : SetRel W W) (T B : Set W) : BarLevFox2020.fcAlts R Tᶜ Bᶜ = {(R.core (T ∩ B))ᶜ, (R.core T)ᶜ, (R.core B)ᶜ, (R.core (T ∪ B))ᶜ}

The alternatives of ◇(¬T ∨ ¬B) are those of ¬□(T ∧ B) in (18b).

theorem DelPinalBassiSauerland2024.negative_free_choice {W : Type u_1} {R : SetRel W W} {w : W} {T B : Set W} (hF : BarLevFox2020.FreeChoiceWitnesses R Tᶜ Bᶜ) : pexPossOr R Tᶜ Bᶜ w = 1 ↔ w ∉ R.core T ∧ w ∉ R.core B

pex^{IE+II}[¬□(T ∧ B)] is true exactly where negative free choice holds, (18) and (19a).

pex^{IE+II} on □(p ∧ q), §2.2

def DelPinalBassiSauerland2024.necAlts {W : Type u_1} (R : SetRel W W) (T B : Set W) : Set (Set W)

The alternatives of □(T ∧ B) replace the conjunction by its conjuncts and their disjunction.

Equations

• DelPinalBassiSauerland2024.necAlts R T B = {R.core (T ∩ B), R.core T, R.core B, R.core (T ∪ B)}

noncomputable def DelPinalBassiSauerland2024.pexNecAnd {W : Type u_1} (R : SetRel W W) (T B : Set W) : W → SignType

pexNecAnd R T B is pex^{IE+II}[□(T ∧ B)] with the disjunctive alternative irrelevant, as in (20) and (57).

Equations

• DelPinalBassiSauerland2024.pexNecAnd R T B = Exhaustification.pexIEII (DelPinalBassiSauerland2024.necAlts R T B) (R.core (T ∩ B)) {R.core (T ∩ B), R.core T, R.core B}

theorem DelPinalBassiSauerland2024.subset_of_mem_necAlts {W : Type u_1} {R : SetRel W W} {T B q : Set W} (hq : q ∈ necAlts R T B) : R.core (T ∩ B) ⊆ q

□(T ∧ B) entails each of its alternatives.

theorem DelPinalBassiSauerland2024.exhIEII_necAlts {W : Type u_1} {R : SetRel W W} {T B : Set W} (h : (R.core (T ∩ B)).Nonempty) : Exhaustification.exhIEII (necAlts R T B) (R.core (T ∩ B)) = R.core (T ∩ B)

□(T ∧ B) entails its alternatives, so exh^{IE+II} is vacuous on it, (56).

theorem DelPinalBassiSauerland2024.not_isInnocentlyExcludable_necAlts {W : Type u_1} {R : SetRel W W} {T B : Set W} (h : (R.core (T ∩ B)).Nonempty) (q : Set W) : ¬Exhaustification.IsInnocentlyExcludable (necAlts R T B) (R.core (T ∩ B)) q

No alternative of □(T ∧ B) is excludable.

theorem DelPinalBassiSauerland2024.II_necAlts_sdiff {W : Type u_1} {R : SetRel W W} {T B : Set W} (h₁ : ∃ w ∈ R.core T, w ∉ R.core B) (h₂ : ∃ w ∈ R.core B, w ∉ R.core T) (h : (R.core (T ∩ B)).Nonempty) : Exhaustification.II (necAlts R T B) (R.core (T ∩ B)) \ {R.core (T ∩ B)} = {R.core T, R.core B, R.core (T ∪ B)}

Apart from the prejacent, every alternative of □(T ∧ B) is innocently includable, (20).

theorem DelPinalBassiSauerland2024.pexNecAnd_ne_zero_iff {W : Type u_1} {R : SetRel W W} {T B : Set W} (h₁ : ∃ w ∈ R.core T, w ∉ R.core B) (h₂ : ∃ w ∈ R.core B, w ∉ R.core T) (h : (R.core (T ∩ B)).Nonempty) {w : W} : pexNecAnd R T B w ≠ 0 ↔ (w ∈ R.core T ↔ w ∈ R.core B)

pex^{IE+II}[□(T ∧ B)] presupposes □T ↔ □B, (20).

theorem DelPinalBassiSauerland2024.negative_free_choice_under_negation {W : Type u_1} {R : SetRel W W} {T B : Set W} (h₁ : ∃ w ∈ R.core T, w ∉ R.core B) (h₂ : ∃ w ∈ R.core B, w ∉ R.core T) (h : (R.core (T ∩ B)).Nonempty) {w : W} : pexNecAnd R T B w = -1 ↔ w ∉ R.core T ∧ w ∉ R.core B

The homogeneity □T ↔ □B projects out of the negation of the strong prejacent, so pex^{IE+II}[□(T ∧ B)] is false, and its negation true, exactly where negative free choice holds, (20).

Free choice under negative factives, §3

def DelPinalBassiSauerland2024.pexPossOrTwoDim {W : Type u_1} (R : SetRel W W) (a b : Set W) : ConventionalImplicature.TwoDim W (W → Prop)

pex^{IE+II}[◇(a ∨ b)] as a two-dimensional meaning, with the prejacent ◇(a ∨ b) at issue and the presupposition of pexPossOr not at issue. A negative factive denies belief in the at-issue content, which it reads apart from the presupposition.

Equations

• DelPinalBassiSauerland2024.pexPossOrTwoDim R a b = { atIssue := fun (x : W) => x ∈ R.preimage (a ∪ b), notAtIssue := fun (x : W) => DelPinalBassiSauerland2024.pexPossOr R a b x ≠ 0 }

theorem DelPinalBassiSauerland2024.toTrivalent_pexPossOrTwoDim {W : Type u_1} {R : SetRel W W} {a b : Set W} : (pexPossOrTwoDim R a b).toTrivalent = pexPossOr R a b

The two-dimensional meaning collapses to pexPossOr.

theorem DelPinalBassiSauerland2024.free_choice_presupposed {W : Type u_1} {R : SetRel W W} {a b : Set W} {w : W} (hF : BarLevFox2020.FreeChoiceWitnesses R a b) (believes : (W → Prop) → W → Prop) : ((pexPossOrTwoDim R a b).negFactive believes).notAtIssue w ↔ w ∈ R.preimage a ∧ w ∈ R.preimage b

Under a negative factive the whole output of pex is presupposed, and that is free choice, (21a) and (31c).

theorem DelPinalBassiSauerland2024.negative_free_choice_presupposed {W : Type u_1} {R : SetRel W W} {w : W} {T B : Set W} (hF : BarLevFox2020.FreeChoiceWitnesses R Tᶜ Bᶜ) (believes : (W → Prop) → W → Prop) : ((pexPossOrTwoDim R Tᶜ Bᶜ).negFactive believes).notAtIssue w ↔ w ∉ R.core T ∧ w ∉ R.core B

Under a negative factive pex^{IE+II}[¬□(T ∧ B)] presupposes negative free choice, (33a) and (34c).

theorem DelPinalBassiSauerland2024.unaware_disbelieves_each_disjunct {W : Type u_1} {R : SetRel W W} {a b : Set W} {w : W} (R' : SetRel W W) (hw : ((pexPossOrTwoDim R a b).negFactive (ModalLogic.Box R')).atIssue w) : ¬ModalLogic.Box R' (fun (x : W) => x ∈ R.preimage a) w ∧ ¬ModalLogic.Box R' (fun (x : W) => x ∈ R.preimage b) w

The assertion of a negative factive denies belief in the prejacent ◇(a ∨ b), hence belief in either disjunct, (21b) and (31d′); at Tᶜ and Bᶜ this is (33b) and (34d).

theorem DelPinalBassiSauerland2024.exh_unaware_too_weak {W : Type u_1} {R : SetRel W W} {a b : Set W} {w : W} (hF : BarLevFox2020.FreeChoiceWitnesses R a b) : ∃ (R' : SetRel W W), ModalLogic.Box R' (fun (x : W) => x ∈ R.preimage a) w ∧ ¬ModalLogic.Box R' (fun (x : W) => x ∈ Exhaustification.exhIEII (BarLevFox2020.fcAlts R a b) (R.preimage (a ∪ b))) w

With a flat exh complement the factive only denies belief in the strengthened content, which an attitude holder who believes Olivia can take Logic but not Algebra satisfies, so the target reading that he believes neither is missed, (24a).

Filtering free choice, §4

theorem DelPinalBassiSauerland2024.free_choice_filtered {W : Type u_1} {R : SetRel W W} {a b A B : Set W} {C : W → SignType} (hA : a ⊆ A) (hB : b ⊆ B) (hF : BarLevFox2020.FreeChoiceWitnesses R a b) (hC : Function.support C = R.preimage A ∩ R.preimage B) : (Function.support fun (w : W) => (-pexPossOr R a b w).joinMiddle (C w)) = Function.support (pexPossOr R a b)

In ¬pex[◇(a ∨ b)] ∨ C, with C presupposing ◇A ∧ ◇B for a ⊆ A and b ⊆ B, the filtering disjunction (45) filters the free-choice presupposition, since the negation of the first disjunct is free choice, and only the homogeneity of the first disjunct projects, (53) and §4.4.

theorem DelPinalBassiSauerland2024.no_filtering_without_pex {W : Type u_1} {R : SetRel W W} {a b A B : Set W} {C : W → SignType} (hC : Function.support C = R.preimage A ∩ R.preimage B) (hw : ∃ w ∈ R.preimage a, w ∉ R.preimage B) : ∃ (w : W), (-SignType.ofProp (w ∈ R.preimage (a ∪ b))).joinMiddle (C w) = 0

Without exhaustification under the negation, the antecedent of the conditional presupposition is only ◇(a ∨ b), and a world permitting a but not B refutes it, (46c).

theorem DelPinalBassiSauerland2024.exh_filters {W : Type u_1} {R : SetRel W W} {a b A B : Set W} {C : W → SignType} (hA : a ⊆ A) (hB : b ⊆ B) (hF : BarLevFox2020.FreeChoiceWitnesses R a b) (hC : Function.support C = R.preimage A ∩ R.preimage B) (w : W) : (-SignType.ofProp (w ∈ Exhaustification.exhIEII (BarLevFox2020.fcAlts R a b) (R.preimage (a ∪ b)))).joinMiddle (C w) ≠ 0

A flat exh under the negation filters the free-choice presupposition, (47c).

theorem DelPinalBassiSauerland2024.exh_loses_double_prohibition {W : Type u_1} {R : SetRel W W} {a b : Set W} (hF : BarLevFox2020.FreeChoiceWitnesses R a b) : ∃ w ∉ Exhaustification.exhIEII (BarLevFox2020.fcAlts R a b) (R.preimage (a ∪ b)), w ∈ R.preimage a

A flat exh under the negation loses double prohibition, since the negated exhaustified disjunction is compatible with permitting a, (47b).

theorem DelPinalBassiSauerland2024.negative_free_choice_filtered {W : Type u_1} {R : SetRel W W} {a b A B : Set W} {C : W → SignType} (hA : a ⊆ A) (hB : b ⊆ B) (h₁ : ∃ w ∈ R.core A, w ∉ R.core B) (h₂ : ∃ w ∈ R.core B, w ∉ R.core A) (h : (R.core (A ∩ B)).Nonempty) (hC : Function.support C = (R.core a)ᶜ ∩ (R.core b)ᶜ) : (Function.support fun (w : W) => (pexNecAnd R A B w).joinMiddle (C w)) = Function.support (pexNecAnd R A B)

In pex[□(A ∧ B)] ∨ C, with C presupposing ¬□a ∧ ¬□b, the negation of the first disjunct is negative free choice for A and B, which entails that presupposition, so it is filtered and only the homogeneity □A ↔ □B projects, (57c).

theorem DelPinalBassiSauerland2024.no_negative_filtering_with_exh {W : Type u_1} {R : SetRel W W} {a b A B : Set W} {C : W → SignType} (h : (R.core (A ∩ B)).Nonempty) (hC : Function.support C = (R.core a)ᶜ ∩ (R.core b)ᶜ) (hw : ∃ w ∈ R.core a, w ∉ R.core B) : ∃ (w : W), (SignType.ofProp (w ∈ Exhaustification.exhIEII (necAlts R A B) (R.core (A ∩ B)))).joinMiddle (C w) = 0

Since exh^{IE+II} is vacuous on □(A ∧ B), the negation of the first disjunct is only ¬□(A ∧ B), and a world requiring a but not B refutes the filtering, (56c).

theorem DelPinalBassiSauerland2024.double_prohibition_accommodated {W : Type u_1} {R : SetRel W W} {a b : Set W} {w : W} : SignType.ofProp (-pexPossOr R a b w = 1) = 1 ↔ w ∉ R.preimage a ∧ w ∉ R.preimage b

Local accommodation over ¬pex[◇(a ∨ b)], Bochvar's assertion operator (acc(p_q) = q ∧ p), keeps double prohibition and stops homogeneity from projecting, (59c).

theorem DelPinalBassiSauerland2024.no_filtering_with_accommodation {W : Type u_1} {R : SetRel W W} {a b A B : Set W} {C : W → SignType} (hC : Function.support C = R.preimage A ∩ R.preimage B) (hw : ∃ w ∈ R.preimage a, w ∉ R.preimage B) : ∃ (w : W), (SignType.ofProp (-pexPossOr R a b w = 1)).joinMiddle (C w) = 0

After local accommodation the negation of the first disjunct is only ◇a ∨ ◇b, and a world permitting a but not B refutes the filtering, (59b).

Free choice under quantifiers, §5

noncomputable def DelPinalBassiSauerland2024.exactlyOne {W : Type u_1} {D : Type u_2} (S : D → Prop) (φ : D → W → SignType) : W → SignType

Exactly one x in S satisfies φ x, with universal projection. The sentence is defined where every instance in S is, and true where exactly one of them is true.

Equations

• DelPinalBassiSauerland2024.exactlyOne S φ = {w : W | ∀ (x : D), S x → φ x w ≠ 0}.indicator fun (w : W) => SignType.ofProp (∃! x : D, S x ∧ φ x w = 1)

theorem DelPinalBassiSauerland2024.universal_double_prohibition {W : Type u_1} {R : SetRel W W} {D : Type u_2} {S : D → Prop} {p q : D → Set W} {w : W} : (-Trivalent.existsWeak fun (x : { x : D // S x }) => pexPossOr R (p ↑x) (q ↑x) w) = 1 ↔ (¬∃ (x : D), S x ∧ w ∈ R.preimage (p x)) ∧ ¬∃ (x : D), S x ∧ w ∈ R.preimage (q x)

With universal projection, ¬∃x ∈ S[pex[◇(px ∨ qx)]] is true exactly where universal double prohibition holds, (70b) and (71), the reading the elided second sentence of (69) needs.

theorem DelPinalBassiSauerland2024.universal_free_choice {W : Type u_1} {R : SetRel W W} {D : Type u_2} {S : D → Prop} {p q : D → Set W} {w : W} (hF : ∀ (x : D), S x → BarLevFox2020.FreeChoiceWitnesses R (p x) (q x)) : (Trivalent.forallWeak fun (x : { x : D // S x }) => pexPossOr R (p ↑x) (q ↑x) w) = 1 ↔ (∀ (x : D), S x → w ∈ R.preimage (p x)) ∧ ∀ (x : D), S x → w ∈ R.preimage (q x)

With universal projection, ∀x ∈ S[pex[◇(px ∨ qx)]] is true exactly where universal free choice holds, (66a) and (67).

theorem DelPinalBassiSauerland2024.existential_free_choice {W : Type u_1} {R : SetRel W W} {D : Type u_2} {S : D → Prop} {p q : D → Set W} {w : W} (hF : ∀ (x : D), S x → BarLevFox2020.FreeChoiceWitnesses R (p x) (q x)) (hw : (Trivalent.existsWeak fun (x : { x : D // S x }) => pexPossOr R (p ↑x) (q ↑x) w) = 1) : ∃ (x : D), S x ∧ w ∈ R.preimage (p x) ∧ w ∈ R.preimage (q x)

With universal projection, ∃x ∈ S[pex[◇(px ∨ qx)]] gives existential free choice, (73) and (74).

theorem DelPinalBassiSauerland2024.existential_free_choice_bound {W : Type u_1} {R : SetRel W W} {D : Type u_2} {S : D → Prop} {p q : D → Set W} {w : W} (hF : ∀ (x : D), S x → BarLevFox2020.FreeChoiceWitnesses R (p x) (q x)) : (Trivalent.existsStrong fun (x : { x : D // S x }) => pexPossOr R (p ↑x) (q ↑x) w) = 1 ↔ ∃ (x : D), S x ∧ w ∈ R.preimage (p x) ∧ w ∈ R.preimage (q x)

With the presupposition bound by the existential, as in the strong Kleene existential Trivalent.existsStrong, ∃x ∈ S[pex[◇(px ∨ qx)]] is true exactly where existential free choice holds, (75).

theorem DelPinalBassiSauerland2024.exactly_one_free_choice {W : Type u_1} {R : SetRel W W} {D : Type u_2} {S : D → Prop} {p q : D → Set W} {w : W} (hF : ∀ (x : D), S x → BarLevFox2020.FreeChoiceWitnesses R (p x) (q x)) (hw : exactlyOne S (fun (x : D) => pexPossOr R (p x) (q x)) w = 1) : ∃ (x : D), S x ∧ (w ∈ R.preimage (p x) ∧ w ∈ R.preimage (q x)) ∧ ∀ (y : D), S y → y ≠ x → w ∉ R.preimage (p y) ∧ w ∉ R.preimage (q y)

Exactly one student can take Logic or Calculus says that one student has free choice and every other has double prohibition, (81), (83) and (76a).

theorem DelPinalBassiSauerland2024.exactly_one_double_prohibition {W : Type u_1} {R : SetRel W W} {D : Type u_2} {S : D → Prop} {p q : D → Set W} {w : W} (hF : ∀ (x : D), S x → BarLevFox2020.FreeChoiceWitnesses R (p x) (q x)) (hw : exactlyOne S (fun (x : D) => -pexPossOr R (p x) (q x)) w = 1) : ∃ (x : D), S x ∧ (w ∉ R.preimage (p x) ∧ w ∉ R.preimage (q x)) ∧ ∀ (y : D), S y → y ≠ x → w ∈ R.preimage (p y) ∧ w ∈ R.preimage (q y)

Exactly one student can't take Logic or Calculus says that one student has double prohibition and every other has free choice, (82), (84) and (77a).

theorem DelPinalBassiSauerland2024.universal_negative_free_choice {W : Type u_1} {R : SetRel W W} {D : Type u_2} {S : D → Prop} {p q : D → Set W} {w : W} (h₁ : ∀ (x : D), S x → ∃ w ∈ R.core (p x), w ∉ R.core (q x)) (h₂ : ∀ (x : D), S x → ∃ w ∈ R.core (q x), w ∉ R.core (p x)) (h : ∀ (x : D), S x → (R.core (p x ∩ q x)).Nonempty) : (-Trivalent.existsWeak fun (x : { x : D // S x }) => pexNecAnd R (p ↑x) (q ↑x) w) = 1 ↔ (¬∃ (x : D), S x ∧ w ∈ R.core (p x)) ∧ ¬∃ (x : D), S x ∧ w ∈ R.core (q x)

With universal projection, ¬∃x ∈ S[pex[□(px ∧ qx)]] is true exactly where universal negative free choice holds, (66b) and (68).