Antiexhaustive Operator O⁻ @cite{chierchia-2006}

Chierchia's O⁻ is distinct from O (exhaustification/only) and E (even-like enrichment). While O negates stronger alternatives, O⁻ requires that every alternative in C entails every other — i.e., the alternative set is a complete join semilattice. This yields "antiexhaustive" universal-like force from an existential base.

Formally: O⁻_C(p) = p ∧ ∀q ∈ C. q (the assertion together with every alternative being true).

The key use: when C = D-variants (subdomain alternatives) of an existential ∃x∈D.P(x), asserting all D-variants gives ∀D'⊆D. ∃x∈D'.P(x) — a distribution requirement across subdomains, i.e., universal force.

Deriving Universal Force from Antiexhaustive Enrichment

@cite{chierchia-2006} §5.1: When O⁻ is applied to an existential ∃x∈D.P(x) with D-MIN alternatives (all subdomains), the enriched meaning requires the existential to hold over every subdomain — equivalent to universal force. The formal engine behind FCI universal readings.

def Exhaustification.oMinus {World : Type u_1} (C : Set (Set World)) (p : Set World) : Set World

Antiexhaustive enrichment O⁻: assert the prejacent and every alternative.

Simplified from @cite{chierchia-2006} definition (108c) / (62). The paper defines O⁻_C(p) = p ∧ ∀q,q'∈C [q → q'] where q' has domain complementary to q — i.e., mutual entailment between all domain-alternative pairs. We simplify to the equivalent truth conditions p ∧ ∀q∈C. q (asserting all alternatives), which produces the same result when C consists of subdomain existentials forming a lattice.

When C is a set of D-variants (subdomain existentials), asserting all of them yields: for every subdomain D' of D, ∃x∈D'.P(x).

Equations

• Exhaustification.oMinus C p w = (p w ∧ ∀ q ∈ C, q w)

theorem Exhaustification.oMinus_entails {World : Type u_1} (C : Set (Set World)) (p : Set World) : oMinus C p ⊆ p

O⁻ is a strengthening operation: O⁻_C(p) ⊆ p.

theorem Exhaustification.oMinus_entails_alt {World : Type u_1} (C : Set (Set World)) (p q : Set World) (hq : q ∈ C) : oMinus C p ⊆ q

O⁻ is at least as strong as any individual alternative.

def Exhaustification.existsIn {World : Type u_1} {Entity : Type u_2} (D : List Entity) (P : Entity → Set World) : Set World

An existential over a finite domain (list-based for computability).

Equations

• Exhaustification.existsIn D P w = ∃ x ∈ D, P x w

def Exhaustification.dMinAlts {World : Type u_1} {Entity : Type u_2} (D : List Entity) (P : Entity → Set World) : Set (Set World)

D-MIN alternatives: existentials over all sublists (subdomains).

Equations

• Exhaustification.dMinAlts D P = {q : Set World | ∃ (D' : List Entity), (∀ x ∈ D', x ∈ D) ∧ q = Exhaustification.existsIn D' P}

theorem Exhaustification.antiexh_yields_universal {World : Type u_1} {Entity : Type u_2} (D : List Entity) (P : Entity → Set World) (w : World) (h : oMinus (dMinAlts D P) (existsIn D P) w) (a : Entity) : a ∈ D → P a w

Antiexhaustiveness yields universal distribution.

O⁻ applied to ∃x∈D.P(x) with D-MIN alternatives entails that for every individual a ∈ D, P(a) holds — i.e., universal force.

Chierchia 2006's key formal result: the "birth of universal readings" (§5.1) from antiexhaustive enrichment of an existential base.