TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passverified 2026-07-29 (claude-fable-5)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Inclusion and exclusion: $ι ∣ ⋃_{i \in I} A_{i} ∣ = \sum_{\emptyset \neq J \subseteq I} (- 1)^{∣ J ∣ + 1} ι ∣ A_{J} ∣$ , together with the complementary form counting the elements in none of the $A_{i}$

Statement

Let $X$ , $I$ , $(A_{i})_{i \in I}$ and the intersections $A_{J}$ be a sieve family (A finite family $(A_{i})_{i \in I}$ of subsets of a finite set $X$ , the intersections $A_{J}$ for $J \subseteq I$ , and the convention $A_{\emptyset} = X$ ), let $U : = ⋃_{i \in I} A_{i}$ , and let $ι : N \to R$ be the canonical natural (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field). Then, in $R$ :

The sieve identity. $ι ∣ U ∣ = \sum_{J \in P (I) ∖ {\emptyset}} (- 1)^{∣ J ∣ + 1} ι ∣ A_{J} ∣,$ the sum being over the finite index set of nonempty subsets of $I$ .
The complementary form. $ι ∣ X ∖ U ∣ = \sum_{J \in P (I)} (- 1)^{∣ J ∣} ι ∣ A_{J} ∣,$ the sum now being over all subsets of $I$ , its term at $J = \emptyset$ being $ι ∣ X ∣$ by the stipulation $A_{\emptyset} = X$ .

The identities are stated in $R$ because their terms carry signs and $N$ has no subtraction; every cardinality appearing is a natural number carried into $R$ by $ι$ , and $ι$ is injective, so an identity between two of them may be read back in $N$ (Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , clause 7).

Both readings at $I = \emptyset$ are part of the statement. Then $U = \emptyset$ and clause 1 reads $0 = 0$ , the index set of its sum being empty. Clause 2 reads $ι ∣ X ∣ = ι ∣ A_{\emptyset} ∣$ , its sum having the single term at $J = \emptyset$ . At $∣ J ∣ = 1$ the sign in clause 1 is $(- 1)^{2} = 1$ and $A_{{i}} = A_{i}$ , so the singleton terms enter with a plus sign.

Facts & Assumptions

Given: A sieve family $X$ , $I$ , $(A_{i})_{i \in I}$ with intersections $A_{J}$ , union $U$ , traces $T (x)$ and $t (x) : = ∣ T (x) ∣$ , all as in A finite family $(A_{i})_{i \in I}$ of subsets of a finite set $X$ , the intersections $A_{J}$ for $J \subseteq I$ , and the convention $A_{\emptyset} = X$ ; the abbreviation $J : = P (I) ∖ {\emptyset}$ ; and, for $V \subseteq X$ , the indicator $1_{V} : X \to R$ with $1_{V} (x) = 1$ for $x \in V$ and $1_{V} (x) = 0$ otherwise.

[L1]

Sieve facts (A finite family $(A_{i})_{i \in I}$ of subsets of a finite set $X$ , the intersections $A_{J}$ for $J \subseteq I$ , and the convention $A_{\emptyset} = X$ ): $P (I)$ , $J$ , each $[I]^{j}$ , each $A_{J}$ , $U$ and each $T (x)$ are finite ( $∣ P (A) ∣ = 2^{∣ A ∣}$ for finite $A$ , A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , The cardinality $∣ A ∣$ of a finite set); for nonempty $J$ , $x \in A_{J}$ if and only if $J \subseteq T (x)$ ; $x \in U$ if and only if $T (x) \neq \emptyset$ ; and $∣ [I]^{j} ∣ = (\binom{∣ I ∣}{j})$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ ).

[L2]

Splitting a sum along a partition of its index set, and the sum rule for two disjoint blocks (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition, clauses 3 and 1).

[L3]

Sums over a finite index set (The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form): the value is independent of the enumeration used; $\sum_{i \in n} a_{i} = \sum_{i < n} a_{i}$ (clause (a)); a sum over $\emptyset$ is $0$ and a constant real summand gives $\sum_{i \in S} λ = ι (∣ S ∣) λ$ (clause (c)).

[L4]

Interchange of a double sum over two finite index sets ( $\sum_{i \in S} \sum_{j \in T} a_{i j} = \sum_{(i, j) \in S \times T} a_{i j} = \sum_{j \in T} \sum_{i \in S} a_{i j}$ for finite index sets $S$ and $T$ ).

[L5]

Additivity and scaling of a real finite sum over a finite index set: $\sum_{i \in S} (u_{i} + v_{i}) = \sum_{i \in S} u_{i} + \sum_{i \in S} v_{i}$ and $\sum_{i \in S} λ u_{i} = λ \sum_{i \in S} u_{i}$ . Both are clauses 1 and 2 of Laws of finite sums and finite products read through an enumeration of $S$ (The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form, Finite sums and finite products, by recursion).

[L6]

Partition of a power set by cardinality: for a finite $S$ with $N : = ∣ S ∣$ , the sets $[S]^{j}$ for $j \in σ (N)$ are pairwise disjoint with union $P (S)$ , since a subset of $S$ has exactly one cardinality and that cardinality is at most $N$ (A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , clause 2).

[L7]

Powers of $- 1$ and the alternating row sum: $(- 1)^{0} = 1$ and $(- 1)^{p + 1} = - (- 1)^{p}$ (Integer powers $a^{m}$ ); and $\sum_{j < t + 1} (- 1)^{j} ι (\binom{t}{j}) = 0$ for every $t \geq 1$ ( $\sum_{k < n + 1} (\binom{n}{k}) = 2^{n}$ , and $\sum_{k < n + 1} (- 1)^{k} ι ⁣ (\binom{n}{k}) = 0$ for $n \geq 1$ , clause 2). The hypothesis $t \geq 1$ there is not decoration: at $t = 0$ that sum is $1$ .

[L8]

$ι$ is additive and injective (Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , clauses 0 and 7), and $R$ is an ordered field, so subtraction is available (Ordered field, Field).

Proof

technique · direct

1.1

Indicator sums. For every $V \subseteq X$ one has $\sum_{x \in X} 1_{V} (x) = ι ∣ V ∣$ : the sets $V$ and $X ∖ V$ are disjoint finite sets with union $X$ , so [L2] splits the sum into $\sum_{x \in V} 1 + \sum_{x \in X ∖ V} 0$ , which is $ι ∣ V ∣ \cdot 1 + ι ∣ X ∖ V ∣ \cdot 0 = ι ∣ V ∣$ by the constant clause of [L3].

L1L2L3construct

1.2

The double list. Define $h : J \times X \to R$ by $h (J, x) : = (- 1)^{∣ J ∣ + 1} 1_{A_{J}} (x)$ ; both $J$ and $X$ are finite by [L1], so both iterated sums of $h$ are defined.

L1construct

1.3

Fix $x \in X$ and write $t : = t (x)$ . The sets $J_{1} : = {J \in J : J \subseteq T (x)}$ and $J ∖ J_{1}$ are disjoint with union $J$ ; by [L1] we have $1_{A_{J}} (x) = 1$ for $J \in J_{1}$ and $1_{A_{J}} (x) = 0$ for $J \in J ∖ J_{1}$ , so splitting by [L2] gives $\sum_{J \in J} h (J, x) = \sum_{J \in J_{1}} (- 1)^{∣ J ∣ + 1}$ , and $J_{1} = P (T (x)) ∖ {\emptyset}$ .

L1L2L3

1.4

Grouping the subsets of $T (x)$ by size. By [L6] applied to $T (x)$ , then the constant clause of [L3] on each block, then scaling by $- 1$ and $(- 1)^{j + 1} = - (- 1)^{j}$ from [L7], $\sum_{J \in P (T (x))} (- 1)^{∣ J ∣ + 1} = \sum_{j < t + 1} (\sum_{J \in [T (x)]^{j}} (- 1)^{j + 1}) = \sum_{j < t + 1} ι (\binom{t}{j}) (- 1)^{j + 1} = - \sum_{j < t + 1} (- 1)^{j} ι (\binom{t}{j}) .$

L1L2L3L5L6L7

1.5

Splitting off the empty subset. ${\emptyset}$ and $P (T (x)) ∖ {\emptyset}$ are disjoint with union $P (T (x))$ , so [L2] and [L7] give $\sum_{J \in P (T (x))} (- 1)^{∣ J ∣ + 1} = (- 1)^{0 + 1} + \sum_{J \in P (T (x)) ∖ {\emptyset}} (- 1)^{∣ J ∣ + 1} = - 1 + \sum_{J \in P (T (x)) ∖ {\emptyset}} (- 1)^{∣ J ∣ + 1}$ .

L2L3L7

2.1

The inner sum is the indicator of $U$ . If $t \geq 1$ then [L7] makes the right-hand side of step 1.4 zero, so step 1.5 gives $\sum_{J \in P (T (x)) ∖ {\emptyset}} (- 1)^{∣ J ∣ + 1} = 1$ . If $t = 0$ then $T (x) = \emptyset$ , so $P (T (x)) ∖ {\emptyset} = \emptyset$ and that sum is $0$ by [L3]. Since $x \in U$ exactly when $t \geq 1$ by [L1], step 1.3 gives $\sum_{J \in J} h (J, x) = 1_{U} (x)$ for every $x \in X$ .

step 1.3step 1.4step 1.5L1L3L7

2.2

The outer sum recovers the sieve terms. Scaling by the constant $(- 1)^{∣ J ∣ + 1}$ and applying step 1.1 to $V = A_{J}$ gives $\sum_{x \in X} h (J, x) = (- 1)^{∣ J ∣ + 1} ι ∣ A_{J} ∣$ for every $J \in J$ .

step 1.1L5

3.1

Clause 1. Summing step 2.2 over $J$ , interchanging by [L4], and then using step 2.1 and step 1.1 with $V = U$ : $\sum_{J \in J} (- 1)^{∣ J ∣ + 1} ι ∣ A_{J} ∣ = \sum_{J \in J} \sum_{x \in X} h (J, x) = \sum_{x \in X} \sum_{J \in J} h (J, x) = \sum_{x \in X} 1_{U} (x) = ι ∣ U ∣ .$

step 1.1step 2.1step 2.2L4

4.1

Clause 2. The sets $U$ and $X ∖ U$ are disjoint finite sets with union $X$ , so $∣ X ∣ = ∣ U ∣ + ∣ X ∖ U ∣$ by [L2] and hence $ι ∣ X ∖ U ∣ = ι ∣ X ∣ - ι ∣ U ∣$ by the additivity of $ι$ in [L8]. On the other side, ${\emptyset}$ and $J$ are disjoint with union $P (I)$ , so [L2], [L3] and [L7] give $\sum_{J \in P (I)} (- 1)^{∣ J ∣} ι ∣ A_{J} ∣ = ι ∣ A_{\emptyset} ∣ + \sum_{J \in J} (- 1)^{∣ J ∣} ι ∣ A_{J} ∣ = ι ∣ X ∣ - \sum_{J \in J} (- 1)^{∣ J ∣ + 1} ι ∣ A_{J} ∣$ , which by step 3.1 is $ι ∣ X ∣ - ι ∣ U ∣$ . The two right-hand sides agree, which is clause 2.

step 3.1L2L3L5L7L8∎

Remarks

Where the alternating row sum is spent, and why its hypothesis matters. The whole content of the proof is that each $x$ contributes $1$ to the right-hand side when it lies in some $A_{i}$ and $0$ otherwise. The first case is the vanishing of the full alternating row sum of $t (x)$ , which holds only for $t (x) \geq 1$ ; the second case is not that identity at all but the emptiness of the index set. Applying the identity at $t (x) = 0$ would give $1$ , not $0$ , and would make the theorem false.
The empty intersection is used once. Only in clause 2, at the term $J = \emptyset$ , where $A_{\emptyset} = X$ contributes $ι ∣ X ∣$ . Clause 1 never mentions it.
No choice principle is used. A sum over a finite index set is defined because all its enumerations agree, not by selecting one, and the family $(A_{i})_{i \in I}$ is given as a function.

Depends on

Used by

Dependency tree · two levels

61 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Inclusion-exclusion principle (Wikipedia) (standard reference, not scraped)
Binomial coefficient (Wikipedia) (standard reference, not scraped)
R. Stanley, Enumerative Combinatorics, Vol. 1, Ch. 2 (standard reference, not scraped)
Guichard, The Inclusion-Exclusion Formula (LibreTexts) (standard reference, not scraped)

Inclusion and exclusion: ι∣⋃i∈IAi∣=∑∅≠J⊆I(−1)∣J∣+1 ι∣AJ∣ι∣⋃i∈I​Ai​∣=∑∅=J⊆I​(−1)∣J∣+1ι∣AJ​∣, together with the complementary form counting the elements in none of the AiAi​