I'm trying to find a way to express the relation $y=x!$ as a $\Sigma_1$ formula. Here's what I've got so far:
I know that we can code the sequence $0!,1!,2!,...,x!$ in the pair $(c,d)$ using a $\beta$-function. I also know that there is a nice $\Delta_0$ (and therefore $\Sigma_1$) formula expressing $m = \beta(c,d,n)$, so let's call this formula $B(c,d,n,m)$.
I think that my formula should look like
\begin{equation*} \exists c\exists d \bigg(B(c,d,0,1) \land \\ \forall i <x \big(\beta(c,d,s(i)) = s(i)\times\beta(c,d,i)\big) \land \\ B(c,d,x,y)\bigg) \end{equation*}
(Apologies for the rough formatting).
What I'm stuck on is how to express the middle line. I know how to express that a $\beta$-function is equal to a constant, but I don't know how to deal with the fact that it appears on both sides of the equality sign.
You have two invocations of the $\beta$ function, so introduce a fresh variable to stand for each function value:
$$ \beta(c,d,s(i)) = s(i)\times \beta(c,d,i) $$ becomes $$ \exists v\exists w(\; B(c,d,s(i),v) \land B(c,d,i,w) \land v = s(i)\times w \;) $$ (or alternatively $$ \forall v\forall w(\; B(c,d,s(i),v) \land B(c,d,i,w) \to v = s(i)\times w \;) $$ but for the $\exists$ variants you can make the quantifiers bounded simply by stipulating that $v$ and $w$ must be less than something that you quantify once and for all together with $c$ and $d$, such that the end result is still $\Sigma_1$).