What does it mean to say that a particular mathematical theory is a foundation for mathematics?

That's an interesting question!

For sure there is not the answer, and I guess my opinion will also change (and hopefully, at some point, converge) during through forthcoming discussions and other answers, but here's a first try which fits with my experience.

Proposal for the definition of foundational system:

The underlying datum of a foundational system should include the following:

• A collection of syntactic entities (e.g. formulas, proof trees) and relations between them (e.g. well-formedness of formulas or proof trees).
• Translations from mathematical concepts (e.g. objects, statements, proofs) into syntactic objects and from judgements about them (e.g. "Proposition $A$ is provable" or "$P$ proves proposition $A$"") into statements about relations between the associated syntactic objects.

This datum should ideally be

• sufficiently expressive: All mathematical concepts, ideas and judgements should have a translation.

• sufficiently meaningful: 'Most' of what can be expressed through the system in terms of the syntactic entities and their relations should have an intuitive meaning, and translation should preserve that meaning.

The last part of the second conditions rules out trivial "foundational systems" with constant translations.

Examples

1) (ZFC) Set theory. This seems to mostly satisfy the expressiveness condition, but not the property of being sufficiently meaningful:

• Sufficiently expressive: To my knowledge, ZFC is sufficiently expressive to allow for the formalization of all mathematics which is in no need of treating classes as first-'class' objects. Category theory however can only be treated on the level of metatheorems, replacing statements like 'For every category ${\mathcal C}$ ...' by a meta-theoretical quantification over FOL formulas in one free variables satisfying the axioms of a category. This has a remedy by considering ZFC + U(niverses). I never encountered some idea or concept I would have liked to formalize but couldn't in ZFC + U.

  This addresses also your second and third question. It is also conceivable that at some point it will become common to add even stronger set theoretic statements to the standard set of axioms. For example, there is Vopenka's principle having very pleasant categorical consequences (see http://ncatlab.org/nlab/show/Vop%C4%9Bnka%27s+principle).

• Sufficiently meaningful: In my opinion, not at all: For example, you can ask the ill-posed question as to what the intersection of two arbitrary sets is. For example: what is the intersection of $\text{sin}$ and $\pi$? Sure, intuitively this is nonsense, but nevertheless we can ask and even answer this, provided we settled on some explicit construction of the reals.

2) Category Theoretical foundations, for example Lawvere's [E]lementary [T]heory of the [C]ategory of [S]ets, corrects, in my opinion, the latter deficiency of set theory: For example, it is not imposed that any two sets have something to do with each other; instead we may only form their intersection ( in the form of a pullback) provided they both come equipped with a monomorphism into some common third object. I'm not sure but concerning the expressiveness I think ETCS + Universes is as expressive as ZFC.

However, as I'm writing this, I get aware that despite the above suggests that ETCS meets the proposed requirements of a foundational system better than ZFC does, I still tend to think in ZFC instead of ETCS. Apart from habit, that might be because translation of concepts into ETCS is sometimes not as straightforward as it is in ZFC, so maybe this should be a criterion as well?

Please don't get me wrong - I'm not at all meaning to downgrade ZFC with the above, but I only want to note that its expressive power and flexibility comes at the cost of the presence of meaningless statements as well.

There is probably not one definition of "foundation" that everybody will agree on. However, there is an answer to the question why set theory lies at the foundation of all of mathematics:

Set theory is an extension of propositional logic, the framework of strict reasoning implicitly underlying everything mathematicians do. Let $P$ and $Q$ be propositions, and let $A$ and $B$ be the sets of entities for which propositions $P$ and $Q$ hold. One can now put all boolean operations on $P,Q$ in direct correspondence with set operations on $A,B$, for example

$$P∨ Q\quad\leftrightarrow\quad A∪B$$

$$P∧ Q\quad\leftrightarrow\quad A∩B$$

$$¬ P\quad\leftrightarrow\quad \overline A$$

etc.

The key advantage of the set-theoretic formulation of logic is that its elements (sets) can be objects that are of mathematical interest anyway, such as numbers. Thus set theory blurs the distinction between object of study and method of study and provides a natural foundation for such branches of mathematics as algebra, probability theory and topology.