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