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.
"My house is supposedly built on concrete pad foundations, but I've been fixing the pipes upstairs, and I haven't seen any foundation yet."
This is analogous - you don't see them because they're so deep beneath the surface of where you're working. If you lifted the floorboards and poked around, you'd find the foundations.
Though they might actually be wooden pile or columns-on-ball-bearings, in the same way you might actually be using a system besides ZFC. Though until you go and check, you probably won't know the difference.
As going down to the foundation level is way beyond scope for most house repairs, so is going down to axioms beyond scope for most mathematics.
Given a set $X$, we write $\mathcal{P}(X)$ for the set of all subsets of $X$. This is called the powerset of $X$. Here's an example of how powersets are used. Let $X$ denote a vector space. Maybe you want to define the concept "linear subspace of $X$" in a formal way. One viewpoint is that this concept "is" the function $$f : \mathcal{P}(X) \rightarrow \{\mathrm{true},\mathrm{false}\}$$ $$f(A) \iff (...),$$ where $(...)$ is the definition of the phrase "$A$ is a subspace of $X$." So, to give the "is a subspace of" function a proper domain, you need powersets.
But, how do we know powersets even exist? Well, because its an axiom.
But you may say:
Wait, I can define the set of all subsets (the "powerset"), right? Let $X$ denote a set. Then $$\mathcal{P}(X) = \{A \mid A \subseteq X\}$$ Ergo, $\mathcal{P}(X)$ exists. So I don't need an axiom for this!
Seems convincing, right? It was Russell whom first realized that this reasoning, which is formalized by the (contradictory) axiom schema of unrestricted comprehension, is untenable. The proof goes something like this. Suppose that for any formula $\phi(x)$ I can write down, there exists a set of all $x$ satisfying $\phi(x)$. Then, there exists a set of all $x$ satisfying $x \notin x$, call it $R$. Thus $y \in R$ iff $y \notin y$, for all $y$. So $R \in R$ iff $R \notin R$, a contradiction. Basically, this happens because we cannot consistently decide whether or not $R$ should be an element of itself. See also, Russell's Paradox.
This leads to the search for new set-existence principles, which (hopefully!) don't lead to an outright contradiction like that. ZFC is one such collection of set-existence principles, perhaps the standard one, and it includes the axiom of powerset.
(By the way, I copied a large chunk of this answer from this old post of mine. I guess that makes it self-plagiarism!)
Onward.
You write:
It is said that our current basis for mathematics are the ZFC-axioms.
I agree that the current basis for mathematics is set theory. But there's more than one way of doing set theory! So I don't agree with the above statement. Here's a necessarily incomplete list:
Also, I reject the claim that ITT isn't a set theory. It deals with collections, and functions between collections; in my books, that makes it a set theory. And of course there's people out there like me who are unhappy with the existing approaches and are secretly at work on our own secret One Set Theory To Rule Them All. You're allowed to dream, you know :) And of course you're not forced into using any particular foundation. Invent your own, if you like (this is harder than it sounds!). But anyway, no authority figure can tell you which foundation to use.
By the way, the terms in the above list aren't just set theories, they're also distinct styles of set theory. For example, you can add various kinds of axioms positing the existence of large cardinals to ZFC, for example, and you're still doing ZFC-style set theory. The theory has changed, but the style is the same. The real challenge, from a practical formalization of math standpoint, is not to create a new set theory, its to create a new, more user-friendly style of set theory.
You probably use ZFC all the time!
By analogy, in university level real analysis, the first order of business is to clearly define the set of real numbers. In many modern texts, the set of reals is defined as the unique, complete, ordered field. This simply means that the real numbers satisfies a particular list of properties - like $$a+b=b+a$$ for all real numbers $a$ and $b$. Of course, grade schoolers know that addition is commutative and use it frequently. Only very few of them ever study the real numbers from the axiomatic perspective, however. In fact, plenty of fine applied mathematics can be done without ever studying the theoretical underpinnings of the subject.
In a similar vein, mathematicians use the axioms of ZFC (well, at least ZF) all the time. When you write down an interval in so called set builder notation like $$\{x\in\mathbb R: -1\leq x \leq 1\},$$ you've just invoked the third axiom of ZFC, or the axiom of specification, as you can look up on Wikipedia. Again, it makes perfect sense that you should be able to define a set this way and you can do plenty of fine mathematics without ever questioning this fact. It's only when you study the theoretical underpinnings of set theory that this and other similar assumptions need to be made explicit.
Consider the question: what is a set?
ZFC gives an answer to this question.
If you feel that your intuition is good enough to solve the problems you are faced with, without asking this question, then you do not need a good understanding of ZFC.
This question is fundamental, since the other mathematical concepts like numbers, functions, relations, groups are defined using sets.
At my university it is common for maths students in 1st-3rd year to have very limited understanding of ZFC.
If you are interested in mathematical logic and set theory, then ZFC is very important.
Your point is very well taken because even when the axioms are used in a proof in an essential way, they are not mentioned explicitly. This is because the lecturers typically rely on naive set theory rather than any formalisation, often because they are no more familiar with such formalisations than you are. For example, in a real analysis or measure theory course you may well sit through a proof of the countable-additivity of the Lebesgue measure. What the lecturer did not admit is that the proof relies essentially on the Axiom of Choice.
ZFC offers a conceptual framework with the sanity of FOL where you can talk about objects small and large, and even consider classes as syntactic sugar. There are many statements that are nevertheless not
decided in ZFC, like the Continuum Hypothesis, V = L, Large Cardinal Axioms, etc.. So when you do mathematics, you might add further foundational axioms, besides working in the conceptual framework of ZFC.
See also:
Logical Dreams - Past and Future of Set Theory
Saharon Shelah - 2002
https://arxiv.org/abs/math/0211398
