# Equivalence relation: checking the three axioms on a complete finite relation and emitting the classes [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-equivalence-relation/) 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-equivalence-relation-01 · production-20261019-adopted-96 ## Goal and scope On X={0,1,2,3,4} the relation R is listed completely as 13 ordered pairs: (0,0), (1,1), (2,2), (3,3), (4,4), (0,2), (2,0), (1,3), (3,1), (1,4), (4,1), (3,4), (4,3). Check reflexivity, symmetry and transitivity item by item, prove that R is an equivalence relation and emit its classes; then show that R′, obtained by removing (3,4) and (4,3), is reflexive and symmetric but not an equivalence relation. Stays inside the MKO: carrier labelled 0 to n−1 and the relation listed completely as distinct ordered pairs (assumption a1); classes are emitted only after all three checks pass, and one counterexample refutes the corresponding axiom (assumption a2). Transitivity is settled for all composable pairs at once by a block-relation lemma, not by sampling. Quotient sets and cardinality comparison are not treated, and the canonical MKO and its English edition are not changed. ## Givens and symbols - cartesian_product_def - set_extensionality - set_operations_def - relation_def - finite_forall - G1 — X={0,1,2,3,4}; R={(0,0),(1,1),(2,2),(3,3),(4,4),(0,2),(2,0),(1,3),(3,1),(1,4),(4,1),(3,4),(4,3)}, 13 distinct ordered pairs, listed completely. - G2 — For comparison: R′ consists of the 11 ordered pairs left after removing (3,4) and (4,3) from R. - X — carrier {0,1,2,3,4} - R,\ R' — the fully listed relation and the comparison relation with two pairs removed - xRy — (x,y)∈R - B_1,\ B_2 — the blocks {0,2} and {1,3,4} - T — block relation B_1×B_1 ∪ B_2×B_2 - [x] — equivalence class of x, {y∈X : xRy} ## Rules and sources - cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d. - set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements. - set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A. - def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable. - finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements. - subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B). - eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true. - exists_elim · prerequisite — ∃-elimination: from ∃x∈D, P(x) we may name some element a with P(a) by a fresh name; reasoning with a is allowed as long as the final conclusion does not mention a. - contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds. - forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x). - quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x). - de_morgan_logic · prerequisite — De Morgan's laws for logic: ¬(P∧Q) ⇔ ¬P∨¬Q and ¬(P∨Q) ⇔ ¬P∧¬Q. - mko_equiv_def · cited — A relation R on X is an equivalence relation when every x satisfies xRx, xRy implies yRx, and xRy together with yRz implies xRz. This slice checks each obligation on a complete finite carrier and complete set of relation pairs. · mko-equivalence-relation - relation_def · prerequisite — A relation on X is a subset R⊆X×X; xRy means (x,y)∈R. When the list is complete, an unlisted ordered pair is not in R. - finite_forall · prerequisite — Finite universal: for a finite set D, 'for all t∈D, Φ(t)' is equivalent to the conjunction of the instances obtained by substituting each element of D; the list must be complete. - eq_class_def · prerequisite — Equivalence class: when R is an equivalence relation, [x]={y∈X : xRy}. By the MKO, classes are emitted only after all three axioms pass. - L_block_trans · lemma — If B_1 and B_2 are pairwise disjoint subsets of X, then T=(B_1×B_1)∪(B_2×B_2) is transitive: (x,y)∈T and (y,z)∈T imply (x,z)∈T. ## Main derivation S01 · definitionBefore R\ \text{is an equivalence relation on}\ X After \forall x\,(xRx)\ \land\ \forall x,y\,(xRy\Rightarrow yRx)\ \land\ \forall x,y,z\,(xRy\land yRz\Rightarrow xRz) Conditions: none Rule: mko_equiv_def · Uses: G1, relation_def Leaf basis: mko_equiv_def + def_unfold Unfold the definition of the MKO: all three axioms, reflexivity, symmetry and transitivity, must hold. Each is a universal statement over a finite set and can be checked completely; one counterexample to any of them means R is not an equivalence relation. S02 · equivalentBefore \forall x\in X:\ (x,x)\in R After (0,0),(1,1),(2,2),(3,3),(4,4)\in R Conditions: none Rule: finite_forall · Uses: S01, G1, finite_forall Leaf basis: finite_forall + relation_def X has five elements, so reflexivity is equivalent to all five diagonal pairs lying in R. Look each one up in the list of G1: all five are there. Reflexivity holds. S03 · equivalentBefore \forall (x,y)\in R:\ (y,x)\in R After (0,2)\leftrightarrow(2,0),\ (1,3)\leftrightarrow(3,1),\ (1,4)\leftrightarrow(4,1),\ (3,4)\leftrightarrow(4,3);\ (x,x)\ \text{self-reverse} Conditions: none Rule: finite_forall · Uses: S01, G1, finite_forall Leaf basis: finite_forall + relation_def + numeric_evaluation Symmetry needs checking only on the pairs of R (when xRy is false the implication holds automatically). Of the 13 pairs, the 5 diagonal pairs are their own reverses; the other 8 form 4 pairs of mutually reversed ordered pairs, with both members of each pair listed. Symmetry holds. S04 · definitionBefore X=\{0,1,2,3,4\} After B_1=\{0,2\},\ B_2=\{1,3,4\},\ T=(B_1\times B_1)\cup(B_2\times B_2) Conditions: none Rule: def_intro · Uses: G1 Leaf basis: def_intro + set_operations_def To treat all composable pairs at once, introduce two candidate blocks and the block relation T. B_1 and B_2 are disjoint with union X. This is only naming; whether T equals R must be proved in S05 to S07, not guessed from a picture. S05 · equivalentBefore (B_1\times B_1)\cup(B_2\times B_2) After \{(0,0),(0,2),(2,0),(2,2)\}\cup\{(1,1),(1,3),(1,4),(3,1),(3,3),(3,4),(4,1),(4,3),(4,4)\} Conditions: none Rule: cartesian_product_def · Uses: S04, cartesian_product_def Leaf basis: cartesian_product_def + finite_counting_basics List by the definition of the Cartesian product: B_1×B_1 has 2·2=4 pairs and B_2×B_2 has 3·3=9 pairs. The two products are disjoint (the blocks are disjoint), so |T|=4+9=13. S06 · impliesBefore (x,y)\in R After R\subseteq T Conditions: none Rule: subset_def · Uses: G1, S05 Leaf basis: subset_def + finite_forall Check the 13 pairs of R one by one: each diagonal pair lies in its own block product; (0,2) and (2,0) have both ends in B_1; (1,3), (3,1), (1,4), (4,1), (3,4), (4,3) have both ends in B_2. Every pair lies in T. S07 · impliesBefore R\subseteq T,\ (x,y)\in T After T\subseteq R,\ \text{hence}\ R=T Conditions: none Rule: set_extensionality · Uses: S05, S06, G1 Leaf basis: set_extensionality + subset_def + finite_counting_basics Each of the 13 pairs of T listed in S05 appears in the list of R in G1, so T⊆R. With R⊆T from S06, set extensionality gives R=T. (A further check: both have exactly 13 distinct elements.) S08 · theorem_applicationBefore R=T=(B_1\times B_1)\cup(B_2\times B_2),\ B_1\cap B_2=\varnothing After xRy\land yRz\Rightarrow xRz\ \text{for all}\ x,y,z\in X Conditions: B_1\cap B_2=\varnothing Rule: L_block_trans · Uses: S04, S07 Leaf basis: L_block_trans + eq_replace By Lemma L_block_trans (proved in S08.1 to S08.3), T is transitive; since R=T, R is transitive too. This covers all 35 composable chains (x,y), (y,z) at once, not a sample. S09 · impliesBefore \text{reflexive, symmetric, transitive} After R\ \text{is an equivalence relation on}\ X Conditions: none Rule: and_intro_elim · Uses: S01, S02, S03, S08 Leaf basis: mko_equiv_def + and_intro_elim Reflexivity (S02), symmetry (S03) and transitivity (S08) all pass, so by the definition in S01, R is an equivalence relation. Only now may the classes be emitted. S10 · impliesBefore [x]=\{y\in X: xRy\} After [0]=[2]=\{0,2\},\ [1]=[3]=[4]=\{1,3,4\} Conditions: R\ \text{equivalence relation (S09)} Rule: eq_class_def · Uses: S09, G1, eq_class_def Leaf basis: eq_class_def + set_builder + relation_def Read off the row of each x: the pairs starting with 0 are (0,0), (0,2), so [0]={0,2}; with 2, (2,2), (2,0), so [2]={0,2}; with 1, (1,1), (1,3), (1,4), so [1]={1,3,4}; with 3, (3,3), (3,1), (3,4); with 4, (4,4), (4,1), (4,3); so [3]=[4]={1,3,4}. S11 · impliesBefore \{0,2\},\ \{1,3,4\} After \{0,2\}\cap\{1,3,4\}=\varnothing,\ \{0,2\}\cup\{1,3,4\}=X Conditions: none Rule: set_operations_def · Uses: S10 Leaf basis: set_operations_def + finite_counting_basics The two distinct classes are disjoint with union X, and 2+3=5=|X|. They are exactly the blocks of S04: the blocks come out of the verified relation, not from a guess based on a picture. S12 · impliesBefore R'=R\setminus\{(3,4),(4,3)\} After R'\ \text{reflexive and symmetric} Conditions: none Rule: finite_forall · Uses: G2, S02, S03 Leaf basis: finite_forall + relation_def + numeric_evaluation R′ keeps all five diagonal pairs, so it is still reflexive; the two removed pairs are mutual reverses, and the remaining 3 pairs of mutually reversed ordered pairs (0,2)/(2,0), (1,3)/(3,1), (1,4)/(4,1) are kept whole, so it is still symmetric. S13 · impliesBefore (3,1)\in R',\ (1,4)\in R' After (3,4)\notin R'\Rightarrow R'\ \text{not transitive} Conditions: none Rule: contradiction · Uses: G2, S12 Leaf basis: contradiction + quantifier_negation + relation_def Take x=3, y=1, z=4: 3R′1 and 1R′4, but (3,4) was removed, so 3R′4 fails. Transitivity is a universal statement, and one counterexample refutes it. S14 · impliesBefore R'\ \text{reflexive, symmetric, not transitive} After R'\ \text{not an equivalence relation; no classes emitted} Conditions: none Rule: mko_equiv_def · Uses: S01, S12, S13, eq_class_def Leaf basis: mko_equiv_def + de_morgan_logic Without transitivity, R′ is not an equivalence relation by S01, and no classes are emitted. Forcing the computation of {y : xR′y} gives {1,3} for x=3 and {1,4} for x=4, which meet in 1 without being equal, so they do not form a partition. This shows that reflexive plus symmetric is not enough, and that grouping by eye is unreliable. ## Substeps and lemmas S08.1 · impliesBefore (x,y)\in T,\ (y,z)\in T After (x,y)\in B_i\times B_i,\ (y,z)\in B_j\times B_j,\ y\in B_i\cap B_j Conditions: none Rule: set_operations_def · Uses: cartesian_product_def, set_operations_def Leaf basis: set_operations_def + cartesian_product_def + exists_elim Take any x, y, z with (x,y) and (y,z) in T. T is the union of two products, so (x,y)∈B_i×B_i for some i and (y,z)∈B_j×B_j for some j. By the definition of the Cartesian product, y lies in B_i (as a second coordinate) and in B_j (as a first coordinate). S08.2 · impliesBefore y\in B_i\cap B_j,\ B_1\cap B_2=\varnothing After i=j Conditions: B_1\cap B_2=\varnothing Rule: contradiction · Uses: S08.1, contradiction Leaf basis: contradiction + set_operations_def If i≠j then {i,j}={1,2} and y∈B_1∩B_2=∅, a contradiction. So i=j. This uses that the blocks are disjoint; with overlapping blocks the step would fail. S08.3 · impliesBefore x\in B_i,\ z\in B_j,\ i=j After (x,z)\in B_i\times B_i\subseteq T Conditions: none Rule: cartesian_product_def · Uses: S08.1, S08.2, forall_intro Leaf basis: cartesian_product_def + forall_intro By S08.1, x∈B_i and z∈B_j, and S08.2 gives i=j, so x and z both lie in B_i and (x,z)∈B_i×B_i⊆T. Since x, y, z were arbitrary, generalization shows T is transitive. S08.1 to S08.3 together prove Lemma L_block_trans. ## Reverse audits - S14 · sufficient_goal_reduction · S01, S13 — Goal G: R′ is not an equivalence relation. Sufficient condition H: some axiom fails; H⇒G by the definition (all three are required). H is supplied forwards by S13. - S13 · premise_audit · G2, contradiction — The complete list of R′ is needed to know (3,4)∉R′. One counterexample suffices; no other chains need checking. - S12 · premise_audit · G2, finite_forall — All 11 pairs of R′ are checked (5+2·3=11); the step does not claim that R′ is transitive. - S11 · premise_audit · S10, set_operations_def — Only the intersection and union of these two concrete sets are computed; the general theorem that classes form a partition is not proved here. - S10 · premise_audit · S09, eq_class_def — Emitting classes requires S09; if not all three checks passed (as for R′), the MKO says no classes are emitted. - S09 · sufficient_goal_reduction · S01, S02, S03, S08 — Goal G: R is an equivalence relation. Sufficient condition H: all three axioms hold; H⇒G by the definition. H is proved forwards in S02, S03 and S08; G is never used as a premise. - S08.3 · premise_audit · S08.2, cartesian_product_def, forall_intro — The proof puts no extra assumption on x, y, z, so generalization applies; this sub-step does not use L_block_trans. - S08.2 · premise_audit · S08.1, contradiction — The argument by contradiction rests on disjoint blocks; this sub-step does not use L_block_trans. - S08.1 · premise_audit · set_operations_def, cartesian_product_def — It only unfolds membership in a union and a Cartesian product; this sub-step does not use L_block_trans. - S08 · premise_audit · S07, L_block_trans — It needs R=T exactly (S07) and disjoint blocks (S04); with only R⊆T, transitivity of T would not transfer to R. - S07 · premise_audit · S06, set_extensionality — Both inclusions come from element-by-element checks; equality may be claimed only because both directions hold. - S06 · premise_audit · G1, S05, subset_def — Only R⊆T is proved here; the reverse inclusion is proved separately in S07. - S05 · inverse_equivalence · cartesian_product_def, set_extensionality — The listed set and the defined set agree element by element, so the step holds both ways. - S04 · premise_audit · def_intro — A definition derives no fact; B_1∩B_2=∅ is immediate and is needed by the lemma later. - S03 · inverse_equivalence · finite_forall, relation_def — All 13 pairs are accounted for (5+2·4=13), with none missed, so the itemwise check and the universal statement are equivalent. - S02 · inverse_equivalence · finite_forall — The universal gives each instance; since the five instances cover all of X, the converse holds as well. - S01 · premise_audit · mko_equiv_def, relation_def — This step only unfolds the definition and lists the three obligations; it derives no new fact. ## Error controls and negative controls Reflexive and symmetric are not enoughThe common mistake named by the MKO is to call a relation an equivalence relation after checking only reflexivity and symmetry. R′ passes both (S12), yet 3R′1 and 1R′4 while (3,4)∉R′ (S13). Transitivity is an independent third obligation. Do not group by looking at the pictureDraw R′: 0 and 2 form one cluster and 1, 3, 4 also look connected; but the would-be classes {1,3} and {1,4} of R′ overlap without being equal. Classes may be read off the relation itself only after all three checks pass (S10). Transitivity must cover every composable chainR has 2·2²+3·3²=35 composable chains (x,y), (y,z). Spot-checking a few (for example (0,2), (2,0) giving (0,0)) is not a proof; this guide uses R=T and Lemma L_block_trans to cover all 35 at once. - R′ is reflexive and symmetric, so R′ is an equivalence relation → reject — 3R′1 and 1R′4 but (3,4)∉R′, so transitivity fails. - A symmetric and transitive relation is always reflexive → reject — On {0,1,2}, S={0,1}×{0,1} is symmetric and transitive (a single block), but (2,2)∉S. - In R′ the chain (0,2), (2,0) gives (0,0)∈R′, so R′ is transitive → reject — One chain succeeding does not mean all do; the chain (3,1), (1,4) fails. - The equivalence classes of R′ are {0,2} and {1,3,4} → reject — R′ is not an equivalence relation, so no classes are emitted; the forced sets {1,3} and {1,4} do not form a partition either. ## Result and limitations R is reflexive (5 diagonal pairs), symmetric (4 pairs of mutually reversed ordered pairs) and transitive (R equals the block relation (B_1×B_1)∪(B_2×B_2), and Lemma L_block_trans covers all 35 composable chains), so R is an equivalence relation with classes {0,2} and {1,3,4}. R′ is reflexive and symmetric, but 3R′1 and 1R′4 without 3R′4, so it is not an equivalence relation and no classes are emitted. - This guide does not prove in general that equivalence classes partition the carrier; S11 checks only the two sets of this example. - finite_forall, relation_def and eq_class_def are premises of this guide. ## Verification and source binding 5 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: 90ad3357e3d147bcb375215a2ad86359916fc907de884703d58672c5ebc480e1 - original source SHA-256: 90ad3357e3d147bcb375215a2ad86359916fc907de884703d58672c5ebc480e1 - Lean: NOT_RUN · independent AI: NOT_MEASURED [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-equivalence-relation-01.json)