The Set Monad: Indeterminacy and Scope

@cite{charlow-2020}

Alternative-denoting expressions (indefinites, wh-words, focused elements) interact with their semantic context by taking scope. @cite{charlow-2020} shows that this can be accomplished by decomposing Partee's LIFT into two freely-applying type-shifters — η (unit, = IDENT generalized) and ⫝̸ (bind, = a polymorphic scope-taker) — that together form a monad over sets.

The set monad (S, η, ⫝̸) is the "indeterminacy" effect from @cite{bumford-charlow-2024}'s effect taxonomy. Its key property is ASSOCIATIVITY: because ⫝̸ is associative (monad law), indefinites can iteratively take scope out of nested islands via scopal pied-piping, without any island-violating movement.

Organization

• §1 Set monad operations: η (pure/unit), ⫝̸ (bind), map
• §2 Monad laws: left identity, right identity, ASSOCIATIVITY
• §3 Closure operators: ∃̣ (existential closure), if (conditional)
• §4 Bridge to Applicative.lean: setAp derives from setBind + setPure
• §5 LIFT decomposition: lift = A ∘ η (Partee's triangle, eq. 28)
• §6 Exceptional scope: ASSOCIATIVITY derives island-escaping readings

§1 Set monad operations

The set monad S a := a → Prop with:

• η x := {x} (singleton set)
• m ⫝̸ f := ⋃_{x ∈ m} f(x) (flatmap / bind)

These are eqs (16) and (27), generalized to arbitrary types (the paper uses S as abbreviation for Set).

def Semantics.Composition.SetMonad.eta {A : Type} (x : A) : A → Prop

η (unit): inject a value into a singleton set.

eq. (16): η := λp. {p}. Equivalent to setPure from Applicative.lean (shown in eta_eq_setPure).

Equations

• Semantics.Composition.SetMonad.eta x y = (y = x)

def Semantics.Composition.SetMonad.setBind {A B : Type} (m : A → Prop) (f : A → B → Prop) : B → Prop

⫝̸ (bind): monadic bind for sets.

eq. (27): m ⫝̸ f := ⋃_{x ∈ m} f(x). For each element a in the set m, apply f to get a new set, then take the union of all results.

Equations

• Semantics.Composition.SetMonad.setBind m f b = ∃ (a : A), m a ∧ f a b

def Semantics.Composition.SetMonad.setMap {A B : Type} (f : A → B) (m : A → Prop) : B → Prop

map for the set functor, derived from η and ⫝̸.

Equations

• Semantics.Composition.SetMonad.setMap f m = Semantics.Composition.SetMonad.setBind m fun (a : A) => Semantics.Composition.SetMonad.eta (f a)

§2 Monad laws

The three monad laws for (S, η, ⫝̸). ASSOCIATIVITY (the third law) is the key property: it guarantees that an indefinite can iteratively scope out of nested islands, and that the result is the same as if it had directly taken wide scope (§4.2, eq. 34).

theorem Semantics.Composition.SetMonad.set_left_identity {A B : Type} (x : A) (f : A → B → Prop) : setBind (eta x) f = f x

LEFT IDENTITY: η x ⫝̸ f = f x.

Applying the singleton {x} to a function f yields exactly f x. eq. (42), first law.

theorem Semantics.Composition.SetMonad.set_right_identity {A : Type} (m : A → Prop) : setBind m eta = m

RIGHT IDENTITY: m ⫝̸ η = m.

Binding a set with the singleton constructor recovers the original set. eq. (42), second law.

theorem Semantics.Composition.SetMonad.set_associativity {A B C : Type} (m : A → Prop) (f : A → B → Prop) (g : B → C → Prop) : setBind (setBind m f) g = setBind m fun (a : A) => setBind (f a) g

ASSOCIATIVITY: (m ⫝̸ f) ⫝̸ g = m ⫝̸ (λx. f x ⫝̸ g).

The central theorem of §4.2. Because ⫝̸ is associative, taking scope at the edge of an island (one application of ⫝̸) and then taking scope at the next level (another ⫝̸) is equivalent to taking scope directly out of the island. This is what generates exceptional scope readings without island-violating movement.

Concretely (eq. 34): (m ⫝̸ λx. f x) ⫝̸ g = m ⫝̸ (λx. f x ⫝̸ g) guarantees that the tree on the left of Figure 7 (local scope at the island edge, then further scope) equals the tree on the right (direct wide scope).

§3 Closure operators

Operations that discharge sets of alternatives, turning them into propositions or combining them with other sets.

• ∃̣ (existential closure): turns a set of truth values into a single truth value — true iff the set contains a true member.

def Semantics.Composition.SetMonad.existsClosure (m : Prop → Prop) : Prop

∃̣ (existential closure): a set of propositions is "true" iff it contains a true member.

eq. (19): m^∃̣ := T ∈ m. In classical set theory this checks whether True is literally in the set. In Lean's type theory, we use ∃ p, m p ∧ p (there exists a true member), which avoids propext issues when propositions are logically but not definitionally equal to True.

Equations

• Semantics.Composition.SetMonad.existsClosure m = ∃ (p : Prop), m p ∧ p

§4 Bridge to Applicative.lean

The set applicative (setPure, setAp) from Applicative.lean is a consequence of the set monad. This section proves that:

1. eta = setPure (same operation, same type)
2. setAp derives from setBind + eta (the standard monad→applicative derivation)

This makes precise observation that the pointwise composition of alternative semantics (the applicative ⊛) is strictly weaker than scope-taking composition (the monadic ⫝̸): the former is derivable from the latter, but not vice versa.

theorem Semantics.Composition.SetMonad.eta_eq_setPure {A : Type} (x : A) : eta x = Applicative.setPure x

eta and setPure are the same operation.

theorem Semantics.Composition.SetMonad.setAp_from_setBind {A B : Type} (m : (A → B) → Prop) (n : A → Prop) : Applicative.setAp m n = setBind m fun (f : A → B) => setBind n fun (x : A) => eta (f x)

The standard monad-to-applicative derivation: m ⊛ n = m ⫝̸ λf. n ⫝̸ λx. η(f x).

The set applicative setAp from Applicative.lean agrees with the derived applicative from the set monad.

§5 LIFT decomposition

§3.2 (eq. 28): Partee's LIFT operation — which maps an individual to a generalized quantifier — decomposes as ⫝̸ ∘ η. Starting from the predicative (set) meaning of an indefinite, η injects it into a singleton set, and ⫝̸ produces a scope-taking function.

More precisely: for an entity j, lift(j) = A(η(j)) where A is Partee's existential type-shifter (TypeShifting.lean) and η is the set monad's unit.

The key insight: LIFT need not be a primitive. It falls out of the monad structure. This means we need only η and ⫝̸ — not the full suite of Partee's type-shifters (η, A, +wh) — to handle indefinites compositionally.

theorem Semantics.Composition.SetMonad.lift_eq_A_eta {m : Montague.Model} (domain : List m.Entity) (j : m.interpTy Montague.Ty.e) (hj : j ∈ domain) (hnd : domain.Nodup) (P : m.interpTy Montague.Ty.et) : TypeShifting.A domain (fun (x : m.interpTy Montague.Ty.e) => decide (j = x)) P = TypeShifting.lift j P

LIFT = A ∘ η on the domain.

eq. (28): (η x)^⫝̸ = λf. ⋃_{y ∈ {x}} f y = λf. f x = lift(x).

In linglib's formulation using A (which takes an explicit domain): A(domain)(η(j))(P) = domain.any (λx. η(j)(x) && P(x)). When j ∈ domain, this reduces to P(j) = lift(j)(P).

This theorem uses Bool-level equality rather than Prop because lift and A produce Bool-valued GQs (matching linglib's Model).

§6 Higher-order alternative sets

§5.2, eq. (48): when a scope argument f is itself a function into sets, ⫝̸ with an extra η produces higher-order alternative sets of type S(S b). These preserve the identity of distinct sources of alternatives, enabling selective exceptional scope when multiple indefinites occur on an island.

See Phenomena/FillerGap/Studies/Charlow2020.lean for worked derivations of exceptional scope, selectivity, and the Binder Roof Constraint.

theorem Semantics.Composition.SetMonad.higher_order_from_eta {A B : Type} (m : A → Prop) (f : A → B) : (setBind m fun (x : A) => eta (eta (f x))) = fun (s : B → Prop) => ∃ (a : A), m a ∧ s = eta (f a)

Applying η inside a ⫝̸ computation produces higher-order alternative sets: the result is of type S(S b), a set of sets.

§5.2, eq. (48): if m : S a and f : a → b, then m ⫝̸ (λx. η(η(f x))) has type S(S b). Each member of the outer set is a singleton containing one alternative.