In the context of KP, is the formula $\forall w(w\in x \leftrightarrow\forall y\exists z F(w,y,z))$ $\Pi\_3$ when $F(w,y,x)$ is $\Delta\_0$? 



On whether a formula of KP is $\Pi_3$
It seems so:


Unwinding the expression, we get $$G(x)\equiv\forall w [(w\in x\implies \forall y\exists z(F(w, y, z)))\wedge (\forall y\exists z(F(w, y, z))\implies w\in x)]$$ $$\iff \forall w[(\forall y\exists z(F(w, y, z))\vee w\not\in x)\wedge (\exists y\forall z(F(w, y, z))\vee w\in x)]$$ $$\iff [\forall w\forall y\exists z(F(w, y, z)\vee w\not\in x)]\wedge[\forall w\exists y\forall z(F(w, y, z)\vee w\in x)];$$ this last statement is of the form $\Pi^0\_2\wedge \Pi^0\_3$ (using $F\in \Sigma^0\_1$ for the left conjunct, and $F\in \Pi^0\_1$ for the right conjunct), so is $\Pi^0\_3$.


(I'm using, e.g., "$\Pi^0\_3$" instead of "$\Pi\_3$" because I sometimes quantify over subsets of an admissible set, so I like keeping track of the relative type I'm talking about.)


