There is a theorem $(∀m)(∀n)(0 < n ⇒ (∃!q)(∃r)(m = q·n + r∧r < n)) $
Now consider to use this theorem to define division over natural number.
The principle of function definition says that:
It seems that we cannot directly use the principle of function definition to define the division over natural number. But where exactly is something wrong here? If we cannot directly apply the principle above to make the definiton. Could someone please tell me why?
And if I really want to do so. That it, use the principle to define division over the natural numbers. Then could someone please tell me what should I do? How may I modify the principle of function definiton?
EDIT:
Now I think probably I can change the theorem $\vdash (∀x_1)(∀x_2)...(∀x_n)(∃!u)P(u,x_1,x_2,...,x_n) $ into $\vdash (∀x_1)(∀x_2)...(∀x_n)(∃!u)(\exists y_1)(\exists y_2)...(\exists y_m)P(u,x_1,x_2,...,x_n,y_1,y_2,...,y_m) $ with $P$ in $A$.
May I ask if it is correct?
Thanks in advance!
First, you need to get clear on how you define division for the natural numbers mathematically, before we should try and formalize this in logic.
I think it is reasonable to use the quotient as your definition, and thus $m$ divided by $n$ (with $n > 0$) would be the $q$ in the formula in the beginning of your post. For $n=0$, we could just stipulate that $m$ divided by $n = 0$ is $0$ (we have to pick something, since we want $\forall x_1 \forall x_2 \exists ! u P(u,x_1,x_2)$)
So, as a general formula $P(u,x_1,x_2)$, the intended meaning of which is: "u is the result of dividing $x_1$ by $x_2$", we can take:
$P(u,x_1,x_2): (x_2 = 0 \land u = 0) \lor \exists r (x_1 = u \cdot x_2 + r \land r < x_2)$