The factorial function is primitive recursive, and therefore definable by a $\Sigma_1$ formula. Is it also definable by a $\Delta_0$ formula (i.e. bounded quantifiers)? If not, why?
-
3$\begingroup$ Emil has already given an excellent high level positive answer to the question, but it is worth pointing out that the following paper of Paula D'Aquino includes all the details of $\Delta_0$-definability of the factorial function (in section 5). Local Behaviour of the Chebyshev Theorem in Models of I$\Delta_0$. The Journal of Symbolic Logic Vol. 57, No. 1 (Mar., 1992), pp. 12-27 $\endgroup$– Ali EnayatCommented Feb 25, 2015 at 18:37
2 Answers
Yes, the graph of factorial is $\Delta_0$.
As mentioned above by Ali Enayat, a direct $\Delta_0$ definition of factorial was constructed by D’Aquino [4]. It is based on collecting contributions of all primes (similar to Gabriel Nivasch’s answer), using a result of Paris, Wikie, and Woods [7] that the sum of a polylogarithmically long $\Delta_0$-definable sequence of integers is $\Delta_0$-definable. Generalizing this method, Berarducci and D’Aquino [2] proved that the graph of a product of a bounded $\Delta_0$-definable sequence is $\Delta_0$-definable.
Here is the original answer, showing that a much more general class of functions are $\Delta_0$-definable based on their computational complexity:
The problem can be restated in terms of computational complexity. By a characterization going back to Bennett, $\Delta_0$-definable predicates are exactly those computable in the linear-time hierarchy. A convenient sufficient condition is provided by Nepomnjaščiĭ’s theorem [6]: a predicate is in $\Delta_0$ whenever it is decidable by an algorithm working simultaneously in polynomial time and space $n^\epsilon$ for some $\epsilon<1$. In particular, all predicates computable in logarithmic space are $\Delta_0$.
Chiu, Davida, and Litow [3], building on earlier work by Beame, Cook, and Hoover [1], proved that logarithmic space (in fact, log-space uniform $\mathrm{TC}^0$, subsequently improved to fully uniform $\mathrm{TC}^0$ by Hesse, Allender, and Barrington [5]) contains the iterated multiplication problem: given a sequence $x_1,\dots,x_n$ of integers in binary, compute their product.
By applying their algorithm to the sequence $1,\dots,n$, we can compute in logarithmic space (and in $\mathrm{TC}^0$) the factorial $n!$ when $n$ is given in unary. Consequently, we can decide in logarithmic space the graph $\{(x,y):y=x!\}$, where both $x,y$ are binary: we test whether $x$ is logarithmically smaller than $y$, and if so, compute its factorial and compare it to $y$. (Note that testing the equality of two log-space computable functions can be done in log space: we do not need to write down the intermediate results—we can recompute their individual bits on the fly as needed.)
References
[1] P. W. Beame, S. A. Cook, H. J. Hoover: Log depth circuits for division and related problems, SIAM Journal on Computing 15 (1986), no. 4, pp. 994–1003.
[2] A. Berarducci, P. D’Aquino: $\Delta_0$-complexity of the relation $y=\prod_{i\le n}F(i)$, Annals of Pure and Applied Logic 75 (1995), no. 1–2, pp. 49–56.
[3] A. Chiu, G. Davida, B. Litow: Division in logspace-uniform $\mathit{NC}^1$, RAIRO – Theoretical Informatics and Applications 35 (2001), no. 3, pp. 259–275.
[4] P. D’Aquino: Local behaviour of the Chebyshev theorem in models of $I\Delta_0$, Journal of Symbolic Logic 57 (1992), no. 1, pp. 12–27.
[5] W. Hesse, E. Allender, D. A. M. Barrington: Uniform constant-depth threshold circuits for division and iterated multiplication, Journal of Computer and System Sciences 65 (2002), no. 4, pp. 695–716.
[6] V. A. Nepomnjaščiĭ: Rudimentary predicates and Turing computations [calculations], Doklady Akademii Nauk SSSR 195 (1970), no. 2, pp. 282–284. English translation: Soviet Mathematics, Doklady 11 (1970), pp. 1462–1465.
[7] J. B. Paris, A. J. Wilkie, and A. R. Woods: Provability of the pigeonhole principle and the existence of infinitely many primes, Journal of Symbolic Logic 53 (1988), no. 4, pp. 1235–1244.
-
$\begingroup$ Thank you very much. I am having trouble finding the proof of Bennett's result regarding the equivalence of $\Delta_0$ to the linear time hierarchy. Do you know of a suitable reference? $\endgroup$ Commented Feb 25, 2015 at 15:29
-
$\begingroup$ This is supposed to be in Bennett’s Ph.D. thesis. I don’t really know of a good published reference. I learned the result from Krajíček’s “Bounded arithmetic, propositional logic, and complexity theory”, §3.2; the proofs are only sketched there, though they are not that hard to figure out (it helps to be familiar with Nepomnjaščiĭ’s trick first). $\endgroup$ Commented Feb 25, 2015 at 15:40
-
1$\begingroup$ Checking the book now, it seems I misremembered who exactly proved what. The equivalence with LinH is due to Wrathall dx.doi.org/10.1137/0207018 , where it is stated for rudimentary sets (RUD); the equivalence of RUD with $\Delta_0$ is Bennett’s. $\endgroup$ Commented Feb 25, 2015 at 15:56
-
$\begingroup$ Do you know of any attempt to explicitly write down a $\Delta_0$ formula which defines factorial? Following the steps of the proof you sketch would probably lead to quite long formula, but there might be some way to give it shorter. $\endgroup$– WojowuCommented Feb 25, 2015 at 18:18
-
1$\begingroup$ @Wojowu: See Ali Enayat’s comment above; the formula in D’Aquino’s paper should be shorter. $\endgroup$ Commented Feb 25, 2015 at 19:22
I didn't look at the above references, and I took this as an exercise for myself.
Here is a way to express "$x! = y$" as a $\Delta_0$ formula with two free variables $x$ and $y$.
The idea is to check that, for each prime $p \le x$, $p$ divides $y$ the right number of times.
The number of times the prime $p$ divides $x!$ is $f(x,p) = \sum_{i\ge 1} \lfloor x/p^i \rfloor$. For example, the number of times $7$ divides $1000!$ is $142+20+2=164$. Note that each element $a_{i} = \lfloor x/p^i \rfloor$ in this sum is obtained from the previous one by $a_{i} = \lfloor a_{i-1}/p \rfloor$.
Now, let us recall a method by Nelson of encoding sets using $\Delta_0$ formulas. Consider for example the set $S = \{6,13\}$. Since $6=110_{2}$ and $13=1101_2$ in binary, we encode $S$ by the number $2110211012_4$ (or $2110121102_4$). The $2$'s serve as separators between the elements of the set. Nelson shows how to express "$x \in S$" as a $\Delta_0$ formula.
Also, recall the pairing formula $(a,b) = (a+b)(a+b+1)/2+a$. Hence, we can express "$c=(a,b)$" by the formula $2c=(a+b)(a+b+1)+2a$.
Given $x$ and a prime $p$, let $S(x,p)$ be the set of pairs $S(x,p) = \{(u_1,v_1), \ldots, (u_j,v_j)\}$ where $u_i = a_{i}$ as defined above, $v_i$ is the partial sum $v_i = \sum_{k\le i} u_i$, and $j$ is the least element for which $u_j<p$. Then, we can express "$a$ encodes $S(x,p)$" using bounded quantifiers in the obvious way: We state that $a$ contains the first pair $(u_1,v_1)$, that $a$ contains a pair $(u,v)$ with $u<p$, and that each pair $(u,v)\in a$ with $u<u_1$ is obtained from another pair $(u',v')\in a$ by $u = \lfloor u'/p\rfloor$, $v = v'+u$.
Next, we can express "$z = f(x,p)$" by
\begin{multline*} (\exists a\le y)\, (\exists b\le a)\, (\exists c\le b)\, (\exists d\le b)\,\\ (\text{$a$ encodes $S(x,p)$}\, \wedge\, b\in a\, \wedge\, b=(c,d)\, \wedge\, c<p\, \wedge\, d=z) \end{multline*}
(Recall that $y$ is supposed to be the huge number $x!$.)
Next, recall how to express "$a^b=c$" with a $\Delta_0$ formula using repeated squaring: We state that there exists a set of pairs $S$ such that: (1) We have $(0,1)\in S$; (2) for each $(i,j)$ in $S$ with $i\ge 1$ there exists another pair $(i',j')\in S$ where either $i=2i'$ and $j = (j')^2$, or $i = 2i'+1$ and $j = a(j')^2$; and (3) we have $(b,c) \in S$. For example, if $b=9$ then $S = \{(0,1),(1,a),(2,a^2),(4,a^4),(9,a^9)\}$. The encoding of $S$ can be bounded by something like $c^2\log^2 c$, which is at most $2c^3$.
Finally, we state that $y=x!$ by stating that, for each prime $p\le x$, $n$ divides $y$ for $n=p^k$ and $k = f(x,p)$, but $y$ does not divide $np$; and that $y$ is not divisible by any prime $p$ in the range $x+1\le p\le y$.