equivalence between formal and informal proof I'm reading Cohen's book on the independence of the continuum hypothesis, and I see that all the proofs that he gives when he's defining the basic notions of set theory (ordinals, cardinals, transfinite induction) are informal. However I know that if one has a formal system in first order logic (such as ZFC), in order to be totally rigorous one has to give formal proofs of the propositions (by a formal proof I mean a sequence of statements such that each statement is either an axiom, or derivable from previous statements using rules of inference, etc..). I know that giving formal proofs is completely impractical, so I'd like to ask: what guarantees the existence of formal proofs for each informal proof in Cohen's book (or in general for such proofs)? Is is supposed to be obvious that a formal proof exists for those informal proofs (it's not obvious to me at all, actually I have a hard time writing down a formal proof that for two sets their union is also a set). I know that Gödel's completeness theorem solves this in a way (since by it, if one can 'somehow' show that a statement is true in every model, then there is a formal proof of the statement). But Gödel's completeness theorem relies on the axiom of choice and even for special cases where it doesn't, it's proof is still not finitistic, so it doesn't completely solve the problem (at least for me).
 A: Most texts in axiomatic set theory will present arguments in the theory in informal language. This is because actual formal proofs would be very large and tend to make it difficult to see the forest for trees -- the point is after all to convey understanding to the reader.
Such a text generally assumes that the reader is familiar enough with formal logic to figure out for himself how the informal arguments correspond to formal proofs. That's not just, as mrp makes it sound like, an article of faith -- the author actually knows how to formalize the arguments he gives and simply depends on the reader to be able to do the same thing.
In practice what one should do when writing and reading such an informal argument is not to actually reduce it to a formal, symbolic proof. What one is supposed to know is how to translate an informal argument for such-and-such in the theory into a similarly informal argument at the metalevel that a formal proof of such-and-such exists.
Cohen's book will not tell you how to do that -- it simply assumes as a prerequisite that you as a reader are familiar enough with some proof system for first-order logic that you're comfortable with doing these translations in your head.
One benefit of this is that one can read the book without learning one particular formalization of FOL -- which, no matter which one Cohen chose, would be different from the one some readers already knew. It is more effective to explicitly tell the reader, "you can use whatever standard formalization of logic you want", and there are plenty of introductory texts that do teach enough of formal logic to allow Cohen to avoid writing one himself.
Cohen does need to present the particular logical language he's working with, because several of the things one needs to do when doing metamathematics about ZFC requires one to quantify over "all formulas", and probably to use induction over their structure -- so one has to select a particular set of connectives to use so one knows which cases those induction proofs need.
But the structure of the proof system is much less critical for Cohen's purpose, as long as the entailment relation that it ends up with is the standard one.

So you're not supposed to go via the completeness theorem. However, just for completeness: Many commonly encountered proofs of the completeness theorem are phrased using the axiom of choice, but using AC is not strictly necessary as long as the language of the theory has countably many symbols. Only if the vocabulary of the theory can be an arbitrary set do we need to use AC (or assume that the vocabulary is well-orderable).
A: Let me edit the first part of the answer, as it was at best misleading and at worst false:
There is no guarantee that for every informal proof, there is a corresponding formal proof. This is an assumption, a thesis if you will, that gained a lot of traction in the early 20th century, and was especially popular among the formalist philosophy of mathematics. However, Gödel's incompleteness theorems showed that, given a formal system, there are some true statements in the system that can not be proved within the system. So the question of whether for every informal proof there is a corresponding informal is of course always relative to some specific formal system in which the formal proof is to be given. In the end, however, there have so far been discovered very few informal proofs that can not also be given as a formal proof in ZFC (the Gödel sentence being a somewhat artificial example of one such), so in most cases it is still assumed that an informal proof can be turned into an informal one in ZFC, and it is considered a remarkable discovery when an exception to this is discovered.

A similar, and more well-known, problem is that of an algorithm. On one hand, we have many formal notions of an algorithm, such as Turing machines, $\lambda$-calculus, and so on, which are all equivalent. On the other hand, we almost never specify an algorithm in any of these formalisms, because they are too cumbersome and difficult to understand, so we specify algorithms in some other language, such as a programming language, pseudocode, or just simply natural language, and we then assume that for any such informal algorithm, it is possible to create an equivalent formal algorithm. This assumption is known as the Church-Turing thesis.
