TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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: $\iota\lvert\bigcup_{i \in I} A_i\rvert = \sum_{\varnothing \ne J \subseteq I}(-1)^{\lvert J\rvert + 1}\,\iota\lvert A_J\rvert$ , 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_\varnothing = X$ ), let $U := \bigcup_{i \in I}A_i$ , and let $\iota : \mathbb{N} \to \mathbb{R}$ be the canonical natural (The canonical natural $\iota(n) = n \cdot 1_F$ of a field). Then, in $\mathbb{R}$ :

The sieve identity. $\iota\lvert U\rvert \;=\; \sum_{J \in \mathcal{P}(I)\setminus\{\varnothing\}} (-1)^{\lvert J\rvert + 1}\,\iota\lvert A_J\rvert ,$ the sum being over the finite index set of nonempty subsets of $I$ .
The complementary form. $\iota\lvert X \setminus U\rvert \;=\; \sum_{J \in \mathcal{P}(I)} (-1)^{\lvert J\rvert}\,\iota\lvert A_J\rvert ,$ the sum now being over all subsets of $I$ , its term at $J = \varnothing$ being $\iota\lvert X\rvert$ by the stipulation $A_\varnothing = X$ .

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

Both readings at $I = \varnothing$ are part of the statement. Then $U = \varnothing$ and clause 1 reads $0 = 0$ , the index set of its sum being empty. Clause 2 reads $\iota\lvert X\rvert = \iota\lvert A_\varnothing\rvert$ , its sum having the single term at $J = \varnothing$ . At $\lvert J\rvert = 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) := \lvert T(x)\rvert$ , 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_\varnothing = X$ ; the abbreviation $\mathcal{J} := \mathcal{P}(I)\setminus\{\varnothing\}$ ; and, for $V \subseteq X$ , the indicator $\mathbf{1}_V : X \to \mathbb{R}$ with $\mathbf{1}_V(x) = 1$ for $x \in V$ and $\mathbf{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_\varnothing = X$ ): $\mathcal{P}(I)$ , $\mathcal{J}$ , each $[I]^{j}$ , each $A_J$ , $U$ and each $T(x)$ are finite ( $\lvert\mathcal{P}(A)\rvert = 2^{\lvert A\rvert}$ for finite $A$ , A subset of a finite set is finite, with $\lvert B\rvert \le \lvert A\rvert$ , and equality holds if and only if $B = A$ , The cardinality $\lvert A\rvert$ 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) \ne \varnothing$ ; and $\lvert [I]^{j}\rvert = \binom{\lvert I\rvert}{j}$ (The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$ ).

[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 $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$ , 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 $\varnothing$ is $0$ and a constant real summand gives $\sum_{i \in S}\lambda = \iota(\lvert S\rvert)\,\lambda$ (clause (c)).

[L4]

Interchange of a double sum over two finite index sets ( $\sum_{i \in S}\sum_{j \in T} a_{ij} = \sum_{(i,j) \in S \times T} a_{ij} = \sum_{j \in T}\sum_{i \in S} a_{ij}$ 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}\lambda u_i = \lambda\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 := \lvert S\rvert$ , the sets $[S]^{j}$ for $j \in \sigma(N)$ are pairwise disjoint with union $\mathcal{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 $\lvert B\rvert \le \lvert A\rvert$ , 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}\,\iota\binom{t}{j} = 0$ for every $t \ge 1$ ( $\sum_{k<n+1}\binom{n}{k} = 2^{n}$ , and $\sum_{k<n+1}(-1)^{k}\iota\!\binom{n}{k} = 0$ for $n \ge 1$ , clause 2). The hypothesis $t \ge 1$ there is not decoration: at $t = 0$ that sum is $1$ .

[L8]

$\iota$ is additive and injective (Laws of finite sums and products in $\mathbb{N}$ , and $\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k)$ , clauses 0 and 7), and $\mathbb{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}\mathbf{1}_V(x) = \iota\lvert V\rvert$ : the sets $V$ and $X \setminus V$ are disjoint finite sets with union $X$ , so [L2] splits the sum into $\sum_{x \in V}1 + \sum_{x \in X\setminus V}0$ , which is $\iota\lvert V\rvert\cdot 1 + \iota\lvert X\setminus V\rvert\cdot 0 = \iota\lvert V\rvert$ by the constant clause of [L3].

L1L2L3construct

1.2

The double list. Define $h : \mathcal{J} \times X \to \mathbb{R}$ by $h(J,x) := (-1)^{\lvert J\rvert + 1}\,\mathbf{1}_{A_J}(x)$ ; both $\mathcal{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 $\mathcal{J}_1 := \{\,J \in \mathcal{J} : J \subseteq T(x)\,\}$ and $\mathcal{J}\setminus\mathcal{J}_1$ are disjoint with union $\mathcal{J}$ ; by [L1] we have $\mathbf{1}_{A_J}(x) = 1$ for $J \in \mathcal{J}_1$ and $\mathbf{1}_{A_J}(x) = 0$ for $J \in \mathcal{J}\setminus\mathcal{J}_1$ , so splitting by [L2] gives $\sum_{J \in \mathcal{J}}h(J,x) = \sum_{J \in \mathcal{J}_1}(-1)^{\lvert J\rvert + 1}$ , and $\mathcal{J}_1 = \mathcal{P}(T(x))\setminus\{\varnothing\}$ .

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 \mathcal{P}(T(x))}(-1)^{\lvert J\rvert + 1} = \sum_{j<t+1}\Big(\sum_{J \in [T(x)]^{j}}(-1)^{j+1}\Big) = \sum_{j<t+1}\iota\binom{t}{j}\,(-1)^{j+1} = -\sum_{j<t+1}(-1)^{j}\,\iota\binom{t}{j}.$

L1L2L3L5L6L7

1.5

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

L2L3L7

2.1

The inner sum is the indicator of $U$ . If $t \ge 1$ then [L7] makes the right-hand side of step 1.4 zero, so step 1.5 gives $\sum_{J \in \mathcal{P}(T(x))\setminus\{\varnothing\}}(-1)^{\lvert J\rvert + 1} = 1$ . If $t = 0$ then $T(x) = \varnothing$ , so $\mathcal{P}(T(x))\setminus\{\varnothing\} = \varnothing$ and that sum is $0$ by [L3]. Since $x \in U$ exactly when $t \ge 1$ by [L1], step 1.3 gives $\sum_{J \in \mathcal{J}}h(J,x) = \mathbf{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)^{\lvert J\rvert+1}$ and applying step 1.1 to $V = A_J$ gives $\sum_{x \in X}h(J,x) = (-1)^{\lvert J\rvert + 1}\,\iota\lvert A_J\rvert$ for every $J \in \mathcal{J}$ .

step 1.1L5

3.1

Clause 1. Summing step 2.2 over $\mathcal{J}$ , interchanging by [L4], and then using step 2.1 and step 1.1 with $V = U$ : $\sum_{J \in \mathcal{J}}(-1)^{\lvert J\rvert + 1}\iota\lvert A_J\rvert = \sum_{J \in \mathcal{J}}\sum_{x \in X}h(J,x) = \sum_{x \in X}\sum_{J \in \mathcal{J}}h(J,x) = \sum_{x \in X}\mathbf{1}_U(x) = \iota\lvert U\rvert .$

step 1.1step 2.1step 2.2L4

4.1

Clause 2. The sets $U$ and $X \setminus U$ are disjoint finite sets with union $X$ , so $\lvert X\rvert = \lvert U\rvert + \lvert X\setminus U\rvert$ by [L2] and hence $\iota\lvert X\setminus U\rvert = \iota\lvert X\rvert - \iota\lvert U\rvert$ by the additivity of $\iota$ in [L8]. On the other side, $\{\varnothing\}$ and $\mathcal{J}$ are disjoint with union $\mathcal{P}(I)$ , so [L2], [L3] and [L7] give $\sum_{J \in \mathcal{P}(I)}(-1)^{\lvert J\rvert}\iota\lvert A_J\rvert = \iota\lvert A_\varnothing\rvert + \sum_{J \in \mathcal{J}}(-1)^{\lvert J\rvert}\iota\lvert A_J\rvert = \iota\lvert X\rvert - \sum_{J \in \mathcal{J}}(-1)^{\lvert J\rvert+1}\iota\lvert A_J\rvert$ , which by step 3.1 is $\iota\lvert X\rvert - \iota\lvert U\rvert$ . 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) \ge 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 = \varnothing$ , where $A_\varnothing = X$ contributes $\iota\lvert X\rvert$ . 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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 84 results over 28 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)