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?

1$\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. 1227 $\endgroup$ – Ali Enayat Feb 25 '15 at 18:37
(Sorry for the earlier confusion.)
Yes, the graph of factorial is $\Delta_0$.
First, 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 lineartime hierarchy. A convenient sufficient condition is provided by Nepomnjaščiĭ’s theorem [4]: 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 [2], building on earlier work by Beame, Cook, and Hoover [1], proved that logarithmic space (in fact, logspace uniform $\mathrm{TC}^0$, subsequently improved to fully uniform $\mathrm{TC}^0$ by Hesse, Allender, and Barrington [3]) 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 logspace computable functions can be done in log space: we do not need to write down the intermediate results, we 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. Chiu, G. Davida, B. Litow, Division in logspaceuniform $\mathit{NC}^1$, RAIRO – Theoretical Informatics and Applications 35 (2001), no. 3, pp. 259–275.
[3] W. Hesse, E. Allender, D. A. M. Barrington, Uniform constantdepth threshold circuits for division and iterated multiplication, Journal of Computer and System Sciences 65 (2002), no. 4, pp. 695–716.
[4] V. A. Nepomnjaščiĭ, Rudimentary predicates and Turing computations [calculations], Doklady Akademii Nauk SSSR 195 (1970), pp. 282–284. MR0281611, Zbl 0223.02031.

$\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$ – Yoni Zohar Feb 25 '15 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$ – Emil Jeřábek Feb 25 '15 at 15:40

$\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$ – Emil Jeřábek Feb 25 '15 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$ – Wojowu Feb 25 '15 at 18:18

1$\begingroup$ @Wojowu: See Ali Enayat’s comment above; the formula in D’Aquino’s paper should be shorter. $\endgroup$ – Emil Jeřábek Feb 25 '15 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_{i1}/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$.