# 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.

-

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}$.

-
Thanks a lot. It was very kind of you. I still have two questions: 1) I have read the response you deleted and it seemed to me that the proof worked well enough (at least in this case). Is it true? 2) The fact that the free variable of a relativized formula $\phi^L$ are to vary in L comes from the definition of $\phi^L$ or...? – user35549 Jul 11 '12 at 1:14
This is the answer I deleted; I just edited it before undeleting. Yes, the proof worked well, such as it went, but I noticed it didn't prove enough. The definition of $\phi^{\bf L}$ assumes that all the free variables in are to range over $\bf L$, and the context that $\phi^{\bf L}$ is eventually used in is responsible for ensuring this. The definitions of $(\exists \cdots)^{\bf L}$ and $(\forall \cdots)^{\bf L}$ take care of it for quantified variables, but if there are any free variables left on the top level, we need to bound them explicitly. – Henning Makholm Jul 11 '12 at 1:42
Also what do you mean with top-level formula? – user35549 Jul 11 '12 at 1:53
By the way, isn't all my question totally unuseful? Since every formula in a proof from ZF to some sentence is a sentence, do we really need to spend a lot of time wondering about free variables? – user35549 Jul 11 '12 at 2:14
A formal proof is a sequence of formulas (or depending on your formalism, a tree of formulas connected by inference rules). By a "top-level" formula I mean the formulas that are in the sequence (rather than their subformulas, for example). – Henning Makholm Jul 11 '12 at 11:25