How exactly do logic and mathematics interact and what happens when we change the logic? [Note: this question turned out to be pretty huge, so if you think it would be better to split it up into smaller questions, please comment. The questions here are quite conceptually intertwined and dependent on each other, so I thought it was best to leave them in one piece, since I strongly suspect there might be a short answer that answers all of them at once. (But I really do hope the finale below sufficiently motivates the length of this question.)]
I've been thinking a bit about the foundations of mathematics and decided it's time to clear a few things up. I think it will be easiest to explain what bothers me on some concrete examples, so here goes. (Since, despite always having been fascinated with the subject, I have not yet found the time to study logic deeply, it is very possible that I shall say some things that are just terribly wrong. In this case comments are most welcome, since one of the main purposes of this question is clearing up my misconceptions.)
Suppose I am a mathematician and I want to study vector spaces. Then, as I understand it, what I want to do is the following. First, I define a formal theory $T$, describing the basic properties of vectors. This theory $T$ is the union $V\cup L$ of non-logical axioms (about formal properties of vectors) and logical axioms (these are just the axioms of predicate calculus). Its models are precisely the vector spaces. A model is something that interprets my theory, for example, the models in $\mathrm{ZFC}$ of the theory $T$ are precisely those sets that interpret our theory so it becomes true in this setting. (As you can see from this phrasing, I am already a bit confused by this, so here comes my first question.)

What is the precise role of $\mathrm{ZFC}$ here? Is it just the metatheory or is it something else? Does it even make sense to want to be able to interpret your theory in the metatheory?

As you see, I mention metatheory here. This is the next step. A mathematician always wants to have a good metatheory to be able to talk about the theory. As I understand it, the metatheory is mostly taken to be some sufficiently powerful theory, such as $\mathrm{ZFC}$ or maybe $\mathrm{IZF}$ if you like intuitionism and so on (category theory, perhaps?) What is interesting here is that the theory itself is of almost no use to mathematicians without some kind of metatheory. For example, most of linear algebra doesn't really happen in the theory of the vector space, it happens in this metatheory. The theory alone can't even express a statement like "every vector space has a basis" let alone prove it. (If I have confused every single bit of terminology out there, please let me know. Actually after thinking a bit more, I am becoming convinced that by "metatheory" here I probably mean the metatheory of the theory in which we interpret $T$, in this case the metatheory of $\mathrm{ZFC}$.)
But now comes the interesting thing. The properties we can prove will depend on the theory in which we interpret $T$. For example every $\mathrm{ZFC}$-model of a vector space will have a basis of a uniquely determined cardinality. And I believe I have read somewhere it is possible to construct in some intuitionistic set theory a vector space without a basis. It can also have two bases of different cardinalities.
This sounds as interesting as it confuses me.

Are these actually the models of the same theory $T$ or do we have to change the logical axioms of $T$ also? I imagine if one wants to be able to really interpret $T$ in an intuitionistic set theory, one might want to replace the predicate calculus $L$ with some sort of an intuitionistic variant of it, $L_I$? Or is this completely unnecessary? (In this case it probably is, since the axioms $V$ deal only with finitely many vectors at a time, right? But what about if we were to interpret $\mathrm{ZFC}$ in $\mathrm{IZF}$?)

I am completely fascinated that one can get such different-looking vector spaces by just changing the logic. So I was also wondering how much logic can we replace with something else in order to get interesting results. This, I suspect, would only mean interpreting the theory $T$ in some theory with a different logic. This seems to me to open up many interesting possibilities:

Is it possible to go the other way around and interpret $\mathrm{ZFC}$ in $T$ or something bizarre like that?
  Is there a model of $T$ in some weird theory that has in some sense two finite bases of different cardinalities?

And for the finale, which was actually my main motivation for these considerations:

How much logic (in any sensible sense of the word) do we have to "throw away" in order to make it possible to construct a three-dimensional associative division algebra over the reals?

Thanks in advance.
 A: The role of ZFC in studying vector spaces, among other things, is that we don't just look at the vector space itself, we look at sub_sets_ of the vector space to see if they are subspaces, and we want to look at functions (which are also represented as sets) from one vector space to another. 
The first-order theory of vector spaces is good for studying some properties of a particular vector space, but it is not able to quantify over, or construct, subsets of the vector space or functions between different vector spaces. So to really study vector spaces in the way that mathematicians do, we need to use a system that allows us to work with sets and functions. There are many possible systems that we could use, but ZFC is convenient because (1) we know it pretty well and (2) in practice ZFC is strong enough to do the things that we want to do with vector spaces. 
A: I think you're confusing the idea of a foundational theory with the idea of a metatheory.
ZFC is a commonly used foundational theory in mathematics. For example, it is possible to construct the real number system out of ZFC.
A metatheory is a theory that describes another theory. Here's an example of a theory, which I'll call FOO:
Propositions in FOO consist of strings of the characters A and B.
Axiom 1: B is a theorem.
Axiom 2: If P is a theorem, then PA is a theorem.
If I start proving theorems in FOO, I will prove B, BA, BAA, BAAA, ... All of these are theorems. I start to see a pattern. I say, "Hey, the only theorems I can prove in FOO consist of B followed by zero or more A's." This is a theorem in the metatheory of FOO.
You asked, "What is the precise role of ZFC here? Is it just the metatheory or is it something else?" I think the answer is that it is not just the metatheory -- and it's not even a metatheory at all. In this situation ZFC is a theory that you're using to construct models of T. For example, suppose I'm worried that there is some horrible contradiction lurking at the heart of the theory of vector spaces. If I can construct models of vector spaces using ZFC, then I can prove that any contradiction in the theory of vector spaces also leads to a contradiction in ZFC. This is comforting, because I'm pretty sure that ZFC is consistent.
As far as I can tell, the term "metatheory" is not formally defined. It seems to have originated with Hilbert, which means it predates Godel, model theory, and ZFC. It's a vague, philosophical term. But the general idea seems to be that a metatheory is an informal thing you construct in order to describe some more formal theory. In the example above, FOO is formal, but my observation about the kinds of theorems that can be proved in FOO is informal.
By contrast, a foundational theory like ZFC is formal.
It may help to observe that the relationship of model to theory can be symmetric. Let R be a theory of the real numbers. It has axioms like x+y=y+x, etc. Let E be a theory of Euclidean geometry. It has axioms like the parallel postulate. Both R and E can be formalized, so let's assume they have been. We can make a model of E in R, which is what Descartes did by modeling the plane as ordered pairs of real numbers. But we can also make a model of R in E, which is essentially what Euclid did in the Elements, where he discusses, e.g., the distributive law x(y+z)=xy+xz as a geometrical theorem.
The relationship of a metatheory to the theory is describes is not symmetric in this way.
A: I'll try to answer some of your questions. I think your main problem is some misunderstanding of the concept of metatheory and definition, I'll try to explain here to you.
A definition can be formally "defined" as a predicate of the form "$x$ is an $A$ iff $P(x)$ holds" for some formula $P$ in a language you use.
So in order to make definitions we need a language.
Now suppose we want to study a theory with formal tools, in order to do so we have to define in formal way the objects we want to study: thus to do this we need a language in which we can formalize/define the objects of our theory (formulas, theorems, theory, interpretation and so on) and a theory which states facts from which we can prove our theorems (metatheorems) about the theory, this data (language+theory) are our metatheory.
We can choose many different metatheories, the only thing we require is that this theory is rich enough to allows to formalize (aka define) both the syntax and semantic for the theory that we want to study. Clearly you can use ZFC, or an intuitive set theory, but also an intuitionistic set theory or ETCS (a categorical set theory) or any other theory which satisfies the previous requirements. 
Now we have to focus to the concepts of theory and model of a theory. The first one is just a set of formulae of the language (which are objects of our metatheory) the second is an interpretation of the said theory which satisfy the formulae of the theory. 
Now we have two kinds of definition that we can give in a theory: an explicit definition and an axiomatic definition. 
By explicit definition I mean a definition as I explained above. An axiomatic definition is a way of saying that an object (of my metatheory) is of a given kind if its a model of a certain theory (theory described in my metatheory). So you can see any axiomatic definition as explicit definition in the metatheory and many times you can reverse this construction turning an explicit definition into an axiomatic one: for instance in the case of vector space you can both define a vector space as a set which have certain operations satisfying some axioms, but you can also shortly say that a vector space is a model of the theory of the said axioms, these things being the same thing. 
Hope I made myself clear.
