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

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


  • 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}$.


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

  • $\begingroup$ 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? $\endgroup$
    – user44143
    Jun 2, 2021 at 14:42
  • 1
    $\begingroup$ @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. $\endgroup$
    – abo
    Jun 2, 2021 at 15:26
  • $\begingroup$ @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? $\endgroup$
    – abo
    Jun 2, 2021 at 15:30
  • $\begingroup$ 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. $\endgroup$
    – user44143
    Jun 2, 2021 at 15:46
  • $\begingroup$ @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? $\endgroup$ Jun 2, 2021 at 19:59

1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.