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$
    – Matt F.
    Jun 2 '21 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 '21 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 '21 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$
    – Matt F.
    Jun 2 '21 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 '21 at 19:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.