What changes could possibly be made to FOL so that multiplication can be formalized just in terms of sum?
FOL axiomatizations of natural number arithmetic take multiplication as a primitive, and impose the following axioms:
- $x \times 0=0$
- $x \times S(y)= x\times y + x$
My motivation for this question is that I think that this is not how kids learn multiplication. Instead, they have the meta-definition: $x \times y = x + ... + x$ ($y$ times). If such definition could be expressed in some logic, then those axioms would not be needed; instead they could be defined. I am interested if such a theory in such a logic would be stronger or equivalent to the usual peano axioms.
Here is what I tried:
- Add the logical symbols $\{\bf{0}, \bf{1}, \bf{2}, \bf{3}, ... \}$ to the logic. (I'll be using bold for the logical "numbers" symbols).
- Define $f^\textbf{1} (x)=f(x)$, $f^\textbf{2} (x)=f(f(x))$,... and so on. This has two sides, on the structural/semantic side this just means that the term assignment function maps $f^\textbf{n} (t)$ to $f(f(f...f(x)))$. On the the provability/syntantic side it is necessary to add some rules/axioms to transform sentences about $f^\textbf{n}$ to the usual ones. Though overkill, for simplicity let's say that I also add the $\oplus$ symbol (for sum) and the presburger axioms, define $\textbf{-}$ the obvious way, and let $f^\textbf{n}$ be transformed to $f^\textbf{n-1}(f(t))$. Let's call this logic $FOL^P$.
- Now, for my definition of function iteration in $FOL^P$ to work, the axiomatization of number theory must be a theory of unary functions ($+1$, $+2$, etc), instead of the usual binary $+$ function. Again, start off with presburger axioms and add the successor function as an axiom $S(x) = x+1$. $\{S^\bf{n}\}_{n\in \mathbb N}$ are the required unary functions.
- Finally, we can define $x \times y := (S^\textbf{x})^{\textbf{y-1}}(x)$.
Sadly, this fails, since step 4 is not valid, as there is no way to transform $x$ (in the number theory) to $\textbf x$ (in $FOL^P$). However I think that there must be some way to bridge that gap.
Also, here are some thoughts about this construction: $FOL^P$ keeps the nice things of $FOL$ (that being complete, consistent and semidecidable), as presburger is decidable, complete and consistent. The (slightly) modified presburger is still elementary equivalent to the usual presburger. Hence it seems that Gödel's incompleteness theorem implies that that gap can't be bridged, but I am unsure about that argument. I'd love some references if something like this has already been tried.