A question on recursion in Kripke-Platek set theory with infinity and $\Sigma_{3}$-separation and $\Sigma_3$-collection

Question

$\Sigma_{3}KP\omega$ be Kripke-Platek set theory with infinity and $\Sigma_{3}$-separation and $\Sigma_3$-collection. What strengthening of Barwise's Definition by $\Sigma$ Recursion (Theorem 6.4 on page 26 of Admissible Sets and Structures) is supported by $\Sigma_{3}KP\omega$?

Answer 1

$\newcommand{\dom}{\operatorname{dom}\nolimits}\newcommand{\res}{\mathop{\upharpoonright}}$ The general $\Sigma_n$ case is not simpler than the $\Sigma_3$ case.

Suppose $G(\bar{x},y,z)$ is a $\Sigma_n$-function. We want a $\Sigma_n$-function $F(\bar{x},y)$ such that $$F(\bar{x},y) = G(\bar{x},y,\{\langle u,F(\bar{x},u)\rangle:u \in \operatorname{TC}(y)\})$$ for all $\bar{x},y$.

Fix $\bar{x}$. Let's say that a set function $f$ is an attempt at $F$ (with parameter $\bar{x}$) if $\dom f$ is a transitive set and $f(y) = G(\bar{x},y,f \res \operatorname{TC}(y))$ holds for all $y \in \dom f$. Assuming, $\Sigma_n$-collection, this is a $\Sigma_n$-statement. In more detail that is, $$\exists d(d = \dom f \land \operatorname{trans}(d) \land (\forall y \in d)(f(y) = G(\bar{x},y,f\res \operatorname{TC}(y))$$ and $\Sigma_n$-collection is used to show that the bounded quantifier $(\forall y \in d)$ does not increase complexity.

It's easy to show that any two attempts at $F$ with the same domain must be equal and that the restriction of an attempt at $F$ to a transitive set is again an attempt at $F$. So, assuming $\Sigma_n$-collection, $$z = F(\bar{x},y) \iff \exists f(\text{$f$ is an attempt at $F$ with parameter $\bar{x}$} \land \langle y,z \rangle \in f)$$ is a $\Sigma_n$ description of the desired function $F(\bar{x},y)$ provided that every $y$ is in the domain of an attempt at $F$.

Fix $\bar{x}$ again. That every $y$ is in the domain of an attempt at $F$ (with parameter $\bar{x}$) can be shown as follows. By Foundation, if there is a $y$ which is not in the domain of an attempt at $F$ then there is an $\in$-minimal such $y$, which we will denote $y_0$. Then, every $u \in \operatorname{TC}(y_0)$ is in the domain of an attempt at $F$ and any two such attempts will assign the same value to $u$. Let $f_0$ consist of all pairs $\langle u, v \rangle$ where $u \in \operatorname{TC}(y)$ and there is an attempt $f$ at $F$ with $f(u) = v$. This set $f_0$ can be formed using $\Sigma_n$-collection and $\Sigma_n$-separation. The result is a function $f_0$ with domain $\operatorname{TC}(y_0)$ which clearly satisfies the requirements of an attempt at $F$. But then $f = f_0\cup\{\langle y_0,G(\bar{x},y_0,f_0)\rangle\}$ is an attempt at $F$ containing $y_0$ in its domain, contradicting the fact that there is no such attempt at $F$.