Charlow (2020): the scope of alternatives

Charlow takes an indefinite to denote a set of individuals and lets it take scope through two type-shifters: η forms a singleton, and ≫= feeds the members of a set one by one to a scope and unions the results. They are the unit and bind of the set monad. Because bind is associative, an indefinite that takes scope at the edge of an island turns the island into a set of alternatives, and the island can then take scope in its turn, which gives exceptional scope without movement out of the island. Higher-order alternative sets let two indefinites on one island take scope independently, and once assignments are added to the monad, an indefinite whose restrictor holds a bound pronoun cannot outscope the pronoun's binder.

Main definitions

• closureCond, det, distr: the conditional (31), the determiners (65) and (84), and the distributivity operator (41), each closing off the alternatives of its scope.
• lawyerOuter, relativeOuter: the two higher-order islands of Figure 10.
• Si.pro, Si.beta, Si.det: pronouns (58), β-binding (61) and determiners over ReaderT (Assignment E) Set.
• Si.a, Si.that: the indefinite determiner (83) and the relative pronoun (87).
• Si.abstractChoice: abstraction by a choice function in alternative semantics (74).

Main results

• some_pure, bind_pure_left, plusWh_some: the extended Partee triangle of Figure 4 commutes.
• exceptional_scope, exceptional_ne_narrow: (33), and the exceptional reading of (1) is not the narrow one.
• every_island: pied-piping a universal's island gives nothing new (2).
• intermediate_scope, two_island: intermediate exceptional scope (3), and the distributive scope of a plural indefinite stays in its island (39).
• relative_wide, lawyer_wide, seminar_paper: selective exceptional scope, (43), (47), (49).
• lawyer_wide_not_pointwise: no function of the point-wise island meaning gives the lawyer-wide reading of (43).
• Si.expert_wide_bound: exceptional scope beside a bound pronoun (51).
• Si.paper_wide, Si.paper_narrow, Si.not_dependsOn_paper_wide: the Binder Roof Constraint of (53), Figure 14.
• Si.cf_reading_iff, Si.cf_reading_not_imp_bound: the choice-function reading (69) and its over-generation.
• Si.a_paper_that_she_wrote: the determiners of Appendix A derive (66).
• Si.nobody_met_iff: abstraction by a choice function over-generates (77).

Implementation notes

• η, ≫= and flattening are pure, >>= and joinM of mathlib's Set.monad, and the closure ⇓ (19) is sSup on Set Prop. Truth values are Prop, as in the paper's main text.
• The paper's conditional if : t → t → t is a parameter cond; the witnesses that separate readings use the material conditional. Pluralities are Finsets of atoms.
• A derivation is a term in the monad, and which constituent takes scope where is not represented, so a reading the paper rules out is shown to differ from the derived ones.
• Si.cf_reading_iff assumes that no two candidates wrote the same papers, which the paper's gloss of (69) needs and leaves implicit.
• Figure 9 prints die X for die x.

TODO

• (46), and point-wise composition with a closure inside the island (45) on (46) and (47).
• (79)–(82), (88), and Appendix B.

References

• [Cha20]
• [Cha14b]
• [Par87]
• [Rei97]
• [BF11]

theorem Charlow2020.sSup_iff_true_mem (m : Set Prop) : sSup m ↔ True ∈ m

The closure ⇓ (19), T ∈ m, is the supremum of a set of truth values.

The extended Partee triangle (Figure 4)

def Charlow2020.plusWh {α β : Type} (Q : Quantifier.NP α) (f : α → Set β) : Set β

plusWh Q is the +wh shifter (25), which turns a generalized quantifier into a scope-taker over sets.

Equations

• Charlow2020.plusWh Q f = {y : β | Q fun (x : α) => y ∈ f x}

theorem Charlow2020.some_pure {α : Type} (x : α) : Quantifier.GQ.some (pure x) = Quantifier.NP.individual x

Partee's A, existential closure over a set, sends a singleton to the Montague lift, A ∘ η = LIFT (24).

theorem Charlow2020.bind_pure_left {α β : Type} (x : α) : (fun (f : α → Set β) => pure x >>= f) = fun (f : α → Set β) => f x

Binding a singleton is the Montague lift at result type Set β, (≫=) ∘ η = LIFT (28).

theorem Charlow2020.plusWh_some {α β : Type} (m : Set α) : plusWh (Quantifier.GQ.some m) = fun (f : α → Set β) => m >>= f

Applying +wh to Partee's A gives bind, +wh ∘ A = (≫=) (29).

theorem Charlow2020.plusWh_individual {α β : Type} (x : α) : plusWh (Quantifier.NP.individual x) = fun (f : α → Set β) => f x

Applying +wh to the Montague lift gives the lift at result type Set β, the last face of Figure 4.

Exceptional scope

def Charlow2020.closureCond (cond : Prop → Prop → Prop) (m n : Set Prop) : Set Prop

closureCond cond m n is the conditional (31), {if m⇓ n⇓}, which closes off the alternatives of both arguments.

Equations

• Charlow2020.closureCond cond m n = pure (cond (sSup m) (sSup n))

def Charlow2020.det {E : Type} (D : Quantifier.GQ E) (P : Set E) (f : E → Set Prop) : Set Prop

det D P f is the determiner D over P closing off the alternatives of its scope f, as in (65) and (84) without assignments.

Equations

• Charlow2020.det D P f = pure (D (fun (x : E) => x ∈ P) fun (x : E) => sSup (f x))

theorem Charlow2020.exceptional_scope {E : Type} (cond : Prop → Prop → Prop) (rel : Set E) (dies : E → Prop) (house : Prop) : (do let p ← do let x ← rel pure (dies x) closureCond cond (pure p) (pure house)) = (fun (x : E) => cond (dies x) house) '' rel

Taking scope over its island, which then takes scope over the conditional, gives the indefinite exceptional scope, {if (dies x) house | rel x} (33), as in Examples.ex1.

theorem Charlow2020.exceptional_scope_eq_wide {E : Type} (cond : Prop → Prop → Prop) (rel : Set E) (dies : E → Prop) (house : Prop) : (do let p ← do let x ← rel pure (dies x) closureCond cond (pure p) (pure house)) = do let x ← rel closureCond cond (pure (dies x)) (pure house)

Pied-piping the island is scoping the indefinite out of it directly (Figure 7).

theorem Charlow2020.narrow_scope {E : Type} (cond : Prop → Prop → Prop) (rel : Set E) (dies : E → Prop) (house : Prop) : closureCond cond (do let x ← rel pure (dies x)) (pure house) = {cond (∃ x ∈ rel, dies x) house}

Closing the island off in the antecedent gives the narrow reading if ≫ ∃ (13).

theorem Charlow2020.every_island {E : Type} (cond : Prop → Prop → Prop) (rel : Set E) (dies : E → Prop) (house : Prop) : (do let p ← det Quantifier.GQ.every rel fun (x : E) => pure (dies x) closureCond cond (pure p) (pure house)) = closureCond cond (det Quantifier.GQ.every rel fun (x : E) => pure (dies x)) (pure house)

A universal closes its island off to a singleton, so pied-piping the island gives the narrow reading again (2), as in Examples.ex2.

theorem Charlow2020.intermediate_scope {E : Type} (rel student : Set E) (wrong : E → Prop) (argue : E → Prop → Prop) : (det Quantifier.GQ.every student fun (y : E) => do let p ← do let c ← rel pure (wrong c) pure (argue y p)) = {∀ y ∈ student, ∃ c ∈ rel, argue y (wrong c)}

The island of (3) can scope over three arguments showing that and stop below each student, as in Examples.ex3.

theorem Charlow2020.widest_scope {E : Type} (rel student : Set E) (wrong : E → Prop) (argue : E → Prop → Prop) : (do let p ← do let c ← rel pure (wrong c) det Quantifier.GQ.every student fun (y : E) => pure (argue y p)) = (fun (c : E) => ∀ y ∈ student, argue y (wrong c)) '' rel

The island of (3) can also scope over each student.

theorem Charlow2020.intermediate_ne_widest : ¬∀ (student rel : Set Bool) (wrong : Bool → Prop) (argue : Bool → Prop → Prop), sSup (det Quantifier.GQ.every student fun (y : Bool) => do let p ← do let c ← rel pure (wrong c) pure (argue y p)) ↔ sSup do let p ← do let c ← rel pure (wrong c) det Quantifier.GQ.every student fun (y : Bool) => pure (argue y p)

The intermediate and widest readings of (3) differ.

theorem Charlow2020.exceptional_ne_narrow : ¬∀ (rel : Set Bool) (dies : Bool → Prop) (house : Prop), (sSup do let p ← do let x ← rel pure (dies x) closureCond (fun (x1 x2 : Prop) => x1 → x2) (pure p) (pure house)) ↔ sSup (closureCond (fun (x1 x2 : Prop) => x1 → x2) (do let x ← rel pure (dies x)) (pure house))

The exceptional and narrow readings of (1) differ.

Plural indefinites

def Charlow2020.two {A : Type} (P : Set A) : Set (Finset A)

two P is the set of pluralities of two atoms of P, as two.rels (40).

Equations

• Charlow2020.two P = {X : Finset A | X.card = 2 ∧ ∀ x ∈ X, x ∈ P}

def Charlow2020.distr {A : Type} (f : A → Set Prop) (X : Finset A) : Set Prop

distr f is the distributivity operator ∆ (41), which requires every atom of a plurality to satisfy the closed scope f.

Equations

• Charlow2020.distr f X = pure (∀ x ∈ X, sSup (f x))

theorem Charlow2020.two_wrote_something {A : Type} (ling something : Set A) (wrote : A → A → Prop) : (two ling >>= distr fun (x : A) => do let y ← something pure (wrote y x)) = (fun (X : Finset A) => ∀ x ∈ X, ∃ y ∈ something, wrote y x) '' two ling

With ∆, two linguists wrote something gets its distributive reading (Figure 9, left).

theorem Charlow2020.two_island {A : Type} (cond : Prop → Prop → Prop) (house : Prop) (rel : Set A) (die : A → Prop) : (do let p ← two rel >>= distr fun (x : A) => pure (die x) closureCond cond (pure p) (pure house)) = (fun (X : Finset A) => cond (∀ x ∈ X, die x) house) '' two rel

In if two relatives of mine die the plural's existential scope leaves the island while ∆ stays inside it (Figure 9, right), as in Examples.ex39.

theorem Charlow2020.two_island_ne_distr_wide : ¬∀ (rel : Set Bool) (die : Bool → Prop) (house : Prop), (sSup do let p ← two rel >>= distr fun (x : Bool) => pure (die x) closureCond (fun (x1 x2 : Prop) => x1 → x2) (pure p) (pure house)) ↔ sSup (two rel >>= distr fun (x : Bool) => closureCond (fun (x1 x2 : Prop) => x1 → x2) (pure (die x)) (pure house))

The reading of (39) with ∆ above the conditional, which would need the plural to scope out of the island, differs from the derived one.

Selectivity

def Charlow2020.lawyerOuter {E : Type} (lawyer rel : Set E) (visits : E → E → Prop) : Set (Set Prop)

lawyerOuter is the higher-order island {{visits y x | rel y} | lawyer x} of Figure 10, left, with the lawyer in the outer layer.

Equations

• Charlow2020.lawyerOuter lawyer rel visits = do let x ← lawyer pure do let y ← rel pure (visits y x)

def Charlow2020.relativeOuter {E : Type} (lawyer rel : Set E) (visits : E → E → Prop) : Set (Set Prop)

relativeOuter is the higher-order island {{visits y x | lawyer x} | rel y} of Figure 10, right, with the relative in the outer layer.

Equations

• Charlow2020.relativeOuter lawyer rel visits = do let y ← rel pure do let x ← lawyer pure (visits y x)

theorem Charlow2020.both_wide {E : Type} (cond : Prop → Prop → Prop) (lawyer rel : Set E) (visits : E → E → Prop) (house : Prop) : (do let p ← do let x ← lawyer let y ← rel pure (visits y x) closureCond cond (pure p) (pure house)) = Set.image2 (fun (x y : E) => cond (visits y x) house) lawyer rel

Pied-piping the flat island scopes both indefinites over the conditional (44).

theorem Charlow2020.relative_wide {E : Type} (cond : Prop → Prop → Prop) (lawyer rel : Set E) (visits : E → E → Prop) (house : Prop) : (do let m ← relativeOuter lawyer rel visits closureCond cond m (pure house)) = (fun (y : E) => cond (∃ x ∈ lawyer, visits y x) house) '' rel

Pied-piping the island of Figure 10, right, scopes the relative above the conditional and reconstructs the lawyer below it, (49) and Figure 11.

theorem Charlow2020.lawyer_wide {E : Type} (cond : Prop → Prop → Prop) (lawyer rel : Set E) (visits : E → E → Prop) (house : Prop) : (do let m ← lawyerOuter lawyer rel visits closureCond cond m (pure house)) = (fun (x : E) => cond (∃ y ∈ rel, visits y x) house) '' lawyer

Pied-piping the island of Figure 10, left, scopes the lawyer above the conditional and reconstructs the relative below it (section 5.3).

theorem Charlow2020.joinM_lawyerOuter {E : Type} (lawyer rel : Set E) (visits : E → E → Prop) : joinM (lawyerOuter lawyer rel visits) = pure visits <*> rel <*> lawyer

Flattening a higher-order island gives the point-wise island (11) and forgets the layers.

theorem Charlow2020.joinM_relativeOuter {E : Type} (lawyer rel : Set E) (visits : E → E → Prop) : joinM (relativeOuter lawyer rel visits) = pure visits <*> rel <*> lawyer

Flattening the other higher-order island gives the same point-wise island.

theorem Charlow2020.seminar_paper {E : Type} (cond : Prop → Prop → Prop) (grad seminar paper : Set E) (disc : E → E → Prop) (joy : E → Prop) : (do let m ← do let s ← seminar pure do let p ← paper pure (disc p s) det Quantifier.GQ.every grad fun (g : E) => do let q ← m closureCond cond (pure q) (pure (joy g))) = (fun (s : E) => ∀ g ∈ grad, ∃ p ∈ paper, cond (disc p s) (joy g)) '' seminar

In (47) the seminar scopes above every grad and the paper reconstructs between every grad and the conditional, as in Examples.ex47.

theorem Charlow2020.lawyer_wide_ne_relative_wide : ¬∀ (visits : Fin 4 → Fin 4 → Prop), (sSup do let m ← lawyerOuter {0, 1} {2, 3} visits closureCond (fun (x1 x2 : Prop) => x1 → x2) m (pure False)) ↔ sSup do let m ← relativeOuter {0, 1} {2, 3} visits closureCond (fun (x1 x2 : Prop) => x1 → x2) m (pure False)

The two selective readings of (43) differ, as in Examples.ex43.

theorem Charlow2020.lawyer_wide_not_pointwise : ¬∃ (F : Set Prop → Prop), ∀ (visits : Fin 4 → Fin 4 → Prop), F (pure visits <*> {2, 3} <*> {0, 1}) ↔ sSup do let m ← lawyerOuter {0, 1} {2, 3} visits closureCond (fun (x1 x2 : Prop) => x1 → x2) m (pure False)

No function of the point-wise island meaning gives the lawyer-wide reading of (43), since two visiting relations with the same point-wise island differ on it (section 5.4).

Assignments

The monad of (54)–(56) is ReaderT (Assignment E) Set, whose membership lemmas come from the Reader.Set monad of Charlow2014.

@[simp]

theorem Charlow2020.Si.monadLift_apply {E α : Type} (m : Set α) (g : Assignment E) : monadLift m g = m

def Charlow2020.Si.pro {E : Type} (n : ℕ) : ReaderT (Assignment E) Set E

pro n is the pronoun she_n (58), the singleton of the value of index n.

Equations

• Charlow2020.Si.pro n g = {HeimKratzer.interpPronoun n g}

@[simp]

theorem Charlow2020.Si.pro_apply {E : Type} (n : ℕ) (g : Assignment E) : pro n g = {g n}

def Charlow2020.Si.beta {E α : Type} (n : ℕ) (f : E → ReaderT (Assignment E) Set α) (x : E) : ReaderT (Assignment E) Set α

beta n f x is the binder βⁿ (61), which evaluates the scope f x with index n anchored to x.

Equations

• Charlow2020.Si.beta n f x = withReader (fun (x_1 : ℕ → E) => Function.update x_1 n x) (f x)

@[simp]

theorem Charlow2020.Si.beta_apply {E α : Type} (n : ℕ) (f : E → ReaderT (Assignment E) Set α) (x : E) (g : Assignment E) : beta n f x g = f x (Function.update g n x)

def Charlow2020.Si.det {E : Type} (D : Quantifier.GQ E) (P : Set E) (f : E → ReaderT (Assignment E) Set Prop) : ReaderT (Assignment E) Set Prop

det D P f is the determiner D over P closing off its scope f at each assignment, as everybody (65) and the no candidate of Figure 14 do.

Equations

• Charlow2020.Si.det D P f g = pure (D (fun (x : E) => x ∈ P) fun (y : E) => sSup (f y g))

theorem Charlow2020.Si.ling_cited_her {E : Type} (ling : Set E) (cited : E → E → Prop) : (do let x ← monadLift ling let y ← pro 0 pure (cited y x)) = fun (g : Assignment E) => (fun (x : E) => cited (g 0) x) '' ling

A linguist cited her₀ leaves the pronoun free, (59) and Figure 12, left.

theorem Charlow2020.Si.ling_cited_herself {E : Type} (ling : Set E) (cited : E → E → Prop) : (monadLift ling >>= beta 0 fun (x : E) => do let y ← pro 0 pure (cited y x)) = fun (x : Assignment E) => (fun (x : E) => cited x x) '' ling

In a linguist β⁰ cited herself₀ the pronoun is bound, and the meaning is the same at every assignment (Figure 12, right).

def Charlow2020.Si.expertCites {E : Type} (exp : Set E) (cites : E → E → Prop) : ReaderT (Assignment E) Set (ReaderT (Assignment E) Set Prop)

expertCites is the higher-order island a famous expert on indefinites cites her₀ of Figure 13, left, with the indefinite in the outer layer and the pronoun in the inner.

Equations

• Charlow2020.Si.expertCites exp cites = do let x ← monadLift exp pure do let y ← Charlow2020.Si.pro 0 pure (cites y x)

theorem Charlow2020.Si.expert_wide_bound {E : Type} (exp human : Set E) (cites : E → E → Prop) (lovesWhen : Prop → E → Prop) : (do let m ← expertCites exp cites det Quantifier.GQ.every human (beta 0 fun (y : E) => do let p ← m pure (lovesWhen p y))) = fun (x : Assignment E) => (fun (x : E) => ∀ y ∈ human, lovesWhen (cites y x) y) '' exp

Pied-piping the island over everybody while its inner layer reconstructs under β⁰ gives the indefinite scope over everybody and binds the pronoun, (51) and Figure 13, right, as in Examples.ex51.

The Binder Roof Constraint

def Charlow2020.Si.paperBy {E : Type} (paper : Set E) (wrote : E → E → Prop) : ReaderT (Assignment E) Set E

paperBy paper wrote is a paper he₀ had written (66), the papers written by the value of index 0.

Equations

• Charlow2020.Si.paperBy paper wrote g = {x : E | x ∈ paper ∧ wrote x (g 0)}

theorem Charlow2020.Si.paper_wide {E : Type} (cand paper : Set E) (wrote subm : E → E → Prop) : (do let x ← paperBy paper wrote det Quantifier.GQ.no cand (beta 0 fun (y : E) => pure (subm x y))) = fun (g : Assignment E) => (fun (x : E) => ¬∃ y ∈ cand, subm x y) '' {x : E | x ∈ paper ∧ wrote x (g 0)}

Scoped over no candidate, the indefinite leaves its pronoun free (Figure 14).

theorem Charlow2020.Si.paper_wide_beta {E : Type} (cand paper : Set E) (wrote subm : E → E → Prop) : (do let x ← paperBy paper wrote det Quantifier.GQ.no cand (beta 0 fun (y : E) => pure (subm x y))) = do let x ← paperBy paper wrote det Quantifier.GQ.no cand fun (y : E) => pure (subm x y)

Below the indefinite, β⁰ does nothing (Figure 14).

theorem Charlow2020.Si.dependsOn_paper_wide {E : Type} (cand paper : Set E) (wrote subm : E → E → Prop) : DependsOn (do let x ← paperBy paper wrote det Quantifier.GQ.no cand (beta 0 fun (y : E) => pure (subm x y))) {0}

The wide reading reads the pronoun's index.

theorem Charlow2020.Si.paper_narrow {E : Type} (cand paper : Set E) (wrote subm : E → E → Prop) : det Quantifier.GQ.no cand (beta 0 fun (y : E) => do let x ← paperBy paper wrote pure (subm x y)) = fun (x : Assignment E) => {¬∃ y ∈ cand, ∃ x ∈ paper, wrote x y ∧ subm x y}

Below β⁰ the indefinite has its pronoun bound, and the reading is the same at every assignment, as in Examples.ex53.

theorem Charlow2020.Si.dependsOn_paper_narrow {E : Type} (cand paper : Set E) (wrote subm : E → E → Prop) : DependsOn (det Quantifier.GQ.no cand (beta 0 fun (y : E) => do let x ← paperBy paper wrote pure (subm x y))) ∅

The narrow reading depends on no index.

theorem Charlow2020.Si.not_dependsOn_paper_wide : ¬DependsOn (do let x ← paperBy Set.univ fun (x y : Bool) => y = true det Quantifier.GQ.no Set.univ (beta 0 fun (y : Bool) => pure (x = y))) ∅

The wide reading does depend on the pronoun, so it is not the bound reading.

theorem Charlow2020.Si.cf_reading_iff {E : Type} (cand paper : Set E) (wrote subm : E → E → Prop) [Nonempty E] (hwrote : ∀ x ∈ cand, ∃ y ∈ paper, wrote y x) (hinj : Set.InjOn (fun (x y : E) => y ∈ paper ∧ wrote y x) cand) : (∃ (f : Reference.ChoiceFunction E), ¬∃ x ∈ cand, subm (f fun (y : E) => y ∈ paper ∧ wrote y x) x) ↔ ¬∃ x ∈ cand, ∀ y ∈ paper, wrote y x → subm y x

With a choice function (67), the reading (69) of (53) holds exactly when no candidate submitted every paper she wrote, given that every candidate wrote a paper and no two wrote the same ones.

theorem Charlow2020.Si.cf_reading_not_imp_bound : ¬∀ (cand paper : Set (Fin 3)) (wrote subm : Fin 3 → Fin 3 → Prop) (g : Assignment (Fin 3)), (∃ (f : Reference.ChoiceFunction (Fin 3)), ¬∃ x ∈ cand, subm (f fun (y : Fin 3) => y ∈ paper ∧ wrote y x) x) → sSup (det Quantifier.GQ.no cand (beta 0 fun (y : Fin 3) => do let x ← paperBy paper wrote pure (subm x y)) g)

The reading (69) over-generates, since it does not entail the bound reading of (53), which fails when the one candidate wrote two papers and submitted one.

Building the indefinite (Appendix A)

def Charlow2020.Si.a {E : Type} (f : E → ReaderT (Assignment E) Set Prop) : ReaderT (Assignment E) Set E

a f is the indefinite determiner (83), the set of individuals whose restrictor f holds.

Equations

• Charlow2020.Si.a f g = {x : E | sSup (f x g)}

def Charlow2020.Si.that {E : Type} (r l : ReaderT (Assignment E) Set Prop) : ReaderT (Assignment E) Set Prop

that r l is the relative pronoun (87), which conjoins two assignment-relative sets of propositions.

Equations

• Charlow2020.Si.that r l g = Set.image2 (fun (x1 x2 : Prop) => x1 ∧ x2) (l g) (r g)

theorem Charlow2020.Si.a_pure {E : Type} (ling : Set E) : (a fun (x : E) => pure (x ∈ ling)) = monadLift ling

The determiner scoping over its noun gives the set-denoting indefinite (85).

theorem Charlow2020.Si.a_paper_that_she_wrote {E : Type} (paper : Set E) (wrote : E → E → Prop) : a (beta 1 fun (x : E) => that (do let z ← pro 1 let w ← pro 0 pure (wrote z w)) (pure (x ∈ paper))) = paperBy paper wrote

A paper (that) she₀ had written, with β¹ binding the gap, is (66) (Figure 15, right).

Binding in alternative semantics

def Charlow2020.Si.abstractChoice {E : Type} (n : ℕ) (m : ReaderT (Assignment E) Set Prop) : ReaderT (Assignment E) Set (E → Prop)

abstractChoice n m is abstraction over index n in alternative semantics (74), in which a choice function flattens the alternatives of m at each value of the index.

Equations

• Charlow2020.Si.abstractChoice n m g = Set.range fun (f : Reference.ChoiceFunction Prop) (x : E) => f fun (x_1 : Prop) => x_1 ∈ m (Function.update g n x)

theorem Charlow2020.Si.nobody_met_iff {E : Type} (human phon : Set E) (met : E → E → Prop) (hphon : phon.Nonempty) (g : Assignment E) : sSup ((fun (P : E → Prop) => ¬∃ x ∈ human, P x) '' abstractChoice 0 (fun (g : Assignment E) => (fun (y : E) => met y (g 0)) '' phon) g) ↔ ¬∃ x ∈ human, ∀ y ∈ phon, met y x

Composed point-wise with the abstraction (74), nobody [λ₀ t₀ met a phonologist] has a true alternative exactly when nobody met every phonologist (77).