# Can this weakish system of arithmetic express multiplication for second-sort numbers?

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:

1. $$\forall x \thinspace ¬ x < 0$$

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

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

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

5. 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

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

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

• Or is there an axiom scheme for unique choice, i.e. $(\forall x\, \exists! y\, \phi(x,y))\to (\exists F\,\forall x\, \phi(x,F(x)))$? Or is there at least a binary operation for composition of functions?
– user44143
Jun 2, 2021 at 14:42
• @Matt F. For your first question. There are two cases: there exists a maximum (top), or there doesn't (inf). In the case of top, the axiom scheme for unique choice is a theorem for any $\phi$, provable by induction using the wff ($\forall x≤n \exists ! y \phi(x,y)) \rightarrow (\exists F \forall x≤n \phi(x,F(x)))$. In the case of inf, it's not a theorem. OTOH, in the case of inf, there clearly is a formula which represents multiplication for second-sort numbers even when functions are limited to unary functions, so I'm not sure of the relevance of the question.
– abo
Jun 2, 2021 at 15:26
• @Matt F. For your second question, one can obviously compose functions. If F(t) is a term, and G is a function, then G(F(t)) is a term. Perhaps I am misunderstanding your question?
– abo
Jun 2, 2021 at 15:30
• Thanks, that clarifies the first question, and with that I can answer the second question well enough. It's probably worth mentioning the difference between finite and infinite cases in the post.
– user44143
Jun 2, 2021 at 15:46
• @abo Under the assumption of $\text{top}$, multiplication isn't going to be a total function. Are asking if the graph of multiplication as a partial function is definable? Jun 2, 2021 at 19:59

This is not an answer, but a claim that the question is hard. That is, I believe the answer is negative, and there is no formula defining second-sort multiplication. OTOH, if multiplication can be computed by a multi-tape Turing Machine with symbols $$\{0,1,b\}$$ in time $$O(n)$$, then there does exist a formula for second-order multiplication in this system. This is because a multi-tape Turing Machine can be defined using only monadic functions, and its behaviour can also be defined using only monadic functions up to, in the case of $$top$$, any time which is a product of $$max$$, the largest natural number, and any fixed natural number, plus some fixed natural numbers. But if there exists $$l$$ such that there exists a multi-tape TM which computes the multiplication $$F*G$$ in time ≤ $$l * (length(F) + length(G))$$, then this condition is met and the behaviour of this TM can be described all the way to termination, and so one can write a formula for the computation $$\times(F,G,H)$$ by simply considering a formula for the behaviour of this TM upon termination. But whether multiplication can be computed by a multi-tape Turing Machine with symbols $$\{0,1,b\}$$ in time $$O(n)$$ is a hard problem.