A useful suggestion is Richard Kaye, The Mathematics of Logic, (Cambridge U.P., 2007).
In Chapter 3 : Formal systems, he describes formal systems as :
kinds of mathematical games with strings of symbols and precise rules.
Rules are of two basic kind :
The following chapters deal with the typical formal systems of Math Log : Propositional Logic and First-Order Logic.
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).
Best Answer
A working knowledge of elementary logic, in Kelley's sense, is a matter of the kind of proficiency with informal deductive reasoning that you pick up early in your mathematical career (and elsewhere of course). E.g., understanding how to refute a proposition by assuming the opposite and deriving an absurdity, understanding how to establish a universal generalization by working with an arbitrary instance, understanding how to establish a conditional by supposing the antecedent is true and deriving the consequent.
Formal logical systems, where we carefully define the syntax, carefully define what can be inferred from what, etc., aim to regiment and formalize such patterns of informal deductive reasoning: as Kelley says, the exercise of regimenting can indeed be illuminating about our ordinary reasoning.
A formal mathematical theory (or system) is what you get when you take a formal logical system and add some specific mathematical axioms, and thereby regiment an informal mathematical theory.
(Metalogic is another step further, being the informal mathematical investigation of such formal logico-mathematical systems treated as themselves objects of mathematical interest)