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

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 much more informed answer than my own. Unfortunately, I am unable to delete mine. – mrp Mar 18 '15 at 14:16
• @mrp: No need to delete it, I think. The SE platform deals well with having the same question answered from different perspectives. – Henning Makholm Mar 18 '15 at 14:43

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.

• Your statement about algorithm is utterly wrong. Algorithms are often specified in some real languages as Haskell or Python. Such languages can be translated to e.g. lambda calculus. Every construct in Haskell is defined in kernel language which is in fact lambda calculus. So if algorithm is implemented in Haskell then it can be automatically translated to lambda calculus. – Trismegistos Mar 18 '15 at 12:09
• @Trismegistos But in that case you already have a formal language in which to specify your algorithm. The point still stands that there exist formal algorithms and informal algorithms, and that these are equivalent is the content of the Church-Turing thesis. – mrp Mar 18 '15 at 12:33
• Informal algorithm are not equivalent to anything and has nothing to do with CH-T thesis. Informal algorithm step can say "Check whether Turing machine stops" and such algorithm is not equivalent to any "formal algorithm". Moreover CH-T says about what is computable in our universe while there are "formal algorithms" that are using some kind of hypercomputaion and they are not covered by CH-T thesis. – Trismegistos Mar 18 '15 at 12:45
• @Trismegistos: Most people (who know what they're talking about) would probably deny that anything that says "check whether the Turing machine stops" is an "algorithm" at all, even an informal one. – Henning Makholm Mar 18 '15 at 13:37
• @HenningMakholm Most people (who know what they're talking about) would probably inform themselfes on what hypercomputation has to do with stop problem before answering. – Trismegistos Mar 18 '15 at 14:15