A heuristic for the consistency of ZFC (Fine Structure Theory) The following excerpt is from Frank Drake's 'Large Cardinals' book, in the chapter on Constructibility. He gives a (non-ZFC) proof of the following theorem:
Theroem: There are $\kappa^+$models of ZF of the form $L_\alpha$ for $\alpha$ between $\kappa$ and $\kappa^+$
which he uses to proves results about the famous 'gaps' in the Constructible hierarchy. I will give the proof below. The remarkable thing about this proof is that the actuall non-ZFC part of it is very much 'intuitively true', and therefore the proof seems to be a strong heuristic for believing in the consistency of ZFC. Here is the proof:
Proof: Using the definable well ordering $<_L$ of $L$, define a Skolem function in $L$ for each formula $\phi(x_0,...,x_n)$ by letting $f_\phi(x_0,...,x_n)$ be the $<_L$-least element satisfying $\phi$, or $\emptyset$ otherwise. For each$\phi$, $f_\phi$ is a definable Skolem function in $L$. 
The collection F of all such Skolem functions is not definable in ZFC as if it were, it would imply a truth definition for $L$ (and hence $V$, if $V=L$), and also models of ZFC. But we will make the (non-ZFC) assumption that the countable collection F exists.
Take any $L_\beta$ for $\kappa\le\beta\le\kappa^+$. Form the closure $X$ of $L_\beta$ under F; we shall have $|X|=\kappa$ and also $(X,E(X))\prec L$. Hence $(X,E(X))$ is well-founded and a model of extensionality, do Mostowski's theorem implies that we have a unique collapsing isomorphism $f:X\to Y$ for some transitive $Y$.Since $X\models ZFL$, also $Y\models ZFL$; and so by 1.12 (a previous theorem where he proves that any set-model of ZFL is of the form $L_\alpha$ for some $\alpha$) $Y=L_\alpha$ for some $\alpha$. (There rest of the proof simply shows that there are $\kappa^+$ such models, and is not directly related to my question).
Question: Am I missing something here? It seems like the very intuitive assumption that the non-definable collection F exists gives us a clear reason to believe in the consistency of ZFC. Yet I have read many expository articles on ZFC and have never seen this argument used before. I feel like there must be some circular argument in here somewhere.
 A: If I understand you correctly, you're arguing as follows:


*

*It is very reasonable to assume that a collection F of Skolem functions for $L$ exists.

*From this F, we can produce many set models of ZFC (indeed, transitive set models).

*Therefore, it is very reasonable to assume that ZFC is consistent (indeed, more than that - the existence of a transitive model is a strictly stronger$^*$ hypothesis, consistency-strength wise, than the existence of a model).
However, note that right at the beginning we began with $L$. So we're already assuming at the outset, at least on the face of things, that the constructible universe exists. Baked right into that is already the hypothesis that ZFC is consistent. So at best, I think that what's really going on is a plausibility argument that ZFC has transitive models, starting from the assumption that $L$ "exists."

Proof: First let me give a slick argument which relies on a strong consistency principle, so is in a sense cheating. Let $\alpha$ be the least ordinal such that $L_\alpha\models$ ZFC. Since ZFC is truly consistent and $L_\alpha$ has "true $\omega$ (being transitive), we have $L_\alpha\models$ Con(ZFC). However, $L_\alpha$ can't have any transitive model of ZFC: such a model would have height $<\alpha$, and since its $L$ would satisfy ZFC this contradicts the assumption on $\alpha$.
Now here's an assumption-free proof. Suppose there is a transitive model $M$ of ZFC. Then ZFC is truly consistent, so $M$ - which has standard $\omega$, by transitivity - satisfies Con(ZFC). This means in turn that ZFC+Con(ZFC) is truly consistent.
So we've shown that "there exists a transitive model of ZFC" implies "there exists a transitive model of ZFC+Con(ZFC)." Since the existence of a model of ZFC+Con(ZFC) - transitive or not - is of stronger consistency strength than the existence of a model of ZFC alone, we're done.
Note that the same "true $\omega$ bootstrapping" trick that we've used can be iterated: so "there is a transitive model of ZFC" is of strictly stronger consistency strength than Con(ZFC+Con(ZFC)), or Con(ZFC+Con(ZFC)+Con(ZFC+Con(ZFC))), or ... We can even iterate this transfinitely, at least for a while. The existence of a transitive model is incredibly strong, relative to the usual consistency properties; more generally, soundness is stronger than consistency.
