The egg and the chicken After posting this question (in particular after Carl's and Peter's answers) I have realized that the answer seems to depend on a basic problem in foundations.
Most mathematicians accept as given the ZFC (or at least ZF) axioms for sets. These are treated at an intuitive level. Using set theory they define languages, axioms, theories, models and all the logic toolbox. Then they define (formalized) set theory again, using this language.
The second point of view is typical of logicians. They realize that in order to talk of logic they don't need the full power of set theory, so they take logic as God-given instead. Then set theory is formalized in this framework.
I always thought that the points of view were interchangeable, as far as one was interested in the mathematical consequences. But comparing Carl's and Peter's answers it seems that actual (but still foundational) mathematic may depend on the point of view accepted. I'd like to understand this better.

Are there any mathematical consequences of choosing one of the two points of view?

 A: Well, here's what it seems like: We had the naïve set theories of Cantor (unaxiomatized) and Frege (first axiomatization), and everything was right with the world.  Then, however, it eventually became clear that there were paradoxes that made the theory inconsistent, so Zermelo and Russell (and others) both set to work on coming up with alternative axiomatizations to deal with the paradoxes.  Russell's Theory of Unramified Types ended up being unusable (cf. the proof that 1+1=2 in Principia Mathematica (the full proof is something like 100 pages).  However, Zermelo was able to recover a good deal of naïve set theory in the Z (ZC), or Zermelo (resp. Zermelo + Choice) axiomatization (Zermelo+Choice). 
However, it eventually became clear that Z(C) was too weak in some regards, so Fraenkel and Skolem both proposed (independently) the axiom schema of replacement to improve the power of the theory.  If you include the axiom schema of regularity (which says that $\in$ is well-founded), you get ZF (resp. ZFC).  

Most mathematicians accept as given the ZFC (or at least ZF) axioms for sets. These are treated at an intuitive level. Using set theory they define languages, axioms, theories, models and all the logic toolbox. Then they define (formalized) set theory again, using this language.

ZFC is built on first-order logic.  Mathematicians then can construct models of languages and set theories internal to ZFC.  (To answer your comment: The reason why we want to axiomatize over first order logic is because first order logic has all of the properties one would want from it, completeness, compactness, etc.  In particular, the reason why we must first define theorems and proofs is because we need a proof calculus to be able to formally derive results.)

The second point of view is typical of logicians. They realize that in order to talk of logic they don't need the full power of set theory, so they take logic as God-given instead. Then set theory is formalized in this framework.

In fact, this is true for both mathematicians and logicians (although this view is strangely more popular among mathematicians than logicians).  This would be the "bootstrapping" step for mathematicians to get to ZFC. Even though Bourbaki's book on set theory has an inadequate and confusing approach to set theory, the idea in the first few sections is correct.  One first defines a what it means for something to be a theorem, what it means for something to be a proof, etc, then gives the axioms of formal logic, then constructs a set theory above that (this was one of the areas in which Bourbaki was the most influential as well.  That is, his opinion on the logical grounding of set theory (but then not actually worrying about it once it's developed) is perhaps one of his most important lasting contributions to the world of mathematics.  
A: I would like to question two statements you make because they paint an oversimplified picture, which unfortunately is alluring to mathematicians who do not want to think about foundations (and they should not be blamed for it anymore than I should be blamed for not wanting to think about PDEs).


*

*"Most mathematicians accept as given the ZFC (or at least ZF) axioms for sets." This is what mathematicians say, but most cannot even tell you what ZFC is. Mathematicians work at a more intuitive and informal manner. High party officials once declared that ZFC was being used by everyone, so it has become the party line. But if you read a random text of mathematics, it will be equally easy to interpret it in other kinds of foundations, such as type theory, bounded Zermelo set theory, etc. They do not use the language of ZFC. The language of ZFC is completely unusable for the working mathematician, as it only has a single relation symbol $\in$. As soon as you allow in abbreviations, your exposition becomes expressible more naturally in other formal systems that actually handle abbreviations formally. Informal mathematics is informal, and thankfully, it does not require any foundation to function, just like people do not need an ideology to think. If you doubt that, you have to doubt all mathematics that happened before late 19th century.

*"They [logicians] realize that in order to talk of logic they don't need the full power of set theory, so they take logic as God-given instead." I do not know of any logicians, and I know many, who would say that logic is "God-given", or anything like that. I do not think logicians are born into a life rich with the "full power of set theory" which they throw away  in order to become ascetic first-order logicians. That is a nice philosophical story detached from reality. The logicians I know are usually quite careful, skeptical, and inquisitive about foundational issues, reflect carefully on their own experiences, and almost never give you a straight answer when you ask "where does logic come from?" Your view is naive and inaccurate, if not slightly demeaning.
If I understand your question correctly, you are asking whether there is a difference between the following two views:


*

*We start with naive set theory and on top of it we formalize set theory.

*We start with first-order logic and immediately formalize set theory.
Well, we are proceeding from two different meta-theories. The first one allows us a wide spectrum of semantic methods. We can refer to "the standard model of Peano arithmetic" because we "believe in natural numbers", and we can invent Tarskian model theory without worrying where it came from.
The second method is more restricted. It will lead to syntactic and proof-theoretic methods, since the only thing we have given ourselves initially are syntactic in nature, namely first-order theories. There will be careful analysis of syntax. For advanced methods, however, we will typically resort to at least some amount of "naive mathematics". Ordinals will come into play, it will be hard to live without completeness theorems (which involve semantics), etc.
However, this is not how real life works. The dilemma you present is not really there. A working mathematician does not concern himself with these issues, anyhow, while a logician will likely refuse to be categorized as one or the other breed.
That is my guess, based on the experience that my fellow logicians are complicated animals and it is hard to get to the bottom of their foundational guts.
