$\begin{align}x \text { is predicatively} &\text{ definable } \iff \exists x\_1,..,x\_n \exists \varphi:\\ & \rho(x\_1) < \rho(x) ,.., \rho(x\_n) < \rho(x) \ \land \\&\forall y \, (y \in x \iff V\_{\rho(x)} \models \varphi(y,x\_1,..,x\_n))\end{align} $


Where $\rho(x)$, the rank of $x$, is defined as the ordinal index of the first stage $V\_\alpha$ of which $x$ is a subset.


Now, let $\sf HPD$ be the class of all hereditarily predicatively definable sets.



> 
> What is the maximal fragment of $\sf ZFC$ satisfied by $\sf HPD$?
> 
> 
> 



Which fragment of ZF does the class of all hereditarily predicatively definable sets capture?
HPD satisfy extensionality and regularity trivially.


It satisfy Pairing, as if $x,y\in HPD$ we can explicitly write down the definition of $(x,y)$ using only $x,y$ as parameters (and they have strictly smaller rank).


It satisfy infinity (it has all of the Ordinals and it computes Ordinals correctly).


It has powerset, $V\_{\alpha+2}$ calculate $HPD\cap V\_{\alpha+1}$ correctly.


It doesn't have $\Delta\_0$ separation even when restricted to formulaes without parameters:


Note that $HPD(\omega)$.


Externally we know that $(2^{|\omega|})^{HPD}$ is countable


I claim that $HPD$ also see that, this is because $V\_{\omega+2}$ has a canonical well-ordering for $(\mathcal P(\omega))^{HPD}$ of ordertype $\omega$ (it is even without parameters), simply by intertwining Ackermann coding for parameters with Godel encoding for formulaes (and noting that every $HPD$ subset of $\omega$ must be seen from $V\_{\omega+1}$), so $HPD\models |\omega|=|\mathcal P(\omega)|$


Like @GabeGoldberg stated, for every $X\subseteq \omega$ we have $X'=X\cup\{\omega\}\in HPD$, but most such $X=\{a\in X'\mid a\ne\omega\}\notin HPD$, and $\omega$ is definable without parameters so we don't have $\Delta\_0$-separation w/o parameters.




---


I'm not quite sure about choice and union, but I would imagine that union fails in a strong sense (at every infinite successor level, note that the union of HPD sets with limit rank are closed under union, but at successor ranks we can use parameters from one rank bellow, which causes a problem)


