Antiexhaustive Operator O⁻ [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 is the set of D-variants of an existential ∃x∈D.P(x) over the subdomains that stand a chance, asserting all of them gives ∀D'⊆D. ∃x∈D'.P(x) — a distribution requirement across subdomains, i.e., universal force over the possible witnesses.

Deriving Universal Force from Antiexhaustive Enrichment

[chierchia-2006] §5.1: When O⁻ is applied to an existential ∃x∈D.P(x) with D-MIN alternatives (the subdomains containing a possible witness, (61b)), the enriched meaning requires the existential to hold over every such subdomain — equivalent to universal force over the possible witnesses in D, (63d). The formal engine behind FCI universal readings.

Implementation notes

An alternative domain must contain a possible witness, (61b): without that restriction the empty subdomain would be an alternative, its existential the empty proposition, and O⁻ contradictory everywhere.

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 [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.

theorem Exhaustification.oMinus_image_antitone_eq {World : Type u_1} {C : Set World → Set World} (hC : Antitone C) {A : Set (Set World)} {p : Set World} (hA : ∀ q ∈ A, q ⊆ p) : oMinus (C '' A) (C p) = C p

Under an antitone embedding, alternatives that each entail the prejacent are all entailed by the embedded prejacent, so antiexhaustive enrichment is vacuous: the free-choice implicature of an item under negation disappears, [chierchia-2006] (65)–(66).

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

theorem Exhaustification.existsIn_subset {World : Type u_1} {Entity : Type u_2} (D : List Entity) (P : Entity → Set World) {D' : List Entity} (h : ∀ x ∈ D', x ∈ D) : existsIn D' P ⊆ existsIn D P

A subdomain existential entails the existential over the whole domain.

def Exhaustification.dVariants {World : Type u_1} {Entity : Type u_2} (F : List Entity → Set World) (D : List Entity) (possible : Entity → Prop) : Set (Set World)

The D-variants of a domain-dependent proposition, [chierchia-2006] (96): its values on the subdomains of D that stand a chance, those containing a possible member, (61b).

Equations

• Exhaustification.dVariants F D possible = {q : Set World | ∃ (D' : List Entity), (∀ x ∈ D', x ∈ D) ∧ (∃ x ∈ D', possible x) ∧ q = F D'}

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 the subdomains with a possible witness.

Equations

• Exhaustification.dMinAlts D P = Exhaustification.dVariants (fun (x : List Entity) => Exhaustification.existsIn x P) D fun (x : Entity) => ∃ (v : World), P x v

theorem Exhaustification.oMinus_dMinAlts_iff {World : Type u_1} {Entity : Type u_2} (D : List Entity) (P : Entity → Set World) (w : World) (hD : ∃ a ∈ D, ∃ (v : World), P a v) : oMinus (dMinAlts D P) (existsIn D P) w ↔ ∀ a ∈ D, (∃ (v : World), P a v) → P a w

Antiexhaustiveness is universal force over the possible witnesses.

O⁻ applied to ∃x∈D.P(x) with D-MIN alternatives holds exactly when every possible witness in D is an actual one, [chierchia-2006] (63c)–(63d).

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 → (∃ (v : World), P a v) → P a w

Antiexhaustiveness yields universal distribution.

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