# All seven intersection terms for three sets

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-inclusion-exclusion-principle/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-inclusion-exclusion-principle-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Audit the full alternating sum and each element's multiplicity.

A finite indexed family, retaining separate indices for repeated sets.





## Givens and symbols


- work


- G1 — A={1,2,3}, B={2,3,4}, C={3,4,5}.


- r — number of indexed sets containing an element





## Rules and sources

Some rule statements have reader clarifications in this revision: they are paraphrases, not verbatim quotations. Referenced original source bytes and hashes are unchanged.


- mko_definition · cited — For each nonempty index subset I use sign (−1)^(|I|+1): odd-order intersections add and even-order intersections subtract. Equal sets at different indices remain distinct indexed entries, and empty intersections contribute 0. For an empty family, the union is empty and both its cardinality and the inclusion-exclusion sum are 0. Singles-minus-pairs alone is not a general exact formula for three or more sets; it is a separately identified Bonferroni truncation. · mko-inclusion-exclusion-principle
- work · prerequisite — Set unions and intersections, finite summation by element multiplicity; the binomial identity(1-1)^r=sum_j(-1)^j comb(r,j) is an explicit prerequisite.





## Main derivation

S01 · impliesBefore

A\cup B\cup C

After

\{1,2,3,4,5\},\quad|A\cup B\cup C|=5

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

First compute the union directly from the complete element lists as an independent check.



S02 · impliesBefore

|A|,|B|,|C|

After

3,3,3

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

The three positive first-order terms sum to 9.



S03 · impliesBefore

A\cap B,A\cap C,B\cap C

After

\{2,3\},\{3\},\{3,4\}

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

List all three second-order intersections, of sizes2,1,2.



S04 · impliesBefore

A\cap B\cap C

After

\{3\},\quad|A\cap B\cap C|=1

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

The sole third-order intersection must be added back.



S05 · impliesBefore

3+3+3-2-1-2+1

After

5=|A\cup B\cup C|

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

All seven nonempty index subsets are included.



S06 · impliesBefore

x\text{ belongs to }r\ge1\text{ indexed sets}

After

\sum_{j=1}^{r}(-1)^{j+1}\binom rj=1-(1-1)^r=1

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

Each union element has net multiplicity one, proving the finite formula elementwise.



S07 · impliesBefore

\text{singles minus pairs only}

After

9-5=4\ne5

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

This example explicitly shows the missing third-order term; pairwise truncation is not exact.



S08 · impliesBefore

(A,A)\text{ indexed twice};\quad n=0

After

|A|+|A|-|A|=|A|;\quad|\bigcup\varnothing|=0

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

Indexed repetition still cancels correctly; the empty-family sum and union size are both zero.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — Equal sets do not mean an indexed obligation may be ignored.
- S07 · premise_audit · G1, S06, work — A Bonferroni bound must be separately labeled, not asserted as equality.
- S06 · premise_audit · G1, S05, work — Elements outside the union have r=0 and contribute zero separately.
- S05 · premise_audit · G1, S04, work — Three singles, three pairs and one triple equal2³-1.
- S04 · premise_audit · G1, S03, work — Listing pairwise intersections does not permit omitting the triple.
- S03 · premise_audit · G1, S02, work — Second-order terms carry negative signs.
- S02 · premise_audit · G1, S01, work — Each indexed entry is counted once.
- S01 · premise_audit · G1, work — The expected result is not merely assumed from the formula.





## Error controls and negative controls

Seven termsEnumerate index subsets, not distinct set values.

ElementwiseUse1-(1-1)^r for r≥1 and zero separately for r=0.


- Singles minus pairs is exact for three sets. → reject — Here4 differs from union size 5.
- The triple intersection should be subtracted. → reject — Order three is odd and has positive sign.
- Repeated sets make the union twice as large. → reject — The second-order intersection subtracts the duplicate copy.





## Result and limitations

All seven terms give union size 5; elementwise multiplicity proves the finite-family formula.







## Verification and source binding

3 declared checks for this guide; only the listed expressions are covered.


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: ea75129552baa4d33afae410265a8e2ec2eda5b1a8669c83da8afed4efc43c95
- original source SHA-256: d12d13f29453c49f15f41deea45201369e57e7476d15786a97750ca414dc608a
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-inclusion-exclusion-principle-01.json)