# How do I derive fraction multiplications from Peano axioms

and sorry for the noob questions :) Trying to teach my 10 year old daughter some math and came across the Peano axioms. On the following resource there are two sets of axioms, one is based on symbols for 0 and the successor, and the second axiomatization (based on the ordered semiring) which looks more intuitive and applicable for school math program.

The only hole that I see there is there are addition and multiplication but there is no link to subtraction and division (even though intuitively they are just reverse operation and the same axioms should apply). Also it looks like it's missing axioms where operations(+,x) and their inverse operations(=,/) are combined in one axiomatic sentence (like a*1/a=1), or does it automatically follow from the set of axioms? The reason I am asking is to make a connection from those axioms to fraction multiplication. It's easy to explain to a child how it's done, but it's not that easy to explain why.

• Division is not a "primitve" operation in arithmetic because the set of naturals is not closed with respect to it. We define quotient and remainder proving that $b \ne 0 \to \exists q \exists r(( a = bq+r) \land r < b )$ – Mauro ALLEGRANZA Apr 11 '20 at 19:16

The Peano Axioms are a set of axioms meant for the natural numbers. As such, you can;t really have the normal subtraction and division functions, since applied to two natural numbers they may end up with a non-natural number. What you can do, is to define a modified subtraction function $$\dot{-}$$ where

$$x \dot{-} y = \begin{cases} x - y & \text{if x > y} \\ z & \text{if y * z \leq x and y * (z +1) > x } \end{cases}$$

In FOL, this could be formalized as

$$\forall x \forall y \forall z (z = minus(x,y) \leftrightarrow ((x < y \land z = 0) \lor x = z + y))$$

And for division, you could use quotient and remainder, where:

$$quo(x, y) = \begin{cases} 0 & \text{if y=0} \\ 0 & \text{if x \leq y } \end{cases}$$

and

$$rem(x,y) = x - y*quo(x,y)$$

In FOL, this could be formalized as:

$$\forall x \forall y \forall z (z = quo(x,y) \leftrightarrow ((y = 0 \land z = 0) \lor (\exists w (y * z) + w = x \land \neg \exists w (y * s(z)) + w = x ))$$

$$\forall x \forall y \forall z (z = rem(x,y) \leftrightarrow z = minus(x,y*quo(x,y)))$$

• +1 - modified subtraction is also called "monus." – Noah Schweber Apr 12 '20 at 3:21
• @NoahSchweber "monus" .. I didn't know. Thanks! :) – Bram28 Apr 13 '20 at 1:47