Consider a 2-sorted first-order logic with equality (for first-sort entities). The first sort consists of numbers, the second sort (which will be capitalized) of unary functions. There is one constant, the first-sort $0$. There is one predicate, 2-ary $<$ relating first-sort things, representing “less than”. The only second-sort terms are second-sort (capitalized) variables, and the first-sort terms are just $0$, first-sort variables, and strings of the form $F(t)$, where $F$ is a second-sort term and $t$ is a first-sort term.

To be precise about the logic, use (say) Cook and Nguyen, *Logical Foundations of Proof Complexity*

The mathematical axioms are:

$\forall x \thinspace ¬ x < 0$

$\forall x \forall y (x = y \lor x < y \lor y < x)$

$\forall x \forall y \forall z (x < y \land y < z \Rightarrow x < z)$

Induction: $\phi(0) \land \forall n \forall m (\phi(n) \land \sigma n,m \Rightarrow \phi(m)) \Rightarrow \forall n \phi(n)$

where: $\ \sigma x,y$ abbreviates $x < y \land ¬\exists z(x < z \land z < y) $Replacement: $\forall F \forall c \forall i \exists G \thinspace (G(i) = c \land F =_i G)$

where: $\ F =_i G$ abbreviates $\forall x (x ≠ i \Rightarrow F(x) = G(x))$

We can also consider the possible axioms:

$\text{top}: \exists x \forall y (x=y \vee y<x)$

$\text{inf}: \forall x \exists y (x<y)$

Notes:

*Motivation*: Counting seems to be essential to our intuition of the natural numbers, and, since a count is just a one-to-one sequence, a sequence seems to be conceptually prior to that of a count. (One can imagine a young child learning to count and being told that the sequence they formed is wrong because, “You can’t count the same thing twice.”) Since a sequence is a unary function, this motivates using unary functions as the fundamental second-sort entity (rather than relationships or sets, say).*The two cases*: The two cases of $\text{top}$ and $\text{inf}$ are exhaustive and mutually exclusive. With $\text{inf}$, the system becomes full first-order Peano Arithmetic. It can be proved that $\sigma$ is a partial function, but because of the possibility for $\text{top}$, it cannot be proved that $\sigma$ is a total function, and indeed there is a trivial model of the axioms consisting of one first-sort entity ($0$) and one second-sort entity (the function mapping $0$ to $0$).*Arithmetic*: This system has formulas which express the addition and multiplication relationships of first-sort things in the usual recursive way, and with them one can prove the usual arithmetic theorems, with the evident exception of totality of addition and multiplication and the like.*Consistency*: One can prove the consistency of the system within the system itself, because of the simplicity of its trivial model.

One can also consider functions as a second-sort number. That is, fix a base $s$ with $s>1$. And suppose $\forall i ≤ k, \thinspace F(i) < s$. Then one can consider $F$ up to $k$ as representing the number $\sum_{i=0}^{k} F(i)s^i$. Then one can express addition of second-sort numbers in the system and prove the usual theorems of addition for second-sort addition.

But ... it does not seem one can express multiplication of second-sort numbers in the system. If we added binary functions, we could express multiplication of second-sort numbers. With only the unary functions of this system, one does not have access to sequences of sequences of numbers, which the expression of second-sort multiplication seems to require. So my question is:

**Q: Is there a formula of this system which represents multiplication for second-sort numbers?**

In the case of $\text{inf}$ such a formula clearly exists, so one can restrict the question to the case of $\text{top}$.

APPENDIX.

Let's formalize precisely the notion of representability for second-sort addition, to answer a question in comments which is too long for a comment. For a natural number $n$, let $\overline{n}(x)$ be the formula $x = 0$ when $n$ is 0, and the formula $\exists x_1 ... \exists x_{n-1} (\sigma 0,x_1 \land \sigma x_1,x_2 \land ... \land \sigma x_{n-1},x)$ when $n > 0$. Intuitively, $\overline{n}(x)$ is the formula asserting $x$ to be $n$. Consider the formula $\alpha(x,y,z)$

$$\exists F(F(0) = x \land F(y) = z \land \forall i,j (i < y \land \sigma i,j \Rightarrow \sigma F(i),F(j)))$$

Then $\alpha(a,b,c)$ expresses first-sort addition because (for all $a,b,c$) $a + b = c$ if and only if the following is a theorem of the system:

$$\forall x \forall y \forall z (\overline{a}(x) \land \overline{b}(y) \land \overline{c}(z) \Rightarrow \alpha(x,y,z))$$

For second-sort numbers fix the base $s > 1$. For $n = \sum_{i=0}^{k} n(i)s^i$ let the formula $\tilde{n}(F)$ be the formula $\exists x_0 ... \exists x_k (\overline{0}(x_0) \land ... \land \overline{k}(x_k) \land \overline{n(0)}(F(x_0)) \land \overline{n(1)}(F(x_1)) \land ... \land \overline{n(k)}(F(x_k)))$. Intuitively, $\tilde{n}(F)$ if $F$ is the second-sort number representing $n$ in base $s$. Then $\phi(X,Y,Z)$ represents second-order mulitiplication of base $s$ if (for all $a,b,c$) $a * b = c$ if and only if the following is a theorem of the system: $$\forall F \forall G \forall H(\tilde{a}(F) \land \tilde{b}(G) \land \tilde{c}(H) \Rightarrow \phi(F,G,H)) $$

2more comments