By Reflection I mean the following schema:


**Reflection:** $$\forall X \, (\varphi \implies \exists \alpha : \varphi^{V\_\alpha})$$


where $\varphi$ is a first order formula (defined predicates and functions allowed) in which only symbol "$X$" occurs free, $\varphi^{V\_\alpha}$ is the "$\in {V\_\alpha}$" bounded form of $\varphi$.


$V\_\alpha$ is defined in the customary manner as the set of all subsets of elements of the range of a function from an ordinal $\alpha$ where the image of a successor is the power set of the image of its predecessor, and the image of a limit is the union of all images of prior ordinals. And ordinal is defined after von Neumann as a transitive set well ordered by $\in$.


The point here is that we are allowing the use of defined predicate and function symbols, as long as the formula remain first order, i.e. no quantification allowed over them.


Is reflection here a theorem scheme of $\sf ZF$?



Can we allow defined predicates and functions in reflection?
The first answer took care of the case where "Reflection" was a scheme of formulas in the language of ZF. Now we consider what we now think was the intent of the questioner.


We expand the language of ZF by introducing a predicate symbol P and a function symbol F
for each formula in the language of ZF. We also add additional axioms:


∀x1,...,xn(P(x1,...,xn)<-->(x1,...,xn)) where x1,...,xn are the free variables of .


∀x1,...,xn,y(∀z(((x1,...,xn,z)<-->y=z)-->F(x1,....xn)=y))


where x1,...,xn,y are the free variables of 


∀x1,...,xn,y(((x1,...,xn,y)∧∃z(z≠y∧(x1,...,xn,z)))-->F(x1,...,xn)=0)


where x1,...,xn,y are the free variables of 


Call this theory ZZF.


"Reflection" holds in ZZF.


Proof:Let be a formula in the language of ZZF whose only free variable is X. Let A be the set of formulas such that P is a symbol of . Let B be the set of formulas such that F is a symbol of . To each term t ocurring in we shall associate a variable vt where if s and t are not variables then


vs=vt iff s=t, and vs is not a variable of .


To each term we will also associate a formula ft. We will do this inductively as follows:


if w is a variable then vw=w and fw is w=w.


if s=F(t1,...,tn) then


fs is f(t1)∧...∧f(tn)∧(v(t1),...,v(tn),v(s))


For each subformula θ of we define a formula θ\* in the language of ZF as follows:


(t1=t2)\* is f(t1)∧f(t2)∧v(t1)=v(t2)


(t1∈t2)\* is f(t1)∧f(t2)∧v(t1)∈v(t2)


(P(t1,...,tn))\* is f(t1)∧...∧f(tn)∧(v(t1),...,v(tn))


(θ1∧θ2)\* is (θ1)*∧(θ2)*


(¬θ)\* is ¬(θ\*)


(∃xθ)\* is ∃x(θ\*)


We note that θ\*<-->θ for all subformulas θ of .


Now suppose (X).


By the usual notion of reflection there is an ordinal such that X∈V, V reflects \*, and V reflects all formulas of A and B.


Then \*(X) holds with quantifiers relativized to V.


Therefore (X) holds relativized to V, since relativized to V, (X)<-->\*(X).


