Are there areas of mathematics (current or future) that cannot be formalized in set theory?

Question

I often read that ZFC can formalize "most" of everyday mathematics, but I could never find an example which it cannot. The closest I got is differential geometry (DF), where some article mentions that the translation from concepts of DF into set theory would render it almost "meaningless", in the sense that any intuitions one could have would be lost in the translation. So, if I didn't misunderstand, at least in theory, the translation could be done, so that a future AI machine could prove theorems of differential geometry using set theory. On the other hand, the Stanford Encyclopedia of Philosophy states that "all of mathematics can be reduced to a formal system of set theory"(http://plato.stanford.edu/entries/set-theory/).

So, the questions are:

1. Is there any current area of mathematics that could be not formalized within set theory? If so, which ones? and
2. Is there any reason to think that every math of the future will be always formalizable in set theory? any references to read on the subject are welcomed!

Clarification: by set theory I am not restricting to ZFC, but to any flavor of it, including all additional axioms you want (about large cardinals or any kind)

Answer 1

First let me point out that set theory is a foundation to mathematics as much as electric current is the actual way a computer "thinks". You don't even have to go that far, you can go to the machine code itself.

Have you ever looked at a disassembled code? It takes a piece of code that was compiled from, perhaps, a high level language (such as C++, Visual Basic, C#, and so on), and it shows you what are the operations sent to the computer. It is very un-enlightening about the purpose of the original code, unless the original code itself was in assembly. But it still works.

In a similar way translating everything into the language of $\{\in\}$ and sets ends up in a very strange result, often allowing for insane type errors (e.g. $\{\langle 0,1\rangle\}\subseteq 4$). But the point of foundational set theory is not to have a sensible translation, but to have some sort of a consistent CPU where mathematics can be executed. In this aspect set theory allows us to turn everything into first-order logic theories, where we can apply completeness, incompleteness and deduction theorems on them.

Classic mathematics such as calculus, basic linear algebra, measure theory, classic functional analysis, those things can be easily modeled in $\sf{ZFC}$. Truth to be told, $\sf{ZFC}$ is a lot stronger than needed, and there are people nowadays working on using arithmetics (usually second-order arithmetics, or weakening of it) as the use of foundational theory.

However the more mathematics progressed into abstractions and infinite there were points that were not within the reach of "vanilla $\sf{ZFC}$". For example classes, classes of classes, a lot of category theory, etc.

While it is possible to switch from $\sf{ZFC}$ to $\sf{NBG}$, which is a conservative extension which allows classes, one turns into a two-sorted theory which is often slightly less convenient, but it to can only take you so far and not always enough. So Grothendieck suggested universes, which was a concept later used for the Tarski-Grothendieck set theory which itself is an extension of $\sf{ZFC}$. But large cardinals allow us to correct this situation as well. Large cardinals allow us to have frameworks much stronger than universes. In fact the TG set theory is equivalent to some large cardinal additions to $\sf{ZFC}$.

Speaking of large cardinals, we can go further, it has been suggested that there is a deep connection between some concepts in model categories and homotopy theory and large cardinals. I am not familiar with the details, but I had a couple of short chats with a few people who do, and it seems that in order to formalize some general notion of model category apparently you end up using a lot more than inaccessible cardinals (the words Vopenka principle come to mind). But that too is within the reach of $\sf{ZFC}$+suitable large cardinal axioms.

What cannot be formalized in set theory? Well. Nobody knows the future, I can only assert with certainty that at some point we die. Currently I believe that the way we think about mathematics is such that essentially everything can be turn into set theory. In particular $\sf{ZFC}$+axioms which have not yet been proven inconsistent with $\sf{ZFC}$.

But let us turn our heads, for a moment, to the other side of set theory. Algebraic set theory. The idea is not to put emphasis on elements and membership structure, but rather on functions between our sets. Such set theories like ETCS have been proposed as foundation for a lot of the mathematics in place of the classical $\sf{ZFC}$ foundations. There has been a lot of discussions over the topic a month ago after a paper called "Rethinking Set Theory" by Tom Leister was posted online. Taking part in those discussions I have learned two things that I have known before:

1. Whenever you take "concrete mathematics" (e.g. analysis, measure theory, etc) and turn it into set theory you will invariably lose some of the intuition.
2. Structural set theory while able to serve basis for $\sf{ZFC}$, make a crappy language to discuss a lot of the topics which do interest $\sf{ZFC}$ oriented set theorists. This is in a similar fashion of how $\sf{ZFC}$ make category theory cumbersome.

The discussions sort of faded out and died, but it seemed that they have went out with sort of a hint that type theory's day of the tentacle is nigh. In the form of Martin-Lof and SEAR/SEARC. But I don't know about that. I should stop. Thanks for reading.