Does  (Infer $\phi$ from $\psi$) imply  (Infer $\phi^L$ from $\psi^L$)? I am studying set theory on my own on Drake's famous book and I'm stuck on the (finitary) prove of the relative consistency of the Axiom of Choice.
Is it true that a if we were able to infer $\xi$ from $\zeta$ then we are able to infer $\xi^L$ from $\zeta^L$.
Intuitively of course in $L$ are to hold the rules of the predicative calculus since these are just the "minimum" of our human intuition, but, for example, one of these (from Shoenfield book) is
R) If $x$ is non free in $\psi$ then infer $\exists x \phi \rightarrow \psi$ from $\phi \rightarrow \psi$.
which would become 
RL) If $x$ is non free in $\psi^L$ then infer $\exists x \in L \phi^L \rightarrow \psi^L$ from $\phi^L \rightarrow \psi^L$.
So is R $\Rightarrow$RL? It does not seem so obvious to me: maybe I am missing something.
 A: In general when you relativize proofs to $\bf L$, you need to supplement each top-level formula $\phi$ in the proof with assumptions that its free variables are in $\bf L$. Otherwise you run into problems -- for example, $\phi\equiv\exists x.x=y$ is a theorem, but $\phi^L\equiv \exists x\in{\bf L}.x=y$ is not a theorem (in fact independent of ZFC).
So you want RL to infer
$$\tag B (y\in {\bf L} \land z\in {\bf L}\land \cdots) \to (\exists x\in {\bf L}.\phi^{\bf L})\to\psi^{\bf L} $$
from
$$\tag A (x\in {\bf L}\land y\in {\bf L} \land z\in {\bf L}\land\cdots) \to \phi^{\bf L}\to\psi^{\bf L} $$
where $y, z\ldots$ are the free variables of $\phi$ and $\psi$ other than $x$.
But that is actually easy enough. Here's how it works using the deduction theorem. Since we're aiming to prove (B) assume $y\in {\bf L}$, $z\in {\bf L}$ and so forth. Also temporarily assume $x\in{\bf L}$. Then from (A) we get $\phi^{\bf L}\to \psi^{\bf L}$, and we can now apply the ordinary $R$ to get $(\exists x\phi^{\bf L})\to\psi ^{\bf L}$. Discharging the assumption $x\in {\bf L}$, we get
$$ x \in {\bf L} \to (\exists x\phi^{\bf L})\to\psi ^{\bf L} $$
where the only free $x$ is in $x\to {\bf L}$. We can instantiate this $x$ to $\varnothing$ to make the premise into $\varnothing \in{\bf L}$ which is easily provable. Then what we have is 
$$\tag{1} (\exists x.\phi^{\bf L})\to \psi^{\bf L}$$
It is also easy to prove
$$\tag{2} (\exists x.x\in{\bf L}\land \phi^{\bf L})\to(\exists x.\phi^{\bf L})$$
independently of what ${\bf L}$ and $\phi^L$ are. Combining $(1)$ with $(2)$ gives
$$(\exists x.x\in {\bf L}\land \phi^{\bf L})\to\psi^L$$
and we can then discharge our initial assumptions on $y, z, \ldots$ to get (B).
In general you need an argument along these lines for every rule of inference and logical in the style of logic you're working with. If you also have proofs of $\xi^{\bf L}$ for each set-theoretic axiom $\xi$, then you have enough tools to systematically convert a proof of an arbitrary sentence $\zeta$ into a proof of $\zeta^{\bf L}$.
