Set membership: x∈A is a proposition, kept apart from ⊆, = and a program's membership test

Goal and scope

In a typed context let A={1,2,3}, B={1,2}, 𝓕={{1,2},{3}} (a set whose elements are sets of integers) and E={n∈ℤ ∣ 2∣n}. Decide with reasons whether each holds: 2∈A; 4∈A; B⊆A; A⊆B; B∈𝓕; {1}∈𝓕; 1000000∈E; 7∈E. Also explain why 1∈B and B∈𝓕 do not give 1∈𝓕, and why a programming language's membership test cannot replace the semantics of set membership.

Follows the MKO: given a set A and an object x, x∈A is a proposition stating that x is an element of A. Works in a typed context with sets of integers and a set of sets of integers, using only list and set-builder notation. It does not set up axioms of set theory or the details of the Lean mapping (the MKO's third paragraph serves only as context), and does not change the canonical MKO or its English edition.

Givens and symbols

• subset_def
• set_extensionality
• set_builder
• divides_def
• order_basics
• numeric_evaluation

• G1 — Typed context: the objects are integers; A, B and E are sets of integers; 𝓕 is a set of sets of integers. x∈S is a well-formed proposition only when the type of x is the element type of S. List notation: x∈{a,b,c} ⇔ x=a ∨ x=b ∨ x=c (likewise with two elements or one); the same applies to a list of sets, where = is set equality.
• G2 — A={1,2,3}, B={1,2}, 𝓕={{1,2},{3}} and E={n∈ℤ ∣ 2∣n}.

• x\in A — x is an element of A (a proposition)
• B\subseteq A — every element of B is an element of A
• \mathcal{F} — a set whose elements are sets of integers
• E=\{n\in\mathbb{Z}\mid 2\mid n\} — the set of even integers, given by a condition
• \{1\} — the set whose only element is 1

Rules and sources

• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• 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).
• divides_def · prerequisite — Divisibility: for integers a, b, a∣b means there is an integer k with b=ak.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• de_morgan_logic · prerequisite — De Morgan's laws for logic: ¬(P∧Q) ⇔ ¬P∨¬Q and ¬(P∨Q) ⇔ ¬P∧¬Q.
• 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.
• 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.
• imp_intro · prerequisite — →-introduction (discharging a hypothesis): if Q is derived inside a scope that temporarily assumes P, then P⇒Q follows, and P may no longer be used as known.
• 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.
• 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.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• two_nonzero · prerequisite — In the reals 0<1, hence 0<1+1=2, so 2≠0.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_member · cited — Given a set A and an object x, x∈A is a proposition stating that x is an element of A. · mko-set-membership
• list_set · prerequisite — List notation: x∈{a,b,c} ⇔ x=a ∨ x=b ∨ x=c; likewise with two elements or one.
• typed_membership · prerequisite — Typed membership: x∈S is a well-formed proposition only when the type of x is the element type of S; an integer is not a set of integers, and a set of integers is not an integer.
• int_no_gap · prerequisite — No gaps in the integers: for integers k and m, k≤m or k≥m+1.
• python_in · cited — For the string type, x in y is True if and only if x is a substring of y; hence '12' in '123' evaluates to True. · Python Software Foundation, Python Language Reference, Section 6.10.2 Membership test operations

Main derivation

x,\ A

x\in A\ \text{is a proposition: }x\ \text{is an element of}\ A

2\in A

2=1\lor 2=2\lor 2=3:\ \text{true, since}\ 2=2

4\in A

4\neq 1\land 4\neq 2\land 4\neq 3,\ \text{so}\ 4\notin A

B\subseteq A

\forall x\,(x\in B\Rightarrow x\in A)

x\in B\ (x\ \text{arbitrary})

x=1\ \lor\ x=2

x\in B\Rightarrow x\in A\ \text{for arbitrary}\ x

B\subseteq A

3\in A,\ 3\notin B

A\not\subseteq B

B\in\mathcal{F}

B=\{1,2\}\lor B=\{3\}:\ \text{true}

\{1\}\in\mathcal{F}

\{1\}\neq\{1,2\},\ \{1\}\neq\{3\},\ \text{so}\ \{1\}\notin\mathcal{F}

1\in B,\ B\in\mathcal{F}

1\in\mathcal{F}\ \text{is not a true statement}

1000000\in E

1000000=2\cdot 500000,\ \text{so}\ 1000000\in E

k\in\mathbb{Z}\ \text{with}\ 2k=7\ ?

k\le 3\ \lor\ k\ge 4

\forall k\in\mathbb{Z}:\ 2k\neq 7

7\notin E

\text{Python: }'12'\ \text{in}\ '123'

\text{True (substring test), while}\ '12'\notin\{'1','2','3'\}

\text{verdicts of S02 to S14}

2\in A,\ 4\notin A,\ B\subseteq A,\ A\not\subseteq B,\ B\in\mathcal{F},\ \{1\}\notin\mathcal{F},\ 1000000\in E,\ 7\notin E

Substeps and lemmas

x=1

x\in A\ \ (1=1)

x=2

x\in A\ \ (2=2)

k\le 3

2k\le 6<7,\ \text{so}\ 2k\neq 7

k\ge 4

2k\ge 8>7,\ \text{so}\ 2k\neq 7

Reverse audits

• S15 · sufficient_goal_reduction · S02, S03, S06, S07, S08, S09, S10, S11, S13, S14, and_intro_elim — Goal G: the verdicts and explanations asked for. Sufficient condition H: the conclusions of the listed steps; H⇒G just lists them. H is proved forwards from G1, G2 and the cited rule; G is never used as a premise.
• S14 · premise_audit · python_in, list_set — The program behaviour comes from the cited language reference (citation_verified; no program was run for this guide); the set side uses only list notation. It is not claimed that every language or container type behaves this way.
• S13 · premise_audit · S12, case_analysis, set_builder, divides_def — The two branches must cover every integer (S12).
• S12.2 · premise_audit · order_basics — As in S12.1.
• S12.1 · premise_audit · order_basics, two_nonzero — 2>0 is used; no converse is claimed.
• S12 · premise_audit · int_no_gap — The two branches cover every integer.
• S11 · premise_audit · set_builder, divides_def, exists_intro, numeric_evaluation — One integer witness, 500000, is needed (N8).
• S10 · premise_audit · typed_membership, S08 — The conclusion depends on the type distinction; an untyped verdict would need a coding of numbers, which this guide does not treat.
• S09 · premise_audit · set_extensionality, list_set, de_morgan_logic — Each set inequality needs one element in one set only; with both disjuncts denied, the disjunction is false.
• S08 · premise_audit · list_set, typed_membership, eq_refl_symm_trans — It needs matching types (B is a set of integers) and one true disjunct.
• S07 · premise_audit · list_set, quantifier_negation, exists_intro — One counterexample is enough to refute inclusion.
• S06 · sufficient_goal_reduction · S04, S05, case_analysis, imp_intro, forall_intro — Goal G: B⊆A. Sufficient condition H: ∀x (x∈B⇒x∈A); H⇒G by S04. H is proved forwards in S05 and its sub-steps.
• S05.2 · premise_audit · list_set, S02, eq_replace — This reuses S02 directly.
• S05.1 · premise_audit · list_set, eq_replace — After replacing x by 1, one true disjunct suffices.
• S05 · premise_audit · list_set, imp_intro — List notation gives exhaustive branches; the temporary assumption is discharged in S06.
• S04 · inverse_equivalence · subset_def — Unfolding and folding a definition are two-way.
• S03 · premise_audit · list_set, de_morgan_logic, numeric_evaluation — To deny a disjunction every disjunct must fail (N1 to N3).
• S02 · premise_audit · list_set, eq_refl_symm_trans — A disjunction needs only one true disjunct.
• S01 · premise_audit · G1, G2, mko_member — This step only states the definition and the types and derives no new fact.

Error controls and negative controls

Membership and inclusion are different relations

The MKO names the mistake of confusing x∈A with B⊆A. Here B⊆A (S06) but B is not an element of A; B∈𝓕 (S08) and {1}⊆B, yet {1} is not an element of 𝓕 (S09); and 1∈B, B∈𝓕 do not give 1∈𝓕 (S10). ∈ relates an object to a set, ⊆ relates two sets of the same type, and their inference rules differ.

A program's membership test is not set semantics

Another mistake identified in the MKO is treating a program container's membership test as the whole of set semantics. By the cited Python reference, in on strings is a substring test and '12' in '123' is True, whereas the set-membership statement '12'∈{'1','2','3'} is false (S14). Before checking a set statement with a program, confirm that the operator's semantics agree with ∈.

x∈A is a proposition and can be false

4∈A and 7∈E are false propositions (S03, S13), and they are still propositions. E is given by a condition, so deciding 1000000∈E only requires checking the condition (S11), without listing or storing its elements: a set need not rely on a physical container to exist (the MKO's first paragraph).

• Since B⊆A, B∈A → reject — The elements of A are the integers 1, 2, 3; B is a set and is none of them (in the typed reading B∈A is not even well formed).
• 1∈B and B∈𝓕, so 1∈𝓕 → reject — ∈ is not transitive; the elements of 𝓕 are the sets {1,2} and {3}, and 1 is neither (S10).
• {1}⊆{1,2} and {1,2}∈𝓕, so {1}∈𝓕 → reject — {1} equals neither {1,2} nor {3} (S09).
• In Python '12' in '123' is True, so as sets '12'∈{'1','2','3'} → reject — in on strings is a substring test; '12' equals none of the one-character strings (S14).

Result and limitations

2∈A is true and 4∈A is false (still a proposition); B⊆A is true and A⊆B is false (3∈A, 3∉B); B∈𝓕 is true and {1}∈𝓕 is false although {1}⊆B; 1000000∈E is true (1000000=2·500000) and 7∈E is false. 1∈B and B∈𝓕 do not give 1∈𝓕, because ∈ is not transitive and in the typed context '1∈𝓕' is not even well formed. Python's '12' in '123' is True as a substring test, while '12'∈{'1','2','3'} is false: a program's membership test is not the semantics of set membership.

• The string-membership semantics of python_in have been checked against the official Python Language Reference. This is documentation verification, not a claim that the program in the guide was executed.
• This guide presupposes a typed context (typed_membership); in untyped set theory the verdict on 1∈𝓕 depends on how numbers are coded, which is not treated here.

Verification and source binding

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

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

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