Natural number: deciding membership through the smallest inductive set, and telling numbers from numerals

Goal and scope

Under the OCME convention (0∈N), read the MKO's '0 and the numbers obtained from 0 by finitely many successor steps' as 'the smallest set of reals that contains 0 and is closed under x↦x+1'. On this basis prove 0∈N and 3∈N; show that the binary numeral '11' and the decimal numeral '3' denote the same natural number; prove −1∉N and 1/2∉N; and compare least elements with the convention N⁺=N∖{0}, in which natural numbers start at 1.

Works inside the reals ℝ (using only properties of addition and order) so that membership of numbers such as −1 and 1/2 in N can be decided; this is a characterization of N inside ℝ, not a foundational construction of N (in OCME's construction chain ℝ is in fact built from ℚ, ℤ and N). It does not treat the Peano axioms or the semantic bridge to Lean's Nat, and does not prove that 'smallest inductive set' and 'finitely many successor steps' are equivalent readings. It does not change the canonical MKO or its English edition.

Givens and symbols

• order_basics
• subset_def
• set_operations_def
• numeric_evaluation

• G1 — The numbers discussed are real numbers; the successor operation is S(x)=x+1. n denotes an arbitrary number whose membership in N is under consideration (MKO assumption a2).
• G2 — Formal reading of the MKO: a subset T⊆ℝ is inductive if 0∈T and x+1∈T for every x∈T. N is defined as the intersection of all inductive subsets of ℝ, that is, the smallest set containing 0 and closed under successor. By this entry's convention N contains 0 (MKO assumption a1).
• G3 — Positional notation: a base-b numeral whose digits, read from right to left, are d₀, d₁ and so on up to d_k denotes the number Σ_{i=0}^{k} d_i b^i.
• G4 — Numbers to decide: 0, 3, −1, 1/2; numerals: the decimal '3' and the binary '11'.

• N — the set of natural numbers under the OCME convention (containing 0)
• N^{+} — N∖{0}, the convention that starts at 1
• S(x)=x+1 — successor
• T_1,\ T_2 — two inductive sets used to exclude non-natural numbers
• \bigcap — intersection of a family of sets

Rules and sources

• 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.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• 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.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• 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.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• modus_ponens · prerequisite — Modus ponens: from P and P⇒Q infer Q.
• 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.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• add_zero · prerequisite — Additive identity: u+0=u.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• 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.
• 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.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_nat_def · cited — Under this entry's convention, the natural-number set N contains 0 and the numbers 1, 2, 3, and so on obtained by finitely many successor steps from 0. · mko-natural-number
• inductive_def · prerequisite — Inductive set: T⊆ℝ is inductive if 0∈T and x+1∈T for every x∈T.
• nat_as_intersection · prerequisite — N=⋂{T⊆ℝ ∣ T is inductive}: x∈N if and only if x belongs to every inductive set.
• big_intersection_def · prerequisite — Intersection of a family: for a nonempty family 𝓕, x∈⋂𝓕 ⇔ x∈T for every T∈𝓕; hence ⋂𝓕⊆T for every T∈𝓕.
• positional_def · prerequisite — Positional notation: a base-b numeral with digits d₀, d₁ and so on up to d_k from right to left denotes Σ_{i=0}^{k} d_i b^i.
• L_N_inductive · lemma — N itself is inductive: 0∈N, and x+1∈N for every x∈N.

Main derivation

N

N=\bigcap\{T\subseteq\mathbb{R}\mid 0\in T,\ \forall x\in T:\ x+1\in T\}

N=\bigcap\{T\ \text{inductive}\}

0\in N,\ \forall x\in N:\ x+1\in N

T\subseteq\mathbb{R}\ \text{inductive}

N\subseteq T

3

((0+1)+1)+1

0\in N

1\in N,\ 2\in N,\ 3\in N

\text{binary numeral }11,\ \text{decimal numeral }3

1\cdot2^1+1\cdot2^0=3=3\cdot10^0

T_1=\{x\in\mathbb{R}\mid x\ge 0\}

T_1\ \text{inductive}

T_1\ \text{inductive}

N\subseteq T_1:\ \forall n\in N,\ n\ge 0

-1<0

-1\notin N

T_2=\{0\}\cup\{x\in\mathbb{R}\mid x\ge 1\}

T_2\ \text{inductive}

T_2\ \text{inductive}

N\subseteq T_2

\tfrac{1}{2}\neq 0,\ \tfrac{1}{2}<1

\tfrac{1}{2}\notin N

N^{+}=N\setminus\{0\}

0\notin N^{+},\ 3\in N^{+},\ \min N^{+}=1,\ \min N=0

\text{S05, S06, S09, S12, S13}

0,3\in N;\ 11_{2}=3_{10};\ -1,\tfrac{1}{2}\notin N;\ \min N=0,\ \min N^{+}=1

Substeps and lemmas

T\ \text{inductive}\Rightarrow 0\in T

0\in N

x\in N

x+1\in N

x=0

x+1=1\in T_2

x\ge 1

x+1\ge 2\ge 1,\ x+1\in T_2

Reverse audits

• S14 · sufficient_goal_reduction · S03, S05, S06, S09, S12, S13 — The goal is the list in the goal field. Sufficient condition H: S05, S06, S09, S12 and S13 each hold; H gives the goal by conjunction only. Excluding −1 and 1/2 relies on the induction principle S03 and the two inductive sets; the goal is never used as a premise.
• S13 · premise_audit · set_operations_def, S11, S08, S05 — Each least-element conclusion needs two things: a lower bound, and the bound itself belonging to the set.
• S12 · premise_audit · S11, contrapositive, set_operations_def — 1/2 must both differ from 0 and fail to be ≥1 in order to lie in neither part of T₂.
• S11 · premise_audit · S03, S10.2 — Only that T₂ is inductive is needed; T₂⊆N is not claimed.
• S10.2 · premise_audit · order_basics, case_analysis, S10.1 — It uses that adding the same number preserves order (and equality); only both cases together give closure.
• S10.1 · premise_audit · order_basics, add_zero — Direct computation with no side condition.
• S10 · premise_audit · inductive_def, case_analysis, set_operations_def — x∈T₂ has only two possibilities, and both cases must be handled, otherwise closure is not fully proved.
• S09 · premise_audit · S08, contrapositive, subset_def — The contrapositive is equivalent to the original; the converse (x∈T₁ ⇒ x∈N) is not claimed, and indeed 1/2∈T₁ is not natural.
• S08 · premise_audit · S03, S07, S02 — It uses only that T₁ is inductive; 'least element' also needs 0 itself to be in N.
• S07 · premise_audit · inductive_def, order_basics — It needs 0<1; if the 'successor' were x↦x−1, T₁ would no longer be closed.
• S06 · inverse_equivalence · positional_def, numeric_evaluation — Both evaluations are exact computations (N2, N3), so the equality holds both ways.
• S05 · premise_audit · S02, S04, modus_ponens — Each step is modus ponens; the backward direction (from 3∈N back to 2∈N) is neither claimed nor needed.
• S04 · inverse_equivalence · numeric_evaluation — Exact integer arithmetic, valid both ways (N1).
• S03 · premise_audit · big_intersection_def, subset_def, forall_elim — It needs only that T is inductive; T⊆N is neither needed nor claimed.
• S02.2 · premise_audit · inductive_def, big_intersection_def, forall_intro, forall_elim — T must be arbitrary; checking a single inductive set would not put x+1 into the intersection.
• S02.1 · premise_audit · inductive_def, big_intersection_def — It needs every inductive set to contain 0; one set containing 0 would not be enough.
• S02 · premise_audit · L_N_inductive, S01 — This step only invokes the lemma; its two parts are proved in the sub-steps.
• S01 · premise_audit · G2, nat_as_intersection, mko_nat_def, big_intersection_def — This step only adopts the definition; its equivalence with the MKO's wording is listed as an open item and not proved here.

Error controls and negative controls

Whether 0 is natural depends on the convention

The misconception identified in the MKO is thinking that all textbooks agree on whether 0 is natural. OCME fixes 0∈N (matching Lean's Nat), but some textbooks start natural numbers at 1 (N⁺ here). The same phrase 'the least natural number' means 0 in OCME and 1 under the N⁺ convention (S13). Check an external source's definition before reading it.

Numbers versus numerals

Another misconception identified in the MKO is confusing how a number is written with the number itself. The string '10' denotes ten in decimal (1·10+0=10, N12) and two in binary (1·2+0=2, N11); '11' (binary) and '3' (decimal) denote the same number, and so do the binary '110' and the decimal '6' (N13). Membership in N is a property of the number, so the base of a numeral must be fixed before deciding.

Excluding a number needs an inductive set, not a listing

To prove 1/2∉N one cannot list 0, 1, 2, 3 and say '1/2 is not on the list': the list is always finite and N is not. Nor can one assert without proof that '1/2 is not obtained from 0 by finitely many successor steps'; that is exactly what must be shown. The correct method is to find an inductive set T₂ that misses 1/2 (S10 to S12). Likewise −1+1=0∈N does not give −1∈N, because closure only pushes forwards.

• Every textbook counts 0 as a natural number → reject — Conventions differ; many textbooks start natural numbers at 1 (N⁺), and the MKO explicitly says to check the definition first.
• The string '10' always denotes ten → reject — In binary '10' denotes 1·2+0=2 (N11).
• 1/2 is natural because it is obtained from 0 by adding 1/2 → reject — Successor allows adding 1 only; T₂ is an inductive set missing 1/2, so 1/2∉N (S12).
• −1 is natural because −1+1=0∈N → reject — Closure says x∈N ⇒ x+1∈N, not the reverse; N⊆{x ∣ x≥0} excludes −1 (S09).

Result and limitations

Reading N as the smallest set of reals containing 0 and closed under x↦x+1: 0∈N and 3=S(S(S(0)))∈N; the binary '11' and the decimal '3' both denote 3; since N⊆{x ∣ x≥0}, −1∉N; since N⊆{0}∪{x ∣ x≥1}, 1/2∉N. The least element of OCME's N is 0, while that of N⁺=N∖{0} is 1.

• This guide adopts 'smallest inductive set' as the formal reading of the MKO's 'obtained from 0 by finitely many successor steps'; a proof that the two readings are equivalent, and the semantic bridge to the Peano axioms or Lean's Nat (MKO formal next), are not treated here.
• This guide uses ℝ as an ambient ordered field in which to ask membership questions; in OCME's construction chain ℝ is built from ℚ, ℤ and N, so this is a characterization of N inside ℝ, not a foundational definition of N.

Verification and source binding

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

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

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