Arithmetic operations: whether the same inputs give a defined result in ℕ, ℤ and ℚ

Goal and scope

Take a=3 and b=5. In each of the number systems ℕ (including 0), ℤ and ℚ, decide whether a+b, a·b, a−b and a÷b are defined; when they are, compute the result and decide which systems it belongs to. Then decide whether 3÷0 and 0÷0 are defined in these three systems.

Treats only the three stated systems ℕ⊂ℤ⊂ℚ and one stated pair of inputs; difference and quotient are defined by the equations b+c=a and b·q=a having exactly one solution in the system (G2). It illustrates the MKO's point that whether an operation is defined, and whether its result stays in the original system, must be stated together with the system and the division-by-zero boundary. It does not construct these systems, does not treat other operations such as truncated subtraction or division with remainder, and does not change the canonical MKO or its English edition.

Givens and symbols

• order_basics
• add_inverse
• mul_inverse_nonzero
• mul_zero
• numeric_evaluation

• G1 — Number systems: ℕ={n∈ℤ ∣ n≥0} and ℕ⊂ℤ⊂ℚ; the three share one addition, one multiplication and one order (those of ℚ restricted to ℤ and ℕ).
• G2 — Difference and quotient: let S be one of these systems and a,b∈S. If exactly one c∈S satisfies b+c=a, then a−b is defined in S and a−b=c; if exactly one q∈S satisfies b·q=a, then a÷b is defined in S and a÷b=q. If there is no such element, or more than one, the operation is undefined in S for these inputs.
• G3 — Inputs: a=3 and b=5; in addition, the two inputs with divisor zero, (3,0) and (0,0).

• \mathbb{N} — the set of nonnegative integers 0, 1, 2 and so on
• \mathbb{Z},\ \mathbb{Q} — the integers and the rationals
• a-b — the unique c in the stated system with b+c=a
• a\div b — the unique q in the stated system with b·q=a
• \tfrac{1}{u} — the reciprocal of a nonzero rational u

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.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• 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.
• add_zero · prerequisite — Additive identity: u+0=u.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• 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.
• 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_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• 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.
• 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.
• mul_one · prerequisite — Multiplicative identity: 1·u=u.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_arith · cited — Each arithmetic operation forms a result from two inputs. Whether the operation is defined and whether the result remains in the original number system must be stated together with boundaries such as division by zero. · mko-arithmetic-operations
• nat_closed · prerequisite — ℕ is closed under addition and multiplication: if m,n∈ℕ then m+n∈ℕ and m·n∈ℕ (sums and products of nonnegative integers are nonnegative integers).
• int_no_gap · prerequisite — No gaps in the integers: for integers k and m, k≤m or k≥m+1; in particular no integer lies strictly between m and m+1.
• L_sub · lemma — In ℤ or in ℚ, for a, b, c in that system: b+c=a ⇔ c=a+(−b).
• L_div · lemma — In ℚ, for a,q∈ℚ and b≠0: b·q=a ⇔ q=a·(1/b).

Main derivation

a,b\ \text{and an operation, system not yet stated}

S\in\{\mathbb{N},\mathbb{Z},\mathbb{Q}\};\ a-b=c\iff b+c=a\ (\text{unique }c\in S);\ a\div b=q\iff bq=a\ (\text{unique }q\in S)

3,5\in\mathbb{N}

3+5=8\in\mathbb{N},\quad 3\cdot 5=15\in\mathbb{N}

c\in\mathbb{N}

5+c\ge 5

\forall c\in\mathbb{N}:\ 5+c\ge 5>3

\neg\exists c\in\mathbb{N}:\ 5+c=3

\neg\exists c\in\mathbb{N}:\ 5+c=3

3-5\ \text{is undefined in}\ \mathbb{N}

5+c=3,\ c\in\mathbb{Z}

c=3+(-5)=-2

c=-2\ \text{is the only solution in}\ \mathbb{Z}

3-5=-2\ \text{in}\ \mathbb{Z},\quad -2\notin\mathbb{N}

q\in\mathbb{Z}\ \text{with}\ 5q=3\ ?

q\le 0\ \lor\ q\ge 1

q\le 0\Rightarrow 5q\neq 3,\quad q\ge 1\Rightarrow 5q\neq 3

\neg\exists q\in\mathbb{Z}:\ 5q=3;\ 3\div 5\ \text{undefined in}\ \mathbb{Z}\ \text{and in}\ \mathbb{N}

5q=3,\ q\in\mathbb{Q}

q=3\cdot\tfrac{1}{5}=\tfrac{3}{5}

q=\tfrac{3}{5}\ \text{is the only solution in}\ \mathbb{Q}

3\div 5=\tfrac{3}{5}\ \text{in}\ \mathbb{Q},\quad 0<\tfrac{3}{5}<1,\ \tfrac{3}{5}\notin\mathbb{Z}

q\in\mathbb{Q}

0\cdot q=0

\forall q\in\mathbb{Q}:\ 0\cdot q=0\neq 3

\neg\exists q\in\mathbb{Q}:\ 0\cdot q=3;\ 3\div 0\ \text{undefined in}\ \mathbb{Q},\mathbb{Z},\mathbb{N}

\forall q:\ 0\cdot q=0

0\cdot 0=0,\ 0\cdot 1=0,\ 0\neq 1;\ 0\div 0\ \text{undefined in}\ \mathbb{N},\mathbb{Z},\mathbb{Q}

\text{verdicts of S02, S05, S07, S09, S11, S13, S14}

3+5=8,\ 3\cdot 5=15\ (\mathbb{N});\ 3-5=-2\ (\mathbb{Z});\ 3\div 5=\tfrac{3}{5}\ (\mathbb{Q});\ 3\div 0,\ 0\div 0\ \text{undefined}

Substeps and lemmas

b+c=a

(-b)+(b+c)=(-b)+a

(-b)+(b+c)=(-b)+a

c=a+(-b)

q\le 0

5q\le 0<3,\ \text{so}\ 5q\neq 3

q\ge 1

5q\ge 5>3,\ \text{so}\ 5q\neq 3

bq=a

\tfrac{1}{b}(bq)=\tfrac{1}{b}a

\tfrac{1}{b}(bq)=\tfrac{1}{b}a

q=a\cdot\tfrac{1}{b}

Reverse audits

• S15 · sufficient_goal_reduction · S02, S05, S07, S09, S11, S13, S14, and_intro_elim — Goal G: a verdict for each system and each operation. Sufficient condition H: the conclusions of S02, S05, S07, S09, S11, S13 and S14; H⇒G just lists them together. H is proved forwards from G1 to G3; G is never used as a premise.
• S14 · premise_audit · S12, G2, def_unfold — Two distinct solutions are enough to defeat uniqueness; no particular value of 0÷0 is claimed.
• S13 · premise_audit · S12, contradiction, G2 — The contradiction depends only on S12 holding for all q and on 3≠0; the conclusion is non-existence, not 'the result is 0' and not 'the result is infinity'.
• S12 · premise_audit · mul_zero, mul_comm — mul_zero holds for every q (its reason is in the glossary); this step uses no extra assumption about q.
• S11 · premise_audit · S10, G2, int_no_gap, order_basics — It needs existence and uniqueness from S10 and 0<3/5<1; it says only that this quotient is defined in ℚ, not that every division in ℚ is defined (see S13 and S14).
• S10.2 · inverse_equivalence · mul_assoc, mul_comm, mul_one, mul_inverse_nonzero — Expressions are only replaced by equal ones, so the step is two-way; (1/b)b=1 needs b≠0.
• S10.1 · inverse_equivalence · eq_congruence, mul_inverse_nonzero — Multiplying by 1/b and multiplying by b undo each other, given exactly b≠0.
• S10 · inverse_equivalence · L_div, numeric_evaluation — Backward: substitute, 5·(3/5)=3. The lemma's hypothesis 5≠0 holds and both directions are proved, so the solution exists and is unique.
• S09 · premise_audit · S08, S08.1, S08.2, case_analysis, G2 — It needs the two cases to cover all integers (S08); checking a few values of q would not show that there is no solution.
• S08.2 · premise_audit · order_basics, mul_one — As in S08.1, 5>0 is used; no converse is claimed.
• S08.1 · premise_audit · order_basics, mul_zero — 5>0 is what keeps the direction of the inequality; only 5q≠3 is concluded and no converse is claimed.
• S08 · premise_audit · G1, int_no_gap — The case split needs the two branches to cover every integer; this depends on q being an integer and fails for a rational q such as 3/5.
• S07 · premise_audit · S06, G1, G2, order_basics — It needs existence and uniqueness from S06 and the definition of ℕ; it does not claim that ℤ is closed under every operation (division in S09 is not).
• S06.2 · inverse_equivalence · add_assoc, add_comm, add_inverse, add_zero — Expressions are only replaced by equal ones, which does not change whether the equation holds, so the step is two-way.
• S06.1 · inverse_equivalence · eq_congruence, add_inverse — Adding −b and adding b undo each other, with no side condition in ℤ or ℚ. In ℕ, −b is in general not in ℕ, so the step cannot be carried out inside ℕ, which is exactly the situation of S05.
• S06 · inverse_equivalence · L_sub, numeric_evaluation — Backward: substitute, 5+(−2)=3. Both directions of the lemma are proved in the sub-steps, so 'is a solution' and 'equals −2' are equivalent, which gives both existence and uniqueness.
• S05 · premise_audit · S04, G2, def_unfold — The definition requires a solution that exists and is unique; non-existence already settles that it is undefined. The conclusion is for ℕ only; ℤ is treated separately in S06 and S07.
• S04 · premise_audit · S03, order_basics, quantifier_negation — What is needed is an inequality for every c in ℕ, not a few trial values; S03 was proved for an arbitrary c, so the conclusion covers all c∈ℕ.
• S03 · premise_audit · G1, order_basics, add_zero — Only c≥0 and the fact that adding preserves order are used; c is arbitrary with no other assumption. The converse (recovering c∈ℕ from 5+c≥5) is neither needed nor claimed.
• S02 · premise_audit · G1, G3, nat_closed, numeric_evaluation — It needs 3,5∈ℕ and the closure of ℕ under addition and multiplication; closure is claimed for these two operations only, not for subtraction or division (see S05 and S09).
• S01 · premise_audit · G1, G2, mko_arith — This step only fixes the systems and the definitions and derives no new fact; every later conclusion is relative to a stated S.

Error controls and negative controls

Closure depends on the number system

The MKO names the common mistake of believing the four operations are closed in every number system without conditions. Here ℕ is closed under addition and multiplication (S02), but 3−5 is undefined in ℕ (S05); ℤ supplies subtraction (S07), but 3÷5 is still undefined in ℤ (S09); in ℚ, 3÷5=3/5 (S11), but division by zero is still excluded (S13, S14). Saying that an operation is defined always requires naming the system.

Division by zero is not an ordinary division

Another mistake identified in the MKO is treating division by zero as an ordinary quotient. By G2, a÷b is the unique solution of b·q=a. When b=0, 0·q is always 0: if a≠0 (as in 3÷0) there is no candidate (S13); if a=0 (0÷0) every number is a candidate (S14). Neither case gives a result. '3÷0=0' fails on substitution, 0·0=0≠3; '0÷0=1' does satisfy 0·1=0, but so does q=0, so uniqueness fails.

Division with remainder is not exact division

The MKO notes that 3÷2 is not an exact division in the natural numbers. Likewise, division with remainder gives 3=5·0+3 (quotient 0, remainder 3), but that is a different operation: 3÷5 in the sense of G2 requires 5q=3 exactly, and 5·0=0≠3. Taking the quotient 0 from division with remainder as the value of 3÷5 in ℕ silently changes the operation.

• In ℕ, 3−5=0 → reject — Substituting back gives 5+0=5≠3; truncated subtraction, which replaces a negative difference by 0, is a different operation, not the subtraction of G2.
• 3÷0=0 → reject — Substituting back gives 0·0=0≠3; by S13 every q has 0·q=0≠3, so there is no candidate.
• 0÷0=1, because any number divided by itself is 1 → reject — u÷u=1 needs u≠0; 0·q=0 holds for every q, so q=0 and q=1 are both solutions and the solution is not unique (S14).
• 6÷3=2 is an integer, so ℤ is closed under division → reject — One example cannot prove closure; 3÷5 is undefined in ℤ (S09), and one counterexample is enough to refute closure.

Result and limitations

In ℕ, 3+5=8 and 3·5=15 are defined (with the same values in ℤ and ℚ); 3−5 and 3÷5 are undefined in ℕ. In ℤ (and in ℚ), 3−5=−2, but −2∉ℕ; 3÷5 is undefined in ℤ and equals 3/5 in ℚ, while 3/5∉ℤ. 3÷0 has no candidate value and 0÷0 has no unique one, so both are undefined in ℕ, ℤ and ℚ.

• This guide takes the operations and order properties of ℕ, ℤ and ℚ (nat_closed, int_no_gap, order_basics and the like) as premises and does not construct these systems.
• G2 is one common convention that defines difference and quotient by unique solutions; truncated subtraction, division with remainder, or a programming language's special convention for a÷0 are different operations and need their own definitions.

Verification and source binding

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

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

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