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)) $$
