Does Mostowski's collapsing lemma prove $\Delta_0$-transfinite recursion?

Question

Let $\mathsf{T}$ be the theory comprising Extensionality, Foundation (stating every set has an $\in$-minimal element), Pairing, Infinity, Union, $\Delta_0$-Separation, and the closure under rudimentary functions. (That is, for every rudimentary function $f$ and a set $a$, $f(a)$ exists.) Borrowing terms by Mathias, $\mathsf{T}$ is equal to Gandy-Jensen set theory $\mathsf{GJ_0}$ with Infinity and Foundation. (Mathias defined $\mathsf{GJ_0}$ in his paper Weak Systems of Gandy, Jensen and Devlin.)

It is known that if $J_\alpha$ is a Jensen hierarchy (Starting from $J_\omega=V_\omega$ and $J_{\alpha+1}=\operatorname{rud}(J_\alpha)$) then $J_\alpha\models \mathsf{GJ_0}$ for all $\alpha\ge\omega$. Thus $J_\alpha$ also satisfies $\mathsf{T}$. It means $\mathsf{T}$ does not prove transfinite recursion for $\Sigma_1$-formulas, or $\mathsf{T}$ can define ordinal operators, contradicting with that $J_{\omega+1}$ does not contain ordinals larger than $\omega+\omega$.

However, the situation might be different if we add Mostowski's collapsing lemma, also known as Axiom Beta:

($\mathsf{Beta}$) Suppose that $r$ is a relation such that every nonempty subset of $\operatorname{field} r =\operatorname{dom} r\cup\operatorname{ran}r$ has an $r$-minimal element. Then we have a function $f$ such that $\operatorname{dom}f=\operatorname{field} r$ and for all $x\in \operatorname{field} r$, $$f(x) = \{f(y) \mid (y,x)\in r\}.$$

$\mathsf{Beta}$ is not provable from $\mathsf{KP}$, so also not provable over $\mathsf{T}$. My question is as follows: Let $\mathsf{TCo}$ be the claim that every set $a$ has a transitive closure $\operatorname{TC}(a)$. Then

1. Does $\mathsf{T}$ + $\mathsf{TCo}$ + $\mathsf{Beta}$ prove transfinite recursion for $\Delta_0$-formulas? That is, if $G(x,y,f)$ is a $\Delta_0$-definable class function, then can we define a class function $F$ such that $$F(x,y)=G(x,y,\{F(x,z)\mid z\in\operatorname{TC}(y)\})?$$
2. If the answer for the first question is yes, do we have the same if $G$ is rudimentary? What about if $G$ is a recursively-defined function from a rudimentary function?

(I added $\mathsf{TCo}$ for a technical reason: The typical proof for $\Sigma_1$-recursion over $\mathsf{KP}$ proves $\mathsf{TC}$-recursion first, which relies on the existence of the transitive closure. I am not sure whether $\mathsf{T}$ proves $\mathsf{TCo}$ or not, so I added it as a separate axiom. I am also not sure whether each $J_\alpha$ satisfies $\mathsf{TCo}$.)

Answer 1

It does not directly answer my question, but let me put a partial answer over a slightly stronger setting, which might be a better question to ask.

Before the discussion, let me introduce the set theory named Provident set theory defined by Mathias and Bowler:

Definition. The provident set theory $\mathsf{Prov}$ comprises the following axioms:

1. Extensionality
2. Rudimentary closure: For every rudimentary function $f$, $f(a)$ exists. (Note. It is finitely axiomatizable by stating the closure condition for basic rudimentary functions.)
3. For every set $a$, we can find a transitive set $b\supseteq a$ and a function $f\colon b\to \mathrm{Ord}$ defining the rank function over $b$. (It shows both $\mathsf{TCo}$ and the definability of the rank function.)
4. For every transitive set $c$ and an ordinal $\alpha$, we have a canonical progress $\langle P_\xi(c)\mid\xi<\alpha\rangle$ satisfying the following:

• $P_0(c)=\varnothing$
• $P_{\xi+1}(c)=\mathbb{T}(P_\xi(c))\cup\{c\cap P_\xi(c)\}\cup \{x\in c\mid x\subseteq P_\xi(c)\}$ if $\xi+1<\alpha$.
• $P_\xi(c)=\bigcup_{\eta<\xi}P_\eta(c)$ if $\xi\le\alpha$ is a limit ordinal.

Here $\mathbb{T}(a)$ is the function (roughly) taking a transitive set $u$ and returning the set of values for basic rudimentary functions over $u$. Its definition is available in Definition 3.0 of Mathias and Bowler.

5. For every ordinal $\alpha$ and $\beta$, we have a partial function $f\colon\mathrm{Ord\times Ord\to Ord}$, which is a set, such that $\alpha,\beta\in\operatorname{dom}f$ and $f$ defines an ordinal addition.

Let us call $\mathsf{Prov}^-$ the theory obtained from $\mathsf{Prov}$ by ejecting the last axiom. We also put $\omega$ to denote the axiom of Infinity. From the argument by Mathias and Bowler, we have

Proposition. $\mathsf{Prov\omega}$ with $\Pi_1$-Foundation proves we can define a function by a rudimentary recursion. That is, for a rudimentary function $G$ and a parameter $p$, we can define $G$ such that $$F(x)=G(p,F\upharpoonright x).$$

However, $\mathsf{Prov\omega}$ + $\Pi_1$-Foundation does not prove we can do the recursion when $G$ is a function given by a rudimentary recursion. Mathias and Bowler proved that $J_{\omega^\alpha}$ is always a model of $\mathsf{Prov\omega}$ + $\Pi_1$-Foundation, and we can define $\alpha\mapsto \min(\omega^2,\omega\cdot\alpha)$ by recursion over a rudimentary recursively defined function, namely $\alpha\mapsto \omega+\alpha$. However, $J_{\omega^2}$ is not closed under that function.

To overcome this issue Mathias and Bowler also defined the notion limit provident set theory that allows recursion over rudimentary recursively defined functions, and in fact, it can go further:

Definition. A function $F$ is $p$-rud rec${}^n$ function if there is a $p$-rud rec${}^{n-1}$-function $G$ such that we have $F(x)=G(p,F\upharpoonright x)$. $p$-rud rec${}^1$ function is a rudimentary recursively defined function with parameter $p$.

I believe the semantic argument given by Mathias and Bowler (Theorem 6.52 and (7.3.1) of their paper) shows the following:

Proposition. The following are equivalent over $\mathsf{Prov\omega}$ + $\Pi_1$-Foundation:

1. For every $p$ and (meta-)$n$, $p$-rud rec${}^n$ function is definable.
2. For every ordinal $\alpha$, $\omega\cdot\alpha$ exists.

The limit provident set theory is obtained from $\mathsf{Prov}$ by adding one of the above statement.

In some sense, how much recursion we can do over provident set theory depends on how much ordinal operation we can do.

By an elementary construction of ordinal addition and multiplication in terms of disjoint union and cartesian product, we have

Proposition. $\mathsf{Prov}^-\omega$ + $\Pi_1$-Induction + $\mathsf{Beta}$ proves ordinal addition and multiplication are well-defined, so it can define $p$-rud rec${}^n$ functions.

However, unlike limit provident set theory, $\mathsf{Beta}$ can define multiplication. It raises the following question:

Question. Can $\mathsf{Prov}^-\omega$ + $\Pi_1$-Induction + $\mathsf{Beta}$ define function given by primitive recursive set functions? Roughly equivalently, does the previous theory define $\phi_n(\alpha)$ for all natural number $n$, where $\phi_\alpha(\beta)$ is a Veblen function? What about the general $\phi_\alpha(\beta)$?