Sets: characterized by elements, equal by extensionality, and why unrestricted formation fails

Goal and scope

In the universe ℤ, let A={x∈ℤ ∣ x²=4}, B={−2,2}, C={2,−2,2} and D={2}. Prove A=B and C=B; prove D≠B and distinguish the element 2 from the set {2}. Finally prove that in any domain U with a membership relation there is no R∈U with 'y∈R ⇔ y∉y' for all y∈U, so not every condition forms a set.

Follows the MKO: within a specified universe a set is characterized by its elements, and sets with the same elements are equal. The first part works in the universe ℤ, where all sets are sets of integers; the second part, Russell's argument, uses pure logic and holds for every domain with a membership relation, without choosing ZF, ZFC or any other axiom system. It does not treat the general theory of set operations and does not change the canonical MKO or its English edition.

Givens and symbols

• set_extensionality
• set_builder
• subset_def
• zero_product
• distributive
• numeric_evaluation

• G1 — Universe and types: the first part works in ℤ, and the sets discussed are sets of integers; in x∈S the left side is an integer and the right side a set of integers. List notation: x∈{a,b,c} ⇔ x=a ∨ x=b ∨ x=c, and likewise with two elements or one.
• G2 — A={x∈ℤ ∣ x²=4}, B={−2,2}, C={2,−2,2} and D={2}.
• G3 — Setting for Russell's argument: U is any domain of objects with a binary relation ∈ (for y,z∈U, y∈z is a proposition); no axioms of set theory are assumed; classical logic is used.

• x\in A — x is an element of A
• \{a,b,c\} — list notation: x∈{a,b,c} ⇔ x=a∨x=b∨x=c
• \{x\in\mathbb{Z}\mid P(x)\} — the set carved out of ℤ by the condition P
• A=B — set equality: exactly the same elements
• U — any domain with a membership relation (for Russell's argument)

Rules and sources

• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• eq_congruence · prerequisite — Congruence of equality: if u=v, applying the same defined operation f to both sides gives f(u)=f(v). Operating on one side only is not an instance of this rule.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_zero · prerequisite — Additive identity: u+0=u.
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• 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.
• logic_chain · prerequisite — Chaining: from P⇒Q and Q⇒R infer P⇒R; likewise for ⇔.
• 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.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• 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.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• modus_ponens · prerequisite — Modus ponens: from P and P⇒Q infer Q.
• iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold.
• mko_set · cited — Within a specified universe or type, a set A is characterized by which objects are its elements; sets with exactly the same elements are regarded as equal. · mko-set
• list_set · prerequisite — List notation: x∈{a,b,c} ⇔ x=a ∨ x=b ∨ x=c; likewise with two elements or one.
• or_laws · prerequisite — Commutativity, associativity and idempotence of disjunction: P∨Q ⇔ Q∨P; (P∨Q)∨R ⇔ P∨(Q∨R); P∨P ⇔ P.
• excluded_middle · prerequisite — Excluded middle (classical logic): for every proposition P, P∨¬P.
• typed_membership · prerequisite — Typed membership: in the context of G1, x∈S is a well-formed proposition only when x is an integer and S is a set of integers; a set of integers is not itself an integer.
• L_C · lemma — For every x∈ℤ: x∈C ⇔ x∈B.

Main derivation

\text{a set}\ S\ \text{in the universe}\ \mathbb{Z}

A=B\iff\forall x\in\mathbb{Z}\,(x\in A\iff x\in B)

x\in A

x^2=4

x^2=4

x^2-4=0

x^2-4=0

(x-2)(x+2)=0

(x-2)(x+2)=0

x-2=0\ \lor\ x+2=0

x-2=0\ \lor\ x+2=0

x=2\ \lor\ x=-2

x=2\ \lor\ x=-2

x\in B

\text{for arbitrary}\ x\in\mathbb{Z}:\ x\in A\iff x\in B

A=B

\forall x\in\mathbb{Z}:\ x\in C\iff x\in B

C=B

-2\in B,\ -2\notin D

D\neq B

2\ \text{versus}\ \{2\}

\{2\}\subseteq B\iff 2\in B;\quad \{2\}\in B\ \text{is not a true statement}

\exists R\in U\ \forall y\in U:\ (y\in R\iff y\notin y)

\text{fix such an}\ R\in U

\forall y\in U:\ (y\in R\iff y\notin y)

R\in R\iff R\notin R

R\in R\iff R\notin R

R\in R\ \lor\ R\notin R

\text{the assumption of S12 leads to a contradiction}

\neg\exists R\in U\ \forall y\in U:\ (y\in R\iff y\notin y)

\text{conclusions of S08, S09, S10, S11, S15}

A=B=C,\ D\neq B,\ \{2\}\subseteq B,\ \neg\exists R\in U\ \forall y\in U:\ (y\in R\iff y\notin y)

Substeps and lemmas

x\in C

x=2\lor x=-2\lor x=2

x=2\lor x=-2\lor x=2

x=-2\lor x=2,\ \text{i.e.}\ x\in B

R\in R

R\notin R,\ \text{contradiction}

R\notin R

R\in R,\ \text{contradiction}

Reverse audits

• S16 · sufficient_goal_reduction · S08, S09, S10, S11, S15, and_intro_elim — Goal G: the four conclusions the problem asks for. Sufficient condition H: S08, S09, S10, S11 and S15; H⇒G just lists them. H is proved forwards from G1 to G3; G is never used as a premise.
• S15 · premise_audit · S12, S14, contradiction, exists_elim — The witness name R has no free occurrence in the conclusion, as exists_elim requires; nothing is claimed about which conditions form sets in any particular axiom system (the MKO chooses neither ZF nor ZFC).
• S14.2 · premise_audit · S13, modus_ponens, iff_intro — Only the other direction of the biconditional is used.
• S14.1 · premise_audit · S13, modus_ponens, iff_intro — Only one direction of the biconditional is used.
• S14 · premise_audit · S13, excluded_middle, case_analysis — The two cases cover every possibility, by excluded middle.
• S13 · premise_audit · S12, forall_elim — The instantiation needs R∈U, which is exactly what 'R is a set of the domain' means.
• S12 · premise_audit · G3, exists_elim — This is a temporary assumption, used only inside the proof by contradiction S12 to S14; the witness R has no free occurrence in the final conclusion S15.
• S11 · premise_audit · subset_def, list_set, typed_membership — {2}⊆B ⇔ 2∈B holds both ways by the definition of subset and list notation; '{2}∈B is not true' depends only on the type distinction and needs no further axiom.
• S10 · premise_audit · list_set, set_extensionality, contradiction — One element in one set but not the other is enough to refute equality; it is not claimed that they share no element (2 is in both).
• S09.2 · inverse_equivalence · or_laws, list_set — Commutativity, associativity and idempotence are all two-way equivalences.
• S09.1 · inverse_equivalence · list_set — The definition of list notation is two-way.
• S09 · premise_audit · L_C, set_extensionality — The equivalence is needed for every x; the lemma is proved for an arbitrary x.
• S08 · premise_audit · S02, S07, logic_chain, forall_intro, set_extensionality — Every integer must be covered: x was arbitrary, with no extra assumption. x=3 is only an example and not part of the proof.
• S07 · inverse_equivalence · or_laws, list_set — Commutativity and the definition of list notation are both two-way.
• S06 · inverse_equivalence · eq_congruence, add_inverse, numeric_evaluation — Substituting back: 2−2=0 and (−2)+2=0.
• S05 · inverse_equivalence · zero_product — Both directions are contained in zero_product.
• S04 · inverse_equivalence · distributive, eq_replace — Replacement by an identity is two-way; N1 is an independent polynomial check.
• S03 · inverse_equivalence · eq_congruence, add_inverse — Adding −4 and adding 4 undo each other, with no side condition in ℤ.
• S02 · inverse_equivalence · set_builder, and_intro_elim — The set-builder definition is itself two-way, and dropping the conjunct x∈ℤ, which already holds, is two-way as well.
• S01 · premise_audit · G1, mko_set, set_extensionality — This step only states the criterion and derives no new fact.

Error controls and negative controls

An element and the set containing only it

The MKO names the common mistake of confusing an element x with the set containing only x. 2 is an integer and {2} is a set of integers: 2∈B and {2}⊆B both hold and are equivalent (S11), but '{2}∈B' is not true and {2} is not equal to B (S10). On meeting notation such as 2 or {2}, first identify whether it denotes an integer element or a set of integers in this context, then decide between ∈ and ⊆.

Not every condition forms a set

Another mistake identified in the MKO is believing that any condition defines a set without restriction. S12 to S15 prove that for any domain U, no R∈U satisfies y∈R iff y∉y for every y∈U. This does not exclude forming the relative subset R={y∈U | y∉y}⊆U by separation in ordinary set theory; that R has R∉U. So set formation needs principles, for example carving elements out of a known set (as with {x∈ℤ ∣ x²=4} in S02); this guide does not choose a particular axiom system.

Order and repetition do not create new sets

C={2,−2,2} is written with three symbols, but by extensionality C=B={−2,2} (S09). Distinguishing order or multiplicity needs a different kind of object, such as the ordered triple (2,−2,2) or a multiset; those are not sets in the sense of this MKO.

• {2,−2,2} has three elements, so it differs from {−2,2} → reject — x∈{2,−2,2} ⇔ x=−2∨x=2, the same elements as B, so they are equal by extensionality (S09).
• 2 and {2} are the same thing → reject — 2 is an integer and {2} is a set of integers; 2∈B holds while '{2}∈B' is not true (S11).
• For every condition P(y), {y ∣ P(y)} is a set → reject — Take P(y) to be y∉y; S12 to S15 derive a contradiction.
• A is written with a condition and B as a list, so A≠B → reject — A set is determined by its elements, not by how it is written; S08 proves A=B.

Result and limitations

In the universe ℤ, A={x∈ℤ ∣ x²=4}, B={−2,2} and C={2,−2,2} have the same elements, so A=B=C; D={2}≠B because −2∈B and −2∉D. 2 is an integer and {2} is a set: 2∈B and {2}⊆B hold, while '{2}∈B' is not true. For any domain U with a membership relation, no R∈U satisfies y∈R iff y∉y for every y∈U. This rules out requiring every condition to be represented without restriction by a set within U; it does not prohibit the relative subset R={y∈U | y∉y}⊆U formed by separation in ordinary set theory (which has R∉U).

• The typed context of the first part (typed_membership) is a premise of this guide, matching the MKO's 'specified universe or type'; in untyped set theory the relation between 2 and {2} depends on the chosen axioms and the coding of numbers, which this guide does not treat.
• Russell's argument shows only that no internal R∈U represents y∉y for every y∈U, and does not rule out a relative subset R⊆U formed by separation; which conditions do form sets is fixed by a concrete axiom system (the MKO's third paragraph), which this guide does not choose.

Verification and source binding

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 81bb053444cb9fae0c721ca4c93b2655272c5d7fc28922dbed489183ee255de8
• original source SHA-256: 81bb053444cb9fae0c721ca4c93b2655272c5d7fc28922dbed489183ee255de8
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)