ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)

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.

The sieve run in full on three explicit finite sets and then on four, with every nonempty intersection listed

Example

Take the ambient set $X : = 8 = {0, 1, 2, 3, 4, 5, 6, 7}$ and the subsets

$A_{0} : = {0, 1, 2, 3}, A_{1} : = {2, 3, 4, 5}, A_{2} : = {3, 4, 6}, A_{3} : = {5, 6, 7} .$

First the family $(A_{i})_{i \in 3}$ , a sieve family with ambient set $X$ and index set $I : = 3$ (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$ ). Every intersection $A_{J}$ for $\emptyset \neq J \subseteq 3$ is listed:

$J$	$A_{J}$	$∣ A_{J} ∣$
${0}$	${0, 1, 2, 3}$	$4$
${1}$	${2, 3, 4, 5}$	$4$
${2}$	${3, 4, 6}$	$3$
${0, 1}$	${2, 3}$	$2$
${0, 2}$	${3}$	$1$
${1, 2}$	${3, 4}$	$2$
${0, 1, 2}$	${3}$	$1$

The union is $A_{0} \cup A_{1} \cup A_{2} = {0, 1, 2, 3, 4, 5, 6}$ , of size $7$ , and the sieve returns $(4 + 4 + 3) - (2 + 1 + 2) + 1 = 7$ . The complementary form returns $8 - (4 + 4 + 3) + (2 + 1 + 2) - 1 = 1$ , and indeed $X ∖ (A_{0} \cup A_{1} \cup A_{2}) = {7}$ .

Now the family $(A_{i})_{i \in 4}$ , with $A_{3}$ adjoined and $I : = 4$ :

$J$	$A_{J}$	$∣ A_{J} ∣$
${0}$	${0, 1, 2, 3}$	$4$
${1}$	${2, 3, 4, 5}$	$4$
${2}$	${3, 4, 6}$	$3$
${3}$	${5, 6, 7}$	$3$
${0, 1}$	${2, 3}$	$2$
${0, 2}$	${3}$	$1$
${0, 3}$	$\emptyset$	$0$
${1, 2}$	${3, 4}$	$2$
${1, 3}$	${5}$	$1$
${2, 3}$	${6}$	$1$
${0, 1, 2}$	${3}$	$1$
${0, 1, 3}$	$\emptyset$	$0$
${0, 2, 3}$	$\emptyset$	$0$
${1, 2, 3}$	$\emptyset$	$0$
${0, 1, 2, 3}$	$\emptyset$	$0$

The union is now all of $X$ , of size $8$ , and the sieve returns $(4 + 4 + 3 + 3) - (2 + 1 + 0 + 2 + 1 + 1) + (1 + 0 + 0 + 0) - 0 = 14 - 7 + 1 = 8$ . The complementary form returns $8 - 14 + 7 - 1 + 0 = 0$ , and indeed $X ∖ (A_{0} \cup A_{1} \cup A_{2} \cup A_{3}) = \emptyset$ .

Facts & Assumptions

Given: The ambient set $X = 8$ and the subsets $A_{0}, A_{1}, A_{2}, A_{3}$ above, together with the two index sets $I = 3$ and $I = 4$ and the canonical natural $ι$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[L1]

A listed set with distinct entries has as many elements as entries: if $x_{0}, \dots, x_{k - 1}$ are distinct then $j \mapsto x_{j}$ is a bijection of $k$ onto ${x_{0}, \dots, x_{k - 1}}$ , so that set is finite of cardinality $k$ (The cardinality $∣ A ∣$ of a finite set, clauses (a) and (c), Injection, surjection, bijection).

[L2]

For a sieve family with ambient set $X$ , finite index set $I$ , union $U = ⋃_{i \in I} A_{i}$ and $A_{\emptyset} = X$ , the sieve identity and its complementary form are $ι ∣ U ∣ = \sum_{\emptyset \neq J \subseteq I} (- 1)^{∣ J ∣ + 1} ι ∣ A_{J} ∣, ι ∣ X ∖ U ∣ = \sum_{J \subseteq I} (- 1)^{∣ J ∣} ι ∣ A_{J} ∣$ (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}$ , 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$ ).

[L3]

Every $J \subseteq I$ is finite with a unique natural cardinality $∣ J ∣ \leq ∣ I ∣$ , while $[I]^{j} = {J \subseteq I : ∣ J ∣ = j}$ ; hence the levels $[I]^{j}$ for $1 \leq j \leq ∣ I ∣$ are pairwise disjoint and have union $P (I) ∖ {\emptyset}$ . The sign attached to $J$ is $(- 1)^{∣ J ∣ + 1}$ , positive for odd $∣ J ∣$ and negative for even $∣ J ∣$ (The cardinality $∣ A ∣$ of a finite set, A subset of a finite set is finite, with $∣ B ∣ \leq ∣ A ∣$ , and equality holds if and only if $B = A$ , The set $[A]^{k}$ of $k$ -element subsets and the binomial coefficient $(\binom{n}{k}) : = ∣ [n]^{k} ∣$ , 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, clause 3, The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form, Integer powers $a^{m}$ ).

[L4]

$ι$ is additive and injective, so the arithmetic of the displayed sums may be carried out on the natural numbers and read in $R$ (Laws of finite sums and products in $N$ , and $ι (\sum_{k < n} a_{k}) = \sum_{k < n} ι (a_{k})$ , clauses 0 and 7, Ordered field).

Verification

technique · direct

1.1

The three-set family. $A_{0}$ , $A_{1}$ , $A_{2}$ are subsets of $X = 8$ with $∣ A_{0} ∣ = 4$ , $∣ A_{1} ∣ = 4$ and $∣ A_{2} ∣ = 3$ by [L1], each entry list being strictly increasing and so having distinct entries.

givenL1

1.2

Its intersections. Intersecting the listed sets entry by entry gives $A_{{0, 1}} = {2, 3}$ , $A_{{0, 2}} = {3}$ , $A_{{1, 2}} = {3, 4}$ and $A_{{0, 1, 2}} = {3}$ , of sizes $2$ , $1$ , $2$ and $1$ by [L1].

givenL1

1.3

Its union and complement. An element of $X$ lies in $A_{0} \cup A_{1} \cup A_{2}$ unless it is $7$ , since $0, 1, 2, 3 \in A_{0}$ , $4, 5 \in A_{1}$ and $6 \in A_{2}$ while $7$ belongs to none of the three listed sets; so the union is ${0, 1, 2, 3, 4, 5, 6}$ , of size $7$ , and its complement in $X$ is ${7}$ , of size $1$ .

givenL1

1.4

The four-set family. Adjoining $A_{3} = {5, 6, 7}$ , of size $3$ , the remaining intersections are $A_{{0, 3}} = \emptyset$ , $A_{{1, 3}} = {5}$ , $A_{{2, 3}} = {6}$ , $A_{{0, 1, 3}} = A_{{0, 2, 3}} = A_{{1, 2, 3}} = \emptyset$ and $A_{{0, 1, 2, 3}} = \emptyset$ , of sizes $0$ , $1$ , $1$ , $0$ , $0$ , $0$ and $0$ by [L1] and clause (b) of The cardinality $∣ A ∣$ of a finite set.

givenL1

1.5

The four-set union. Now $7 \in A_{3}$ , so the union is all of $X$ , of size $8$ , and its complement in $X$ is empty, of size $0$ .

givenL1

2.1

The sieve for three sets. Grouping by size as in [L3], clause 1 of [L2] reads $ι ∣ A_{0} \cup A_{1} \cup A_{2} ∣ = ι (4 + 4 + 3) - ι (2 + 1 + 2) + ι (1) = ι (11) - ι (5) + ι (1) = ι (7)$ , which matches step 1.3.

step 1.1step 1.2step 1.3L2L3L4

2.2

The complementary form for three sets. Clause 2 of [L2] adds the term at $J = \emptyset$ , which is $ι ∣ A_{\emptyset} ∣ = ι ∣ X ∣ = ι (8)$ , and reverses every sign, giving $ι (8) - ι (11) + ι (5) - ι (1) = ι (1)$ , which matches the complement computed in step 1.3.

step 1.1step 1.2step 1.3L2L3L4

2.3

The sieve for four sets. The singleton terms now sum to $4 + 4 + 3 + 3 = 14$ , the pair terms to $2 + 1 + 0 + 2 + 1 + 1 = 7$ , the triple terms to $1 + 0 + 0 + 0 = 1$ and the single four-element term is $0$ ; so clause 1 of [L2] reads $ι (14) - ι (7) + ι (1) - ι (0) = ι (8)$ , which matches step 1.5, and clause 2 reads $ι (8) - ι (14) + ι (7) - ι (1) + ι (0) = ι (0)$ , again matching.

step 1.1step 1.2step 1.4step 1.5L2L3L4

3.1

Both families therefore satisfy both forms of the identity, with every intersection exhibited rather than inferred.

step 2.1step 2.2step 2.3∎

Remarks

Adjoining one set changes every level of the sum. Passing from three sets to four adds a singleton term, three pair terms, three triple terms and one four-element term, and the totals at each level move accordingly; what stays fixed is that the alternating combination reproduces the size of the union.
The terms that vanish are not omitted. $A_{{0, 3}}$ and the three four-element-family triples are empty, so their terms are $0$ ; they are still terms of the sum, and writing them keeps the count of terms at each level equal to the number of subsets of that size, which is what the grouping in [L3] asserts.
Where the complementary form gets its extra term. It runs over all subsets of the index set, including $\emptyset$ , whose term is $ι ∣ X ∣$ . That is the only place the ambient set enters the arithmetic, and it is why the ambient set has to be named as part of the family.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

54 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)
Cardinality (Wikipedia) (standard reference, not scraped)
Guichard, The Inclusion-Exclusion Formula (LibreTexts) (standard reference, not scraped)