Set theoretic universe in consistency proofs I am having difficulties understanding the relative consistency proof $Con(ZF)\rightarrow Con(ZFC)$. Most authors seem to assume at the outset the existence of some universe $V$ satisfying $ZF$ and proceed to show that $L$ is a model for $ZFC$, thus proving the consistency of $ZFC$. Is this universe $V$ assumed to be a set in some larger universe, in which we use the completeness theorem to show that $Con(ZF)$ implies the existence of $V$, or is there some finitistic way of showing $Con(ZF)$ implies the existence of a universe where $ZF$ holds? Thank you
 A: There are two ways to look at this:
Model-theoretically: Since ZF is assumed to be consistent, it has a model, and within this model we find a model of ZFC.
This may seem a bit fishy, because the usual proof of the completeness theorem (a consistent theory has a model) used the axiom of choice, but actually the completeness theorem for a countable theory such as ZF does not need choice. We still need to believe in set theory for this way to work, though.
Syntactically: Suppose we can derive a contradiction $\phi\land\neg\phi$ (with no free variables) from ZFC. Then it has a formal proof. Write down the relativization of each step in the proof to $\mathbf L$, and for each axioms in the proof insert our proof that $\mathbf L$ satisfies all axioms of ZFC.
The result is a proof in ZF of $(\phi\land\neg\phi)^{\mathbf L}$ which is the same as $\phi^{\mathbf L}\land \neg\phi^{\mathbf L}$, and therefore a bona fide contradiction proved from ZF. So if ZFC is inconsistent then ZF is inconsistent too.
Note that the syntactic method does not depend on having any model or universe for ZF or ZFC at all -- it proceeds entirely on the level of rules and proof. Thus it can be carried out in PA and is generally considered "finitistic".
