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).
[Math] equivalence between formal and informal proof
formal-proofslogicset-theory
Related Solutions
As the quotations reveal, there are indeed two different notions here.
1 & 2 belong together. A formal theory $T$ is negation-complete if for any sentence of $T$'s language, either $T$ proves $\varphi$ or $T$ proves $\neg\varphi$ (in symbols, either $T \vdash \varphi$, then $T \vdash \neg\varphi$).
3 & 4 belong together. A logical system (e.g. for quantificational logic) is complete if whenever the premisses $\Gamma$ semantically entail the conclusion $\varphi$, there is a formal deduction in the system of $\varphi$ from premisses in $\Gamma$. (In symbols, if whenever $\Gamma \vDash \varphi$, then $\Gamma \vdash \varphi$.)
So quite different ideas: one is to do with how a deductive logic relates to the relevant notion of semantic entailment; the other is a purely syntactic notion. You can have negation-incomplete theories with complete logics, and negation-complete theories with incomplete logics (as well as the other two combinations).
Famously Gödel proved that essentially the Hilbert/Ackermann axiomatic version of quantificational logic is complete -- every semantically valid quantificational consequence (assuming a classical semantics) can be formally derived in that axiomatic system. Hence Gödel's completeness theorem (about a system of logic).
Famously Gödel proved that essentially a cut-down version of Principia's formal theory is not negation-complete: there are sentences which can't be decided one way or the other by the axioms. And the proof generalizes to any consistent formal theory that can "do enough arithmetic" (and which satisfies another condition which doesn't matter here). Hence Gödel's incompleteness theorem (about theories containing enough arithmetic).
Two different Gödelian results about different notions (so, there's no tension between them!).
There's nothing special about formalizing any area of logic. As with formalizing any subject it's quite difficult, but it's not inherently more difficult than any other area of math.
Here are some examples I found with a quick google search:
This CSSE thread discusses formal proofs of the compactness and completeness theorems.
This paper looks at formalizing the independence of CH.
Here's a treatment of the incompleteness theorems.
And so forth. Indeed, the whole starting point of "modern metalogic" is the realization that it can be construed as just another area of mathematics.
Best Answer
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).