Integer: deciding membership, the meaning of the minus sign, and closure under negation

Goal and scope

Inside the reals, take Z={0}∪N⁺∪{−n ∣ n∈N⁺} (N contains 0 by the OCME convention, N⁺=N∖{0}, and −n is the additive inverse of n). Prove −7∈Z; show that the decimal numeral '3.0' denotes the integer 3; prove −2.5∉Z; prove −(−a)=a from uniqueness of additive inverses, in particular −(−4)=4; prove −z∈Z for every z∈Z; and use 5−8=5+(−8)=−3 to tell binary subtraction from the unary minus sign.

Treats only the membership and notation boundary the MKO sets up: the three parts of Z, the minus sign as an additive inverse, and closure under negation. Z is described inside ℝ (using only the addition axioms and order), with N characterized as the smallest inductive set and taken as a premise. It does not prove closure of Z under addition or multiplication and does not treat order or divisibility (the MKO says these need their own claims); it does not treat the semantic correspondence with Lean's Int; and it does not change the canonical MKO or its English edition.

Givens and symbols

• add_assoc
• add_comm
• add_zero
• add_inverse
• order_basics
• numeric_evaluation

• G1 — Work inside the reals ℝ (using only the addition axioms and order). N⊆ℝ is the natural numbers under the OCME convention (containing 0, MKO assumption a1), the smallest inductive subset of ℝ: 0∈N, x∈N ⇒ x+1∈N, and every T⊆ℝ that contains 0 and is closed under x↦x+1 contains N.
• G2 — N⁺=N∖{0}; Z={0}∪N⁺∪{−n ∣ n∈N⁺}.
• G3 — −a denotes the additive inverse of a (a+(−a)=0); binary subtraction a−b is defined as a+(−b).
• G4 — Objects to decide or compute: −7, the decimal numeral '3.0', −2.5, −(−4), 5−8.

• \mathbb{Z} — the set of integers
• N,\ N^{+} — natural numbers (with 0) and positive naturals N∖{0}
• -a — the additive inverse of a (unary minus)
• a-b — binary subtraction, defined as a+(−b)
• T_3 — the inductive set {0,1,2}∪{x ∣ x≥3}

Rules and sources

• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• add_zero · prerequisite — Additive identity: u+0=u.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• 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.
• 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.
• 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.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• 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.
• 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.
• 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.
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• de_morgan_logic · prerequisite — De Morgan's laws for logic: ¬(P∧Q) ⇔ ¬P∨¬Q and ¬(P∨Q) ⇔ ¬P∧¬Q.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• 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.
• 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.
• 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.
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_int_def · cited — The integer set Z contains 0, every positive natural number, and its negative. The notation n∈Z states that n is an integer. · mko-integer
• nat_least_inductive · prerequisite — N is the smallest inductive subset of ℝ: 0∈N and x∈N ⇒ x+1∈N; if T⊆ℝ contains 0 and is closed under x↦x+1, then N⊆T.
• positional_def · prerequisite — Decimal numerals with a point: the digits d_i before the point contribute Σ d_i 10^i and the j-th digit e_j after the point contributes e_j 10^{−j}, added together; for example '3.0' denotes 3·10⁰+0·10⁻¹.
• L_N_T3 · lemma — Let T₃={0,1,2}∪{x∈ℝ ∣ x≥3}; then N⊆T₃.
• L_inv_unique · lemma — For reals a, x, y: if a+x=0 and a+y=0, then x=y (additive inverses are unique).

Main derivation

z\in\mathbb{Z}

z=0\ \lor\ z\in N^{+}\ \lor\ \exists n\in N^{+}:\ z=-n

7=0+1+1+1+1+1+1+1

7\in N^{+},\ -7\in\mathbb{Z}

\text{decimal numeral }3.0

3\cdot10^0+0\cdot10^{-1}=3\in N^{+}\subseteq\mathbb{Z}

-2.5\in\mathbb{Z}

-2.5=0\ \lor\ -2.5\in N^{+}\ \lor\ \exists n\in N^{+}:\ -2.5=-n

-2.5=-n

n=2.5

T_3=\{0,1,2\}\cup\{x\in\mathbb{R}\mid x\ge 3\}

N\subseteq T_3

N\subseteq T_3

2.5\notin N,\ -2.5\notin N

\text{the three disjuncts of S04}

-2.5\notin\mathbb{Z}

(-a)+a=0,\ (-a)+(-(-a))=0

-(-a)=a\quad(a\in\mathbb{R})

-(-4)

4\in N^{+}\subseteq\mathbb{Z}

z\in\mathbb{Z}

-z\in\mathbb{Z}

5-8=5+(-8)

5+(-8)=-3

\text{S02, S03, S08, S10, S11, S12}

-7,\ 3,\ 4,\ -3\in\mathbb{Z};\ -2.5\notin\mathbb{Z};\ \forall z\in\mathbb{Z}:\ -z\in\mathbb{Z}

Substeps and lemmas

0\in T_3;\ x\in\{0,1,2\}

x+1\in\{1,2,3\}\subseteq T_3

x\ge 3

x+1\ge 4\ge 3;\ T_3\ \text{inductive},\ N\subseteq T_3

a+x=0,\ a+y=0

x=x+0=x+(a+y)=(x+a)+y

(x+a)+y

y,\ \text{hence}\ x=y

Reverse audits

• S13 · sufficient_goal_reduction · S02, S03, S08, S09, S10, S11, S12 — The goal is the list in the goal field. Sufficient condition H: S02, S03, S08, S10, S11 and S12 each hold; H gives the goal by conjunction only. The universal statements (S09, S11) come from arguments about an arbitrary element; the goal is never used as a premise.
• S12 · premise_audit · L_inv_unique, add_assoc, add_inverse, numeric_evaluation — Applying uniqueness needs the two equations 3+x=0 and 3+y=0 with x=5+(−8) and y=−3; both are verified (N9, N11).
• S11 · premise_audit · S01, S09, case_analysis, L_inv_unique, forall_intro — The three cases must match the three disjuncts of S01; none may be left out.
• S10 · premise_audit · S09, forall_elim — This is an instance of the general result; conversely, the instance could not prove the general result.
• S09.2 · premise_audit · add_comm, eq_replace, add_zero, eq_refl_symm_trans — Each hypothesis, a+x=0 and a+y=0, is used once; transitivity of equality joins the two parts.
• S09.1 · premise_audit · add_zero, eq_replace, add_assoc — The hypothesis a+y=0 is used once, as a replacement.
• S09 · premise_audit · L_inv_unique, add_comm, forall_intro — The conclusion rests on uniqueness of inverses; it is not a memorized 'two minuses make a plus' but a consequence of uniqueness.
• S08 · premise_audit · S04, S05, S07, de_morgan_logic — All three must be excluded; saying '−2.5 is negative' is not enough, since −7 is negative too and is an integer.
• S07 · premise_audit · S06, contrapositive, subset_def, order_basics — The contrapositive is equivalent to the inclusion; it is not claimed that every element of T₃ is natural.
• S06.2 · premise_audit · S06.1, nat_least_inductive, case_analysis, order_basics — Minimality only needs T₃ to contain 0 and be closed under successor; T₃⊆N is not needed (indeed 3.5∈T₃ is not natural).
• S06.1 · premise_audit · case_analysis, numeric_evaluation — The three cases are checked one by one.
• S06 · premise_audit · L_N_T3 — This step only invokes the lemma; the proof is in the sub-steps.
• S05 · inverse_equivalence · eq_congruence, add_inverse, add_comm, add_assoc — Both directions apply the same defined operation to both sides of an equation.
• S04 · inverse_equivalence · S01, def_unfold — Unfolding a definition holds both ways.
• S03 · premise_audit · positional_def, S01, numeric_evaluation — What is needed is the number the numeral denotes; its appearance (whether it has a decimal point) cannot decide.
• S02 · premise_audit · S01, exists_intro, nat_least_inductive — Only one n∈N⁺ needs to be found; uniqueness is neither needed nor claimed.
• S01 · premise_audit · mko_int_def, G2, G3, def_unfold — This step only unfolds the definition; the three parts cover every member the MKO lists.

Error controls and negative controls

The minus sign is not subtraction itself

One misconception the MKO names is treating the minus sign as the subtraction operation itself. −3 is a number: the additive inverse of 3, with 3+(−3)=0; 5−8 is an operation, defined as 5+(−8), whose value is −3 (S12). −(−4)=4 is not a memorized rule either but a consequence of the uniqueness of inverses (S09).

A decimal point does not decide integrality

Another misconception the MKO names concerns numerals with a decimal point. '3.0' has a decimal point yet denotes the integer 3 (S03); '−2.5' denotes a number that is not an integer (S08). What decides is the number a numeral denotes and whether it falls in one of the three parts of Z, not how it is written.

Examples do not prove general laws

The MKO warns against deriving all integer algebra laws from a few examples. Checking −(−4)=4 and −(−7)=7 (N12) does not prove −(−z)=z for all z; S09 proves it for an arbitrary real a, and S11 proves closure under negation by cases. Closure of Z under addition and multiplication is not proved here and needs its own claims.

• −2.5 is an integer, because it is negative and the integers include negatives → reject — The negative elements of Z are precisely the negatives of positive naturals; 2.5 is not natural (S07), so −2.5∉Z (S08).
• 3.0 is not an integer, because it is written with a decimal point → reject — '3.0' denotes 3, and 3∈N⁺⊆Z (S03).
• −3 denotes the operation 'subtract 3 from something' → reject — −3 is the number with 3+(−3)=0; it is 5−8 that is an operation, 5+(−8), whose value is −3 (S12).
• Since −(−4)=4 and −(−7)=7, −(−z)=z is proved for all integers → reject — Finitely many examples cannot prove a universal statement; the general proof is S09 (uniqueness of inverses).

Result and limitations

With Z={0}∪N⁺∪{−n ∣ n∈N⁺}: −7∈Z; '3.0' denotes 3∈Z; since N⊆{0,1,2}∪{x ∣ x≥3}, neither 2.5 nor −2.5 is natural, so −2.5∉Z. Additive inverses are unique, so −(−a)=a, in particular −(−4)=4; −z∈Z for every z∈Z. 5−8 is the operation 5+(−8), whose value is the number −3∈Z.

• Closure of Z under addition and multiplication, and properties of order and divisibility, need their own claims and are not proved here (as the MKO says).
• nat_least_inductive is a premise (the formal reading of the natural-number MKO); in OCME's construction chain ℝ is built from ℚ, ℤ and N, and this guide uses ℝ only as the setting for membership questions.
• The semantic correspondence with Lean's Int construction, the embedding of naturals and negatives (MKO formal next) is not treated here.

Verification and source binding

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

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

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