$\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$?



A question on recursion in Kripke-Platek set theory with infinity and $\Sigma_{3}$-separation and $\Sigma_3$-collection
$\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$. 


