Is factorial definable using a $\Delta_0$ formula?

(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 linear-time 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, log-space 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 log-space 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 logspace-uniform $\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 constant-depth 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.

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