It is said that our current basis for mathematics are the ZFC-axioms.
Question: Where are these axioms in our mathematics? When do we use them? I have now studied math for a year, and have yet to run into a single one of these ZFC axioms. How can this be if they are supposed to be the basis for everything I have done so far?
I think this is a very good question. I don’t have the time right now to write a complete answer, but let me make a few quick points (and I’ll add more when I get the chance):
Most mathematics is not done in ZFC. Most mathematics, in fact, isn’t done axiomatically at all: rather, we simply use propositions which seem “intuitively obvious” without comment. This is true even when it looks like we’re being rigorous: for example, when we formally define the real numbers in a real analysis class (by Cauchy sequences, Dedekind cuts, or however), we (usually) don’t set forth a list of axioms of set theory which we’re using to do this. The reason is, that the facts about sets which we need seem to be utterly tame: for example, that the intersection of two sets is again a set.
ZFC arose in response to a historical need. The history of modern logic is fascinating, and I don’t want to do it injustice; let me just say (wildly oversimplifying) that you only really need to axiomatize mathematics if there’s real danger of different people using different axioms implicitly, without realizing it. One standard example here is the axiom of choice, which very reasonable people alternately find perfectly intuitive and clearly false. So ZFC, very roughly speaking, won the job of being the “default” axiom system for mathematics: you’re perfectly free to prove theorems using (say) NF instead, but it’s considered gauche if you don’t explicitly say that’s what you’re doing. Are there reasons to prefer some other system to ZFC? I’m a very pro-ZFC person, but even I’d have to say yes. The point isn’t that ZFC is perfect, though; it’s that it’s strong enough to address the vast majority of our mathematical needs, while also being reasonable enough that it doesn’t cause huge problems most of the time. This strength, by the way, is crucial: we don’t want to have to keep updating our axiomatic framework to allow us to do basic mathematics, so overshooting in terms of strength is (I would argue) preferable (the counterargument is that overshooting runs a greater risk of inconsistency; but that’s an issue for a different question, or at least a bit later when I have more time to write).
Even in the ZFC context, ZFC is usually overkill. OK, let’s say you buy the ZFC sales pitch (I certainly did – and I just love the complimentary toaster!). Then you have some class of theorems you want to prove, and – after expressing them in the language of ZFC (which is frankly a tedious process, and one of the practical objections to ZFC emerges from this) – proceed to prove them from the ZFC axioms. But then you notice that you didn’t use most of the ZFC axioms at all! This is in fact the norm – replacement especially is overkill in most situations. This isn’t a problem, though: ZFC doesn’t claim to be minimal, in any sense. And in fact the study of what axioms are needed to prove a given theorem is quite rich: see e.g. reverse mathematics.
Tl;dr: I would say that the sentence “ZFC is the foundation for modern mathematics,” while broadly correct, is hiding a lot of context. In particular:
Most of the time you’re not going to actually be using axioms at all.
ZFC’s claim to prominence is primarily sociological/historical; we could equally well have gone with NF, or something completely different.
The ZFC axioms are wildly overpowered for most of mathematics; in particular, you probably won’t really need the whole of ZFC for almost anything you do.
Most of all: ZFC doesn’t come first. Mathematics comes first; ZFC is a mathematical theory that, among other things, “absorbs” the vast majority of mathematics in a certain way. But you can do math without ZFC. (It’s just that you run the risk of accidentally invoking an “obvious” set-theoretic principle which isn’t so obvious, and so conflicting with other results which invoke the “obvious” negation of your “obvious” axiom. ZFC provides a general language for us to do math in, so we don’t have to worry about things like this. But in practice, this almost never occurs.)
Note that you could also ask this question with regard to formal logic – specifically, classical first-order logic – in general; and there has been a lot written about this (I’ll add some citations when I have more time). But that’s going very far afield.
Really tl;dr (and, I should add, in conflict with a number of people – this is my opinion): foundations do not enable, but rather serve, mathematics.